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