--- a/src/HOL/Tools/TFL/rules.ML Tue Jun 02 17:27:01 2015 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Jun 02 19:56:29 2015 +0200
@@ -47,8 +47,8 @@
val rbeta: thm -> thm
val tracing: bool Unsynchronized.ref
- val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
- -> thm -> thm * term list
+ val CONTEXT_REWRITE_RULE: Proof.context ->
+ term * term list * thm * thm list -> thm -> thm * term list
val RIGHT_ASSOC: Proof.context -> thm -> thm
val prove: Proof.context -> bool -> term * tactic -> thm
@@ -525,8 +525,8 @@
fun print_thms ctxt s L =
say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
-fun print_cterm ctxt s ct =
- say (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)]);
+fun print_term ctxt s t =
+ say (cat_lines [s, Syntax.string_of_term ctxt t]);
(*---------------------------------------------------------------------------
@@ -633,9 +633,9 @@
(fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
t)
-fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
+fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th =
let val globals = func::G
- val ctxt0 = empty_simpset (Proof_Context.init_global (Thm.theory_of_thm th))
+ val ctxt0 = empty_simpset main_ctxt
val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
val cut_lemma' = cut_lemma RS eq_reflection
@@ -647,28 +647,28 @@
val dummy = say "cong rule:"
val dummy = say (Display.string_of_thm ctxt thm)
(* Unquantified eliminate *)
- fun uq_eliminate (thm,imp,thy) =
- let val tych = Thm.global_cterm_of thy
- val dummy = print_cterm ctxt "To eliminate:" (tych imp)
+ fun uq_eliminate (thm,imp) =
+ let val tych = Thm.cterm_of ctxt
+ val _ = print_term ctxt "To eliminate:" imp
val ants = map tych (Logic.strip_imp_prems imp)
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
handle Utils.ERR _ => Thm.reflexive lhs
- val dummy = print_thms ctxt' "proven:" [lhs_eq_lhs1]
+ val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
in
lhs_eeq_lhs2 COMP thm
end
- fun pq_eliminate (thm,thy,vlist,imp_body,lhs_eq) =
+ fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
val dummy = forall (op aconv) (ListPair.zip (vlist, args))
orelse error "assertion failed in CONTEXT_REWRITE_RULE"
val imp_body1 = subst_free (ListPair.zip (args, vstrl))
imp_body
- val tych = Thm.global_cterm_of thy
+ val tych = Thm.cterm_of ctxt
val ants1 = map tych (Logic.strip_imp_prems imp_body1)
val eq1 = Logic.strip_imp_concl imp_body1
val Q = get_lhs eq1
@@ -691,13 +691,13 @@
val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
in ant_th COMP thm
end
- fun q_eliminate (thm,imp,thy) =
+ fun q_eliminate (thm, imp) =
let val (vlist, imp_body, used') = strip_all used imp
val (ants,Q) = dest_impl imp_body
in if (pbeta_redex Q) (length vlist)
- then pq_eliminate (thm,thy,vlist,imp_body,Q)
+ then pq_eliminate (thm, vlist, imp_body, Q)
else
- let val tych = Thm.global_cterm_of thy
+ let val tych = Thm.cterm_of ctxt
val ants1 = map tych ants
val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
@@ -711,12 +711,12 @@
end end
fun eliminate thm =
- case Thm.prop_of thm
- of Const(@{const_name Pure.imp},_) $ imp $ _ =>
+ case Thm.prop_of thm of
+ Const(@{const_name Pure.imp},_) $ imp $ _ =>
eliminate
(if not(is_all imp)
- then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
- else q_eliminate (thm, imp, Thm.theory_of_thm thm))
+ then uq_eliminate (thm, imp)
+ else q_eliminate (thm, imp))
(* Assume that the leading constant is ==, *)
| _ => thm (* if it is not a ==> *)
in SOME(eliminate (rename thm)) end
@@ -747,11 +747,11 @@
val antl = case rcontext of [] => []
| _ => [USyntax.list_mk_conj(map cncl rcontext)]
val TC = genl(USyntax.list_mk_imp(antl, A))
- val dummy = print_cterm ctxt "func:" (Thm.cterm_of ctxt func)
- val dummy = print_cterm ctxt "TC:" (Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC))
- val dummy = tc_list := (TC :: !tc_list)
+ val _ = print_term ctxt "func:" func
+ val _ = print_term ctxt "TC:" (HOLogic.mk_Trueprop TC)
+ val _ = tc_list := (TC :: !tc_list)
val nestedp = is_some (USyntax.find_term is_func TC)
- val dummy = if nestedp then say "nested" else say "not_nested"
+ val _ = if nestedp then say "nested" else say "not_nested"
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)
in case rcontext of
--- a/src/HOL/Tools/TFL/tfl.ML Tue Jun 02 17:27:01 2015 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Jun 02 19:56:29 2015 +0200
@@ -440,8 +440,8 @@
|> fold (Simplifier.add_cong o #case_cong_weak o snd)
(Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
val corollaries' = map (Simplifier.simplify case_simpset) corollaries
- val extract = Rules.CONTEXT_REWRITE_RULE
- (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
+ val extract =
+ Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
val (rules, TCs) = ListPair.unzip (map extract corollaries')
val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
@@ -498,8 +498,8 @@
val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
val corollaries' = map (rewrite_rule ctxt case_rewrites) corollaries
- fun extract X = Rules.CONTEXT_REWRITE_RULE
- (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
+ val extract =
+ Rules.CONTEXT_REWRITE_RULE ctxt (f, R1::SV, @{thm cut_apply}, tflCongs @ context_congs)
in {proto_def = proto_def,
SV=SV,
WFR=WFR,