[isabelle] HOL quantifiers in intro rules



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

Attachment: signature.asc
Description: This is a digitally signed message part



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