--- a/src/HOL/Tools/Function/fun_cases.ML Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/fun_cases.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_context_tree.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/relation.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Mar 06 13:39:34 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 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/termination.ML Fri Mar 06 13:39:34 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)