[isabelle-dev] [isabelle] Tiny minor backward-compatible changes to IFOL

[Lawrence Paulson]

> On 27 Apr 2020, at 12:49, Makarius <makarius at sketis.net> wrote:
> 
> So why not put it into some library theory somewhere?
> 
> There is no need to change the presentation of the core logic, just for
> another variant of quantifiers.

Well, as an experiment, I defined it:

> definition Uniq :: "('a ⇒ bool) ⇒ bool"
>   where "Uniq P ≡ (∀x y. P x ⟶ P y ⟶ y = x)"
> 
> syntax (ascii) "_Uniq" :: "pttrn ⇒ bool ⇒ bool"  ("(4?<=1 _./ _)" [0, 10] 10)
> syntax "_Uniq" :: "pttrn ⇒ bool ⇒ bool"  ("(2∃⇩≤⇩1 _./ _)" [0, 10] 10)
> translations "∃⇩≤⇩1x. P" ⇌ "CONST Uniq (λx. P)"

… and found myself using it almost immediately:

> lemma strict_sorted_equal_Uniq: "∃⇩≤⇩1xs. strict_sorted xs ∧ list.set xs = A"
>   by (simp add: Uniq_def strict_sorted_equal)
> 
> lemma "inj_on f A ⟷ (∀x∈A. ∃⇩≤⇩1y. y∈A ∧ f x = f y)"
>   by (auto simp: Uniq_def inj_on_def)
> 
> lemma "(∃⇩≤⇩1x. x ∈ A) ⟷ (∃a. A ⊆ {a})"
>   unfolding Uniq_def subset_iff by blast

Surely such a simple and useful definition does belong in HOL.thy itself.

Larry