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

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: [isabelle] Shortest way to prove an object-level implication via ML
*From*: Michael FÃrber <michael.faerber at uibk.ac.at>
*Date*: Wed, 18 May 2016 18:00:12 +0200
*Organization*: University of Innsbruck, Austria
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.7.2

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.*