Email Gateway (Aug 22 2022 at 13:23): Email Gateway (Aug 22 2022 at 13:23):From: Michael Färber <michael.faerber@uibk.ac.at>
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
Email Gateway (Aug 22 2022 at 13:24):From: Makarius <makarius@sketis.net>
On 18/05/16 18:00, Michael Färber wrote:
I would like to prove an object-level implication via Isabelle's ML
interface.
This is official called "Isabelle/ML". It is documented to some extent
in the "implementation" manual.
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
*}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.
Thm.assume, Thm.implies_intr are primitive rules of the logical
framework (see "implementation", section 2.3.1). These are typically
used for internal infrastructure or specialized tools. The canonical way
to work with rules in Isabelle is via the resolution-combinators for
object-level rules (see "implementation", section 2.4).
Makarius
Last updated: Apr 26 2024 at 20:16 UTC