[isabelle] Shortest way to prove an object-level implication via ML



Dear mailing list,


I would like to prove an object-level implication via Isabelle's ML interface.
The code looks as follows (to be executed in FOL):

ML {*
val pimp = Thm.assume @{cprop P} |> Thm.implies_intr @{cprop P}
val impi = @{thm IFOL.impI}
val inst = Thm.instantiate' [] [SOME @{cterm "P::o"}, SOME @{cterm "P::o"}] impi
val oimp = Thm.implies_elim inst pimp
*}

The output is:

val pimp = "P â P": thm
val impi = "(?P â ?Q) â ?P â ?Q": thm
val inst = "(P â P) â P â P": thm
val oimp = "P â P": thm

I'm currently quite annnoyed by the fact that I have to instantiate my theorem in order to be able to show my final implication. If I do not use the instantiated version, but the original IFOL.impl theorem, I get the exception "implies_elim: major premise". I had this problem in many different contexts and find it extremely annoying. Is there a faster way to solve this problem and similar ones, e.g. a version of Thm.implies_elim that automatically instantiates variables?


Cheers,
Michael




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