# HG changeset patch # User wenzelm # Date 1519234901 -3600 # Node ID 67caf783b9eec34719206bca91a44ea3cafb39ab # Parent 58f951ce71c884a4560019c7743c521e34c40024 explicit operations to instantiate frees: typ, term, thm, morphism; diff -r 58f951ce71c8 -r 67caf783b9ee src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Wed Feb 21 18:37:04 2018 +0100 +++ b/src/Pure/more_thm.ML Wed Feb 21 18:41:41 2018 +0100 @@ -72,6 +72,7 @@ val forall_intr_name: string * cterm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm + val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm val forall_intr_frees: thm -> thm val unvarify_global: theory -> thm -> thm @@ -406,6 +407,29 @@ end; +(* instantiate frees *) + +fun instantiate_frees ([], []) th = th + | instantiate_frees (instT, inst) th = + let + val idx = Thm.maxidx_of th + 1; + fun index ((a, A), b) = (((a, idx), A), b); + val insts = (map index instT, map index inst); + val frees = (map (#1 o #1) instT, map (#1 o #1) inst); + + val hyps = Thm.chyps_of th; + val inst_cterm = + Thm.generalize_cterm frees idx #> + Thm.instantiate_cterm insts; + in + th + |> fold_rev Thm.implies_intr hyps + |> Thm.generalize frees idx + |> Thm.instantiate insts + |> fold (elim_implies o Thm.assume o inst_cterm) hyps + end; + + (* instantiate by left-to-right occurrence of variables *) fun instantiate' cTs cts thm = diff -r 58f951ce71c8 -r 67caf783b9ee src/Pure/morphism.ML --- a/src/Pure/morphism.ML Wed Feb 21 18:37:04 2018 +0100 +++ b/src/Pure/morphism.ML Wed Feb 21 18:41:41 2018 +0100 @@ -42,6 +42,8 @@ val transfer_morphism': Proof.context -> morphism val transfer_morphism'': Context.generic -> morphism val trim_context_morphism: morphism + val instantiate_frees_morphism: + ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism val instantiate_morphism: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism end; @@ -127,6 +129,22 @@ val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context; + +(* instantiate *) + +fun instantiate_frees_morphism ([], []) = identity + | instantiate_frees_morphism (cinstT, cinst) = + let + val instT = map (apsnd Thm.typ_of) cinstT; + val inst = map (apsnd Thm.term_of) cinst; + in + morphism "instantiate_frees" + {binding = [], + typ = if null instT then [] else [Term_Subst.instantiateT_frees instT], + term = [Term_Subst.instantiate_frees (instT, inst)], + fact = [map (Thm.instantiate_frees (cinstT, cinst))]} + end; + fun instantiate_morphism ([], []) = identity | instantiate_morphism (cinstT, cinst) = let diff -r 58f951ce71c8 -r 67caf783b9ee src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Wed Feb 21 18:37:04 2018 +0100 +++ b/src/Pure/term_subst.ML Wed Feb 21 18:41:41 2018 +0100 @@ -17,6 +17,12 @@ val instantiate_maxidx: ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list -> term -> int -> term * int + val instantiateT_frees_same: ((string * sort) * typ) list -> typ Same.operation + val instantiate_frees_same: ((string * sort) * typ) list * ((string * typ) * term) list -> + term Same.operation + val instantiateT_frees: ((string * sort) * typ) list -> typ -> typ + val instantiate_frees: ((string * sort) * typ) list * ((string * typ) * term) list -> + term -> term val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> term Same.operation @@ -92,6 +98,42 @@ fun generalize names i tm = Same.commit (generalize_same names i) tm; +(* instantiation of free variables (types before terms) *) + +fun instantiateT_frees_same [] _ = raise Same.SAME + | instantiateT_frees_same instT ty = + let + fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts) + | subst (TFree v) = + (case AList.lookup (op =) instT v of + SOME T => T + | NONE => raise Same.SAME) + | subst _ = raise Same.SAME; + in subst ty end; + +fun instantiate_frees_same ([], []) _ = raise Same.SAME + | instantiate_frees_same (instT, inst) tm = + let + val substT = instantiateT_frees_same instT; + fun subst (Const (c, T)) = Const (c, substT T) + | subst (Free (x, T)) = + let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in + (case AList.lookup (op =) inst (x, T') of + SOME t => t + | NONE => if same then raise Same.SAME else Free (x, T')) + end + | subst (Var (xi, T)) = Var (xi, substT T) + | subst (Bound _) = raise Same.SAME + | subst (Abs (x, T, t)) = + (Abs (x, substT T, Same.commit subst t) + handle Same.SAME => Abs (x, T, subst t)) + | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u); + in subst tm end; + +fun instantiateT_frees instT ty = Same.commit (instantiateT_frees_same instT) ty; +fun instantiate_frees inst tm = Same.commit (instantiate_frees_same inst) tm; + + (* instantiation of schematic variables (types before terms) -- recomputes maxidx *) local