Re: [isabelle] HOL quantifiers in intro rules



One reason I sometimes use HOL connectives in premises is that it is more convenient for forward reasoning: you can write closed_Inter[OF ...]. I don't know how to do this as compactly if the premise is not atomic.

Tobias

On 20/11/2014 10:22, 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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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