--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Mar 06 14:01:08 2015 +0100
@@ -213,11 +213,13 @@
fun cterm_instantiate_pos cts thm =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+ val thy = Thm.theory_of_thm thm;
val vars = Term.add_vars (Thm.prop_of thm) [];
val vars' = rev (drop (length vars - length cts) vars);
- val ps = map_filter (fn (_, NONE) => NONE
- | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
+ val ps =
+ map_filter
+ (fn (_, NONE) => NONE
+ | (var, SOME ct) => SOME (Thm.cterm_of thy (Var var), ct)) (vars' ~~ cts);
in
Drule.cterm_instantiate ps thm
end;
--- a/src/HOL/Tools/Function/fun_cases.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/fun_cases.ML Fri Mar 06 14:01:08 2015 +0100
@@ -19,7 +19,6 @@
fun mk_fun_cases ctxt prop =
let
- val thy = Proof_Context.theory_of ctxt;
fun err () =
error (Pretty.string_of (Pretty.block
[Pretty.str "Proposition is not a function equation:",
@@ -30,7 +29,7 @@
val info = Function.get_info ctxt f handle List.Empty => err ();
val {elims, pelims, is_partial, ...} = info;
val elims = if is_partial then pelims else the elims;
- val cprop = Thm.cterm_of thy prop;
+ val cprop = Proof_Context.cterm_of ctxt prop;
fun mk_elim rl =
Thm.implies_intr cprop
(Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
--- a/src/HOL/Tools/Function/function_common.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_common.ML Fri Mar 06 14:01:08 2015 +0100
@@ -325,9 +325,9 @@
elims = Option.map (map fact) elims, pelims = map fact pelims }
end
-fun lift_morphism thy f =
+fun lift_morphism ctxt f =
let
- fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
+ fun term t = Thm.term_of (Drule.cterm_rule f (Proof_Context.cterm_of ctxt t))
in
Morphism.morphism "lift_morphism"
{binding = [],
@@ -338,13 +338,12 @@
fun import_function_data t ctxt =
let
- val thy = Proof_Context.theory_of ctxt
- val ct = Thm.cterm_of thy t
- val inst_morph = lift_morphism thy o Thm.instantiate
+ val ct = Proof_Context.cterm_of ctxt t
+ val inst_morph = lift_morphism ctxt o Thm.instantiate
fun match (trm, data) =
- SOME (transform_function_data data (inst_morph (Thm.match (Thm.cterm_of thy trm, ct))))
- handle Pattern.MATCH => NONE
+ SOME (transform_function_data data (inst_morph (Thm.match (Proof_Context.cterm_of ctxt trm, ct))))
+ handle Pattern.MATCH => NONE
in
get_first match (Item_Net.retrieve (get_functions ctxt) t)
end
--- a/src/HOL/Tools/Function/function_context_tree.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_context_tree.ML Fri Mar 06 14:01:08 2015 +0100
@@ -20,11 +20,11 @@
val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree
- val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree
+ val inst_tree: Proof.context -> term -> term -> ctx_tree -> ctx_tree
val export_term : ctxt -> term -> term
- val export_thm : theory -> ctxt -> thm -> thm
- val import_thm : theory -> ctxt -> thm -> thm
+ val export_thm : Proof.context -> ctxt -> thm -> thm
+ val import_thm : Proof.context -> ctxt -> thm -> thm
val traverse_tree :
(ctxt -> term ->
@@ -116,16 +116,14 @@
val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
val (c, subs) = (Thm.concl_of r, Thm.prems_of r)
- val subst =
- Pattern.match (Proof_Context.theory_of ctxt) (c, tt') (Vartab.empty, Vartab.empty)
+ val subst = Pattern.match thy (c, tt') (Vartab.empty, Vartab.empty)
val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
- val inst = map (fn v =>
- (Thm.cterm_of thy (Var v), Thm.cterm_of thy (Envir.subst_term subst (Var v))))
- (Term.add_vars c [])
+ val inst =
+ map (fn v => apply2 (Proof_Context.cterm_of ctxt) (Var v, Envir.subst_term subst (Var v)))
+ (Term.add_vars c [])
in
- (cterm_instantiate inst r, dep, branches)
- end
- handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
+ (cterm_instantiate inst r, dep, branches)
+ end handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
| find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
@@ -158,10 +156,10 @@
mk_tree' ctxt t
end
-fun inst_tree thy fvar f tr =
+fun inst_tree ctxt fvar f tr =
let
- val cfvar = Thm.cterm_of thy fvar
- val cf = Thm.cterm_of thy f
+ val cfvar = Proof_Context.cterm_of ctxt fvar
+ val cf = Proof_Context.cterm_of ctxt f
fun inst_term t =
subst_bound(f, abstract_over (fvar, t))
@@ -174,7 +172,7 @@
| inst_tree_aux (RCall (t, str)) =
RCall (inst_term t, inst_tree_aux str)
and inst_branch ((fxs, assms), str) =
- ((fxs, map (Thm.assume o Thm.cterm_of thy o inst_term o Thm.prop_of) assms),
+ ((fxs, map (Thm.assume o Proof_Context.cterm_of ctxt o inst_term o Thm.prop_of) assms),
inst_tree_aux str)
in
inst_tree_aux tr
@@ -188,12 +186,12 @@
fold_rev (curry Logic.mk_implies o Thm.prop_of) assumes
#> fold_rev (Logic.all o Free) fixes
-fun export_thm thy (fixes, assumes) =
+fun export_thm ctxt (fixes, assumes) =
fold_rev (Thm.implies_intr o Thm.cprop_of) assumes
- #> fold_rev (Thm.forall_intr o Thm.cterm_of thy o Free) fixes
+ #> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) fixes
-fun import_thm thy (fixes, athms) =
- fold (Thm.forall_elim o Thm.cterm_of thy o Free) fixes
+fun import_thm ctxt (fixes, athms) =
+ fold (Thm.forall_elim o Proof_Context.cterm_of ctxt o Free) fixes
#> fold Thm.elim_implies athms
@@ -242,19 +240,18 @@
fun rewrite_by_tree ctxt h ih x tr =
let
- val thy = Proof_Context.theory_of ctxt
- fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (Thm.cterm_of thy t), x)
+ fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (Proof_Context.cterm_of ctxt t), x)
| rewrite_help fix h_as x (RCall (_ $ arg, st)) =
let
val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
- val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+ val iha = import_thm ctxt (fix, h_as) ha (* (a', h a') : G *)
|> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
(* (a, h a) : G *)
- val inst_ih = instantiate' [] [SOME (Thm.cterm_of thy arg)] ih
+ val inst_ih = instantiate' [] [SOME (Proof_Context.cterm_of ctxt arg)] ih
val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
- val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Thm.cterm_of thy h)) inner
+ val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Proof_Context.cterm_of ctxt h)) inner
val h_a_eq_f_a = eq RS eq_reflection
val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
in
@@ -269,12 +266,12 @@
|> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
|> filter_out Thm.is_reflexive
- val assumes' = map (simplify (put_simpset HOL_basic_ss ctxt addsimps used)) assumes
+ val assumes' = map (simplify (put_simpset HOL_basic_ss ctxt addsimps used)) assumes
val (subeq, x') =
rewrite_help (fix @ fixes) (h_as @ assumes') x st
val subeq_exp =
- export_thm thy (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
+ export_thm ctxt (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
in
(subeq_exp, x')
end
--- a/src/HOL/Tools/Function/function_core.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_core.ML Fri Mar 06 14:01:08 2015 +0100
@@ -145,17 +145,16 @@
val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
- val thy = Proof_Context.theory_of ctxt'
-
fun inst t = subst_bounds (rev qs, t)
val gs = map inst pre_gs
val lhs = inst pre_lhs
val rhs = inst pre_rhs
- val cqs = map (Thm.cterm_of thy) qs
- val ags = map (Thm.assume o Thm.cterm_of thy) gs
+ val cqs = map (Proof_Context.cterm_of ctxt') qs
+ val ags = map (Thm.assume o Proof_Context.cterm_of ctxt') gs
- val case_hyp = Thm.assume (Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
+ val case_hyp =
+ Thm.assume (Proof_Context.cterm_of ctxt' (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
in
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
cqs = cqs, ags = ags, case_hyp = case_hyp }
@@ -183,11 +182,10 @@
val Globals {h, ...} = globals
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
- val cert = Proof_Context.cterm_of ctxt
(* Instantiate the GIntro thm with "f" and import into the clause context. *)
val lGI = GIntro_thm
- |> Thm.forall_elim (cert f)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt f)
|> fold Thm.forall_elim cqs
|> fold Thm.elim_implies ags
@@ -195,7 +193,7 @@
let
val llRI = RI
|> fold Thm.forall_elim cqs
- |> fold (Thm.forall_elim o cert o Free) rcfix
+ |> fold (Thm.forall_elim o Proof_Context.cterm_of ctxt o Free) rcfix
|> fold Thm.elim_implies ags
|> fold Thm.elim_implies rcassm
@@ -262,7 +260,6 @@
(* Generates the replacement lemma in fully quantified form. *)
fun mk_replacement_lemma ctxt h ih_elim clause =
let
- val thy = Proof_Context.theory_of ctxt
val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
RCs, tree, ...} = clause
local open Conv in
@@ -274,7 +271,7 @@
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
val h_assums = map (fn RCInfo {h_assum, ...} =>
- Thm.assume (Thm.cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+ Thm.assume (Proof_Context.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs
val (eql, _) =
Function_Context_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree
@@ -343,12 +340,12 @@
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
|> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
- |> fold_rev (Thm.forall_intr o Thm.cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) RIvs
val existence = fold (curry op COMP o prep_RC) RCs lGI
- val P = Thm.cterm_of thy (mk_eq (y, rhsC))
- val G_lhs_y = Thm.assume (Thm.cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
+ val P = Proof_Context.cterm_of ctxt (mk_eq (y, rhsC))
+ val G_lhs_y = Thm.assume (Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y)))
val unique_clauses =
map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
@@ -359,19 +356,21 @@
|> Seq.list_of |> the_single
val uniqueness = G_cases
- |> Thm.forall_elim (Thm.cterm_of thy lhs)
- |> Thm.forall_elim (Thm.cterm_of thy y)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt lhs)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt y)
|> Thm.forall_elim P
|> Thm.elim_implies G_lhs_y
|> fold elim_implies_eta unique_clauses
|> Thm.implies_intr (Thm.cprop_of G_lhs_y)
- |> Thm.forall_intr (Thm.cterm_of thy y)
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt y)
- val P2 = Thm.cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
+ val P2 = Proof_Context.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
val exactly_one =
@{thm ex1I}
- |> instantiate' [SOME (Thm.ctyp_of thy ranT)] [SOME P2, SOME (Thm.cterm_of thy rhsC)]
+ |> instantiate'
+ [SOME (Proof_Context.ctyp_of ctxt ranT)]
+ [SOME P2, SOME (Proof_Context.cterm_of ctxt rhsC)]
|> curry (op COMP) existence
|> curry (op COMP) uniqueness
|> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
@@ -383,8 +382,8 @@
existence
|> Thm.implies_intr ihyp
|> Thm.implies_intr (Thm.cprop_of case_hyp)
- |> Thm.forall_intr (Thm.cterm_of thy x)
- |> Thm.forall_elim (Thm.cterm_of thy lhs)
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt x)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt lhs)
|> curry (op RS) refl
in
(exactly_one, function_value)
@@ -394,19 +393,18 @@
fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
let
val Globals {h, domT, ranT, x, ...} = globals
- val thy = Proof_Context.theory_of ctxt
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
- |> Thm.cterm_of thy
+ |> Proof_Context.cterm_of ctxt
val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
- |> instantiate' [] [NONE, SOME (Thm.cterm_of thy h)]
+ |> instantiate' [] [NONE, SOME (Proof_Context.cterm_of ctxt h)]
val _ = trace_msg (K "Proving Replacement lemmas...")
val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
@@ -423,11 +421,12 @@
|> Thm.forall_elim_vars 0
|> fold (curry op COMP) ex1s
|> Thm.implies_intr (ihyp)
- |> Thm.implies_intr (Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
- |> Thm.forall_intr (Thm.cterm_of thy x)
+ |> Thm.implies_intr (Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt x)
|> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
|> (fn it =>
- fold (Thm.forall_intr o Thm.cterm_of thy o Var) (Term.add_vars (Thm.prop_of it) []) it)
+ fold (Thm.forall_intr o Proof_Context.cterm_of ctxt o Var)
+ (Term.add_vars (Thm.prop_of it) []) it)
val goalstate = Conjunction.intr graph_is_function complete
|> Thm.close_derivation
@@ -458,7 +457,6 @@
[] (* no special monos *)
||> Local_Theory.restore_naming lthy
- val cert = Proof_Context.cterm_of lthy
fun requantify orig_intro thm =
let
val (qs, t) = dest_all_all orig_intro
@@ -468,7 +466,7 @@
#> the_default ("", 0)
in
fold_rev (fn Free (n, T) =>
- forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
+ forall_intr_rename (n, Proof_Context.cterm_of lthy (Var (varmap (n, T), T)))) qs thm
end
in
((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
@@ -533,7 +531,7 @@
fun fix_globals domT ranT fvar ctxt =
let
- val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
+ val ([h, y, x, z, a, D, P, Pbool], ctxt') = Variable.variant_fixes
["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
in
(Globals {h = Free (h, domT --> ranT),
@@ -565,19 +563,20 @@
fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function =
let
- val thy = Proof_Context.theory_of ctxt
val Globals {domT, z, ...} = globals
fun mk_psimp
(ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
let
- val lhs_acc = Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
- val z_smaller = Thm.cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+ val lhs_acc =
+ Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+ val z_smaller =
+ Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
in
((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
|> (fn it => it COMP graph_is_function)
|> Thm.implies_intr z_smaller
- |> Thm.forall_intr (Thm.cterm_of thy z)
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt z)
|> (fn it => it COMP valthm)
|> Thm.implies_intr lhs_acc
|> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff])
@@ -705,12 +704,11 @@
(* FIXME: broken by design *)
fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
let
- val thy = Proof_Context.theory_of ctxt
val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
qglr = (oqs, _, _, _), ...} = clause
val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
|> fold_rev (curry Logic.mk_implies) gs
- |> Thm.cterm_of thy
+ |> Proof_Context.cterm_of ctxt
in
Goal.init goal
|> (SINGLE (resolve_tac ctxt [accI] 1)) |> the
@@ -730,7 +728,6 @@
fun mk_nest_term_case ctxt globals R' ihyp clause =
let
- val thy = Proof_Context.theory_of ctxt
val Globals {z, ...} = globals
val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
qglr=(oqs, _, _, _), ...} = clause
@@ -740,23 +737,23 @@
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
let
val used = (u @ sub)
- |> map (fn (ctxt, thm) => Function_Context_Tree.export_thm thy ctxt thm)
+ |> map (fn (ctx, thm) => Function_Context_Tree.export_thm ctxt ctx thm)
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
|> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *)
|> Function_Context_Tree.export_term (fixes, assumes)
|> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- |> Thm.cterm_of thy
+ |> Proof_Context.cterm_of ctxt
val thm = Thm.assume hyp
|> fold Thm.forall_elim cqs
|> fold Thm.elim_implies ags
- |> Function_Context_Tree.import_thm thy (fixes, assumes)
+ |> Function_Context_Tree.import_thm ctxt (fixes, assumes)
|> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
- |> Thm.cterm_of thy |> Thm.assume
+ |> Proof_Context.cterm_of ctxt |> Thm.assume
val acc = thm COMP ih_case
val z_acc_local = acc
@@ -764,7 +761,7 @@
(Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
val ethm = z_acc_local
- |> Function_Context_Tree.export_thm thy (fixes,
+ |> Function_Context_Tree.export_thm ctxt (fixes,
z_eq_arg :: case_hyp :: ags @ assumes)
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
@@ -780,7 +777,6 @@
fun mk_nest_term_rule ctxt globals R R_cases clauses =
let
- val thy = Proof_Context.theory_of ctxt
val Globals { domT, x, z, ... } = globals
val acc_R = mk_acc domT R
@@ -792,42 +788,42 @@
val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
(domT --> domT --> boolT) --> boolT) $ R')
- |> Thm.cterm_of thy (* "wf R'" *)
+ |> Proof_Context.cterm_of ctxt (* "wf R'" *)
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
HOLogic.mk_Trueprop (acc_R $ Bound 0)))
- |> Thm.cterm_of thy
+ |> Proof_Context.cterm_of ctxt
val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
- val R_z_x = Thm.cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
+ val R_z_x = Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x))
val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], [])
in
R_cases
- |> Thm.forall_elim (Thm.cterm_of thy z)
- |> Thm.forall_elim (Thm.cterm_of thy x)
- |> Thm.forall_elim (Thm.cterm_of thy (acc_R $ z))
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt z)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt x)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt (acc_R $ z))
|> curry op COMP (Thm.assume R_z_x)
|> fold_rev (curry op COMP) cases
|> Thm.implies_intr R_z_x
- |> Thm.forall_intr (Thm.cterm_of thy z)
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt z)
|> (fn it => it COMP accI)
|> Thm.implies_intr ihyp
- |> Thm.forall_intr (Thm.cterm_of thy x)
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt x)
|> (fn it => Drule.compose (it, 2, wf_induct_rule))
|> curry op RS (Thm.assume wfR')
|> forall_intr_vars
|> (fn it => it COMP allI)
|> fold Thm.implies_intr hyps
|> Thm.implies_intr wfR'
- |> Thm.forall_intr (Thm.cterm_of thy R')
- |> Thm.forall_elim (Thm.cterm_of thy (inrel_R))
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt R')
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt (inrel_R))
|> curry op RS wf_in_rel
|> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def])
- |> Thm.forall_intr (Thm.cterm_of thy Rrel)
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt Rrel)
end
@@ -865,7 +861,7 @@
PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss
- val trees = map (Function_Context_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
+ val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees
val ((R, RIntro_thmss, R_elim), lthy) =
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
@@ -877,18 +873,16 @@
val newthy = Proof_Context.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
- val cert = Proof_Context.cterm_of lthy
-
val xclauses = PROFILE "xclauses"
(@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
RCss GIntro_thms) RIntro_thmss
val complete =
- mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
+ mk_completeness globals clauses abstract_qglrs |> Proof_Context.cterm_of lthy |> Thm.assume
val compat =
mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
- |> map (cert #> Thm.assume)
+ |> map (Proof_Context.cterm_of lthy #> Thm.assume)
val compat_store = store_compat_thms n compat
--- a/src/HOL/Tools/Function/function_elims.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_elims.ML Fri Mar 06 14:01:08 2015 +0100
@@ -80,7 +80,6 @@
fun mk_partial_elim_rules ctxt result =
let
val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
val n_fs = length fs;
@@ -116,12 +115,12 @@
val args = HOLogic.mk_tuple arg_vars;
val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
- val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
+ val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Proof_Context.cterm_of ctxt
val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
- val cprop = cert prop;
+ val cprop = Proof_Context.cterm_of ctxt prop;
- val asms = [cprop, cert (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
+ val asms = [cprop, Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
val asms_thms = map Thm.assume asms;
fun prep_subgoal_tac i =
@@ -134,10 +133,10 @@
val elim_stripped =
nth cases idx
|> Thm.forall_elim P
- |> Thm.forall_elim (cert args)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt args)
|> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
|> fold_rev Thm.implies_intr asms
- |> Thm.forall_intr (cert rhs_var);
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt rhs_var);
val bool_elims =
(case ranT of
@@ -146,7 +145,7 @@
fun unstrip rl =
rl
- |> fold_rev (Thm.forall_intr o cert) arg_vars
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) arg_vars
|> Thm.forall_intr P
in
map unstrip (elim_stripped :: bool_elims)
--- a/src/HOL/Tools/Function/function_lib.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/function_lib.ML Fri Mar 06 14:01:08 2015 +0100
@@ -105,7 +105,7 @@
val ty = fastype_of t
in
Goal.prove_internal ctxt []
- (Thm.cterm_of thy
+ (Proof_Context.cterm_of ctxt
(Logic.mk_equals (t,
if null is
then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
--- a/src/HOL/Tools/Function/induction_schema.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/induction_schema.ML Fri Mar 06 14:01:08 2015 +0100
@@ -204,9 +204,6 @@
fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
(IndScheme {T, cases=scases, branches}) =
let
- val thy = Proof_Context.theory_of ctxt
- val cert = Thm.cterm_of thy
-
val n = length branches
val scases_idx = map_index I scases
@@ -224,7 +221,7 @@
$ (HOLogic.pair_const T T $ Bound 0 $ x)
$ R),
HOLogic.mk_Trueprop (P_comp $ Bound 0)))
- |> cert
+ |> Proof_Context.cterm_of ctxt
val aihyp = Thm.assume ihyp
@@ -237,9 +234,10 @@
fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
let
val fxs = map Free xs
- val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
+ val branch_hyp =
+ Thm.assume (Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
- val C_hyps = map (cert #> Thm.assume) Cs
+ val C_hyps = map (Proof_Context.cterm_of ctxt #> Thm.assume) Cs
val (relevant_cases, ineqss') =
(scases_idx ~~ ineqss)
@@ -249,10 +247,11 @@
fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
let
val case_hyps =
- map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
+ map (Thm.assume o Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq)
+ (fxs ~~ lhs)
- val cqs = map (cert o Free) qs
- val ags = map (Thm.assume o cert) gs
+ val cqs = map (Proof_Context.cterm_of ctxt o Free) qs
+ val ags = map (Thm.assume o Proof_Context.cterm_of ctxt) gs
val replace_x_simpset =
put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps)
@@ -260,16 +259,16 @@
fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
let
- val cGas = map (Thm.assume o cert) Gas
- val cGvs = map (cert o Free) Gvs
+ val cGas = map (Thm.assume o Proof_Context.cterm_of ctxt) Gas
+ val cGvs = map (Proof_Context.cterm_of ctxt o Free) Gvs
val import = fold Thm.forall_elim (cqs @ cGvs)
#> fold Thm.elim_implies (ags @ cGas)
val ipres = pres
- |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt (list_comb (P_of idx, rcargs)))
|> import
in
sih
- |> Thm.forall_elim (cert (inject idx rcargs))
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt (inject idx rcargs))
|> Thm.elim_implies (import ineq) (* Psum rcargs *)
|> Conv.fconv_rule (sum_prod_conv ctxt)
|> Conv.fconv_rule (ind_rulify ctxt)
@@ -284,7 +283,7 @@
|> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev (Logic.all o Free) qs
- |> cert
+ |> Proof_Context.cterm_of ctxt
val Plhs_to_Pxs_conv =
foldl1 (uncurry Conv.combination_conv)
@@ -304,14 +303,15 @@
val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
val bstep = complete_thm
- |> Thm.forall_elim (cert (list_comb (P, fxs)))
- |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt (list_comb (P, fxs)))
+ |> fold (Thm.forall_elim o Proof_Context.cterm_of ctxt) (fxs @ map Free ws)
|> fold Thm.elim_implies C_hyps
|> fold Thm.elim_implies cases (* P xs *)
|> fold_rev (Thm.implies_intr o Thm.cprop_of) C_hyps
- |> fold_rev (Thm.forall_intr o cert o Free) ws
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) ws
- val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
+ val Pxs =
+ Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (P_comp $ x))
|> Goal.init
|> (Simplifier.rewrite_goals_tac ctxt
(map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case}))
@@ -320,7 +320,7 @@
|> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
|> Goal.finish ctxt
|> Thm.implies_intr (Thm.cprop_of branch_hyp)
- |> fold_rev (Thm.forall_intr o cert) fxs
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) fxs
in
(Pxs, steps)
end
@@ -332,7 +332,7 @@
val istep = sum_split_rule
|> fold (fn b => fn th => Drule.compose (b, 1, th)) branches
|> Thm.implies_intr ihyp
- |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt x) (* "!!x. (!!y<x. P y) ==> P x" *)
val induct_rule =
@{thm "wf_induct_rule"}
@@ -351,15 +351,17 @@
let
val (ctxt', _, cases, concl) = dest_hhf ctxt t
val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
- val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
+ val ([Rn, xn], ctxt'') = Variable.variant_fixes ["R", "x"] ctxt'
val R = Free (Rn, mk_relT ST)
val x = Free (xn, ST)
- val cert = Proof_Context.cterm_of ctxt
- val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert)))
+ val ineqss =
+ mk_ineqs R scheme
+ |> map (map (apply2 (Thm.assume o Proof_Context.cterm_of ctxt'')))
val complete =
- map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
- val wf_thm = mk_wf R scheme |> cert |> Thm.assume
+ map_range (mk_completeness ctxt'' scheme #> Proof_Context.cterm_of ctxt'' #> Thm.assume)
+ (length branches)
+ val wf_thm = mk_wf R scheme |> Proof_Context.cterm_of ctxt'' |> Thm.assume
val (descent, pres) = split_list (flat ineqss)
val newgoals = complete @ pres @ wf_thm :: descent
@@ -371,7 +373,7 @@
let
val inst = (foldr1 HOLogic.mk_prod (map Free xs))
|> Sum_Tree.mk_inj ST (length branches) (i + 1)
- |> cert
+ |> Proof_Context.cterm_of ctxt''
in
indthm
|> Drule.instantiate' [] [SOME inst]
@@ -386,7 +388,7 @@
val nbranches = length branches
val npres = length pres
in
- Thm.bicompose (SOME ctxt') {flatten = false, match = false, incremented = false}
+ Thm.bicompose (SOME ctxt'') {flatten = false, match = false, incremented = false}
(false, res, length newgoals) i
THEN term_tac (i + nbranches + npres)
THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
--- a/src/HOL/Tools/Function/lexicographic_order.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri Mar 06 14:01:08 2015 +0100
@@ -66,9 +66,9 @@
fold_rev Logic.all vars (Logic.list_implies (prems, concl))
end
-fun mk_cell thy solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ =>
+fun mk_cell ctxt solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ =>
let
- val goals = Thm.cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
+ val goals = Proof_Context.cterm_of ctxt o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
in
case try_proof (goals @{const_name Orderings.less}) solve_tac of
Solved thm => Less thm
@@ -175,7 +175,6 @@
fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
let
- val thy = Proof_Context.theory_of ctxt
val ((_ $ (_ $ rel)) :: tl) = Thm.prems_of st
val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
@@ -184,7 +183,7 @@
Measure_Functions.get_measure_functions ctxt domT
val table = (* 2: create table *)
- map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
+ map (fn t => map (mk_cell ctxt solve_tac (dest_term t)) measure_funs) tl
in
fn st =>
case search_table table of
@@ -201,10 +200,11 @@
else ()
in (* 4: proof reconstruction *)
- st |> (PRIMITIVE (cterm_instantiate [(Thm.cterm_of thy rel, Thm.cterm_of thy relation)])
- THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
- THEN (rtac @{thm "wf_empty"} 1)
- THEN EVERY (map prove_row clean_table))
+ st |>
+ (PRIMITIVE (cterm_instantiate [apply2 (Proof_Context.cterm_of ctxt) (rel, relation)])
+ THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
+ THEN (rtac @{thm "wf_empty"} 1)
+ THEN EVERY (map prove_row clean_table))
end
end) 1 st;
--- a/src/HOL/Tools/Function/mutual.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/mutual.ML Fri Mar 06 14:01:08 2015 +0100
@@ -149,8 +149,6 @@
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
let
- val thy = Proof_Context.theory_of ctxt
-
val oqnames = map fst pre_qs
val (qs, _) = Variable.variant_fixes oqnames ctxt
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
@@ -160,8 +158,8 @@
val args = map inst pre_args
val rhs = inst pre_rhs
- val cqs = map (Thm.cterm_of thy) qs
- val ags = map (Thm.assume o Thm.cterm_of thy) gs
+ val cqs = map (Proof_Context.cterm_of ctxt) qs
+ val ags = map (Thm.assume o Proof_Context.cterm_of ctxt) gs
val import = fold Thm.forall_elim cqs
#> fold Thm.elim_implies ags
@@ -198,10 +196,10 @@
fun mk_applied_form ctxt caTs thm =
let
- val thy = Proof_Context.theory_of ctxt
val xs =
map_index (fn (i, T) =>
- Thm.cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
+ Proof_Context.cterm_of ctxt
+ (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
in
fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
|> Conv.fconv_rule (Thm.beta_conversion true)
@@ -211,7 +209,6 @@
fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) =
let
- val cert = Proof_Context.cterm_of ctxt
val newPs =
map2 (fn Pname => fn MutualPart {cargTs, ...} =>
Free (Pname, cargTs ---> HOLogic.boolT))
@@ -229,7 +226,7 @@
val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
val induct_inst =
- Thm.forall_elim (cert case_exp) induct
+ Thm.forall_elim (Proof_Context.cterm_of ctxt case_exp) induct
|> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
|> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
@@ -239,9 +236,9 @@
val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
in
(rule
- |> Thm.forall_elim (cert inj)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt inj)
|> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
- |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) (afs @ newPs),
k + length cargTs)
end
in
@@ -261,8 +258,7 @@
val argsT = fastype_of (HOLogic.mk_tuple arg_vars)
val (args, name_ctxt) = mk_var "x" argsT name_ctxt
- val cert = Proof_Context.cterm_of ctxt
- val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
+ val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Proof_Context.cterm_of ctxt
val sumtree_inj = Sum_Tree.mk_inj ST n i args
val sum_elims =
@@ -274,9 +270,9 @@
in
cases_rule
|> Thm.forall_elim P
- |> Thm.forall_elim (cert sumtree_inj)
+ |> Thm.forall_elim (Proof_Context.cterm_of ctxt sumtree_inj)
|> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal)
- |> Thm.forall_intr (cert args)
+ |> Thm.forall_intr (Proof_Context.cterm_of ctxt args)
|> Thm.forall_intr P
end
--- a/src/HOL/Tools/Function/pat_completeness.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/pat_completeness.ML Fri Mar 06 14:01:08 2015 +0100
@@ -40,12 +40,13 @@
(avs, pvs, j)
end
-fun filter_pats thy cons pvars [] = []
- | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
- | filter_pats thy cons pvars (((pat as Free _) :: pats, thm) :: pts) =
- let val inst = list_comb (cons, pvars)
- in (inst :: pats, inst_free (Thm.cterm_of thy pat) (Thm.cterm_of thy inst) thm)
- :: (filter_pats thy cons pvars pts)
+fun filter_pats ctxt cons pvars [] = []
+ | filter_pats ctxt cons pvars (([], thm) :: pts) = raise Match
+ | filter_pats ctxt cons pvars (((pat as Free _) :: pats, thm) :: pts) =
+ let val inst = list_comb (cons, pvars) in
+ (inst :: pats,
+ inst_free (Proof_Context.cterm_of ctxt pat) (Proof_Context.cterm_of ctxt inst) thm)
+ :: (filter_pats ctxt cons pvars pts)
end
| filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
if fst (strip_comb pat) = cons
@@ -55,65 +56,66 @@
fun transform_pat _ avars c_assum ([] , thm) = raise Match
| transform_pat ctxt avars c_assum (pat :: pats, thm) =
- let
- val thy = Proof_Context.theory_of ctxt
- val (_, subps) = strip_comb pat
- val eqs = map (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
- val c_eq_pat = simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum
- in
- (subps @ pats,
- fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
- end
+ let
+ val (_, subps) = strip_comb pat
+ val eqs =
+ map (Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
+ val c_eq_pat =
+ simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum
+ in
+ (subps @ pats,
+ fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
+ end
exception COMPLETENESS
fun constr_case ctxt P idx (v :: vs) pats cons =
- let
- val thy = Proof_Context.theory_of ctxt
- val (avars, pvars, newidx) = invent_vars cons idx
- val c_hyp = Thm.cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
- val c_assum = Thm.assume c_hyp
- val newpats = map (transform_pat ctxt avars c_assum) (filter_pats thy cons pvars pats)
- in
- o_alg ctxt P newidx (avars @ vs) newpats
- |> Thm.implies_intr c_hyp
- |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) avars
- end
+ let
+ val (avars, pvars, newidx) = invent_vars cons idx
+ val c_hyp =
+ Proof_Context.cterm_of ctxt
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
+ val c_assum = Thm.assume c_hyp
+ val newpats = map (transform_pat ctxt avars c_assum) (filter_pats ctxt cons pvars pats)
+ in
+ o_alg ctxt P newidx (avars @ vs) newpats
+ |> Thm.implies_intr c_hyp
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) avars
+ end
| constr_case _ _ _ _ _ _ = raise Match
and o_alg _ P idx [] (([], Pthm) :: _) = Pthm
| o_alg _ P idx (v :: vs) [] = raise COMPLETENESS
| o_alg ctxt P idx (v :: vs) pts =
- if forall (is_Free o hd o fst) pts (* Var case *)
- then o_alg ctxt P idx vs
- (map (fn (pv :: pats, thm) =>
- (pats, refl RS
- (inst_free (Proof_Context.cterm_of ctxt pv)
- (Proof_Context.cterm_of ctxt v) thm))) pts)
- else (* Cons case *)
- let
- val thy = Proof_Context.theory_of ctxt
- val T as Type (tname, _) = fastype_of v
- val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
- val constrs = inst_constrs_of ctxt T
- val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
- in
- inst_case_thm thy v P case_thm
- |> fold (curry op COMP) c_cases
- end
+ if forall (is_Free o hd o fst) pts (* Var case *)
+ then o_alg ctxt P idx vs
+ (map (fn (pv :: pats, thm) =>
+ (pats, refl RS
+ (inst_free (Proof_Context.cterm_of ctxt pv)
+ (Proof_Context.cterm_of ctxt v) thm))) pts)
+ else (* Cons case *)
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val T as Type (tname, _) = fastype_of v
+ val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
+ val constrs = inst_constrs_of ctxt T
+ val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
+ in
+ inst_case_thm thy v P case_thm
+ |> fold (curry op COMP) c_cases
+ end
| o_alg _ _ _ _ _ = raise Match
fun prove_completeness ctxt xs P qss patss =
let
- val thy = Proof_Context.theory_of ctxt
fun mk_assum qs pats =
HOLogic.mk_Trueprop P
|> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats)
|> fold_rev Logic.all qs
- |> Thm.cterm_of thy
+ |> Proof_Context.cterm_of ctxt
val hyps = map2 mk_assum qss patss
- fun inst_hyps hyp qs = fold (Thm.forall_elim o Thm.cterm_of thy) qs (Thm.assume hyp)
+ fun inst_hyps hyp qs = fold (Thm.forall_elim o Proof_Context.cterm_of ctxt) qs (Thm.assume hyp)
val assums = map2 inst_hyps hyps qss
in
o_alg ctxt P 2 xs (patss ~~ assums)
@@ -122,7 +124,6 @@
fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
let
- val thy = Proof_Context.theory_of ctxt
val (vs, subgf) = dest_all_all subgoal
val (cases, _ $ thesis) = Logic.strip_horn subgf
handle Bind => raise COMPLETENESS
@@ -141,7 +142,7 @@
val patss = map (map snd) x_pats
val complete_thm = prove_completeness ctxt xs thesis qss patss
- |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) vs
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) vs
in
PRIMITIVE (fn st => Drule.compose (complete_thm, i, st))
end
--- a/src/HOL/Tools/Function/relation.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/relation.ML Fri Mar 06 14:01:08 2015 +0100
@@ -16,10 +16,11 @@
(* tactic version *)
fun inst_state_tac inst st =
- (case Term.add_vars (Thm.prop_of st) [] of
+ (case Term.add_vars (Thm.prop_of st) [] of (* FIXME tactic should not inspect main conclusion *)
[v as (_, T)] =>
- let val cert = Thm.cterm_of (Thm.theory_of_thm st);
- in PRIMITIVE (Thm.instantiate ([], [(cert (Var v), cert (inst T))])) st end
+ let val thy = Thm.theory_of_thm st in
+ PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of thy (Var v), Thm.cterm_of thy (inst T))])) st
+ end
| _ => Seq.empty);
fun relation_tac ctxt rel i =
@@ -30,17 +31,16 @@
(* version with type inference *)
fun inst_state_infer_tac ctxt rel st =
- (case Term.add_vars (Thm.prop_of st) [] of
+ (case Term.add_vars (Thm.prop_of st) [] of (* FIXME tactic should not inspect main conclusion *)
[v as (_, T)] =>
let
- val cert = Proof_Context.cterm_of ctxt;
val rel' = singleton (Variable.polymorphic ctxt) rel
|> map_types Type_Infer.paramify_vars
|> Type.constraint T
|> Syntax.check_term ctxt
- |> cert;
+ |> Proof_Context.cterm_of ctxt;
in
- PRIMITIVE (Thm.instantiate ([], [(cert (Var v), rel')])) st
+ PRIMITIVE (Thm.instantiate ([], [(Proof_Context.cterm_of ctxt (Var v), rel')])) st
end
| _ => Seq.empty);
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Mar 06 14:01:08 2015 +0100
@@ -272,7 +272,7 @@
val level_mapping =
map_index pt_lev lev
|> Termination.mk_sumcases D (setT nat_pairT)
- |> Thm.cterm_of thy
+ |> Proof_Context.cterm_of ctxt
in
PROFILE "Proof Reconstruction"
(CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1
@@ -307,7 +307,7 @@
fun gen_decomp_scnp_tac orders autom_tac ctxt =
Termination.TERMINATION ctxt autom_tac (fn D =>
let
- val decompose = Termination.decompose_tac D
+ val decompose = Termination.decompose_tac ctxt D
val scnp_full = single_scnp_tac true orders ctxt D
in
REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
--- a/src/HOL/Tools/Function/termination.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Function/termination.ML Fri Mar 06 14:01:08 2015 +0100
@@ -29,7 +29,7 @@
val wf_union_tac : Proof.context -> tactic
- val decompose_tac : ttac
+ val decompose_tac : Proof.context -> ttac
end
@@ -137,14 +137,14 @@
mk_skel (fold collect_pats cs [])
end
-fun prove_chain thy chain_tac (c1, c2) =
+fun prove_chain ctxt chain_tac (c1, c2) =
let
val goal =
HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2),
Const (@{const_abbrev Set.empty}, fastype_of c1))
|> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
in
- case Function_Lib.try_proof (Thm.cterm_of thy goal) chain_tac of
+ case Function_Lib.try_proof (Proof_Context.cterm_of ctxt goal) chain_tac of
Function_Lib.Solved thm => SOME thm
| _ => NONE
end
@@ -166,10 +166,10 @@
fun dest_call (sk, _, _, _, _) = dest_call' sk
-fun mk_desc thy tac vs Gam l r m1 m2 =
+fun mk_desc ctxt tac vs Gam l r m1 m2 =
let
fun try rel =
- try_proof (Thm.cterm_of thy
+ try_proof (Proof_Context.cterm_of ctxt
(Logic.list_all (vs,
Logic.mk_implies (HOLogic.mk_Trueprop Gam,
HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
@@ -187,23 +187,24 @@
| _ => raise Match
end
-fun prove_descent thy tac sk (c, (m1, m2)) =
+fun prove_descent ctxt tac sk (c, (m1, m2)) =
let
val (vs, _, l, _, r, Gam) = dest_call' sk c
in
- mk_desc thy tac vs Gam l r m1 m2
+ mk_desc ctxt tac vs Gam l r m1 m2
end
fun create ctxt chain_tac descent_tac T rel =
let
- val thy = Proof_Context.theory_of ctxt
val sk = mk_sum_skel rel
val Ts = node_types sk T
val M = Inttab.make (map_index (apsnd (Measure_Functions.get_measure_functions ctxt)) Ts)
- val chain_cache = Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
- (prove_chain thy chain_tac)
- val descent_cache = Cache.create Term3tab.empty Term3tab.lookup Term3tab.update
- (prove_descent thy descent_tac sk)
+ val chain_cache =
+ Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
+ (prove_chain ctxt chain_tac)
+ val descent_cache =
+ Cache.create Term3tab.empty Term3tab.lookup Term3tab.update
+ (prove_descent ctxt descent_tac sk)
in
(sk, nth Ts, M, chain_cache, descent_cache)
end
@@ -275,7 +276,6 @@
fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
- val cert = Thm.cterm_of thy
val ((_ $ (_ $ rel)) :: ineqs) = Thm.prems_of st
fun mk_compr ineq =
@@ -302,7 +302,7 @@
THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *)
) i
in
- (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
+ (PRIMITIVE (Drule.cterm_instantiate [apply2 (Proof_Context.cterm_of ctxt) (rel, relation)])
THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
THEN rewrite_goal_tac ctxt Un_aci_simps 1) (* eliminate duplicates *)
end) 1 st
@@ -326,7 +326,7 @@
ORELSE' rtac @{thm union_comp_emptyL}
ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
-fun regroup_calls_tac cs = CALLS (fn (cs', i) =>
+fun regroup_calls_tac ctxt cs = CALLS (fn (cs', i) =>
let
val is = map (fn c => find_index (curry op aconv c) cs') cs
in
@@ -342,14 +342,14 @@
| _ => no_tac)
| _ => no_tac)
-fun decompose_tac D = CALLS (fn (cs, i) =>
+fun decompose_tac ctxt D = CALLS (fn (cs, i) =>
let
val G = mk_dgraph D cs
val sccs = Term_Graph.strong_conn G
fun split [SCC] i = TRY (solve_trivial_tac D i)
| split (SCC::rest) i =
- regroup_calls_tac SCC i
+ regroup_calls_tac ctxt SCC i
THEN rtac @{thm wf_union_compatible} i
THEN rtac @{thm less_by_empty} (i + 2)
THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
--- a/src/HOL/Tools/Meson/meson.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Meson/meson.ML Fri Mar 06 14:01:08 2015 +0100
@@ -352,10 +352,10 @@
in
fun freeze_spec th ctxt =
let
- val cert = Proof_Context.cterm_of ctxt;
val ([x], ctxt') =
Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
- val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
+ val spec' = spec
+ |> Thm.instantiate ([], [(spec_var, Proof_Context.cterm_of ctxt' (Free (x, spec_varT)))]);
in (th RS spec', ctxt') end
end;
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Mar 06 14:01:08 2015 +0100
@@ -398,21 +398,19 @@
(case Thm.tpairs_of th of
[] => th
| pairs =>
- let
- val thy = Thm.theory_of_thm th
- val cert = Thm.cterm_of thy
- val certT = Thm.ctyp_of thy
- val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
-
- fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
- fun mk (v, (T, t)) = (cert (Var (v, Envir.subst_type tyenv T)), cert t)
-
- val instsT = Vartab.fold (cons o mkT) tyenv []
- val insts = Vartab.fold (cons o mk) tenv []
- in
- Thm.instantiate (instsT, insts) th
- end
- handle THM _ => th)
+ let
+ val thy = Thm.theory_of_thm th
+ val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
+
+ fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of thy) (TVar (v, S), T)
+ fun mk (v, (T, t)) = apply2 (Thm.cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
+
+ val instsT = Vartab.fold (cons o mkT) tyenv []
+ val insts = Vartab.fold (cons o mk) tenv []
+ in
+ Thm.instantiate (instsT, insts) th
+ end
+ handle THM _ => th)
fun is_metis_literal_genuine (_, (s, _)) =
not (String.isPrefix class_prefix (Metis_Name.toString s))
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Mar 06 14:01:08 2015 +0100
@@ -609,8 +609,6 @@
val (indrule_lemma_prems, indrule_lemma_concls) =
split_list (map2 mk_indrule_lemma descr' recTs);
- val cert = Thm.cterm_of thy6;
-
val indrule_lemma =
Goal.prove_sorry_global thy6 [] []
(Logic.mk_implies
@@ -627,7 +625,8 @@
val frees =
if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
else map (Free o apfst fst o dest_Var) Ps;
- val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
+ val indrule_lemma' =
+ cterm_instantiate (map (Thm.cterm_of thy6) Ps ~~ map (Thm.cterm_of thy6) frees) indrule_lemma;
val dt_induct_prop = Old_Datatype_Prop.make_ind descr;
val dt_induct =
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Mar 06 14:01:08 2015 +0100
@@ -126,7 +126,7 @@
fun ind_tac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
let
- val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
+ val thy = Thm.theory_of_cterm cgoal;
val goal = Thm.term_of cgoal;
val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule));
val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal));
@@ -148,7 +148,8 @@
map_filter (fn (t, u) =>
(case abstr (getP u) of
NONE => NONE
- | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts');
+ | SOME u' =>
+ SOME (apply2 (Thm.cterm_of thy) (t |> getP |> snd |> head_of, u')))) (ts ~~ ts');
val indrule' = cterm_instantiate insts indrule;
in resolve0_tac [indrule'] i end);
@@ -157,7 +158,6 @@
fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
let
- val thy = Thm.theory_of_cterm cgoal;
val goal = Thm.term_of cgoal;
val params = Logic.strip_params goal;
val (_, Type (tname, _)) = hd (rev params);
@@ -166,8 +166,8 @@
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
val exhaustion' =
cterm_instantiate
- [(Thm.cterm_of thy (head_of lhs),
- Thm.cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))]
+ [apply2 (Proof_Context.cterm_of ctxt)
+ (head_of lhs, fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0))]
exhaustion;
in compose_tac ctxt (false, exhaustion', Thm.nprems_of exhaustion) i end);
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Mar 06 14:01:08 2015 +0100
@@ -46,8 +46,7 @@
Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
Var (("P", 0), HOLogic.boolT));
val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
- val cert = Thm.cterm_of thy;
- val insts' = map cert induct_Ps ~~ map cert insts;
+ val insts' = map (Thm.cterm_of thy) induct_Ps ~~ map (Thm.cterm_of thy) insts;
val induct' =
refl RS
(nth (Old_Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i
@@ -204,11 +203,12 @@
Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
absfree ("y", T2) (set_t $ Old_Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
(rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
- val cert = Thm.cterm_of thy1;
val insts =
map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
- val induct' = cterm_instantiate (map cert induct_Ps ~~ map cert insts) induct;
+ val induct' = induct
+ |> cterm_instantiate
+ (map (Thm.cterm_of thy1) induct_Ps ~~ map (Thm.cterm_of thy1) insts);
in
Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
(HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
@@ -379,9 +379,9 @@
fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
let
- val cert = Thm.cterm_of thy;
val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
- val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
+ val exhaustion' = exhaustion
+ |> cterm_instantiate [apply2 (Thm.cterm_of thy) (lhs, Free ("x", T))];
fun tac ctxt =
EVERY [resolve_tac ctxt [exhaustion'] 1,
ALLGOALS (asm_simp_tac
@@ -450,10 +450,10 @@
let
val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
- val cert = Thm.cterm_of thy;
val nchotomy' = nchotomy RS spec;
val [v] = Term.add_vars (Thm.concl_of nchotomy') [];
- val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy';
+ val nchotomy'' =
+ cterm_instantiate [apply2 (Thm.cterm_of thy) (Var v, Ma)] nchotomy';
in
Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {context = ctxt, prems, ...} =>
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 06 14:01:08 2015 +0100
@@ -89,24 +89,25 @@
(HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
val Type (_, [_, iT]) = T;
val icT = Thm.ctyp_of thy iT;
- val cert = Thm.cterm_of thy;
val inst = Thm.instantiate_cterm ([(aT, icT)], []);
fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
val t_rhs = lambda t_k proto_t_rhs;
val eqs0 = [subst_v @{term "0::natural"} eq,
subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
- val ((_, (_, eqs2)), lthy') = BNF_LFP_Compat.add_primrec_simple
- [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
+ val ((_, (_, eqs2)), lthy') = lthy
+ |> BNF_LFP_Compat.add_primrec_simple
+ [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1;
val cT_random_aux = inst pt_random_aux;
val cT_rhs = inst pt_rhs;
val rule = @{thm random_aux_rec}
- |> Drule.instantiate_normalize ([(aT, icT)],
- [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
+ |> Drule.instantiate_normalize
+ ([(aT, icT)],
+ [(cT_random_aux, Thm.cterm_of thy t_random_aux), (cT_rhs, Thm.cterm_of thy t_rhs)]);
fun tac ctxt =
ALLGOALS (rtac rule)
THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
- THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
+ THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2));
val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
in (simp, lthy') end;
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Mar 06 14:01:08 2015 +0100
@@ -108,15 +108,13 @@
fun match_instantiateT ctxt t thm =
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- let val certT = Proof_Context.ctyp_of ctxt
- in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
+ Thm.instantiate (gen_certify_inst fst TVar (Proof_Context.ctyp_of ctxt) ctxt thm t, []) thm
else thm
fun match_instantiate ctxt t thm =
- let
- val cert = Proof_Context.cterm_of ctxt
- val thm' = match_instantiateT ctxt t thm
- in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
+ let val thm' = match_instantiateT ctxt t thm in
+ Thm.instantiate ([], gen_certify_inst snd Var (Proof_Context.cterm_of ctxt) ctxt thm' t) thm'
+ end
fun apply_rule ctxt t =
(case Z3_Replay_Rules.apply ctxt (certify_prop ctxt t) of
--- a/src/HOL/Tools/code_evaluation.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/code_evaluation.ML Fri Mar 06 14:01:08 2015 +0100
@@ -204,13 +204,13 @@
fun certify_eval ctxt value conv ct =
let
- val cert = Proof_Context.cterm_of ctxt;
val t = Thm.term_of ct;
val T = fastype_of t;
- val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
+ val mk_eq =
+ Thm.mk_binop (Proof_Context.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT)));
in case value ctxt t
of NONE => Thm.reflexive ct
- | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
+ | SOME t' => conv ctxt (mk_eq ct (Proof_Context.cterm_of ctxt t')) RS @{thm eq_eq_TrueD}
handle THM _ =>
error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
end;
--- a/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 14:01:08 2015 +0100
@@ -27,7 +27,6 @@
fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
let
val ctxt = Proof_Context.init_global thy;
- val cert = Thm.cterm_of thy;
val recTs = Old_Datatype_Aux.get_rec_types descr;
val pnames =
@@ -106,11 +105,11 @@
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
- val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
+ val inst = map (apply2 (Thm.cterm_of thy)) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
val thm =
- Goal.prove_internal ctxt (map cert prems) (cert concl)
+ Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems) (Thm.cterm_of thy concl)
(fn prems =>
EVERY [
rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
@@ -160,7 +159,6 @@
fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
let
val ctxt = Proof_Context.init_global thy;
- val cert = Thm.cterm_of thy;
val rT = TFree ("'P", @{sort type});
val rT' = TVar (("'P", 0), @{sort type});
@@ -187,11 +185,12 @@
val y' = Free ("y", T);
val thm =
- Goal.prove_internal ctxt (map cert prems)
- (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
+ Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems)
+ (Thm.cterm_of thy
+ (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
(fn prems =>
EVERY [
- rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
+ rtac (cterm_instantiate [apply2 (Thm.cterm_of thy) (y, y')] exhaust) 1,
ALLGOALS (EVERY'
[asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
--- a/src/HOL/Tools/record.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/record.ML Fri Mar 06 14:01:08 2015 +0100
@@ -1460,8 +1460,6 @@
avoid problems with higher order unification.*)
fun try_param_tac ctxt s rule = CSUBGOAL (fn (cgoal, i) =>
let
- val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
-
val g = Thm.term_of cgoal;
val params = Logic.strip_params g;
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
@@ -1475,7 +1473,7 @@
| [x] => (head_of x, false));
val rule'' =
cterm_instantiate
- (map (apply2 cert)
+ (map (apply2 (Proof_Context.cterm_of ctxt))
(case rev params of
[] =>
(case AList.lookup (op =) (Term.add_frees g []) s of
--- a/src/HOL/Tools/reification.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/HOL/Tools/reification.ML Fri Mar 06 14:01:08 2015 +0100
@@ -48,7 +48,6 @@
let
val Const (fN, _) = th |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
|> fst |> strip_comb |> fst;
- val cert = Proof_Context.cterm_of ctxt;
val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
fun add_fterms (t as t1 $ t2) =
@@ -84,7 +83,7 @@
(fn {context, prems, ...} =>
Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym;
val (cong' :: vars') =
- Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs);
+ Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o Proof_Context.cterm_of ctxt'') vs);
val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
in (vs', cong') end;
@@ -134,8 +133,6 @@
fun decomp_reify da cgns (ct, ctxt) bds =
let
val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
fun tryabsdecomp (ct, ctxt) bds =
(case Thm.term_of ct of
Abs (_, xT, ta) =>
@@ -143,8 +140,8 @@
val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt;
val (xn, ta) = Syntax_Trans.variant_abs (raw_xn, xT, ta); (* FIXME !? *)
val x = Free (xn, xT);
- val cx = cert x;
- val cta = cert ta;
+ val cx = Proof_Context.cterm_of ctxt' x;
+ val cta = Proof_Context.cterm_of ctxt' ta;
val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of
NONE => error "tryabsdecomp: Type not found in the Environement"
| SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT,
@@ -172,10 +169,12 @@
val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv);
val (fts, its) =
(map (snd o snd) fnvs,
- map (fn ((vn, vi), (tT, t)) => (cert (Var ((vn, vi), tT)), cert t)) invs);
- val ctyenv = map (fn ((vn, vi), (s, ty)) => (certT (TVar((vn, vi), s)), certT ty)) (Vartab.dest tyenv);
+ map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of thy) (Var ((vn, vi), tT), t)) invs);
+ val ctyenv =
+ map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of thy) (TVar ((vn, vi), s), ty))
+ (Vartab.dest tyenv);
in
- ((map cert fts ~~ replicate (length fts) ctxt,
+ ((map (Thm.cterm_of thy) fts ~~ replicate (length fts) ctxt,
apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds))
end;
@@ -196,8 +195,6 @@
val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt;
val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt';
val thy = Proof_Context.theory_of ctxt'';
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
val vsns_map = vss ~~ vsns;
val xns_map = fst (split_list nths) ~~ xns;
val subst = map (fn (nt, xn) => (nt, Var ((xn, 0), fastype_of nt))) xns_map;
@@ -205,15 +202,15 @@
val (tyenv, tmenv) = Pattern.match thy (rhs_P, Thm.term_of ct) (Vartab.empty, Vartab.empty);
val sbst = Envir.subst_term (tyenv, tmenv);
val sbsT = Envir.subst_type tyenv;
- val subst_ty = map (fn (n, (s, t)) =>
- (certT (TVar (n, s)), certT t)) (Vartab.dest tyenv)
+ val subst_ty =
+ map (fn (n, (s, t)) => apply2 (Thm.ctyp_of thy) (TVar (n, s), t)) (Vartab.dest tyenv)
val tml = Vartab.dest tmenv;
val (subst_ns, bds) = fold_map
(fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
let
val name = snd (the (AList.lookup (op =) tml xn0));
val (idx, bds) = index_of name bds;
- in ((cert n, idx |> (HOLogic.mk_nat #> cert)), bds) end) subst bds;
+ in (apply2 (Thm.cterm_of thy) (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
val subst_vs =
let
fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
@@ -222,12 +219,13 @@
val lT' = sbsT lT;
val (bsT, _) = the (AList.lookup Type.could_unify bds lT);
val vsn = the (AList.lookup (op =) vsns_map vs);
- val cvs = cert (fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT')));
- in (cert vs, cvs) end;
+ val vs' = fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT'));
+ in apply2 (Thm.cterm_of thy) (vs, vs') end;
in map h subst end;
- val cts = map (fn ((vn, vi), (tT, t)) => (cert (Var ((vn, vi), tT)), cert t))
- (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
- (map (fn n => (n, 0)) xns) tml);
+ val cts =
+ map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of thy) (Var ((vn, vi), tT), t))
+ (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
+ (map (fn n => (n, 0)) xns) tml);
val substt =
let
val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
@@ -261,15 +259,17 @@
|> fst)) eqs [];
val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs [];
val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt;
- val cert = Proof_Context.cterm_of ctxt';
val subst =
- the o AList.lookup (op =) (map2 (fn T => fn v => (T, cert (Free (v, T)))) tys vs);
+ the o AList.lookup (op =)
+ (map2 (fn T => fn v => (T, Proof_Context.cterm_of ctxt' (Free (v, T)))) tys vs);
fun prep_eq eq =
let
val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> fst |> strip_comb;
- val subst = map_filter (fn (v as Var (_, T)) => SOME (cert v, subst T)
- | _ => NONE) vs;
+ val subst =
+ map_filter
+ (fn (v as Var (_, T)) => SOME (Proof_Context.cterm_of ctxt' v, subst T)
+ | _ => NONE) vs;
in Thm.instantiate ([], subst) eq end;
val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
val bds = AList.make (K ([], [])) tys;
@@ -285,10 +285,9 @@
| is_list_var _ = false;
val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd
|> strip_comb |> snd |> filter is_list_var;
- val cert = Proof_Context.cterm_of ctxt;
val vs = map (fn v as Var (_, T) =>
(v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
- val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th;
+ val th' = Drule.instantiate_normalize ([], map (apply2 (Proof_Context.cterm_of ctxt)) vs) th;
val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
in Thm.transitive th'' th' end;
--- a/src/Pure/Isar/element.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/element.ML Fri Mar 06 14:01:08 2015 +0100
@@ -201,9 +201,9 @@
(case Object_Logic.elim_concl th of
SOME C =>
let
- val cert = Thm.cterm_of (Thm.theory_of_thm th);
+ val thy = Thm.theory_of_thm th;
val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
- val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
+ val th' = Thm.instantiate ([], [(Thm.cterm_of thy C, Thm.cterm_of thy thesis)]) th;
in (th', true) end
| NONE => (th, false));
@@ -338,9 +338,8 @@
fun instantiate_tfrees thy subst th =
let
- val certT = Thm.ctyp_of thy;
val idx = Thm.maxidx_of th + 1;
- fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T);
+ fun cert_inst (a, (S, T)) = (Thm.ctyp_of thy (TVar ((a, idx), S)), Thm.ctyp_of thy T);
fun add_inst (a, S) insts =
if AList.defined (op =) insts a then insts
@@ -355,10 +354,8 @@
end;
fun instantiate_frees thy subst =
- let val cert = Thm.cterm_of thy in
- Drule.forall_intr_list (map (cert o Free o fst) subst) #>
- Drule.forall_elim_list (map (cert o snd) subst)
- end;
+ Drule.forall_intr_list (map (Thm.cterm_of thy o Free o fst) subst) #>
+ Drule.forall_elim_list (map (Thm.cterm_of thy o snd) subst);
fun hyps_rule rule th =
let val {hyps, ...} = Thm.crep_thm th in
--- a/src/Pure/Isar/expression.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/expression.ML Fri Mar 06 14:01:08 2015 +0100
@@ -678,18 +678,17 @@
[((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
- val cert = Thm.cterm_of defs_thy;
-
val intro = Goal.prove_global defs_thy [] norm_ts statement
(fn {context = ctxt, ...} =>
rewrite_goals_tac ctxt [pred_def] THEN
compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
compose_tac defs_ctxt
- (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+ (false,
+ Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_thy) norm_ts), 0) 1);
val conjuncts =
(Drule.equal_elim_rule2 OF
- [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
+ [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_thy statement))])
|> Conjunction.elim_balanced (length ts);
val (_, axioms_ctxt) = defs_ctxt
--- a/src/Pure/Isar/generic_target.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/generic_target.ML Fri Mar 06 14:01:08 2015 +0100
@@ -176,11 +176,10 @@
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
let
- val thy = Proof_Context.theory_of lthy;
- val thy_ctxt = Proof_Context.init_global thy;
+ val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
(*term and type parameters*)
- val ((defs, _), rhs') = Thm.cterm_of thy rhs
+ val ((defs, _), rhs') = Proof_Context.cterm_of lthy rhs
|> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
val xs = Variable.add_fixed lthy rhs' [];
@@ -218,10 +217,7 @@
fun import_export_proof ctxt (name, raw_th) =
let
- val thy = Proof_Context.theory_of ctxt;
- val thy_ctxt = Proof_Context.init_global thy;
- val certT = Thm.ctyp_of thy;
- val cert = Thm.cterm_of thy;
+ val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt);
(*export assumes/defines*)
val th = Goal.norm_result ctxt raw_th;
@@ -232,7 +228,7 @@
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
val frees = map Free (Thm.fold_terms Term.add_frees th' []);
val (th'' :: vs) =
- (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
+ (th' :: map (Drule.mk_term o Proof_Context.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
|> Variable.export ctxt thy_ctxt
|> Drule.zero_var_indexes_list;
@@ -246,8 +242,10 @@
val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
val inst = filter (is_Var o fst) (vars ~~ frees);
- val cinstT = map (apply2 certT o apfst TVar) instT;
- val cinst = map (apply2 (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
+ val cinstT = instT
+ |> map (apply2 (Proof_Context.ctyp_of ctxt) o apfst TVar);
+ val cinst = inst
+ |> map (apply2 (Proof_Context.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
val result' = Thm.instantiate (cinstT, cinst) result;
(*import assumes/defines*)
--- a/src/Pure/Isar/obtain.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/obtain.ML Fri Mar 06 14:01:08 2015 +0100
@@ -112,8 +112,6 @@
name raw_vars raw_asms int state =
let
val _ = Proof.assert_forward_or_chain state;
- val thy = Proof.theory_of state;
- val cert = Thm.cterm_of thy;
val ctxt = Proof.context_of state;
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
@@ -131,6 +129,7 @@
(*obtain parms*)
val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
val parms = map Free (xs' ~~ Ts);
+ val cparms = map (Proof_Context.cterm_of ctxt) parms;
val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
(*obtain statements*)
@@ -149,7 +148,7 @@
Proof.local_qed (NONE, false)
#> `Proof.the_fact #-> (fn rule =>
Proof.fix vars
- #> Proof.assm (obtain_export fix_ctxt rule (map cert parms)) asms);
+ #> Proof.assm (obtain_export fix_ctxt rule cparms) asms);
in
state
|> Proof.enter_forward
@@ -187,18 +186,18 @@
fun result tac facts ctxt =
let
- val cert = Proof_Context.cterm_of ctxt;
-
val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
+ val st = Goal.init (Proof_Context.cterm_of ctxt thesis);
val rule =
- (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
+ (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
| SOME th =>
check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
- val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
+ val closed_rule = Thm.forall_intr (Proof_Context.cterm_of ctxt (Free thesis_var)) rule;
val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
- val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
+ val obtain_rule =
+ Thm.forall_elim (Proof_Context.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule';
val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
val (prems, ctxt'') =
Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
@@ -214,8 +213,6 @@
fun unify_params vars thesis_var raw_rule ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val certT = Thm.ctyp_of thy;
- val cert = Thm.cterm_of thy;
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
@@ -240,20 +237,20 @@
val xs = map (apsnd norm_type o fst) vars;
val ys = map (apsnd norm_type) (drop m params);
val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
- val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
+ val terms = map (Drule.mk_term o Thm.cterm_of thy o Free) (xs @ ys');
val instT =
fold (Term.add_tvarsT o #2) params []
- |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
+ |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
val closed_rule = rule
- |> Thm.forall_intr (cert (Free thesis_var))
+ |> Thm.forall_intr (Thm.cterm_of thy (Free thesis_var))
|> Thm.instantiate (instT, []);
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
val vars' =
map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
(map snd vars @ replicate (length ys) NoSyn);
- val rule'' = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
+ val rule'' = Thm.forall_elim (Thm.cterm_of thy (Logic.varify_global (Free thesis_var))) rule';
in ((vars', rule''), ctxt') end;
fun inferred_type (binding, _, mx) ctxt =
@@ -270,7 +267,6 @@
let
val _ = Proof.assert_forward_or_chain state;
val ctxt = Proof.context_of state;
- val cert = Proof_Context.cterm_of ctxt;
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
@@ -292,7 +288,8 @@
|> Proof.map_context (K ctxt')
|> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
- (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
+ (obtain_export fix_ctxt rule (map (Proof_Context.cterm_of ctxt) ts))
+ [(Thm.empty_binding, asms)])
|> Proof.bind_terms Auto_Bind.no_facts
end;
@@ -314,7 +311,8 @@
|> Proof.chain_facts chain_facts
|> Proof.local_goal print_result (K I) (pair o rpair I)
"guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
- |> Proof.refine (Method.primitive_text (fn _ => fn _ => Goal.init (cert thesis))) |> Seq.hd
+ |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
+ Goal.init (Proof_Context.cterm_of ctxt thesis))) |> Seq.hd
end;
in
--- a/src/Pure/Isar/proof.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/proof.ML Fri Mar 06 14:01:08 2015 +0100
@@ -894,7 +894,6 @@
fun generic_goal prepp kind before_qed after_qed raw_propp state =
let
val ctxt = context_of state;
- val cert = Proof_Context.cterm_of ctxt;
val chaining = can assert_chain state;
val pos = Position.thread_data ();
@@ -910,7 +909,8 @@
val propss' = vars :: propss;
val goal_propss = filter_out null propss';
val goal =
- cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
+ Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
+ |> Proof_Context.cterm_of ctxt
|> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
val statement = ((kind, pos), propss', Thm.term_of goal);
val after_qed' = after_qed |>> (fn after_local =>
--- a/src/Pure/Isar/proof_context.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Isar/proof_context.ML Fri Mar 06 14:01:08 2015 +0100
@@ -1166,10 +1166,10 @@
fun gen_assms prepp exp args ctxt =
let
- val cert = cterm_of ctxt;
val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
val _ = Variable.warn_extra_tfrees ctxt ctxt1;
- val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1;
+ val (premss, ctxt2) =
+ fold_burrow (Assumption.add_assms exp o map (cterm_of ctxt)) propss ctxt1;
in
ctxt2
|> auto_bind_facts (flat propss)
--- a/src/Pure/Tools/rule_insts.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/Tools/rule_insts.ML Fri Mar 06 14:01:08 2015 +0100
@@ -81,8 +81,6 @@
fun read_insts ctxt mixed_insts (tvars, vars) =
let
val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts;
@@ -118,7 +116,8 @@
val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
val inst_vars = map_filter (make_inst inst2) vars2;
in
- (map (apply2 certT) inst_tvars, map (apply2 cert) inst_vars)
+ (map (apply2 (Thm.ctyp_of thy)) inst_tvars,
+ map (apply2 (Thm.cterm_of thy)) inst_vars)
end;
fun where_rule ctxt mixed_insts fixes thm =
@@ -282,9 +281,9 @@
fun make_elim_preserve ctxt rl =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm rl);
+ val thy = Thm.theory_of_thm rl;
val maxidx = Thm.maxidx_of rl;
- fun cvar xi = cert (Var (xi, propT));
+ fun cvar xi = Thm.cterm_of thy (Var (xi, propT));
val revcut_rl' =
Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
(cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
--- a/src/Pure/drule.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/drule.ML Fri Mar 06 14:01:08 2015 +0100
@@ -210,10 +210,8 @@
(*generalize outermost parameters*)
fun gen_all th =
let
- val thy = Thm.theory_of_thm th;
- val {prop, maxidx, ...} = Thm.rep_thm th;
- val cert = Thm.cterm_of thy;
- fun elim (x, T) = Thm.forall_elim (cert (Var ((x, maxidx + 1), T)));
+ val {thy, prop, maxidx, ...} = Thm.rep_thm th;
+ fun elim (x, T) = Thm.forall_elim (Thm.cterm_of thy (Var ((x, maxidx + 1), T)));
in fold elim (outer_params prop) th end;
(*lift vars wrt. outermost goal parameters
@@ -221,16 +219,15 @@
fun lift_all goal th =
let
val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
- val cert = Thm.cterm_of thy;
val maxidx = Thm.maxidx_of th;
val ps = outer_params (Thm.term_of goal)
|> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
val Ts = map Term.fastype_of ps;
val inst = Thm.fold_terms Term.add_vars th [] |> map (fn (xi, T) =>
- (cert (Var (xi, T)), cert (Term.list_comb (Var (xi, Ts ---> T), ps))));
+ (Thm.cterm_of thy (Var (xi, T)), Thm.cterm_of thy (Term.list_comb (Var (xi, Ts ---> T), ps))));
in
th |> Thm.instantiate ([], inst)
- |> fold_rev (Thm.forall_intr o cert) ps
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) ps
end;
(*direct generalization*)
@@ -250,10 +247,9 @@
| zero_var_indexes_list ths =
let
val thy = Theory.merge_list (map Thm.theory_of_thm ths);
- val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
- val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
- val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
+ val cinstT = map (fn (v, T) => (Thm.ctyp_of thy (TVar v), Thm.ctyp_of thy T)) instT;
+ val cinst = map (fn (v, t) => (Thm.cterm_of thy (Var v), Thm.cterm_of thy t)) inst;
in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
val zero_var_indexes = singleton zero_var_indexes_list;
@@ -647,12 +643,10 @@
fun mk_term ct =
let
val thy = Thm.theory_of_cterm ct;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
val T = Thm.typ_of_cterm ct;
- val a = certT (TVar (("'a", 0), []));
- val x = cert (Var (("x", 0), T));
- in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
+ val a = Thm.ctyp_of thy (TVar (("'a", 0), []));
+ val x = Thm.cterm_of thy (Var (("x", 0), T));
+ in Thm.instantiate ([(a, Thm.ctyp_of thy T)], [(x, ct)]) termI end;
fun dest_term th =
let val cprop = strip_imp_concl (Thm.cprop_of th) in
@@ -793,10 +787,9 @@
| cterm_instantiate ctpairs th =
let
val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0);
- val certT = Thm.ctyp_of thy;
val instT =
Vartab.fold (fn (xi, (S, T)) =>
- cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye [];
+ cons (Thm.ctyp_of thy (TVar (xi, S)), Thm.ctyp_of thy (Envir.norm_type tye T))) tye [];
val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs;
in instantiate_normalize (instT, inst) th end
handle TERM (msg, _) => raise THM (msg, 0, [th])
@@ -846,18 +839,18 @@
fun rename_bvars [] thm = thm
| rename_bvars vs thm =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+ val thy = Thm.theory_of_thm thm;
fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t)
| ren (t $ u) = ren t $ ren u
| ren t = t;
- in Thm.equal_elim (Thm.reflexive (cert (ren (Thm.prop_of thm)))) thm end;
+ in Thm.equal_elim (Thm.reflexive (Thm.cterm_of thy (ren (Thm.prop_of thm)))) thm end;
(* renaming in left-to-right order *)
fun rename_bvars' xs thm =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+ val thy = Thm.theory_of_thm thm;
val prop = Thm.prop_of thm;
fun rename [] t = ([], t)
| rename (x' :: xs) (Abs (x, T, t)) =
@@ -869,9 +862,10 @@
val (xs'', u') = rename xs' u
in (xs'', t' $ u') end
| rename xs t = (xs, t);
- in case rename xs prop of
- ([], prop') => Thm.equal_elim (Thm.reflexive (cert prop')) thm
- | _ => error "More names than abstractions in theorem"
+ in
+ (case rename xs prop of
+ ([], prop') => Thm.equal_elim (Thm.reflexive (Thm.cterm_of thy prop')) thm
+ | _ => error "More names than abstractions in theorem")
end;
end;
--- a/src/Pure/goal.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/goal.ML Fri Mar 06 14:01:08 2015 +0100
@@ -128,20 +128,20 @@
fun future_result ctxt result prop =
let
val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
val assms = Assumption.all_assms_of ctxt;
val As = map Thm.term_of assms;
val xs = map Free (fold Term.add_frees (prop :: As) []);
- val fixes = map cert xs;
+ val fixes = map (Thm.cterm_of thy) xs;
val tfrees = fold Term.add_tfrees (prop :: As) [];
- val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
+ val instT =
+ map (fn (a, S) => (Thm.ctyp_of thy (TVar ((a, 0), S)), Thm.ctyp_of thy (TFree (a, S)))) tfrees;
val global_prop =
- cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
+ Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
+ |> Thm.cterm_of thy
|> Thm.weaken_sorts (Variable.sorts_of ctxt);
val global_result = result |> Future.map
(Drule.flexflex_unique (SOME ctxt) #>
--- a/src/Pure/more_thm.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/more_thm.ML Fri Mar 06 14:01:08 2015 +0100
@@ -116,18 +116,21 @@
fun add_cterm_frees ct =
let
- val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
+ val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
- in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (cert v) | _ => I) t end;
+ in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.cterm_of thy v) | _ => I) t end;
(* cterm constructors and destructors *)
fun all_name (x, t) A =
let
- val cert = Thm.cterm_of (Thm.theory_of_cterm t);
+ val thy = Thm.theory_of_cterm t;
val T = Thm.typ_of_cterm t;
- in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
+ in
+ Thm.apply (Thm.cterm_of thy (Const ("Pure.all", (T --> propT) --> propT)))
+ (Thm.lambda_name (x, t) A)
+ end;
fun all t A = all_name ("", t) A;
--- a/src/Pure/subgoal.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/subgoal.ML Fri Mar 06 14:01:08 2015 +0100
@@ -67,7 +67,6 @@
*)
fun lift_import idx params th ctxt =
let
- val cert = Proof_Context.cterm_of ctxt;
val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
val Ts = map Thm.typ_of_cterm params;
@@ -86,7 +85,8 @@
else (Ts ---> T, ts);
val u = Free (y, U);
in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
- val (inst1, inst2) = split_list (map (apply2 (apply2 cert)) (map2 var_inst vars ys));
+ val (inst1, inst2) =
+ split_list (map (apply2 (apply2 (Proof_Context.cterm_of ctxt))) (map2 var_inst vars ys));
val th'' = Thm.instantiate ([], inst1) th';
in ((inst2, th''), ctxt'') end;
--- a/src/Pure/variable.ML Fri Mar 06 12:48:03 2015 +0000
+++ b/src/Pure/variable.ML Fri Mar 06 14:01:08 2015 +0100
@@ -587,9 +587,9 @@
fun focus_cterm goal ctxt =
let
- val cert = Thm.cterm_of (Thm.theory_of_cterm goal);
+ val thy = Thm.theory_of_cterm goal;
val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
- val ps' = map (cert o Free) ps;
+ val ps' = map (Thm.cterm_of thy o Free) ps;
val goal' = fold forall_elim_prop ps' goal;
in ((xs ~~ ps', goal'), ctxt') end;