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
On Do, 2014-11-20 at 10:22 +0100, Joachim Breitner wrote:
> 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)"
> -- 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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and