# [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

```

• Follow-Ups:

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