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"
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