[isabelle] Query about instantiating theorems in Isabelle/ML



Dear Isabelle/ML experts,

Suppose I have a lemma:

lemma foo: "(x::int) = y+z ==> x - y = z" sorry

I want to instantiate y to 1. In Isabelle/Isar I can do this easily by foo[of _ 1] or foo[where y=1]. How can I do such things in Isabelle/ML?

I believe the answer should have something to do with the Drule.instantiate' method in drule.ML, but I don't know how to use this method properly in my case.

If variables in foo don't have type restrictions, then the following would work:

lemma foo1: "x = y+z ==> x - y = z" sorry
ML{*
Drule.instantiate' [SOME @{ctyp "int"}] [NONE,SOME @{cterm "(1::int)"}] @{thm foo1};
*}

However, with foo,

ML{*
Drule.instantiate' [SOME @{ctyp "int"}] [NONE,SOME @{cterm "(1::int)"}] @{thm foo};
*}

Isabelle/ML will complain:

exception TYPE raised (line 810 of "drule.ML"):
  instantiate': more instantiations than variables in thm
  int
  1

Many thanks in advance,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




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