Seems reasonable to me. As I said already privately, there should then definitely be an abbreviation for entering ∃⇩≤⇩1 using autocomplete.
Manuel On 02/05/2020 16:17, Lawrence Paulson wrote: >> 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 > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
