Re: [isabelle] HOL quantifiers in intro rules



I would guess that in many cases the format of these theorems has been copied from HOL4, where the distinction does not exist. I agree, it is unfortunate. Generally it’s best to express your theorem in the form that is most convenient in its applications (of which there will probably be many) rather than in the proof of the theorem itself (of which there is only one).

Larry Paulson


> On 20 Nov 2014, at 09:22, Joachim Breitner <breitner at kit.edu> wrote:
> 
> Hi,
> 
> sometimes I stumble over rules like
> 
>        lemma closed_Inter [continuous_intros, intro]: "∀S∈K. closed S ⟹ closed (⋂ K)"
> 
> that use HOL quantifiers, despite being declared as intros. This is
> probably no problem in uses in auto, and may even be required for
> whatever continuous_intros is used, but it is certainly inconvenient for
> use in Isar:
> 
>        lemma "closed (⋂K)"
>        proof
>          -- Now I have to write
>          show "∀S∈K. closed S"
>          -- when I instead want to write
>          fix S
>          assume "X ∈ K"
> 
> Is that just an historic artifact from when Isar was not there yet, or
> is there a deeper reason behind this?
> 
> (I’ll be giving an introductory talk on Isabelle next week, and without
> this the proofs would be a bit more elegant.)
> 
> Greetings,
> Joachim
> 
> 
> -- 
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.