## Stream: Isabelle/ML

### Topic: Instantiating a theorem based on matching result

#### Mohammad Abdulaziz (Sep 19 2021 at 18:42):

I am trying to instantiate the schematic variables of a theorem based on the environment found by the matcher. For instance, in the example below, I instantiate the two schematic variables in the theorem `exI`, and that works.

``````fun prep_trm ctxt (x, (T, t)) = ((x, T), Thm.cterm_of ctxt t)
fun prep_ty ctxt (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty)
fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty

val P = Free ("P", @{typ "'a ⇒ bool"})
val x = Free ("x", @{typ 'a})
val trm = (Thm.term_of (Thm.cterm_of @{context} (P \$ x)))

fun inst_exI ctxt trm =
let
val pat = (HOLogic.dest_Trueprop (nth (Logic.strip_imp_prems (Thm.prop_of exI)) 0))
val univ = Unify.matchers (Context.Proof ctxt) [(pat, trm)]
val env = nth (Seq.list_of univ) 1
val tenv = Vartab.dest (Envir.term_env env)
val tyenv = Vartab.dest (Envir.type_env env)
val instantiation = (Thm.instantiate (map (prep_ty ctxt) tyenv, map (prep_trm ctxt) tenv) exI)
in
instantiation
end

val _ = inst_exI @{context} trm
``````

However, when I try to instantiate only one of the schematic variables, as in the example below, this does not work.

``````fun prep_trm ctxt (x, (T, t)) = ((x, T), Thm.cterm_of ctxt t)
fun prep_ty ctxt (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty)
fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty

val x = Free ("x", @{typ 'a})
val trm = (Thm.term_of (Thm.cterm_of @{context} x))

fun inst_exI ctxt trm =
let
val pat = snd (Term.dest_comb (HOLogic.dest_Trueprop (nth (Logic.strip_imp_prems (Thm.prop_of exI)) 0)))
val univ = Unify.matchers (Context.Proof ctxt) [(pat, trm)]
val env = nth (Seq.list_of univ) 1
val tenv = Vartab.dest (Envir.term_env env)
val tyenv = Vartab.dest (Envir.type_env env)
val instantiation = (Thm.instantiate (map (prep_ty ctxt) tyenv, map (prep_trm ctxt) tenv) exI)
in
instantiation
end

val _ = inst_exI @{context} trm
``````

Does any one know a work around for that?

#### Kevin Kappelmann (Sep 20 2021 at 07:43):

can you also post the definition of `prep_trm`?

image.png

#### Kevin Kappelmann (Sep 20 2021 at 09:20):

the problem is that in the term substitution, `?x` has type `?'a` but `?'a` will be mapped to `'a`, so you need to normalise the types in your term substitution as well

#### Kevin Kappelmann (Sep 20 2021 at 09:21):

Here's something I use to normalise a theorem wrt an environment. You can adapt it to your use case:

``````fun norm_thm ctxt (env as Envir.Envir {tyenv,...}) thm =
let
val prop = Thm.prop_of thm
val norm_type = Envir.norm_type tyenv
val norm_term = Envir.norm_term env
fun prep_type_entry x = (x, Thm.ctyp_of ctxt (norm_type (TVar x)))
val type_inst = Term.add_tvars prop [] |> map prep_type_entry
fun prep_term_entry (x as (n, T)) = ((n, norm_type T), Thm.cterm_of ctxt (norm_term (Var x)))
val term_inst = Term.add_vars prop [] |> map prep_term_entry
val inst = (type_inst, term_inst)
in Thm.instantiate inst thm end
``````

#### Mohammad Abdulaziz (Sep 20 2021 at 10:15):

Thanks! That works. In general, is it a good idea to always normalise terms and types in thms or instantatiations?

#### Kevin Kappelmann (Sep 21 2021 at 06:53):

Normalisation wrt arbitrary environments can be quite expensive, so if you can avoid the normalisation step, do so. Sometimes however, I think, you cannot get around it since `thm.ML` checks for type consistency at certain places (as in your case above).
Moreover, if you already now that you only want to instantiate certain variables, you can get around the term traversals (the `add_(t)vars` calls in my function above) by only normalising those variables explicitly.

Last updated: Dec 07 2023 at 16:21 UTC