--- a/Nominal/nominal_function_core.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_function_core.ML Thu Jul 09 02:32:46 2015 +0100
@@ -83,7 +83,7 @@
{no: int,
qglr : ((string * typ) list * term list * term * term),
cdata : clause_context,
- tree: Function_Ctx_Tree.ctx_tree,
+ tree: Function_Context_Tree.ctx_tree,
lGI: thm,
RCs: rec_call_info list}
@@ -109,7 +109,7 @@
([], (fixes, assumes, arg) :: xs)
| add_Ri _ _ _ _ = raise Match
in
- rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
+ rev (Function_Context_Tree.traverse_tree add_Ri tree [])
end
(* nominal *)
@@ -147,14 +147,14 @@
(** building proof obligations *)
fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) =
mk_eqvt_at (fvar, arg)
- |> curry Logic.list_implies (map prop_of assms)
+ |> curry Logic.list_implies (map Thm.prop_of assms)
|> fold_rev (Logic.all o Free) vs
|> fold_rev absfree qs
|> strip_abs_body
fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) =
mk_inv inv (fvar, arg)
- |> curry Logic.list_implies (map prop_of assms)
+ |> curry Logic.list_implies (map Thm.prop_of assms)
|> fold_rev (Logic.all o Free) vs
|> fold_rev absfree qs
|> strip_abs_body
@@ -207,17 +207,15 @@
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 (cterm_of thy) qs
- val ags = map (Thm.assume o cterm_of thy) gs
+ val cqs = map (Thm.cterm_of ctxt') qs
+ val ags = map (Thm.assume o Thm.cterm_of ctxt') gs
- val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
+ val case_hyp = Thm.assume (Thm.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 }
@@ -245,7 +243,7 @@
val Globals {h, ...} = globals
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
+ val cert = Thm.cterm_of ctxt
(* Instantiate the GIntro thm with "f" and import into the clause context. *)
val lGI = GIntro_thm
@@ -263,7 +261,7 @@
val h_assum =
HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
|> fold_rev (Logic.all o Free) rcfix
|> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] []
|> abstract_over_list (rev qs)
@@ -293,12 +291,12 @@
(* nominal *)
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
(* if j < i, then turn around *)
-fun get_compat_thm thy cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj =
+fun get_compat_thm ctxt cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj =
let
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
- val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
+ val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
in if j < i then
let
@@ -333,7 +331,7 @@
(* Generates the replacement lemma in fully quantified form. *)
-fun mk_replacement_lemma thy h ih_elim clause =
+fun mk_replacement_lemma ctxt h ih_elim clause =
let
val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
RCs, tree, ...} = clause
@@ -346,16 +344,16 @@
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
val h_assums = map (fn RCInfo {h_assum, ...} =>
- Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+ Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs
val (eql, _) =
- Function_Ctx_Tree.rewrite_by_tree (Proof_Context.init_global thy)
+ Function_Context_Tree.rewrite_by_tree ctxt
h ih_elim_case (Ris ~~ h_assums) tree
val replace_lemma = (eql RS meta_eq_to_obj_eq)
- |> Thm.implies_intr (cprop_of case_hyp)
- |> fold_rev (Thm.implies_intr o cprop_of) h_assums
- |> fold_rev (Thm.implies_intr o cprop_of) ags
+ |> Thm.implies_intr (Thm.cprop_of case_hyp)
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev Thm.forall_intr cqs
|> Thm.close_derivation
in
@@ -364,7 +362,7 @@
(* nominal *)
(* Generates the eqvt lemmas for each clause *)
-fun mk_eqvt_lemma thy ih_eqvt clause =
+fun mk_eqvt_lemma ctxt ih_eqvt clause =
let
val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
@@ -377,18 +375,18 @@
fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) =
(llRI RS ih_eqvt_case)
- |> fold_rev (Thm.implies_intr o cprop_of) CCas
- |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
in
map prep_eqvt RCs
- |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
- |> map (Thm.implies_intr (cprop_of case_hyp))
+ |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags)
+ |> map (Thm.implies_intr (Thm.cprop_of case_hyp))
|> map (fold_rev Thm.forall_intr cqs)
|> map (Thm.close_derivation)
end
(* nominal *)
-fun mk_invariant_lemma thy ih_inv clause =
+fun mk_invariant_lemma ctxt ih_inv clause =
let
val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
@@ -401,19 +399,21 @@
fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) =
(llRI RS ih_inv_case)
- |> fold_rev (Thm.implies_intr o cprop_of) CCas
- |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
in
map prep_inv RCs
- |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
- |> map (Thm.implies_intr (cprop_of case_hyp))
+ |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags)
+ |> map (Thm.implies_intr (Thm.cprop_of case_hyp))
|> map (fold_rev Thm.forall_intr cqs)
|> map (Thm.close_derivation)
end
(* nominal *)
-fun mk_uniqueness_clause thy globals compat_store eqvts invs clausei clausej RLj =
+fun mk_uniqueness_clause ctxt globals compat_store eqvts invs clausei clausej RLj =
let
+ val thy = Proof_Context.theory_of ctxt
+
val Globals {h, y, x, fvar, ...} = globals
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi,
ags = agsi, ...}, ...} = clausei
@@ -425,10 +425,11 @@
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
val Ghsj' = map
- (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
+ (fn RCInfo {h_assum, ...} =>
+ Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj
- val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
- val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
+ val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+ val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
(* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
@@ -458,7 +459,7 @@
|> map (fold Thm.elim_implies [case_hypj'])
|> map (fold Thm.elim_implies agsj')
- val compat = get_compat_thm thy compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj
+ val compat = get_compat_thm ctxt compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj
in
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
@@ -468,70 +469,71 @@
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
|> (fn it => trans OF [y_eq_rhsj'h, it])
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
- |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
- |> fold_rev (Thm.implies_intr o cprop_of) agsj'
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) Ghsj'
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) agsj'
(* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
- |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
- |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
- |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
+ |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h)
+ |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj')
+ |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj')
end
(* nominal *)
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems
- clausei =
+fun mk_uniqueness_case ctxt
+ globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems clausei =
let
+ val thy = Proof_Context.theory_of ctxt
+
val Globals {x, y, ranT, fvar, ...} = globals
val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
val ih_intro_case =
- full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
+ full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp])
ih_intro
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) =
(llRI RS ih_intro_case)
- |> fold_rev (Thm.implies_intr o cprop_of) CCas
- |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
val existence = fold (curry op COMP o prep_RC) RCs lGI
- val P = cterm_of thy (mk_eq (y, rhsC))
- val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
+ val P = Thm.cterm_of ctxt (mk_eq (y, rhsC))
+ val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y)))
val unique_clauses =
- map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems
+ map2 (mk_uniqueness_clause ctxt globals compat_store eqvtlems invlems clausei) clauses replems
fun elim_implies_eta A AB =
- Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
+ Thm.bicompose NONE {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
|> Seq.list_of |> the_single
val uniqueness = G_cases
- |> Thm.forall_elim (cterm_of thy lhs)
- |> Thm.forall_elim (cterm_of thy y)
+ |> Thm.forall_elim (Thm.cterm_of ctxt lhs)
+ |> Thm.forall_elim (Thm.cterm_of ctxt y)
|> Thm.forall_elim P
|> Thm.elim_implies G_lhs_y
|> fold elim_implies_eta unique_clauses
- |> Thm.implies_intr (cprop_of G_lhs_y)
- |> Thm.forall_intr (cterm_of thy y)
+ |> Thm.implies_intr (Thm.cprop_of G_lhs_y)
+ |> Thm.forall_intr (Thm.cterm_of ctxt y)
- val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
+ val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
val exactly_one =
- ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+ ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
|> curry (op COMP) existence
|> curry (op COMP) uniqueness
- |> simplify
- (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp RS sym])
- |> Thm.implies_intr (cprop_of case_hyp)
- |> fold_rev (Thm.implies_intr o cprop_of) ags
+ |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
+ |> Thm.implies_intr (Thm.cprop_of case_hyp)
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev Thm.forall_intr cqs
val function_value =
existence
|> Thm.implies_intr ihyp
- |> Thm.implies_intr (cprop_of case_hyp)
- |> Thm.forall_intr (cterm_of thy x)
- |> Thm.forall_elim (cterm_of thy lhs)
+ |> Thm.implies_intr (Thm.cprop_of case_hyp)
+ |> Thm.forall_intr (Thm.cterm_of ctxt x)
+ |> Thm.forall_elim (Thm.cterm_of ctxt lhs)
|> curry (op RS) refl
in
(exactly_one, function_value)
@@ -539,57 +541,58 @@
(* nominal *)
-fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def =
+fun prove_stuff ctxt
+ globals G f R clauses complete compat compat_store G_elim G_eqvt invariant 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))))
- |> cterm_of thy
+ |> Thm.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 (cterm_of thy h)]
+ |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
val _ = trace_msg (K "Proving Replacement lemmas...")
- val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
+ val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
val _ = trace_msg (K "Proving Equivariance lemmas...")
- val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
+ val eqvtLemmas = map (mk_eqvt_lemma ctxt ih_eqvt) clauses
val _ = trace_msg (K "Proving Invariance lemmas...")
- val invLemmas = map (mk_invariant_lemma thy ih_inv) clauses
+ val invLemmas = map (mk_invariant_lemma ctxt ih_inv) clauses
val _ = trace_msg (K "Proving cases for unique existence...")
val (ex1s, values) =
- split_list (map (mk_uniqueness_case thy globals G f
+ split_list (map (mk_uniqueness_case ctxt globals G f
ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses)
val _ = trace_msg (K "Proving: Graph is a function")
val graph_is_function = complete
|> Thm.forall_elim_vars 0
|> fold (curry op COMP) ex1s
- |> Thm.implies_intr (ihyp)
- |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
- |> Thm.forall_intr (cterm_of thy x)
+ |> Thm.implies_intr ihyp
+ |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+ |> Thm.forall_intr (Thm.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 cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
+ |> (fn it =>
+ fold (Thm.forall_intr o Thm.cterm_of ctxt o Var) (Term.add_vars (Thm.prop_of it) []) it)
val goalstate =
- Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt
+ Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt
|> Thm.close_derivation
|> Goal.protect 0
- |> fold_rev (Thm.implies_intr o cprop_of) compat
- |> Thm.implies_intr (cprop_of complete)
- |> Thm.implies_intr (cprop_of invariant)
- |> Thm.implies_intr (cprop_of G_eqvt)
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat
+ |> Thm.implies_intr (Thm.cprop_of complete)
+ |> Thm.implies_intr (Thm.cprop_of invariant)
+ |> Thm.implies_intr (Thm.cprop_of G_eqvt)
in
(goalstate, values)
end
@@ -599,7 +602,7 @@
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
lthy
- |> Local_Theory.conceal
+ |> Proof_Context.concealed
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
@@ -612,14 +615,14 @@
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
[] (* no special monos *)
- ||> Local_Theory.restore_naming lthy
+ ||> Proof_Context.restore_naming lthy
- val cert = cterm_of (Proof_Context.theory_of lthy)
+ val cert = Thm.cterm_of lthy
fun requantify orig_intro thm =
let
val (qs, t) = dest_all_all orig_intro
val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
- val vars = Term.add_vars (prop_of thm) []
+ val vars = Term.add_vars (Thm.prop_of thm) []
val varmap = AList.lookup (op =) (frees ~~ map fst vars)
#> the_default ("",0)
in
@@ -640,7 +643,7 @@
let
fun mk_h_assm (rcfix, rcassm, rcarg) =
HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
|> fold_rev (Logic.all o Free) rcfix
in
HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
@@ -663,7 +666,7 @@
in
Local_Theory.define
((Binding.name (function_name fname), mixfix),
- ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
+ ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy
end
(* nominal *)
@@ -674,7 +677,7 @@
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev (Logic.all o Free) rcfix
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
@@ -691,7 +694,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),
@@ -708,11 +711,11 @@
ctxt')
end
-fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
+fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) =
let
fun inst_term t = subst_bound(f, abstract_over (fvar, t))
in
- (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
+ (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg)
end
@@ -721,23 +724,23 @@
* PROVING THE RULES
**********************************************************)
-fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
+fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function =
let
val Globals {domT, z, ...} = globals
fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
let
- val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
- val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+ val lhs_acc = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+ val z_smaller = Thm.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 (cterm_of thy z)
+ |> Thm.forall_intr (Thm.cterm_of ctxt z)
|> (fn it => it COMP valthm)
|> Thm.implies_intr lhs_acc
- |> asm_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [f_iff])
- |> fold_rev (Thm.implies_intr o cprop_of) ags
+ |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff])
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
in
@@ -751,34 +754,34 @@
val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
-fun mk_partial_induct_rule thy globals R complete_thm clauses =
+fun mk_partial_induct_rule ctxt globals R complete_thm clauses =
let
val Globals {domT, x, z, a, P, D, ...} = globals
val acc_R = mk_acc domT R
- val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
- val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
+ val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x)))
+ val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a))
- val D_subset = cterm_of thy (Logic.all x
+ val D_subset = Thm.cterm_of ctxt (Logic.all x
(Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
HOLogic.mk_Trueprop (D $ z)))))
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
HOLogic.mk_Trueprop (P $ Bound 0)))
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val aihyp = Thm.assume ihyp
fun prove_case clause =
let
- val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
+ val ClauseInfo {cdata = ClauseContext {ctxt = ctxt', qs, cqs, ags, gs, lhs, case_hyp, ...},
RCs, qglr = (oqs, _, _, _), ...} = clause
val case_hyp_conv = K (case_hyp RS eq_reflection)
@@ -786,23 +789,23 @@
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
val sih =
fconv_rule (Conv.binder_conv
- (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+ (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt') aihyp
end
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
- |> Thm.forall_elim (cterm_of thy rcarg)
+ |> Thm.forall_elim (Thm.cterm_of ctxt rcarg)
|> Thm.elim_implies llRI
- |> fold_rev (Thm.implies_intr o cprop_of) CCas
- |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
val step = HOLogic.mk_Trueprop (P $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+ |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs
|> fold_rev (curry Logic.mk_implies) gs
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val P_lhs = Thm.assume step
|> fold Thm.forall_elim cqs
@@ -810,12 +813,13 @@
|> fold Thm.elim_implies ags
|> fold Thm.elim_implies P_recs
- val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
+ val res =
+ Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x))
|> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
|> Thm.symmetric (* P lhs == P x *)
|> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
- |> Thm.implies_intr (cprop_of case_hyp)
- |> fold_rev (Thm.implies_intr o cprop_of) ags
+ |> Thm.implies_intr (Thm.cprop_of case_hyp)
+ |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
|> fold_rev Thm.forall_intr cqs
in
(res, step)
@@ -827,8 +831,8 @@
|> Thm.forall_elim_vars 0
|> fold (curry op COMP) cases (* P x *)
|> Thm.implies_intr ihyp
- |> Thm.implies_intr (cprop_of x_D)
- |> Thm.forall_intr (cterm_of thy x)
+ |> Thm.implies_intr (Thm.cprop_of x_D)
+ |> Thm.forall_intr (Thm.cterm_of ctxt x)
val subset_induct_rule =
acc_subset_induct
@@ -843,16 +847,16 @@
val simple_induct_rule =
subset_induct_rule
- |> Thm.forall_intr (cterm_of thy D)
- |> Thm.forall_elim (cterm_of thy acc_R)
- |> assume_tac 1 |> Seq.hd
+ |> Thm.forall_intr (Thm.cterm_of ctxt D)
+ |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
+ |> atac 1 |> Seq.hd
|> (curry op COMP) (acc_downward
- |> (instantiate' [SOME (ctyp_of thy domT)]
- (map (SOME o cterm_of thy) [R, x, z]))
- |> Thm.forall_intr (cterm_of thy z)
- |> Thm.forall_intr (cterm_of thy x))
- |> Thm.forall_intr (cterm_of thy a)
- |> Thm.forall_intr (cterm_of thy P)
+ |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)]
+ (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
+ |> Thm.forall_intr (Thm.cterm_of ctxt z)
+ |> Thm.forall_intr (Thm.cterm_of ctxt x))
+ |> Thm.forall_intr (Thm.cterm_of ctxt a)
+ |> Thm.forall_intr (Thm.cterm_of ctxt P)
in
simple_induct_rule
end
@@ -861,16 +865,15 @@
(* 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
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
in
Goal.init goal
- |> (SINGLE (resolve_tac [accI] 1)) |> the
- |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
+ |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the
+ |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1)) |> the
|> (SINGLE (auto_tac ctxt)) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
@@ -884,36 +887,36 @@
val wf_in_rel = @{thm Fun_Def.wf_in_rel}
val in_rel_def = @{thm Fun_Def.in_rel_def}
-fun mk_nest_term_case thy globals R' ihyp clause =
+fun mk_nest_term_case ctxt globals R' ihyp clause =
let
val Globals {z, ...} = globals
val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
qglr=(oqs, _, _, _), ...} = clause
val ih_case =
- full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
+ full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp])
ihyp
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
let
val used = (u @ sub)
- |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx 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 prop_of) used (* additional hyps *)
- |> Function_Ctx_Tree.export_term (fixes, assumes)
- |> fold_rev (curry Logic.mk_implies o prop_of) ags
+ |> 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)
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val thm = Thm.assume hyp
|> fold Thm.forall_elim cqs
|> fold Thm.elim_implies ags
- |> Function_Ctx_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))
- |> cterm_of thy |> Thm.assume
+ |> Thm.cterm_of ctxt |> Thm.assume
val acc = thm COMP ih_case
val z_acc_local = acc
@@ -921,7 +924,7 @@
(Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
val ethm = z_acc_local
- |> Function_Ctx_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)
@@ -931,11 +934,11 @@
end
| step _ _ _ _ = raise Match
in
- Function_Ctx_Tree.traverse_tree step tree
+ Function_Context_Tree.traverse_tree step tree
end
-fun mk_nest_term_rule thy globals R R_cases clauses =
+fun mk_nest_term_rule ctxt globals R R_cases clauses =
let
val Globals { domT, x, z, ... } = globals
val acc_R = mk_acc domT R
@@ -948,42 +951,42 @@
val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
(domT --> domT --> boolT) --> boolT) $ R')
- |> cterm_of thy (* "wf R'" *)
+ |> Thm.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)))
- |> cterm_of thy
+ |> Thm.cterm_of ctxt
val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
- val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
+ val R_z_x = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x))
- val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
+ val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], [])
in
R_cases
- |> Thm.forall_elim (cterm_of thy z)
- |> Thm.forall_elim (cterm_of thy x)
- |> Thm.forall_elim (cterm_of thy (acc_R $ z))
+ |> Thm.forall_elim (Thm.cterm_of ctxt z)
+ |> Thm.forall_elim (Thm.cterm_of ctxt x)
+ |> Thm.forall_elim (Thm.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 (cterm_of thy z)
+ |> Thm.forall_intr (Thm.cterm_of ctxt z)
|> (fn it => it COMP accI)
|> Thm.implies_intr ihyp
- |> Thm.forall_intr (cterm_of thy x)
+ |> Thm.forall_intr (Thm.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 (cterm_of thy R')
- |> Thm.forall_elim (cterm_of thy (inrel_R))
+ |> Thm.forall_intr (Thm.cterm_of ctxt R')
+ |> Thm.forall_elim (Thm.cterm_of ctxt (inrel_R))
|> curry op RS wf_in_rel
- |> full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [in_rel_def])
- |> Thm.forall_intr (cterm_of thy Rrel)
+ |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def])
+ |> Thm.forall_intr (Thm.cterm_of ctxt Rrel)
end
@@ -1014,7 +1017,7 @@
val n = length abstract_qglrs
fun build_tree (ClauseContext { ctxt, rhs, ...}) =
- Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
+ Function_Context_Tree.mk_tree (fname, fT) h ctxt rhs
val trees = map build_tree clauses
val RCss = map find_calls trees
@@ -1025,8 +1028,8 @@
val ((f, (_, f_defthm)), lthy) =
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_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
+ val RCss = map (map (inst_RC lthy fvar f)) RCss
+ 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
@@ -1037,10 +1040,10 @@
val newthy = Proof_Context.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
- val cert = cterm_of (Proof_Context.theory_of lthy)
+ val cert = Thm.cterm_of lthy
val xclauses = PROFILE "xclauses"
- (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
+ (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
RCss GIntro_thms) RIntro_thmss
val complete =
@@ -1062,7 +1065,8 @@
fun mk_partial_rules provedgoal =
let
- val newthy = theory_of_thm provedgoal (*FIXME*)
+ val newthy = Thm.theory_of_thm provedgoal (*FIXME*)
+ val newctxt = Proof_Context.init_global newthy (*FIXME*)
val ((graph_is_function, complete_thm), graph_is_eqvt) =
provedgoal
@@ -1075,13 +1079,13 @@
val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
val psimps = PROFILE "Proving simplification rules"
- (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
+ (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function
val simple_pinduct = PROFILE "Proving partial induction rule"
- (mk_partial_induct_rule newthy globals R complete_thm) xclauses
+ (mk_partial_induct_rule newctxt globals R complete_thm) xclauses
val total_intro = PROFILE "Proving nested termination rule"
- (mk_nest_term_rule newthy globals R R_elim) xclauses
+ (mk_nest_term_rule newctxt globals R R_elim) xclauses
val dom_intros =
if domintros then SOME (PROFILE "Proving domain introduction rules"