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?

can you also post the definition of `prep_trm`

?

I added it

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

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
```

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

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: Oct 12 2024 at 20:18 UTC