Re: [isabelle] HOL quantifiers in intro rules



Yes, this looks like it got lost (missed) in translation from HOL4 or
HOL Light. I try to state theorems using meta-quantifiers, especially
intro rules like closed_Inter.

@Joachim: In your specific case you can also use intro:

lemma "closed (⋂K)"
proof (intro continuous_intros ballI)
  fix S assume "S : K" shows "closed S"
     ...
qed

 - Johannes

Am Donnerstag, den 20.11.2014, 12:51 +0000 schrieb Lawrence Paulson:
> 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.