> On 27 Apr 2020, at 12:49, Makarius <[email protected]> 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
