Instantiating a theorem based on matching result · Isabelle/ML

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

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

Mohammad Abdulaziz (Sep 20 2021 at 08:26):

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

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.

Stream: Isabelle/ML

Topic: Instantiating a theorem based on matching result