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



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





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