Re: [isabelle] HOL quantifiers in intro rules



As Johannes already pointed out, you could use intro.

I usually use something like the following in those cases:
  proof rule safe
    fix S
    assume ...	

--
  Peter


On Do, 2014-11-20 at 10:22 +0100, Joachim Breitner 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
>         
> 






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