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

[Manuel Eberl]

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 <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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>