# HG changeset patch # User wenzelm # Date 1438033317 -7200 # Node ID 622d45ca75ee75d4f6e85299dece437cefcad634 # Parent 080a979a985b3cc6a9333f7590af344102f5802a# Parent 4cc49ead6e7583c8f49ea34dd012202989c916ef merged diff -r 080a979a985b -r 622d45ca75ee src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/HOL/Eisbach/match_method.ML Mon Jul 27 23:41:57 2015 +0200 @@ -504,7 +504,7 @@ Subgoal.focus_params ctxt i bindings goal; val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt'; - val (_, schematic_terms) = Thm.certify_inst ctxt'' inst; + val schematic_terms = map (apsnd (Thm.cterm_of ctxt'')) (#2 inst); val goal'' = Thm.instantiate ([], schematic_terms) goal'; val concl' = Thm.instantiate_cterm ([], schematic_terms) concl; diff -r 080a979a985b -r 622d45ca75ee src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Jul 27 23:41:57 2015 +0200 @@ -947,9 +947,11 @@ val U = TFree ("'u", @{sort type}) val y = Free (yname, U) val f' = absdummy (U --> T') (Bound 0 $ y) - val th' = Thm.certify_instantiate ctxt' - ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')], - [((fst (dest_Var f), (U --> T') --> T'), f')]) th + val th' = + Thm.instantiate + ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')), + (dest_TVar uninst_T', Thm.ctyp_of ctxt' T')], + [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th'] in th' @@ -1075,10 +1077,10 @@ val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^ - " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred') ^ - " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")" ^ - " in " ^ Display.string_of_thm ctxt th) - in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end + " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^ + " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^ + " in " ^ Display.string_of_thm ctxt' th) + in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end fun instantiate_typ th = let val (pred', _) = strip_intro_concl th @@ -1086,13 +1088,13 @@ if not (fst (dest_Const pred) = fst (dest_Const pred')) then raise Fail "Trying to instantiate another predicate" else () - in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end + in Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt')) (subst_of (pred', pred)), []) th end fun instantiate_ho_args th = let val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th val ho_args' = map dest_Var (ho_args_of_typ T args') - in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end + in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end val outp_pred = Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred val ((_, ths'), ctxt1) = diff -r 080a979a985b -r 622d45ca75ee src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Mon Jul 27 23:41:57 2015 +0200 @@ -693,10 +693,11 @@ val err_msg = "Transfer failed to convert goal to an object-logic formula" val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} val thm1 = Drule.forall_intr_vars thm - val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) []) - |> map (fn v as ((a, _), S) => (v, TFree (a, S))) + val instT = + rev (Term.add_tvars (Thm.full_prop_of thm1) []) + |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S)))) val thm2 = thm1 - |> Thm.certify_instantiate ctxt (instT, []) + |> Thm.instantiate (instT, []) |> Raw_Simplifier.rewrite_rule ctxt pre_simps val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) @@ -709,7 +710,7 @@ THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 handle TERM (_, ts) => raise TERM (err_msg, ts) val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac) - val tnames = map (fst o dest_TFree o snd) instT + val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT in thm3 |> Raw_Simplifier.rewrite_rule ctxt' post_simps @@ -729,10 +730,11 @@ val err_msg = "Transfer failed to convert goal to an object-logic formula" val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} val thm1 = Drule.forall_intr_vars thm - val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) []) - |> map (fn v as ((a, _), S) => (v, TFree (a, S))) + val instT = + rev (Term.add_tvars (Thm.full_prop_of thm1) []) + |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S)))) val thm2 = thm1 - |> Thm.certify_instantiate ctxt (instT, []) + |> Thm.instantiate (instT, []) |> Raw_Simplifier.rewrite_rule ctxt pre_simps val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) @@ -745,7 +747,7 @@ THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 handle TERM (_, ts) => raise TERM (err_msg, ts) val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac) - val tnames = map (fst o dest_TFree o snd) instT + val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT in thm3 |> Raw_Simplifier.rewrite_rule ctxt' post_simps diff -r 080a979a985b -r 622d45ca75ee src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/Pure/Isar/code.ML Mon Jul 27 23:41:57 2015 +0200 @@ -638,14 +638,15 @@ fun desymbolize_tvars thy thms = let val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; - val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs; - in map (Thm.global_certify_instantiate thy (tvar_subst, [])) thms end; + val instT = + mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs; + in map (Thm.instantiate (instT, [])) thms end; fun desymbolize_vars thy thm = let val vs = Term.add_vars (Thm.prop_of thm) []; - val var_subst = mk_desymbolization I I Var vs; - in Thm.global_certify_instantiate thy ([], var_subst) thm end; + val inst = mk_desymbolization I I (Thm.global_cterm_of thy o Var) vs; + in Thm.instantiate ([], inst) thm end; fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); @@ -700,13 +701,13 @@ val mapping = map2 (fn (v, sort) => fn sort' => (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts; val inst = map2 (fn (v, sort) => fn (_, sort') => - (((v, 0), sort), TFree (v, sort'))) vs mapping; + (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping; val subst = (map_types o map_type_tfree) (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v))); in thm |> Thm.varifyT_global - |> Thm.global_certify_instantiate thy (inst, []) + |> Thm.instantiate (inst, []) |> pair subst end; @@ -771,7 +772,7 @@ val sorts = map_transpose inter_sorts vss; val vts = Name.invent_names Name.context Name.aT sorts; val thms' = - map2 (fn vs => Thm.certify_instantiate ctxt (vs ~~ map TFree vts, [])) vss thms; + map2 (fn vs => Thm.instantiate (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts, [])) vss thms; val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms')))); fun head_conv ct = if can Thm.dest_comb ct then Conv.fun_conv head_conv ct diff -r 080a979a985b -r 622d45ca75ee src/Pure/Isar/subgoal.ML --- a/src/Pure/Isar/subgoal.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/Pure/Isar/subgoal.ML Mon Jul 27 23:41:57 2015 +0200 @@ -55,7 +55,7 @@ val text = asms @ (if do_concl then [concl] else []); val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2; - val (_, schematic_terms) = Thm.certify_inst ctxt3 inst; + val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst); val schematics = (schematic_types, schematic_terms); val asms' = map (Thm.instantiate_cterm schematics) asms; diff -r 080a979a985b -r 622d45ca75ee src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/Pure/drule.ML Mon Jul 27 23:41:57 2015 +0200 @@ -206,10 +206,10 @@ val Ts = map Term.fastype_of ps; val inst = Thm.fold_terms Term.add_vars th [] - |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps))); + |> map (fn (xi, T) => ((xi, T), Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps)))); in th - |> Thm.certify_instantiate ctxt ([], inst) + |> Thm.instantiate ([], inst) |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps end; @@ -230,8 +230,11 @@ | zero_var_indexes_list ths = let val thy = Theory.merge_list (map Thm.theory_of_thm ths); - val insts = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths); - in map (Thm.adjust_maxidx_thm ~1 o Thm.global_certify_instantiate thy insts) ths end; + val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths); + val insts' = + (map (apsnd (Thm.global_ctyp_of thy)) instT, + map (apsnd (Thm.global_cterm_of thy)) inst); + in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate insts') ths end; val zero_var_indexes = singleton zero_var_indexes_list; diff -r 080a979a985b -r 622d45ca75ee src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/Pure/more_thm.ML Mon Jul 27 23:41:57 2015 +0200 @@ -61,16 +61,6 @@ val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm - val global_certify_inst: theory -> - ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> - ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list - val global_certify_instantiate: theory -> - ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm - val certify_inst: Proof.context -> - ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> - ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list - val certify_instantiate: Proof.context -> - ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm val forall_intr_frees: thm -> thm val unvarify_global: thm -> thm val close_derivation: thm -> thm @@ -375,23 +365,6 @@ in thm'' end; -(* certify_instantiate *) - -fun global_certify_inst thy (instT, inst) = - (map (apsnd (Thm.global_ctyp_of thy)) instT, - map (apsnd (Thm.global_cterm_of thy)) inst); - -fun global_certify_instantiate thy insts th = - Thm.instantiate (global_certify_inst thy insts) th; - -fun certify_inst ctxt (instT, inst) = - (map (apsnd (Thm.ctyp_of ctxt)) instT, - map (apsnd (Thm.cterm_of ctxt)) inst); - -fun certify_instantiate ctxt insts th = - Thm.instantiate (certify_inst ctxt insts) th; - - (* forall_intr_frees: generalization over all suitable Free variables *) fun forall_intr_frees th = @@ -417,8 +390,8 @@ val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => let val T' = Term_Subst.instantiateT instT T - in (((a, i), T'), Free ((a, T'))) end); - in global_certify_instantiate thy (instT, inst) th end; + in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end); + in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end; (* close_derivation *) diff -r 080a979a985b -r 622d45ca75ee src/Pure/variable.ML --- a/src/Pure/variable.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/Pure/variable.ML Mon Jul 27 23:41:57 2015 +0200 @@ -600,8 +600,8 @@ fun importT ths ctxt = let val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; - val insts' as (instT', _) = Thm.certify_inst ctxt' (instT, []); - val ths' = map (Thm.instantiate insts') ths; + val instT' = map (apsnd (Thm.ctyp_of ctxt')) instT; + val ths' = map (Thm.instantiate (instT', [])) ths; in ((instT', ths'), ctxt') end; fun import_prf is_open prf ctxt = @@ -612,8 +612,10 @@ fun import is_open ths ctxt = let - val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; - val insts' = Thm.certify_inst ctxt' insts; + val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; + val insts' = + (map (apsnd (Thm.ctyp_of ctxt')) instT, + map (apsnd (Thm.cterm_of ctxt')) inst); val ths' = map (Thm.instantiate insts') ths; in ((insts', ths'), ctxt') end; diff -r 080a979a985b -r 622d45ca75ee src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Mon Jul 27 22:44:02 2015 +0200 +++ b/src/Tools/Code/code_preproc.ML Mon Jul 27 23:41:57 2015 +0200 @@ -168,17 +168,19 @@ fun normalized_tfrees_sandwich ctxt ct = let val t = Thm.term_of ct; - val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =) - o dest_TFree))) t []; + val vs_original = + fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original); - val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized)); + val normalize = + map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized)); val normalization = - map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), TFree (v, sort))) vs_original vs_normalized; + map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), Thm.ctyp_of ctxt (TFree (v, sort)))) + vs_original vs_normalized; in if eq_list (eq_fst (op =)) (vs_normalized, vs_original) then (I, ct) else - (Thm.certify_instantiate ctxt (normalization, []) o Thm.varifyT_global, + (Thm.instantiate (normalization, []) o Thm.varifyT_global, Thm.cterm_of ctxt (map_types normalize t)) end;