--- a/NEWS Sat Dec 14 07:45:30 2013 +0800
+++ b/NEWS Sun Dec 15 05:11:46 2013 +0100
@@ -115,6 +115,11 @@
Note that 'ML_file' is the canonical command to load ML files into the
formal context.
+* Proper context for basic Simplifier operations: rewrite_rule,
+rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
+pass runtime Proof.context (and ensure that the simplified entity
+actually belongs to it).
+
*** System ***
--- a/src/CCL/CCL.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/CCL/CCL.thy Sun Dec 15 05:11:46 2013 +0100
@@ -280,7 +280,7 @@
fun mk_dstnct_thm rls s =
Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
(fn _ =>
- rewrite_goals_tac defs THEN
+ rewrite_goals_tac ctxt defs THEN
simp_tac (ctxt addsimps (rls @ inj_rls)) 1)
in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
--- a/src/Doc/IsarImplementation/Eq.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Doc/IsarImplementation/Eq.thy Sun Dec 15 05:11:46 2013 +0100
@@ -91,30 +91,30 @@
text %mlref {*
\begin{mldecls}
- @{index_ML rewrite_rule: "thm list -> thm -> thm"} \\
- @{index_ML rewrite_goals_rule: "thm list -> thm -> thm"} \\
- @{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\
- @{index_ML rewrite_goals_tac: "thm list -> tactic"} \\
- @{index_ML fold_goals_tac: "thm list -> tactic"} \\
+ @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
+ @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
+ @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
+ @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
+ @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
\end{mldecls}
\begin{description}
- \item @{ML rewrite_rule}~@{text "rules thm"} rewrites the whole
+ \item @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole
theorem by the given rules.
- \item @{ML rewrite_goals_rule}~@{text "rules thm"} rewrites the
+ \item @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the
outer premises of the given theorem. Interpreting the same as a
goal state (\secref{sec:tactical-goals}) it means to rewrite all
subgoals (in the same manner as @{ML rewrite_goals_tac}).
- \item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal
+ \item @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal
@{text "i"} by the given rewrite rules.
- \item @{ML rewrite_goals_tac}~@{text "rules"} rewrites all subgoals
+ \item @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals
by the given rewrite rules.
- \item @{ML fold_goals_tac}~@{text "rules"} essentially uses @{ML
+ \item @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML
rewrite_goals_tac} with the symmetric form of each member of @{text
"rules"}, re-ordered to fold longer expression first. This supports
to idea to fold primitive definitions that appear in expended form
--- a/src/HOL/BNF/Tools/bnf_comp.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Sun Dec 15 05:11:46 2013 +0100
@@ -590,10 +590,10 @@
fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
val expand_rels =
fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
- val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
- val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
- val unfold_rels = unfold_thms lthy rel_unfolds;
- val unfold_all = unfold_sets o unfold_maps o unfold_rels;
+ fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
+ fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
+ fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
+ fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
val bnf_sets = map (expand_maps o expand_sets)
(mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
@@ -627,7 +627,7 @@
map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
fun mk_tac thm {context = ctxt, prems = _} =
- (rtac (unfold_all thm) THEN'
+ (rtac (unfold_all ctxt thm) THEN'
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
@@ -638,7 +638,8 @@
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
- fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
+ fun wit_tac {context = ctxt, prems = _} =
+ mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
val (bnf', lthy') =
bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Sun Dec 15 05:11:46 2013 +0100
@@ -130,7 +130,7 @@
REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN
EVERY [REPEAT_DETERM_N r
(HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
- if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, HEADGOAL atac,
+ if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac,
mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs]
end;
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML Sun Dec 15 05:11:46 2013 +0100
@@ -168,7 +168,7 @@
cterm_instantiate_pos cts rel_xtor_co_induct_thm
|> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
|> funpow (2 * n) (fn thm => thm RS spec)
- |> Conv.fconv_rule Object_Logic.atomize
+ |> Conv.fconv_rule (Object_Logic.atomize lthy)
|> funpow n (fn thm => thm RS mp)
end);
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Dec 15 05:11:46 2013 +0100
@@ -567,7 +567,7 @@
EVERY' [rtac allI, fo_rtac induct ctxt,
select_prem_tac n (dtac @{thm meta_spec2}) i,
REPEAT_DETERM_N n o
- EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac,
+ EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac],
atac];
in
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Sun Dec 15 05:11:46 2013 +0100
@@ -45,7 +45,7 @@
rtac (Drule.instantiate_normalize insts thm) 1
end);
-fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
+fun mk_unfold_thms_then_tac ctxt defs tac x = unfold_thms_tac ctxt defs THEN tac x;
(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
fun mk_pointfree ctxt thm = thm
--- a/src/HOL/Bali/Example.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Bali/Example.thy Sun Dec 15 05:11:46 2013 +0100
@@ -894,7 +894,7 @@
declare member_is_static_simp [simp]
declare wt.Skip [rule del] wt.Init [rule del]
-ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
+ML {* bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
@@ -1189,7 +1189,7 @@
ML {* bind_thms ("eval_intros", map
(simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o
- rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
+ rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
axiomatization
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Dec 15 05:11:46 2013 +0100
@@ -2920,7 +2920,7 @@
struct
fun tactic ctxt alternative T ps =
- Object_Logic.full_atomize_tac
+ Object_Logic.full_atomize_tac ctxt
THEN' CSUBGOAL (fn (g, i) =>
let
val th = frpar_oracle (ctxt, alternative, T, ps, g)
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Dec 15 05:11:46 2013 +0100
@@ -62,7 +62,7 @@
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
-fun linz_tac ctxt q = Object_Logic.atomize_prems_tac THEN' SUBGOAL (fn (g, i) =>
+fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
let
val thy = Proof_Context.theory_of ctxt
(* Transform the term*)
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun Dec 15 05:11:46 2013 +0100
@@ -66,7 +66,7 @@
fun linr_tac ctxt q =
- Object_Logic.atomize_prems_tac
+ Object_Logic.atomize_prems_tac ctxt
THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
THEN' SUBGOAL (fn (g, i) =>
let
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Dec 15 05:11:46 2013 +0100
@@ -224,7 +224,7 @@
(case dlo_instance ctxt p of
NONE => no_tac
| SOME instance =>
- Object_Logic.full_atomize_tac i THEN
+ Object_Logic.full_atomize_tac ctxt i THEN
simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN (* FIXME already part of raw_ferrack_qe_conv? *)
CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
simp_tac ctxt i)); (* FIXME really? *)
--- a/src/HOL/Decision_Procs/langford.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/langford.ML Sun Dec 15 05:11:46 2013 +0100
@@ -237,11 +237,11 @@
(case dlo_instance ctxt p of
(ss, NONE) => simp_tac (put_simpset ss ctxt) i
| (ss, SOME instance) =>
- Object_Logic.full_atomize_tac i THEN
+ Object_Logic.full_atomize_tac ctxt i THEN
simp_tac (put_simpset ss ctxt) i
THEN (CONVERSION Thm.eta_long_conversion) i
THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
- THEN Object_Logic.full_atomize_tac i
+ THEN Object_Logic.full_atomize_tac ctxt i
THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ctxt ss instance)) i
THEN (simp_tac (put_simpset ss ctxt) i)));
end;
\ No newline at end of file
--- a/src/HOL/Decision_Procs/mir_tac.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Dec 15 05:11:46 2013 +0100
@@ -82,7 +82,7 @@
fun mir_tac ctxt q =
- Object_Logic.atomize_prems_tac
+ Object_Logic.atomize_prems_tac ctxt
THEN' simp_tac (put_simpset HOL_basic_ss ctxt
addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
--- a/src/HOL/HOL.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOL.thy Sun Dec 15 05:11:46 2013 +0100
@@ -1496,8 +1496,9 @@
| is_conj _ = false
in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
| _ => NONE))]
- |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
- map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback})))))
+ |> Simplifier.set_mksimps (fn ctxt =>
+ Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
+ map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
*}
text {* Pre-simplification of induction and cases rules *}
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Sun Dec 15 05:11:46 2013 +0100
@@ -208,29 +208,29 @@
txt {* 10 - 7 *}
apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
txt {* 6 *}
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
txt {* 6 - 5 *}
apply (tactic "EVERY1 [tac2,tac2]")
txt {* 4 *}
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
apply (tactic "tac2 1")
txt {* 3 *}
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
(@{thm raw_inv1} RS @{thm invariantE})] 1 *})
apply (tactic "tac2 1")
- apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
+ apply (tactic {* fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
(@{thm Impl.hdr_sum_def})] *})
apply arith
txt {* 2 *}
apply (tactic "tac2 1")
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
apply (intro strip)
apply (erule conjE)+
@@ -238,11 +238,12 @@
txt {* 1 *}
apply (tactic "tac2 1")
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
apply (intro strip)
apply (erule conjE)+
- apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
+ apply (tactic {* fold_goals_tac @{context}
+ [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
apply simp
done
@@ -286,13 +287,13 @@
apply (intro strip, (erule conjE)+)
apply (rule imp_disjL [THEN iffD1])
apply (rule impI)
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
(@{thm raw_inv2} RS @{thm invariantE})] 1 *})
apply simp
apply (erule conjE)+
apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
- apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm inv1_def}]
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
apply (simp add: hdr_sum_def Multiset.count_def)
apply (rule add_le_mono)
@@ -307,7 +308,7 @@
apply (intro strip, (erule conjE)+)
apply (rule imp_disjL [THEN iffD1])
apply (rule impI)
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
(@{thm raw_inv2} RS @{thm invariantE})] 1 *})
apply simp
done
@@ -333,7 +334,7 @@
txt {* 2 b *}
apply (intro strip, (erule conjE)+)
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
(@{thm raw_inv2} RS @{thm invariantE})] 1 *})
apply simp
@@ -341,9 +342,9 @@
apply (tactic "tac4 1")
apply (intro strip, (erule conjE)+)
apply (rule ccontr)
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
(@{thm raw_inv2} RS @{thm invariantE})] 1 *})
- apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
+ apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
(@{thm raw_inv3} RS @{thm invariantE})] 1 *})
apply simp
apply (erule_tac x = "m" in allE)
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Dec 15 05:11:46 2013 +0100
@@ -101,8 +101,8 @@
: thm =
let
fun tac {prems, context} =
- rewrite_goals_tac defs THEN
- EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
+ rewrite_goals_tac context defs THEN
+ EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
in
Goal.prove_global thy [] [] goal tac
end
@@ -213,8 +213,10 @@
in (n2, mk_ssumT (t1, t2)) end
val ct = ctyp_of thy (snd (cons2typ 1 spec'))
val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
- val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
- val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2
+ val thm2 = rewrite_rule (Proof_Context.init_global thy)
+ (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
+ val thm3 = rewrite_rule (Proof_Context.init_global thy)
+ [mk_meta_eq @{thm conj_assoc}] thm2
val y = Free ("y", lhsT)
fun one_con (con, args) =
@@ -225,15 +227,15 @@
in Library.foldr mk_ex (vs, conj) end
val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
(* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
- val tacs = [
+ fun tacs {context = ctxt, prems} = [
rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
- rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
+ rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
rtac thm3 1]
in
- val nchotomy = prove thy con_betas goal (K tacs)
+ val nchotomy = prove thy con_betas goal tacs
val exhaust =
(nchotomy RS @{thm exh_casedist0})
- |> rewrite_rule @{thms exh_casedists}
+ |> rewrite_rule (Proof_Context.init_global thy) @{thms exh_casedists}
|> Drule.zero_var_indexes
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Dec 15 05:11:46 2013 +0100
@@ -161,12 +161,12 @@
val simplify = asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules)
fun arg_tac (lazy, _) =
rtac (if lazy then allI else case_UU_allI) 1
- val tacs =
- rewrite_goals_tac @{thms atomize_all atomize_imp} ::
+ fun tacs ctxt =
+ rewrite_goals_tac ctxt @{thms atomize_all atomize_imp} ::
map arg_tac args @
[REPEAT (rtac impI 1), ALLGOALS simplify]
in
- Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
+ Goal.prove ctxt [] [] subgoal (EVERY o tacs o #context)
end
fun eq_thms (p, cons) = map (con_thm p) cons
val conss = map #con_specs constr_infos
@@ -321,7 +321,7 @@
val rules = @{thm Rep_cfun_strict1} :: take_0_thms
fun tacf {prems, context = ctxt} =
let
- val prem' = rewrite_rule [bisim_def_thm] (hd prems)
+ val prem' = rewrite_rule ctxt [bisim_def_thm] (hd prems)
val prems' = Project_Rule.projections ctxt prem'
val dests = map (fn th => th RS spec RS spec RS mp) prems'
fun one_tac (dest, rews) =
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Dec 15 05:11:46 2013 +0100
@@ -157,10 +157,10 @@
(* prove applied version of definitions *)
fun prove_proj (lhs, rhs) =
let
- val tac = rewrite_goals_tac fixdef_thms THEN
+ fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN
(simp_tac (Simplifier.global_context thy beta_ss)) 1
val goal = Logic.mk_equals (lhs, rhs)
- in Goal.prove_global thy [] [] goal (K tac) end
+ in Goal.prove_global thy [] [] goal (tac o #context) end
val proj_thms = map prove_proj projs
(* mk_tuple lhss == fixpoint *)
@@ -328,7 +328,7 @@
in
Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
EVERY
- [rewrite_goals_tac map_apply_thms,
+ [rewrite_goals_tac ctxt map_apply_thms,
rtac (map_cont_thm RS @{thm cont_fix_ind}) 1,
REPEAT (resolve_tac adm_rules 1),
simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
@@ -533,11 +533,11 @@
let
val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
val DEFL_simps = RepData.get (Proof_Context.init_global thy)
- val tac =
- rewrite_goals_tac (map mk_meta_eq DEFL_simps)
+ fun tac ctxt =
+ rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
THEN TRY (resolve_tac defl_unfold_thms 1)
in
- Goal.prove_global thy [] [] goal (K tac)
+ Goal.prove_global thy [] [] goal (tac o #context)
end
val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns
@@ -641,7 +641,7 @@
in
Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
EVERY
- [rewrite_goals_tac (defl_apply_thms @ map_apply_thms),
+ [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms),
rtac (@{thm cont_parallel_fix_ind}
OF [defl_cont_thm, map_cont_thm]) 1,
REPEAT (resolve_tac adm_rules 1),
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Dec 15 05:11:46 2013 +0100
@@ -470,15 +470,15 @@
fun prove_finite_thm (absT, finite_const) =
let
val goal = mk_trp (finite_const $ Free ("x", absT))
- val tac =
+ fun tac ctxt =
EVERY [
- rewrite_goals_tac finite_defs,
+ rewrite_goals_tac ctxt finite_defs,
rtac @{thm lub_ID_finite} 1,
resolve_tac chain_take_thms 1,
resolve_tac lub_take_thms 1,
resolve_tac decisive_thms 1]
in
- Goal.prove_global thy [] [] goal (K tac)
+ Goal.prove_global thy [] [] goal (tac o #context)
end
val finite_thms =
map prove_finite_thm (absTs ~~ finite_consts)
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Dec 15 05:11:46 2013 +0100
@@ -411,8 +411,8 @@
: thm =
let
fun tac {prems, context} =
- rewrite_goals_tac defs THEN
- EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
+ rewrite_goals_tac context defs THEN
+ EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
in
Goal.prove_global thy [] [] goal tac
end;
--- a/src/HOL/Library/State_Monad.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Library/State_Monad.thy Sun Dec 15 05:11:46 2013 +0100
@@ -145,7 +145,7 @@
"_sdo_block (_sdo_final e)" => "e"
text {*
- For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
+ For an example, see @{file "~~/src/HOL/Proofs/Extraction/Higman.thy"}.
*}
end
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sun Dec 15 05:11:46 2013 +0100
@@ -938,7 +938,7 @@
fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
fun sos_tac print_cert prover ctxt =
- Object_Logic.full_atomize_tac THEN'
+ Object_Logic.full_atomize_tac ctxt THEN'
elim_denom_tac ctxt THEN'
core_sos_tac print_cert prover ctxt;
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sun Dec 15 05:11:46 2013 +0100
@@ -325,7 +325,7 @@
apply( fast intro: hext_trans)
-apply( tactic prune_params_tac)
+apply( tactic "prune_params_tac @{context}")
-- "Level 52"
-- "1 Call"
--- a/src/HOL/Multivariate_Analysis/normarith.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Sun Dec 15 05:11:46 2013 +0100
@@ -399,7 +399,7 @@
fun norm_arith_tac ctxt =
clarify_tac (put_claset HOL_cs ctxt) THEN'
- Object_Logic.full_atomize_tac THEN'
+ Object_Logic.full_atomize_tac ctxt THEN'
CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
end;
--- a/src/HOL/NSA/transfer.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/NSA/transfer.ML Sun Dec 15 05:11:46 2013 +0100
@@ -58,11 +58,11 @@
val meta = Local_Defs.meta_rewrite_rule ctxt;
val ths' = map meta ths;
val unfolds' = map meta unfolds and refolds' = map meta refolds;
- val (_$_$t') = concl_of (Raw_Simplifier.rewrite true unfolds' (cterm_of thy t))
+ val (_$_$t') = concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (cterm_of thy t))
val u = unstar_term consts t'
val tac =
- rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
- ALLGOALS Object_Logic.full_atomize_tac THEN
+ rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
+ ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
match_tac [transitive_thm] 1 THEN
resolve_tac [@{thm transfer_start}] 1 THEN
REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
@@ -76,7 +76,7 @@
val tr = transfer_thm_of ctxt ths t
val (_$l$r) = concl_of tr;
val trs = if l aconv r then [] else [tr];
- in rewrite_goals_tac trs th end))
+ in rewrite_goals_tac ctxt trs th end))
local
--- a/src/HOL/Nat.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nat.thy Sun Dec 15 05:11:46 2013 +0100
@@ -1536,19 +1536,19 @@
simproc_setup nateq_cancel_sums
("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
- {* fn phi => fn ss => try Nat_Arith.cancel_eq_conv *}
+ {* fn phi => try o Nat_Arith.cancel_eq_conv *}
simproc_setup natless_cancel_sums
("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
- {* fn phi => fn ss => try Nat_Arith.cancel_less_conv *}
+ {* fn phi => try o Nat_Arith.cancel_less_conv *}
simproc_setup natle_cancel_sums
("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
- {* fn phi => fn ss => try Nat_Arith.cancel_le_conv *}
+ {* fn phi => try o Nat_Arith.cancel_le_conv *}
simproc_setup natdiff_cancel_sums
("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
- {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
+ {* fn phi => try o Nat_Arith.cancel_diff_conv *}
ML_file "Tools/lin_arith.ML"
setup {* Lin_Arith.global_setup *}
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nominal/nominal_atoms.ML Sun Dec 15 05:11:46 2013 +0100
@@ -829,6 +829,7 @@
(* instantiations. *)
val (_, thy33) =
let
+ val ctxt32 = Proof_Context.init_global thy32;
(* takes a theorem thm and a list of theorems [t1,..,tn] *)
(* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *)
@@ -918,7 +919,7 @@
||>> add_thmss_string
let
val thms1 = inst_pt_at [all_eqvt];
- val thms2 = map (fold_rule [inductive_forall_def]) thms1
+ val thms2 = map (fold_rule ctxt32 [inductive_forall_def]) thms1
in
[(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
end
--- a/src/HOL/Nominal/nominal_datatype.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Dec 15 05:11:46 2013 +0100
@@ -134,7 +134,7 @@
val at_fin_set_fresh = @{thm at_fin_set_fresh};
val abs_fun_eq1 = @{thm abs_fun_eq1};
-val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
+fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq mem_Collect_eq];
fun mk_perm Ts t u =
let
@@ -595,10 +595,12 @@
end))
(types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
+ val ctxt6 = Proof_Context.init_global thy6;
+
val perm_defs = map snd typedefs;
- val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
+ val Abs_inverse_thms = map (collect_simp ctxt6 o #Abs_inverse o snd o fst) typedefs;
val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
- val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
+ val Rep_thms = map (collect_simp ctxt6 o #Rep o snd o fst) typedefs;
(** prove that new types are in class pt_<name> **)
@@ -616,7 +618,7 @@
(Sign.intern_type thy name,
map (inter_sort thy sort o snd) tvs, [pt_class])
(fn ctxt => EVERY [Class.intro_classes_tac [],
- rewrite_goals_tac [perm_def],
+ rewrite_goals_tac ctxt [perm_def],
asm_full_simp_tac (ctxt addsimps [Rep_inverse]) 1,
asm_full_simp_tac (ctxt addsimps
[Rep RS perm_closed RS Abs_inverse]) 1,
@@ -645,7 +647,7 @@
(Sign.intern_type thy name,
map (inter_sort thy sort o snd) tvs, [cp_class])
(fn ctxt => EVERY [Class.intro_classes_tac [],
- rewrite_goals_tac [perm_def],
+ rewrite_goals_tac ctxt [perm_def],
asm_full_simp_tac (ctxt addsimps
((Rep RS perm_closed1 RS Abs_inverse) ::
(if atom1 = atom2 then []
@@ -783,7 +785,7 @@
new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
(thy7, [], [], []);
- val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
+ val abs_inject_thms = map (collect_simp ctxt6 o #Abs_inject o snd o fst) typedefs
val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
(* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *)
@@ -792,9 +794,9 @@
let
val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
- in Goal.prove_global_future thy8 [] [] eqn (fn _ => EVERY
+ in Goal.prove_global_future thy8 [] [] eqn (fn {context = ctxt, ...} => EVERY
[resolve_tac inj_thms 1,
- rewrite_goals_tac rewrites,
+ rewrite_goals_tac ctxt rewrites,
rtac refl 3,
resolve_tac rep_intrs 2,
REPEAT (resolve_tac Rep_thms 1)])
@@ -1043,7 +1045,7 @@
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn {prems, context = ctxt} => EVERY
[rtac indrule_lemma' 1,
- (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms' 1),
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
@@ -2017,8 +2019,8 @@
Goal.prove_global_future thy12 []
(map (augment_sort thy12 fs_cp_sort) prems')
(augment_sort thy12 fs_cp_sort concl')
- (fn {prems, ...} => EVERY
- [rewrite_goals_tac reccomb_defs,
+ (fn {context = ctxt, prems} => EVERY
+ [rewrite_goals_tac ctxt reccomb_defs,
rtac @{thm the1_equality} 1,
solve rec_unique_thms prems 1,
resolve_tac rec_intrs 1,
--- a/src/HOL/Nominal/nominal_induct.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nominal/nominal_induct.ML Sun Dec 15 05:11:46 2013 +0100
@@ -87,7 +87,7 @@
val cert = Thm.cterm_of thy;
val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
- val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
+ val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm ctxt))) defs;
val finish_rule =
split_all_tuples defs_ctxt
@@ -101,7 +101,7 @@
(fn i => fn st =>
rules
|> inst_mutual_rule ctxt insts avoiding
- |> Rule_Cases.consume (flat defs) facts
+ |> Rule_Cases.consume ctxt (flat defs) facts
|> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
(CONJUNCTS (ALLGOALS
@@ -118,10 +118,10 @@
else
Induct.arbitrary_tac defs_ctxt k xs)
end)
- THEN' Induct.inner_atomize_tac) j))
- THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
+ THEN' Induct.inner_atomize_tac defs_ctxt) j))
+ THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' =>
Induct.guess_instance ctxt
- (finish_rule (Induct.internalize more_consumes rule)) i st'
+ (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
|> Seq.maps (fn rule' =>
CASES (rule_cases ctxt rule' cases)
(rtac (rename_params_rule false [] rule') i THEN
@@ -129,7 +129,7 @@
THEN_ALL_NEW_CASES
((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
else K all_tac)
- THEN_ALL_NEW Induct.rulify_tac)
+ THEN_ALL_NEW Induct.rulify_tac ctxt)
end;
--- a/src/HOL/Nominal/nominal_primrec.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Dec 15 05:11:46 2013 +0100
@@ -373,8 +373,8 @@
|> snd
end)
[goals] |>
- Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
- rewrite_goals_tac defs_thms THEN
+ Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ =>
+ rewrite_goals_tac ctxt defs_thms THEN
compose_tac (false, rule, length rule_prems) 1))) |>
Seq.hd
end;
--- a/src/HOL/TLA/Action.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/Action.thy Sun Dec 15 05:11:46 2013 +0100
@@ -108,23 +108,26 @@
"world" parameter of the form (s,t) and apply additional rewrites.
*)
-fun action_unlift th =
- (rewrite_rule @{thms action_rews} (th RS @{thm actionD}))
- handle THM _ => int_unlift th;
+fun action_unlift ctxt th =
+ (rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD}))
+ handle THM _ => int_unlift ctxt th;
(* Turn |- A = B into meta-level rewrite rule A == B *)
val action_rewrite = int_rewrite
-fun action_use th =
+fun action_use ctxt th =
case (concl_of th) of
Const _ $ (Const ("Intensional.Valid", _) $ _) =>
- (flatten (action_unlift th) handle THM _ => th)
+ (flatten (action_unlift ctxt th) handle THM _ => th)
| _ => th;
*}
-attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *}
-attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *}
-attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *}
+attribute_setup action_unlift =
+ {* Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of)) *}
+attribute_setup action_rewrite =
+ {* Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of)) *}
+attribute_setup action_use =
+ {* Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of)) *}
(* =========================== square / angle brackets =========================== *)
@@ -258,11 +261,11 @@
should plug in only "very safe" rules that can be applied blindly.
Note that it applies whatever simplifications are currently active.
*)
-fun action_simp_tac ss intros elims =
+fun action_simp_tac ctxt intros elims =
asm_full_simp_tac
- (ss setloop (fn _ => (resolve_tac ((map action_use intros)
+ (ctxt setloop (fn _ => (resolve_tac ((map (action_use ctxt) intros)
@ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
- ORELSE' (eresolve_tac ((map action_use elims)
+ ORELSE' (eresolve_tac ((map (action_use ctxt) elims)
@ [conjE,disjE,exE]))));
*}
--- a/src/HOL/TLA/Intensional.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/Intensional.thy Sun Dec 15 05:11:46 2013 +0100
@@ -243,12 +243,12 @@
|- F --> G becomes F w --> G w
*)
-fun int_unlift th =
- rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
+fun int_unlift ctxt th =
+ rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
(* Turn |- F = G into meta-level rewrite rule F == G *)
-fun int_rewrite th =
- zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection}))
+fun int_rewrite ctxt th =
+ zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))
(* flattening turns "-->" into "==>" and eliminates conjunctions in the
antecedent. For example,
@@ -282,17 +282,20 @@
hflatten t
end
-fun int_use th =
+fun int_use ctxt th =
case (concl_of th) of
Const _ $ (Const ("Intensional.Valid", _) $ _) =>
- (flatten (int_unlift th) handle THM _ => th)
+ (flatten (int_unlift ctxt th) handle THM _ => th)
| _ => th
*}
-attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *}
-attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *}
+attribute_setup int_unlift =
+ {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}
+attribute_setup int_rewrite =
+ {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}
attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
-attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *}
+attribute_setup int_use =
+ {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
by (simp add: Valid_def)
--- a/src/HOL/TLA/Memory/Memory.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/Memory/Memory.thy Sun Dec 15 05:11:46 2013 +0100
@@ -223,11 +223,11 @@
apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
apply (case_tac "arg (ch w p)")
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Read_def},
- temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
+ temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
apply (force dest: base_pair [temp_use])
apply (erule contrapos_np)
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Write_def},
- temp_rewrite @{thm enabled_ex}])
+ temp_rewrite @{context} @{thm enabled_ex}])
[@{thm WriteInner_enabled}, exI] [] 1 *})
done
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Dec 15 05:11:46 2013 +0100
@@ -233,7 +233,7 @@
setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
-ML {* val temp_elim = make_elim o temp_use *}
+ML {* val temp_elim = make_elim oo temp_use *}
@@ -352,7 +352,7 @@
--> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
@{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
- @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
+ @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1 *})
(* ------------------------------ State S2 ---------------------------------------- *)
@@ -566,7 +566,8 @@
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p
--> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
- (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
+ (map (temp_elim @{context})
+ [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
using [[fast_solver]]
apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
done
@@ -576,7 +577,8 @@
--> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
- (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
+ (map (temp_elim @{context})
+ [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
using [[fast_solver]]
apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
done
@@ -586,9 +588,10 @@
--> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
| ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
- (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
+ (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{context} []
- (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
+ (@{thm squareE} ::
+ map (temp_elim @{context}) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
apply (auto dest!: S3Hist [temp_use])
done
@@ -599,9 +602,10 @@
| ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
| ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
- (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
+ (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
- (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
+ (@{thm squareE} ::
+ map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
apply (auto dest!: S4Hist [temp_use])
done
@@ -610,8 +614,8 @@
--> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
| ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
- (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
- apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
+ (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
+ apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
using [[fast_solver]]
apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
done
@@ -621,9 +625,9 @@
--> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
| ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
- (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
+ (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{context} []
- (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
+ (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
apply (auto dest: S6Hist [temp_use])
done
@@ -795,8 +799,8 @@
SELECT_GOAL
(TRY (rtac @{thm actionI} 1) THEN
Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
- rewrite_goals_tac @{thms action_rews} THEN
- forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
+ rewrite_goals_tac ctxt @{thms action_rews} THEN
+ forward_tac [temp_use ctxt @{thm Step1_4_7}] 1 THEN
asm_full_simp_tac ctxt 1);
*}
@@ -898,7 +902,7 @@
lemma S1_RNextdisabled: "|- S1 rmhist p -->
~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
- @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
+ @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
apply force
done
@@ -1103,7 +1107,7 @@
apply (erule InfiniteEnsures)
apply assumption
apply (tactic {* action_simp_tac @{context} []
- (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
+ (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
apply (auto simp: SF_def)
apply (erule contrapos_np)
apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
@@ -1190,7 +1194,7 @@
==> sigma |= []<>S1 rmhist p"
apply (rule classical)
apply (tactic {* asm_lr_simp_tac (@{context} addsimps
- [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
+ [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
done
--- a/src/HOL/TLA/TLA.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/TLA/TLA.thy Sun Dec 15 05:11:46 2013 +0100
@@ -118,25 +118,30 @@
functions defined in theory Intensional in that they introduce a
"world" parameter of type "behavior".
*)
-fun temp_unlift th =
- (rewrite_rule @{thms action_rews} (th RS @{thm tempD})) handle THM _ => action_unlift th;
+fun temp_unlift ctxt th =
+ (rewrite_rule ctxt @{thms action_rews} (th RS @{thm tempD}))
+ handle THM _ => action_unlift ctxt th;
(* Turn |- F = G into meta-level rewrite rule F == G *)
val temp_rewrite = int_rewrite
-fun temp_use th =
+fun temp_use ctxt th =
case (concl_of th) of
Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) =>
- ((flatten (temp_unlift th)) handle THM _ => th)
+ ((flatten (temp_unlift ctxt th)) handle THM _ => th)
| _ => th;
-fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
+fun try_rewrite ctxt th = temp_rewrite ctxt th handle THM _ => temp_use ctxt th;
*}
-attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *}
-attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *}
-attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *}
-attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *}
+attribute_setup temp_unlift =
+ {* Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of)) *}
+attribute_setup temp_rewrite =
+ {* Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of)) *}
+attribute_setup temp_use =
+ {* Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of)) *}
+attribute_setup try_rewrite =
+ {* Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of)) *}
(* ------------------------------------------------------------------------- *)
@@ -584,7 +589,7 @@
(EVERY
[auto_tac ctxt,
TRY (merge_box_tac 1),
- rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
+ rtac (temp_use ctxt @{thm INV1}) 1, (* fail if the goal is not a box *)
TRYALL (etac @{thm Stable})]);
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Sun Dec 15 05:11:46 2013 +0100
@@ -40,7 +40,7 @@
in
thms
|> Conjunction.intr_balanced
- |> rewrite_rule [Thm.symmetric (Thm.assume assum)]
+ |> rewrite_rule (Proof_Context.init_global thy) [Thm.symmetric (Thm.assume assum)]
|> Thm.implies_intr assum
|> Thm.generalize ([], params) 0
|> Axclass.unoverload thy
@@ -94,14 +94,14 @@
(def, lthy')
end;
- fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
+ fun tac ctxt thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms);
val qualify =
Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
in
Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
#> add_def
- #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single
+ #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single
#-> fold Code.del_eqn
#> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
#-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
--- a/src/HOL/Tools/Datatype/datatype.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Dec 15 05:11:46 2013 +0100
@@ -32,8 +32,6 @@
val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover};
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
-val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
-
fun exh_thm_of (dt_info : Datatype_Aux.info Symtab.table) tname =
#exhaust (the (Symtab.lookup dt_info tname));
@@ -271,6 +269,8 @@
val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
+ val collect_simp = rewrite_rule (Proof_Context.init_global thy4) [mk_meta_eq mem_Collect_eq];
+
val newT_iso_axms = typedefs |> map (fn (_, (_, {Abs_inverse, Rep_inverse, Rep, ...})) =>
(collect_simp Abs_inverse, Rep_inverse, collect_simp Rep));
@@ -355,7 +355,7 @@
val rewrites = def_thms @ map mk_meta_eq rec_rewrites;
val char_thms' =
map (fn eqn => Goal.prove_sorry_global thy' [] [] eqn
- (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
+ (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac refl 1])) eqns;
in (thy', char_thms' @ char_thms) end;
@@ -418,13 +418,13 @@
Goal.prove_sorry_global thy5 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
(fn {context = ctxt, ...} => EVERY
- [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
REPEAT (EVERY
[rtac allI 1, rtac impI 1,
Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
REPEAT (EVERY
[hyp_subst_tac ctxt 1,
- rewrite_goals_tac rewrites,
+ rewrite_goals_tac ctxt rewrites,
REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
(eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
ORELSE (EVERY
@@ -443,9 +443,10 @@
val elem_thm =
Goal.prove_sorry_global thy5 [] []
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
- (fn _ =>
- EVERY [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
- rewrite_goals_tac rewrites,
+ (fn {context = ctxt, ...} =>
+ EVERY [
+ (Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
+ rewrite_goals_tac ctxt rewrites,
REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
@@ -480,11 +481,11 @@
else
drop (length newTs) (Datatype_Aux.split_conj_thm
(Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
- [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
REPEAT (rtac TrueI 1),
- rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
+ rewrite_goals_tac ctxt (mk_meta_eq @{thm choice_eq} ::
Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
- rewrite_goals_tac (map Thm.symmetric range_eqs),
+ rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
REPEAT (EVERY
[REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
@@ -511,9 +512,9 @@
val rewrites = @{thm o_def} :: constr_defs @ map (mk_meta_eq o #2) newT_iso_axms;
in
Goal.prove_sorry_global thy5 [] [] eqn
- (fn _ => EVERY
+ (fn {context = ctxt, ...} => EVERY
[resolve_tac inj_thms 1,
- rewrite_goals_tac rewrites,
+ rewrite_goals_tac ctxt rewrites,
rtac refl 3,
resolve_tac rep_intrs 2,
REPEAT (resolve_tac iso_elem_thms 1)])
@@ -634,7 +635,7 @@
(fn {context = ctxt, prems, ...} =>
EVERY
[rtac indrule_lemma' 1,
- (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+ (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms 1),
simp_tac (put_simpset HOL_basic_ss ctxt
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sun Dec 15 05:11:46 2013 +0100
@@ -27,6 +27,9 @@
fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype.info) is thy =
let
+ val ctxt = Proof_Context.init_global thy;
+ val cert = cterm_of thy;
+
val recTs = Datatype_Aux.get_rec_types descr;
val pnames =
if length descr = 1 then ["P"]
@@ -104,7 +107,6 @@
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
- val cert = cterm_of thy;
val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
@@ -112,10 +114,10 @@
Goal.prove_internal (map cert prems) (cert concl)
(fn prems =>
EVERY [
- rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
+ rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
rtac (cterm_instantiate inst induct) 1,
- ALLGOALS Object_Logic.atomize_prems_tac,
- rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
+ ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
+ rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
REPEAT (etac allE i) THEN atac i)) 1)])
|> Drule.export_without_context;
--- a/src/HOL/Tools/Datatype/primrec.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Datatype/primrec.ML Sun Dec 15 05:11:46 2013 +0100
@@ -245,8 +245,10 @@
let
val frees = fold (Variable.add_free_names ctxt) eqs [];
val rewrites = rec_rewrites' @ map (snd o snd) defs;
- fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
- in map (fn eq => Goal.prove ctxt frees [] eq tac) eqs end;
+ in
+ map (fn eq => Goal.prove ctxt frees [] eq
+ (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs
+ end;
in ((prefix, (fs, defs)), prove) end
handle PrimrecError (msg, some_eqn) =>
error ("Primrec definition error:\n" ^ msg ^
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Sun Dec 15 05:11:46 2013 +0100
@@ -207,8 +207,8 @@
(HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts))
(fn {context = ctxt, ...} =>
#1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
- (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1 THEN
- rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
+ (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
+ rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
end;
val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
@@ -247,8 +247,8 @@
val rec_thms =
map (fn t =>
Goal.prove_sorry_global thy2 [] [] t
- (fn _ => EVERY
- [rewrite_goals_tac reccomb_defs,
+ (fn {context = ctxt, ...} => EVERY
+ [rewrite_goals_tac ctxt reccomb_defs,
rtac @{thm the1_equality} 1,
resolve_tac rec_unique_thms 1,
resolve_tac rec_intrs 1,
@@ -327,8 +327,8 @@
val case_thms =
(map o map) (fn t =>
Goal.prove_sorry_global thy2 [] [] t
- (fn _ =>
- EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
+ (fn {context = ctxt, ...} =>
+ EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
(Datatype_Prop.make_cases case_names descr thy2);
in
thy2
--- a/src/HOL/Tools/Function/function_lib.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Function/function_lib.ML Sun Dec 15 05:11:46 2013 +0100
@@ -107,12 +107,14 @@
fun regroup_conv neu cn ac is ct =
let
+ val thy = theory_of_cterm ct
+ val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
+
val mk = HOLogic.mk_binop cn
val t = term_of ct
val xs = dest_binop_list cn t
val js = subtract (op =) is (0 upto (length xs) - 1)
val ty = fastype_of t
- val thy = theory_of_cterm ct
in
Goal.prove_internal []
(cterm_of thy
@@ -122,7 +124,7 @@
else if null js
then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
- (K (rewrite_goals_tac ac
+ (K (rewrite_goals_tac ctxt ac
THEN rtac Drule.reflexive_thm 1))
end
--- a/src/HOL/Tools/Function/induction_schema.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Function/induction_schema.ML Sun Dec 15 05:11:46 2013 +0100
@@ -38,12 +38,12 @@
branches: scheme_branch list,
cases: scheme_case list}
-val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
-val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
+fun ind_atomize ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_atomize}
+fun ind_rulify ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_rulify}
fun meta thm = thm RS eq_reflection
-val sum_prod_conv = Raw_Simplifier.rewrite true
+fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
(map meta (@{thm split_conv} :: @{thms sum.cases}))
fun term_conv thy cv t =
@@ -187,13 +187,15 @@
end
-fun mk_ind_goal thy branches =
+fun mk_ind_goal ctxt branches =
let
+ val thy = Proof_Context.theory_of ctxt
+
fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
HOLogic.mk_Trueprop (list_comb (P, map Free xs))
|> fold_rev (curry Logic.mk_implies) Cs
|> fold_rev (Logic.all o Free) ws
- |> term_conv thy ind_atomize
+ |> term_conv thy (ind_atomize ctxt)
|> Object_Logic.drop_judgment thy
|> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
in
@@ -203,6 +205,9 @@
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 = cterm_of thy
+
val n = length branches
val scases_idx = map_index I scases
@@ -210,10 +215,7 @@
SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
- val thy = Proof_Context.theory_of ctxt
- val cert = cterm_of thy
-
- val P_comp = mk_ind_goal thy branches
+ val P_comp = mk_ind_goal ctxt branches
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
val ihyp = Logic.all_const T $ Abs ("z", T,
@@ -270,8 +272,8 @@
sih
|> Thm.forall_elim (cert (inject idx rcargs))
|> Thm.elim_implies (import ineq) (* Psum rcargs *)
- |> Conv.fconv_rule sum_prod_conv
- |> Conv.fconv_rule ind_rulify
+ |> Conv.fconv_rule (sum_prod_conv ctxt)
+ |> Conv.fconv_rule (ind_rulify ctxt)
|> (fn th => th COMP ipres) (* P rs *)
|> fold_rev (Thm.implies_intr o cprop_of) cGas
|> fold_rev Thm.forall_intr cGvs
@@ -312,8 +314,9 @@
val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
|> Goal.init
- |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
- THEN CONVERSION ind_rulify 1)
+ |> (Simplifier.rewrite_goals_tac ctxt
+ (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+ THEN CONVERSION (ind_rulify ctxt) 1)
|> Seq.hd
|> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
|> Goal.finish ctxt
@@ -375,7 +378,7 @@
indthm
|> Drule.instantiate' [] [SOME inst]
|> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
- |> Conv.fconv_rule ind_rulify
+ |> Conv.fconv_rule (ind_rulify ctxt'')
end
val res = Conjunction.intr_balanced (map_index project branches)
--- a/src/HOL/Tools/Function/partial_function.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Function/partial_function.ML Sun Dec 15 05:11:46 2013 +0100
@@ -180,6 +180,7 @@
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
in
+ (* FIXME ctxt vs. ctxt' (!?) *)
rule
|> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
|> Tactic.rule_by_tactic ctxt
@@ -188,7 +189,7 @@
THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
|> (fn thm => thm OF [mono_thm, f_def])
|> Conv.fconv_rule (Conv.concl_conv ~1 (* simplify conclusion *)
- (Raw_Simplifier.rewrite false [mk_meta_eq @{thm Product_Type.curry_split}]))
+ (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_split}]))
|> singleton (Variable.export ctxt' ctxt)
end
--- a/src/HOL/Tools/Function/termination.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Function/termination.ML Sun Dec 15 05:11:46 2013 +0100
@@ -305,7 +305,7 @@
in
(PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
- THEN rewrite_goal_tac Un_aci_simps 1) st (* eliminate duplicates *)
+ THEN rewrite_goal_tac ctxt Un_aci_simps 1) st (* eliminate duplicates *)
end
end
--- a/src/HOL/Tools/Lifting/lifting_def.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Sun Dec 15 05:11:46 2013 +0100
@@ -85,7 +85,7 @@
in
Conv.fconv_rule
((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
- (Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm
+ (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
end
fun inst_relcomppI thy ant1 ant2 =
@@ -482,7 +482,7 @@
val eq_thm =
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
in
- Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
+ Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
end
fun rename_to_tnames ctxt term =
@@ -533,7 +533,8 @@
fun after_qed' thm_list lthy =
let
val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm
- (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac (hd thm_list) 1)
+ (fn {context = ctxt, ...} =>
+ rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1)
in
after_qed internal_rsp_thm lthy
end
--- a/src/HOL/Tools/Meson/meson.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Meson/meson.ML Sun Dec 15 05:11:46 2013 +0100
@@ -552,9 +552,9 @@
@{const_name Let}]
fun presimplify ctxt =
- rewrite_rule (map safe_mk_meta_eq nnf_simps)
+ rewrite_rule ctxt (map safe_mk_meta_eq nnf_simps)
#> simplify (put_simpset nnf_ss ctxt)
- #> rewrite_rule @{thms Let_def [abs_def]}
+ #> rewrite_rule ctxt @{thms Let_def [abs_def]}
fun make_nnf ctxt th = case prems_of th of
[] => th |> presimplify ctxt |> make_nnf1 ctxt
@@ -706,7 +706,7 @@
Function mkcl converts theorems to clauses.*)
fun MESON preskolem_tac mkcl cltac ctxt i st =
SELECT_GOAL
- (EVERY [Object_Logic.atomize_prems_tac 1,
+ (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
rtac ccontr 1,
preskolem_tac,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun Dec 15 05:11:46 2013 +0100
@@ -193,6 +193,8 @@
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
fun old_skolem_theorem_of_def thy rhs0 =
let
+ val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
+
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
val rhs' = rhs |> Thm.dest_comb |> snd
val (ch, frees) = c_variant_abs_multi (rhs', [])
@@ -208,8 +210,8 @@
Drule.list_comb (rhs, frees)
|> Drule.beta_conv cabs |> Thm.apply cTrueprop
fun tacf [prem] =
- rewrite_goals_tac @{thms skolem_def [abs_def]}
- THEN rtac ((prem |> rewrite_rule @{thms skolem_def [abs_def]})
+ rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
+ THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
in
Goal.prove_internal [ex_tm] conc tacf
@@ -308,7 +310,7 @@
|> zero_var_indexes
|> new_skolem ? forall_intr_vars
val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
- val th = th |> Conv.fconv_rule Object_Logic.atomize
+ val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
|> cong_extensionalize_thm thy
|> abs_extensionalize_thm ctxt
|> make_nnf ctxt
--- a/src/HOL/Tools/Metis/metis_generate.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Metis/metis_generate.ML Sun Dec 15 05:11:46 2013 +0100
@@ -135,8 +135,8 @@
Isa_Raw of thm
val proxy_defs = map (fst o snd o snd) proxy_table
-val prepare_helper =
- Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
+fun prepare_helper ctxt =
+ Meson.make_meta_clause #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
if is_tptp_variable s then
@@ -160,7 +160,7 @@
fun metis_literals_of_atp type_enc (AConn (AOr, phis)) =
maps (metis_literals_of_atp type_enc) phis
| metis_literals_of_atp type_enc phi = [metis_literal_of_atp type_enc phi]
-fun metis_axiom_of_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
+fun metis_axiom_of_atp ctxt type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
let
fun some isa =
SOME (phi |> metis_literals_of_atp type_enc
@@ -178,7 +178,7 @@
nth (AList.lookup (op =) helper_table (const, needs_fairly_sound)
|> the)
(the (Int.fromString j) - 1)
- |> snd |> prepare_helper
+ |> snd |> prepare_helper ctxt
|> Isa_Raw |> some
| _ => raise Fail ("malformed helper identifier " ^ quote ident)
else case try (unprefix fact_prefix) ident of
@@ -196,7 +196,7 @@
end
| NONE => TrueI |> Isa_Raw |> some
end
- | metis_axiom_of_atp _ _ _ = raise Fail "not CNF -- expected formula"
+ | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
eliminate_lam_wrappers t
@@ -249,7 +249,7 @@
(* "rev" is for compatibility with existing proof scripts. *)
val axioms =
atp_problem
- |> maps (map_filter (metis_axiom_of_atp type_enc clauses) o snd) |> rev
+ |> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev
fun ord_info () = atp_problem_term_order_info atp_problem
in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Dec 15 05:11:46 2013 +0100
@@ -249,16 +249,16 @@
"P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
don't use this trick in general because it makes the proof object uglier than
necessary. FIXME. *)
-fun negate_head th =
+fun negate_head ctxt th =
if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
(th RS @{thm select_FalseI})
- |> fold (rewrite_rule o single)
+ |> fold (rewrite_rule ctxt o single)
@{thms not_atomize_select atomize_not_select}
else
- th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
+ th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not}
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
-val select_literal = negate_head oo make_last
+fun select_literal ctxt = negate_head ctxt oo make_last
fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
let
@@ -293,7 +293,7 @@
i_th2)
| j2 =>
(trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2);
- resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
+ resolve_inc_tyvars thy (select_literal ctxt j1 i_th1) j2 i_th2
handle TERM (s, _) =>
raise METIS_RECONSTRUCT ("resolve_inference", s)))
end
@@ -448,7 +448,7 @@
|> distinct Term.aconv_untyped
val goal = Logic.list_implies (prems, concl)
val tac = cut_tac th 1
- THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
+ THEN rewrite_goals_tac ctxt @{thms not_not [THEN eq_reflection]}
THEN ALLGOALS assume_tac
in
if length prems = length prems0 then
--- a/src/HOL/Tools/Metis/metis_tactic.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sun Dec 15 05:11:46 2013 +0100
@@ -65,7 +65,7 @@
fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
let
val thy = Proof_Context.theory_of ctxt
- val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
+ val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sun Dec 15 05:11:46 2013 +0100
@@ -219,8 +219,8 @@
|> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
val case_th =
- rewrite_rule (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
- val prems' = maps (dest_conjunct_prem o rewrite_rule tuple_rew_rules) prems
+ rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
+ val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems
val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
OF (replicate nargs @{thm refl})
@@ -236,7 +236,7 @@
(PEEK nprems_of
(fn n =>
ALLGOALS (fn i =>
- rewrite_goal_tac [@{thm split_paired_all}] i
+ rewrite_goal_tac ctxt [@{thm split_paired_all}] i
THEN (SUBPROOF (instantiate i n) ctxt i))))
in
Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Dec 15 05:11:46 2013 +0100
@@ -1017,8 +1017,9 @@
fun peephole_optimisation thy intro =
let
+ val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val process =
- rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
+ rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
fun process_False intro_t =
if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
fun process_True intro_t =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sun Dec 15 05:11:46 2013 +0100
@@ -203,7 +203,7 @@
SOME specss => (specss, thy)
| NONE =>*)
let
- val ctxt = Proof_Context.init_global thy
+ val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val intros =
if forall is_pred_equation specs then
map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
@@ -213,7 +213,7 @@
error ("unexpected specification for constant " ^ quote constname ^ ":\n"
^ commas (map (quote o Display.string_of_thm_global thy) specs))
val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
- val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros
+ val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros
val _ = print_specs options thy "normalized intros" intros
(*val intros = maps (split_cases thy) intros*)
val (intros', (local_defs, thy')) = flatten_intros constname intros thy
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Dec 15 05:11:46 2013 +0100
@@ -79,11 +79,11 @@
@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
| Free _ =>
- Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} =>
+ Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end) ctxt 1
| Abs _ => raise Fail "prove_param: No valid parameter term"
in
@@ -118,7 +118,7 @@
end
| (Free _, _) =>
print_tac options "proving parameter call.."
- THEN Subgoal.FOCUS_PREMS (fn {context, params, prems, asms, concl, schematics} =>
+ THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
let
val param_prem = nth prems premposition
val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
@@ -126,7 +126,7 @@
fun param_rewrite prem =
param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
val SOME rew_eq = find_first param_rewrite prems'
- val param_prem' = rewrite_rule
+ val param_prem' = rewrite_rule ctxt'
(map (fn th => th RS @{thm eq_reflection})
[rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
param_prem
@@ -168,7 +168,7 @@
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- rewrite_goal_tac
+ rewrite_goal_tac ctxt
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end
THEN REPEAT_DETERM (rtac @{thm refl} 1))
@@ -205,12 +205,12 @@
THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
THEN print_tac options "before single intro rule"
THEN Subgoal.FOCUS_PREMS
- (fn {context, params, prems, asms, concl, schematics} =>
- let
- val prems' = maps dest_conjunct_prem (take nargs prems)
- in
- rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
- end) ctxt 1
+ (fn {context = ctxt', params, prems, asms, concl, schematics} =>
+ let
+ val prems' = maps dest_conjunct_prem (take nargs prems)
+ in
+ rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ end) ctxt 1
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
| prove_prems out_ts ((p, deriv) :: ps) =
let
@@ -293,7 +293,7 @@
val nargs = length (binder_types T)
val pred_case_rule = the_elim_of ctxt pred
in
- REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))
+ REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
THEN print_tac options "before applying elim rule"
THEN etac (predfun_elim_of ctxt pred mode) 1
THEN etac pred_case_rule 1
@@ -370,7 +370,7 @@
val ho_args = ho_args_of mode args
in
etac @{thm bindE} 1
- THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
+ THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
THEN print_tac options "prove_expr2-before"
THEN etac (predfun_elim_of ctxt name mode) 1
THEN print_tac options "prove_expr2"
@@ -483,11 +483,11 @@
THEN (prove_clause2 options ctxt pred mode clause i)
in
(DETERM (TRY (rtac @{thm unit.induct} 1)))
- THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
+ THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
THEN (rtac (predfun_intro_of ctxt pred mode) 1)
THEN (REPEAT_DETERM (rtac @{thm refl} 2))
- THEN (if null moded_clauses then
- etac @{thm botE} 1
+ THEN (
+ if null moded_clauses then etac @{thm botE} 1
else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
end;
--- a/src/HOL/Tools/Qelim/cooper.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Dec 15 05:11:46 2013 +0100
@@ -865,19 +865,19 @@
val aprems = Arith_Data.get_arith_facts ctxt
in
Method.insert_tac aprems
- THEN_ALL_NEW Object_Logic.full_atomize_tac
+ THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW simp_tac simpset_ctxt
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
- THEN_ALL_NEW Object_Logic.full_atomize_tac
+ THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
- THEN_ALL_NEW Object_Logic.full_atomize_tac
+ THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
THEN_ALL_NEW div_mod_tac ctxt
THEN_ALL_NEW splits_tac ctxt
THEN_ALL_NEW simp_tac simpset_ctxt
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW nat_to_int_tac ctxt
- THEN_ALL_NEW (core_tac ctxt)
+ THEN_ALL_NEW core_tac ctxt
THEN_ALL_NEW finish_tac elim
end 1);
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun Dec 15 05:11:46 2013 +0100
@@ -107,7 +107,7 @@
fun tac ctxt =
ALLGOALS (rtac rule)
THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
- THEN (ALLGOALS (Proof_Context.fact_tac eqs2))
+ THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
in (simp, lthy') end;
@@ -166,7 +166,7 @@
fun prove_simps proto_simps lthy =
let
val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
- val tac = ALLGOALS (Proof_Context.fact_tac ext_simps);
+ val tac = ALLGOALS (Proof_Context.fact_tac lthy ext_simps);
in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
val b = Binding.conceal (Binding.qualify true prfx
(Binding.qualify true name (Binding.name "simps")));
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Dec 15 05:11:46 2013 +0100
@@ -129,7 +129,7 @@
val eq_thm =
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
in
- Object_Logic.rulify (eq_thm RS Drule.equal_elim_rule2)
+ Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
end
@@ -187,7 +187,7 @@
case thm_list of
[] => the maybe_proven_rsp_thm
| [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
- (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
+ (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
in
snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
end
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Dec 15 05:11:46 2013 +0100
@@ -40,10 +40,10 @@
(* composition of two theorems, used in maps *)
fun OF1 thm1 thm2 = thm2 RS thm1
-fun atomize_thm thm =
+fun atomize_thm ctxt thm =
let
val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
- val thm'' = Object_Logic.atomize (cprop_of thm')
+ val thm'' = Object_Logic.atomize ctxt (cprop_of thm')
in
@{thm equal_elim_rule1} OF [thm'', thm']
end
@@ -480,7 +480,7 @@
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
- val thm3 = rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
+ val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
val (insp, inst) =
if ty_c = ty_d
then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
@@ -635,7 +635,7 @@
val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
in
full_simp_tac simpset
- THEN' Object_Logic.full_atomize_tac
+ THEN' Object_Logic.full_atomize_tac ctxt
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
let
@@ -652,7 +652,7 @@
val mk_tac_raw =
descend_procedure_tac ctxt simps
THEN' RANGE
- [Object_Logic.rulify_tac THEN' (K all_tac),
+ [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
regularize_tac ctxt,
all_injection_tac ctxt,
clean_tac ctxt]
@@ -685,7 +685,7 @@
val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
in
full_simp_tac simpset
- THEN' Object_Logic.full_atomize_tac
+ THEN' Object_Logic.full_atomize_tac ctxt
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
let
@@ -702,7 +702,7 @@
val mk_tac_raw =
partiality_descend_procedure_tac ctxt simps
THEN' RANGE
- [Object_Logic.rulify_tac THEN' (K all_tac),
+ [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
all_injection_tac ctxt,
clean_tac ctxt]
in
@@ -720,7 +720,7 @@
val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
in
full_simp_tac simpset
- THEN' Object_Logic.full_atomize_tac
+ THEN' Object_Logic.full_atomize_tac ctxt
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
let
@@ -730,7 +730,7 @@
rthm |> full_simplify simpset
|> Drule.eta_contraction_rule
|> Thm.forall_intr_frees
- |> atomize_thm
+ |> atomize_thm ctxt
val rule = procedure_inst ctxt (prop_of rthm') goal
in
--- a/src/HOL/Tools/Quotient/quotient_type.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sun Dec 15 05:11:46 2013 +0100
@@ -193,7 +193,7 @@
val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name
val quotient_thm =
(quot_thm RS @{thm quot_type.Quotient})
- |> fold_rule [abs_def, rep_def]
+ |> fold_rule lthy3 [abs_def, rep_def]
(* name equivalence theorem *)
val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Sun Dec 15 05:11:46 2013 +0100
@@ -68,7 +68,7 @@
fun prove_inj_prop ctxt def lhs =
let
val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
- val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
+ val rule = disjE OF [Object_Logic.rulify ctxt (Thm.assume lhs)]
in
Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
|> apply (rtac @{thm injI})
@@ -94,7 +94,7 @@
fun prove_lhs ctxt rhs =
let
- val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
+ val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs)))
val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt
in
Z3_Proof_Tools.by_tac (
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sun Dec 15 05:11:46 2013 +0100
@@ -38,16 +38,19 @@
val merge = Net.merge eq
)
- val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true]
+ fun prep context =
+ `Thm.prop_of o rewrite_rule (Context.proof_of context) [Z3_Proof_Literals.rewrite_true]
- fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
- fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
+ fun ins thm context =
+ context |> Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net)
+ fun rem thm context =
+ context |> Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net)
- val add = Thm.declaration_attribute (Z3_Rules.map o ins)
- val del = Thm.declaration_attribute (Z3_Rules.map o del)
+ val add = Thm.declaration_attribute ins
+ val del = Thm.declaration_attribute rem
in
-val add_z3_rule = Z3_Rules.map o ins
+val add_z3_rule = ins
fun by_schematic_rule ctxt ct =
the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
--- a/src/HOL/Tools/TFL/post.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/TFL/post.ML Sun Dec 15 05:11:46 2013 +0100
@@ -68,10 +68,11 @@
| _ => r RS P_imp_P_eq_True
(*Is this the best way to invoke the simplifier??*)
-fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L))
+fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
fun join_assums th =
let val thy = Thm.theory_of_thm th
+ val ctxt = Proof_Context.init_global thy
val tych = cterm_of thy
val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *)
@@ -80,7 +81,7 @@
in
Rules.GEN_ALL
(Rules.DISCH_ALL
- (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
+ (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
end
val gen_all = USyntax.gen_all
in
@@ -139,7 +140,7 @@
let
val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
val {rules,rows,TCs,full_pats_TCs} =
- Prim.post_definition congs (thy, (def, pats))
+ Prim.post_definition congs thy ctxt (def, pats)
val {lhs=f,rhs} = USyntax.dest_eq (concl def)
val (_,[R,_]) = USyntax.strip_comb rhs
val dummy = Prim.trace_thms "congs =" congs
@@ -149,9 +150,9 @@
{f = f, R = R, rules = rules,
full_pats_TCs = full_pats_TCs,
TCs = TCs}
- val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
+ val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
(Rules.CONJUNCTS rules)
- in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
+ in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
rules = ListPair.zip(rules', rows),
tcs = (termination_goals rules') @ tcs}
end
@@ -170,7 +171,7 @@
| solve_eq _ (th, [a], i) = [(a, i)]
| solve_eq ctxt (th, splitths, i) =
(writeln "Proving unsplit equation...";
- [((Drule.export_without_context o Object_Logic.rulify_no_asm)
+ [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
(CaseSplit.splitto ctxt splitths th), i)])
handle ERROR s =>
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
--- a/src/HOL/Tools/TFL/rules.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/TFL/rules.ML Sun Dec 15 05:11:46 2013 +0100
@@ -42,14 +42,14 @@
val DISJ_CASESL: thm -> thm list -> thm
val list_beta_conv: cterm -> cterm list -> thm
- val SUBS: thm list -> thm -> thm
+ val SUBS: Proof.context -> thm list -> thm -> thm
val simpl_conv: Proof.context -> thm list -> cterm -> thm
val rbeta: thm -> thm
val tracing: bool Unsynchronized.ref
val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
-> thm -> thm * term list
- val RIGHT_ASSOC: thm -> thm
+ val RIGHT_ASSOC: Proof.context -> thm -> thm
val prove: bool -> cterm * tactic -> thm
end;
@@ -417,8 +417,8 @@
* Rewriting
*---------------------------------------------------------------------------*)
-fun SUBS thl =
- rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
+fun SUBS ctxt thl =
+ rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
@@ -426,7 +426,7 @@
rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
-val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];
+fun RIGHT_ASSOC ctxt = rewrite_rule ctxt [Thms.disj_assoc];
@@ -602,24 +602,24 @@
* the wrong word to use).
*---------------------------------------------------------------------------*)
-fun VSTRUCT_ELIM tych a vstr th =
+fun VSTRUCT_ELIM ctxt tych a vstr th =
let val L = USyntax.free_vars_lr vstr
val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
- val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
+ val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
val thm2 = forall_intr_list (map tych L) thm1
val thm3 = forall_elim_list (XFILL tych a vstr) thm2
in refl RS
- rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
+ rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
end;
-fun PGEN tych a vstr th =
+fun PGEN ctxt tych a vstr th =
let val a1 = tych a
val vstr1 = tych vstr
in
Thm.forall_intr a1
(if (is_Free vstr)
then cterm_instantiate [(vstr1,a1)] th
- else VSTRUCT_ELIM tych a vstr th)
+ else VSTRUCT_ELIM ctxt tych a vstr th)
end;
@@ -701,7 +701,7 @@
val impth = implies_intr_list ants1 QeeqQ3
val impth1 = impth RS meta_eq_to_obj_eq
(* Need to abstract *)
- val ant_th = Utils.itlist2 (PGEN tych) args vstrl impth1
+ val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
in ant_th COMP thm
end
fun q_eliminate (thm,imp,thy) =
--- a/src/HOL/Tools/TFL/tfl.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/TFL/tfl.ML Sun Dec 15 05:11:46 2013 +0100
@@ -12,7 +12,7 @@
type pattern
val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
val wfrec_definition0: theory -> string -> term -> term -> theory * thm
- val post_definition: thm list -> theory * (thm * pattern list) ->
+ val post_definition: thm list -> theory -> Proof.context -> thm * pattern list ->
{rules: thm,
rows: int list,
TCs: term list list,
@@ -415,7 +415,7 @@
fun givens pats = map pat_of (filter given pats);
-fun post_definition meta_tflCongs (theory, (def, pats)) =
+fun post_definition meta_tflCongs theory ctxt (def, pats) =
let val tych = Thry.typecheck theory
val f = #lhs(USyntax.dest_eq(concl def))
val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
@@ -440,7 +440,7 @@
val extract = Rules.CONTEXT_REWRITE_RULE
(f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
val (rules, TCs) = ListPair.unzip (map extract corollaries')
- val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
+ val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
in
@@ -460,7 +460,8 @@
*---------------------------------------------------------------------------*)
fun wfrec_eqns thy fid tflCongs eqns =
- let val {lhs,rhs} = USyntax.dest_eq (hd eqns)
+ let val ctxt = Proof_Context.init_global thy
+ val {lhs,rhs} = USyntax.dest_eq (hd eqns)
val (f,args) = USyntax.strip_comb lhs
val (fname,fty) = dest_atom f
val (SV,a) = front_last args (* SV = schematic variables *)
@@ -493,7 +494,7 @@
val R1 = USyntax.rand WFR
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 case_rewrites) corollaries
+ 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
in {proto_def = proto_def,
@@ -625,6 +626,7 @@
fun mk_case ty_info usednames thy =
let
+ val ctxt = Proof_Context.init_global thy
val divide = ipartition (gvvariant usednames)
val tych = Thry.typecheck thy
fun tych_binding(x,y) = (tych x, tych y)
@@ -657,7 +659,7 @@
(new_formals, disjuncts)
val constraints = map #1 existentials
val vexl = map #2 existentials
- fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS [Rules.ASSUME (tych tm)] th, b))
+ fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
val news = map (fn (nf,rows,c) => {path = nf@rstp,
rows = map (expnd c) rows})
(Utils.zip3 new_formals groups constraints)
@@ -675,7 +677,8 @@
fun complete_cases thy =
- let val tych = Thry.typecheck thy
+ let val ctxt = Proof_Context.init_global thy
+ val tych = Thry.typecheck thy
val ty_info = Thry.induct_info thy
in fn pats =>
let val names = List.foldr Misc_Legacy.add_term_names [] pats
@@ -691,7 +694,7 @@
val rows = map (fn x => ([x], (th0,[]))) pats
in
Rules.GEN (tych a)
- (Rules.RIGHT_ASSOC
+ (Rules.RIGHT_ASSOC ctxt
(Rules.CHOOSE(tych v, ex_th0)
(mk_case ty_info (vname::aname::names)
thy {path=[v], rows=rows})))
@@ -826,7 +829,8 @@
* the antecedent of Rinduct.
*---------------------------------------------------------------------------*)
fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
-let val tych = Thry.typecheck thy
+let val ctxt = Proof_Context.init_global thy
+ val tych = Thry.typecheck thy
val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases thy pats
@@ -848,7 +852,7 @@
domain)
val vtyped = tych v
val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
- val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
+ val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
(substs, proved_cases)
val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
--- a/src/HOL/Tools/choice_specification.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/choice_specification.ML Sun Dec 15 05:11:46 2013 +0100
@@ -113,6 +113,8 @@
fun process_spec axiomatic cos alt_props thy =
let
+ val ctxt = Proof_Context.init_global thy
+
fun zip3 [] [] [] = []
| zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
| zip3 _ _ _ = error "Choice_Specification.process_spec internal error"
@@ -122,7 +124,7 @@
| myfoldr f [] = error "Choice_Specification.process_spec internal error"
val rew_imps = alt_props |>
- map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
+ map (Object_Logic.atomize ctxt o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
val props' = rew_imps |>
map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
--- a/src/HOL/Tools/coinduction.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/coinduction.ML Sun Dec 15 05:11:46 2013 +0100
@@ -53,9 +53,9 @@
val cases = Rule_Cases.get raw_thm |> fst
in
NO_CASES (HEADGOAL (
- Object_Logic.rulify_tac THEN'
+ Object_Logic.rulify_tac ctxt THEN'
Method.insert_tac prems THEN'
- Object_Logic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
let
val vars = raw_vars @ map (term_of o snd) params;
@@ -110,7 +110,7 @@
unfold_thms_tac ctxt eqs
end)) ctxt)))])
end) ctxt) THEN'
- K (prune_params_tac))) st
+ K (prune_params_tac ctxt))) st
|> Seq.maps (fn (_, st) =>
CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
end;
--- a/src/HOL/Tools/groebner.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/groebner.ML Sun Dec 15 05:11:46 2013 +0100
@@ -928,7 +928,7 @@
delsimps del_thms addsimps add_thms);
fun ring_tac add_ths del_ths ctxt =
- Object_Logic.full_atomize_tac
+ Object_Logic.full_atomize_tac ctxt
THEN' presimplify ctxt add_ths del_ths
THEN' CSUBGOAL (fn (p, i) =>
rtac (let val form = Object_Logic.dest_judgment p
@@ -970,7 +970,7 @@
end
in
clarify_tac (put_claset claset ctxt) i
- THEN Object_Logic.full_atomize_tac i
+ THEN Object_Logic.full_atomize_tac ctxt i
THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i
THEN clarify_tac (put_claset claset ctxt) i
THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i))
--- a/src/HOL/Tools/inductive.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/inductive.ML Sun Dec 15 05:11:46 2013 +0100
@@ -396,7 +396,7 @@
val intrs = map_index (fn (i, intr) =>
Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
- [rewrite_goals_tac rec_preds_defs,
+ [rewrite_goals_tac ctxt rec_preds_defs,
rtac (unfold RS iffD2) 1,
EVERY1 (select_disj (length intr_ts) (i + 1)),
(*Not ares_tac, since refl must be tried before any equality assumptions;
@@ -440,14 +440,15 @@
map mk_elim_prem (map #1 c_intrs)
in
(Goal.prove_sorry ctxt'' [] prems P
- (fn {prems, ...} => EVERY
+ (fn {context = ctxt4, prems} => EVERY
[cut_tac (hd prems) 1,
- rewrite_goals_tac rec_preds_defs,
+ rewrite_goals_tac ctxt4 rec_preds_defs,
dtac (unfold RS iffD1) 1,
REPEAT (FIRSTGOAL (eresolve_tac rules1)),
REPEAT (FIRSTGOAL (eresolve_tac rules2)),
EVERY (map (fn prem =>
- DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
+ DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
+ (tl prems))])
|> singleton (Proof_Context.export ctxt'' ctxt'''),
map #2 c_intrs, length Ts)
end
@@ -503,12 +504,12 @@
(if null ts andalso null us then rtac intr 1
else
EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
- Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
+ Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
let
val (eqs, prems') = chop (length us) prems;
val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
in
- rewrite_goal_tac rew_thms 1 THEN
+ rewrite_goal_tac ctxt'' rew_thms 1 THEN
rtac intr 1 THEN
EVERY (map (fn p => rtac p 1) prems')
end) ctxt' 1);
@@ -545,7 +546,7 @@
in
-fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
+fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac ctxt;
fun mk_cases ctxt prop =
let
@@ -598,7 +599,7 @@
val props = Syntax.read_props ctxt' raw_props;
val ctxt'' = fold Variable.declare_term props ctxt';
val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
- in Method.erule 0 rules end))
+ in Method.erule ctxt 0 rules end))
"dynamic case analysis on predicates";
@@ -724,30 +725,30 @@
val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct});
val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
- (fn {prems, ...} => EVERY
- [rewrite_goals_tac [inductive_conj_def],
+ (fn {context = ctxt3, prems} => EVERY
+ [rewrite_goals_tac ctxt3 [inductive_conj_def],
DETERM (rtac raw_fp_induct 1),
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
- rewrite_goals_tac simp_thms2,
+ rewrite_goals_tac ctxt3 simp_thms2,
(*This disjE separates out the introduction rules*)
REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
(*Now break down the individual cases. No disjE here in case
some premise involves disjunction.*)
- REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
+ REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)),
REPEAT (FIRSTGOAL
(resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
- EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
+ EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
(inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
conjI, refl] 1)) prems)]);
val lemma = Goal.prove_sorry ctxt'' [] []
- (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
- [rewrite_goals_tac rec_preds_defs,
+ (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
+ [rewrite_goals_tac ctxt3 rec_preds_defs,
REPEAT (EVERY
[REPEAT (resolve_tac [conjI, impI] 1),
REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
atac 1,
- rewrite_goals_tac simp_thms1,
+ rewrite_goals_tac ctxt3 simp_thms1,
atac 1])]);
in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
@@ -961,9 +962,9 @@
(if no_ind then Drule.asm_rl
else if coind then
singleton (Proof_Context.export lthy2 lthy1)
- (rotate_prems ~1 (Object_Logic.rulify
- (fold_rule rec_preds_defs
- (rewrite_rule simp_thms3
+ (rotate_prems ~1 (Object_Logic.rulify lthy2
+ (fold_rule lthy2 rec_preds_defs
+ (rewrite_rule lthy2 simp_thms3
(mono RS (fp_def RS @{thm def_coinduct}))))))
else
prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
--- a/src/HOL/Tools/inductive_realizer.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Dec 15 05:11:46 2013 +0100
@@ -393,11 +393,11 @@
val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
val thm = Goal.prove_global thy []
(map attach_typeS prems) (attach_typeS concl)
- (fn {prems, ...} => EVERY
+ (fn {context = ctxt, prems} => EVERY
[rtac (#raw_induct ind_info) 1,
- rewrite_goals_tac rews,
+ rewrite_goals_tac ctxt rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
- [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
+ [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
(Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
@@ -459,8 +459,8 @@
[cut_tac (hd prems) 1,
etac elimR 1,
ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
- rewrite_goals_tac rews,
- REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
+ rewrite_goals_tac ctxt rews,
+ REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
(name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
--- a/src/HOL/Tools/lin_arith.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/lin_arith.ML Sun Dec 15 05:11:46 2013 +0100
@@ -871,8 +871,9 @@
in
-fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
- Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
+fun gen_tac ex ctxt =
+ FIRST' [simple_tac ctxt,
+ Object_Logic.full_atomize_tac ctxt THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
val tac = gen_tac true;
--- a/src/HOL/Tools/nat_arith.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/nat_arith.ML Sun Dec 15 05:11:46 2013 +0100
@@ -6,10 +6,10 @@
signature NAT_ARITH =
sig
- val cancel_diff_conv: conv
- val cancel_eq_conv: conv
- val cancel_le_conv: conv
- val cancel_less_conv: conv
+ val cancel_diff_conv: Proof.context -> conv
+ val cancel_eq_conv: Proof.context -> conv
+ val cancel_le_conv: Proof.context -> conv
+ val cancel_less_conv: Proof.context -> conv
end;
structure Nat_Arith: NAT_ARITH =
@@ -26,9 +26,9 @@
val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
-fun move_to_front path = Conv.every_conv
+fun move_to_front ctxt path = Conv.every_conv
[Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
- Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
+ Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
add_atoms (add1::path) x #> add_atoms (add2::path) y
@@ -54,12 +54,12 @@
find (sort ord' xs) (sort ord' ys)
end
-fun cancel_conv rule ct =
+fun cancel_conv rule ctxt ct =
let
val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
- val lconv = move_to_front lpath
- val rconv = move_to_front rpath
+ val lconv = move_to_front ctxt lpath
+ val rconv = move_to_front ctxt rpath
val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
val conv = conv1 then_conv Conv.rewr_conv rule
in conv ct end
--- a/src/HOL/Tools/record.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/record.ML Sun Dec 15 05:11:46 2013 +0100
@@ -1616,9 +1616,9 @@
val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_meta_prop
- (fn _ =>
+ (fn {context = ctxt, ...} =>
EVERY1
- [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
+ [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
etac @{thm meta_allE}, atac,
rtac (@{thm prop_subst} OF [surject]),
REPEAT o etac @{thm meta_allE}, atac]));
@@ -1742,12 +1742,13 @@
HOLogic.mk_Trueprop (HOLogic.mk_eq
(Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
- fun tac eq_def =
+ fun tac ctxt eq_def =
Class.intro_classes_tac []
- THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
+ THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
THEN ALLGOALS (rtac @{thm refl});
fun mk_eq thy eq_def =
- rewrite_rule [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
+ rewrite_rule (Proof_Context.init_global thy)
+ [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
fun mk_eq_refl thy =
@{thm equal_refl}
|> Thm.instantiate
@@ -1765,8 +1766,7 @@
|-> (fn eq => Specification.definition
(NONE, (Attrib.empty_binding, eq)))
|-> (fn (_, (_, eq_def)) =>
- Class.prove_instantiation_exit_result Morphism.thm
- (fn _ => fn eq_def => tac eq_def) eq_def)
+ Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
|-> (fn eq_def => fn thy =>
thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
|> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
@@ -2139,18 +2139,18 @@
val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_meta_prop
- (fn _ =>
+ (fn {context = ctxt', ...} =>
EVERY1
- [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
+ [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
etac @{thm meta_allE}, atac,
rtac (@{thm prop_subst} OF [surjective]),
REPEAT o etac @{thm meta_allE}, atac]));
val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] split_object_prop
- (fn _ =>
+ (fn {context = ctxt, ...} =>
rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
- rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
+ rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
rtac split_meta 1));
val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
--- a/src/HOL/Tools/sat_funcs.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/sat_funcs.ML Sun Dec 15 05:11:46 2013 +0100
@@ -427,9 +427,9 @@
(* subgoal *)
(* ------------------------------------------------------------------------- *)
-val pre_cnf_tac =
+fun pre_cnf_tac ctxt =
rtac ccontr THEN'
- Object_Logic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
CONVERSION Drule.beta_eta_conversion;
(* ------------------------------------------------------------------------- *)
@@ -460,7 +460,7 @@
(* ------------------------------------------------------------------------- *)
fun sat_tac ctxt i =
- pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
+ pre_cnf_tac ctxt i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
(* ------------------------------------------------------------------------- *)
(* satx_tac: tactic for calling an external SAT solver, taking as input an *)
@@ -469,6 +469,6 @@
(* ------------------------------------------------------------------------- *)
fun satx_tac ctxt i =
- pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
+ pre_cnf_tac ctxt i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
end;
--- a/src/HOL/Tools/simpdata.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/simpdata.ML Sun Dec 15 05:11:46 2013 +0100
@@ -71,10 +71,10 @@
Goal.prove_global (Thm.theory_of_thm st) []
[mk_simp_implies @{prop "(x::'a) == y"}]
(mk_simp_implies @{prop "(x::'a) = y"})
- (fn {prems, ...} => EVERY
- [rewrite_goals_tac @{thms simp_implies_def},
+ (fn {context = ctxt, prems} => EVERY
+ [rewrite_goals_tac ctxt @{thms simp_implies_def},
REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
- map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
+ map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
end
end;
--- a/src/HOL/Tools/transfer.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Tools/transfer.ML Sun Dec 15 05:11:46 2013 +0100
@@ -193,7 +193,7 @@
by (unfold is_equality_def, rule, drule meta_spec,
erule meta_mp, rule refl, simp)}
-fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
+fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
let
val thy = Thm.theory_of_thm thm
val prop = Thm.prop_of thm
@@ -212,7 +212,7 @@
val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
val cprop = Thm.cterm_of thy prop2
- val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop
+ val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
in
forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -234,11 +234,11 @@
Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
handle CTERM _ => thm
in
- gen_abstract_equalities dest contracted_eq_thm
+ gen_abstract_equalities ctxt dest contracted_eq_thm
end
-fun abstract_equalities_relator_eq rel_eq_thm =
- gen_abstract_equalities (fn x => (x, I))
+fun abstract_equalities_relator_eq ctxt rel_eq_thm =
+ gen_abstract_equalities ctxt (fn x => (x, I))
(rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
fun abstract_equalities_domain ctxt thm =
@@ -256,7 +256,7 @@
val contracted_eq_thm =
Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
in
- gen_abstract_equalities dest contracted_eq_thm
+ gen_abstract_equalities ctxt dest contracted_eq_thm
end
@@ -288,7 +288,7 @@
| t => t)
end
-fun gen_abstract_domains (dest : term -> term * (term -> term)) thm =
+fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
let
val thy = Thm.theory_of_thm thm
val prop = Thm.prop_of thm
@@ -305,14 +305,14 @@
val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
val prop2 = Logic.list_rename_params (rev names) prop1
val cprop = Thm.cterm_of thy prop2
- val equal_thm = Raw_Simplifier.rewrite false [Domainp_lemma] cprop
+ val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
in
forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
end
handle TERM _ => thm
-fun abstract_domains_transfer thm =
+fun abstract_domains_transfer ctxt thm =
let
fun dest prop =
let
@@ -324,7 +324,7 @@
Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
end
in
- gen_abstract_domains dest thm
+ gen_abstract_domains ctxt dest thm
end
fun detect_transfer_rules thm =
@@ -587,11 +587,11 @@
handle TERM (_, ts) => raise TERM (err_msg, ts)
in
EVERY
- [rewrite_goal_tac pre_simps i THEN
+ [rewrite_goal_tac ctxt pre_simps i THEN
SUBGOAL main_tac i,
(* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
- rewrite_goal_tac post_simps i,
- Goal.norm_hhf_tac i]
+ rewrite_goal_tac ctxt post_simps i,
+ Goal.norm_hhf_tac ctxt i]
end
fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
@@ -626,7 +626,7 @@
|> map (fn v as ((a, _), S) => (v, TFree (a, S)))
val thm2 = thm1
|> Thm.certify_instantiate (instT, [])
- |> Raw_Simplifier.rewrite_rule pre_simps
+ |> Raw_Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
val rule = transfer_rule_of_lhs ctxt' t
@@ -641,7 +641,7 @@
val tnames = map (fst o dest_TFree o snd) instT
in
thm3
- |> Raw_Simplifier.rewrite_rule post_simps
+ |> Raw_Simplifier.rewrite_rule ctxt' post_simps
|> Raw_Simplifier.norm_hhf
|> Drule.generalize (tnames, [])
|> Drule.zero_var_indexes
@@ -662,7 +662,7 @@
|> map (fn v as ((a, _), S) => (v, TFree (a, S)))
val thm2 = thm1
|> Thm.certify_instantiate (instT, [])
- |> Raw_Simplifier.rewrite_rule pre_simps
+ |> Raw_Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
val rule = transfer_rule_of_term ctxt' true t
@@ -677,7 +677,7 @@
val tnames = map (fst o dest_TFree o snd) instT
in
thm3
- |> Raw_Simplifier.rewrite_rule post_simps
+ |> Raw_Simplifier.rewrite_rule ctxt' post_simps
|> Raw_Simplifier.norm_hhf
|> Drule.generalize (tnames, [])
|> Drule.zero_var_indexes
@@ -700,8 +700,8 @@
(* Attribute for transfer rules *)
-fun prep_rule ctxt thm =
- (abstract_domains_transfer o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv) thm
+fun prep_rule ctxt =
+ abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
val transfer_add =
Thm.declaration_attribute (fn thm => fn ctxt =>
@@ -742,10 +742,14 @@
val relator_eq_setup =
let
val name = @{binding relator_eq}
- fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
- #> Data.map (map_relator_eq_raw (Item_Net.update (abstract_equalities_relator_eq thm)))
- fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
- #> Data.map (map_relator_eq_raw (Item_Net.remove (abstract_equalities_relator_eq thm)))
+ fun add_thm thm context = context
+ |> Data.map (map_relator_eq (Item_Net.update thm))
+ |> Data.map (map_relator_eq_raw
+ (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
+ fun del_thm thm context = context
+ |> Data.map (map_relator_eq (Item_Net.remove thm))
+ |> Data.map (map_relator_eq_raw
+ (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
val add = Thm.declaration_attribute add_thm
val del = Thm.declaration_attribute del_thm
val text = "declaration of relator equality rule (used by transfer method)"
--- a/src/HOL/Word/Word.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/HOL/Word/Word.thy Sun Dec 15 05:11:46 2013 +0100
@@ -14,7 +14,7 @@
Word_Miscellaneous
begin
-text {* see @{text "Examples/WordExamples.thy"} for examples *}
+text {* See @{file "Examples/WordExamples.thy"} for examples. *}
subsection {* Type definition *}
@@ -1463,7 +1463,7 @@
(put_simpset HOL_ss ctxt
|> fold Splitter.add_split @{thms uint_splits}
|> fold Simplifier.add_cong @{thms power_False_cong})),
- rewrite_goals_tac @{thms word_size},
+ rewrite_goals_tac ctxt @{thms word_size},
ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN
REPEAT (etac conjE n) THEN
REPEAT (dtac @{thm word_of_int_inverse} n
@@ -1964,7 +1964,7 @@
(put_simpset HOL_ss ctxt
|> fold Splitter.add_split @{thms unat_splits}
|> fold Simplifier.add_cong @{thms power_False_cong})),
- rewrite_goals_tac @{thms word_size},
+ rewrite_goals_tac ctxt @{thms word_size},
ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN
REPEAT (etac conjE n) THEN
REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
--- a/src/Provers/blast.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Provers/blast.ML Sun Dec 15 05:11:46 2013 +0100
@@ -1265,7 +1265,7 @@
fun depth_tac ctxt lim i st =
SELECT_GOAL
- (Object_Logic.atomize_prems_tac 1 THEN
+ (Object_Logic.atomize_prems_tac ctxt 1 THEN
raw_blast (Timing.start ()) ctxt lim) i st;
fun blast_tac ctxt i st =
@@ -1274,7 +1274,7 @@
val lim = Config.get ctxt depth_limit;
in
SELECT_GOAL
- (Object_Logic.atomize_prems_tac 1 THEN
+ (Object_Logic.atomize_prems_tac ctxt 1 THEN
DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
end;
--- a/src/Provers/clasimp.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Provers/clasimp.ML Sun Dec 15 05:11:46 2013 +0100
@@ -150,7 +150,7 @@
TRY (Classical.safe_tac ctxt) THEN
REPEAT_DETERM (FIRSTGOAL main_tac) THEN
TRY (Classical.safe_tac (addSss ctxt)) THEN
- prune_params_tac
+ prune_params_tac ctxt
end;
fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
--- a/src/Provers/classical.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Provers/classical.ML Sun Dec 15 05:11:46 2013 +0100
@@ -166,7 +166,13 @@
else rule;
(*flatten nested meta connectives in prems*)
-val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
+fun flat_rule opt_context th =
+ let
+ val ctxt =
+ (case opt_context of
+ NONE => Proof_Context.init_global (Thm.theory_of_thm th)
+ | SOME context => Context.proof_of context);
+ in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
(*** Useful tactics for classical reasoning ***)
@@ -325,7 +331,7 @@
if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
else
let
- val th' = flat_rule th;
+ val th' = flat_rule context th;
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
List.partition Thm.no_prems [th'];
val nI = Item_Net.length safeIs + 1;
@@ -354,7 +360,7 @@
error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
let
- val th' = classical_rule (flat_rule th);
+ val th' = classical_rule (flat_rule context th);
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
List.partition (fn rl => nprems_of rl=1) [th'];
val nI = Item_Net.length safeIs;
@@ -386,7 +392,7 @@
if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
else
let
- val th' = flat_rule th;
+ val th' = flat_rule context th;
val nI = Item_Net.length hazIs + 1;
val nE = Item_Net.length hazEs;
val _ = warn_claset context th cs;
@@ -415,7 +421,7 @@
error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
let
- val th' = classical_rule (flat_rule th);
+ val th' = classical_rule (flat_rule context th);
val nI = Item_Net.length hazIs;
val nE = Item_Net.length hazEs + 1;
val _ = warn_claset context th cs;
@@ -443,12 +449,12 @@
to insert.
***)
-fun delSI th
+fun delSI context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if Item_Net.member safeIs th then
let
- val th' = flat_rule th;
+ val th' = flat_rule context th;
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
in
CS
@@ -466,12 +472,12 @@
end
else cs;
-fun delSE th
+fun delSE context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if Item_Net.member safeEs th then
let
- val th' = classical_rule (flat_rule th);
+ val th' = classical_rule (flat_rule context th);
val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
in
CS
@@ -493,7 +499,7 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if Item_Net.member hazIs th then
- let val th' = flat_rule th in
+ let val th' = flat_rule context th in
CS
{haz_netpair = delete ([th'], []) haz_netpair,
dup_netpair = delete ([dup_intr th'], []) dup_netpair,
@@ -511,11 +517,11 @@
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *)
error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
-fun delE th
+fun delE context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if Item_Net.member hazEs th then
- let val th' = classical_rule (flat_rule th) in
+ let val th' = classical_rule (flat_rule context th) in
CS
{haz_netpair = delete ([], [th']) haz_netpair,
dup_netpair = delete ([], [dup_elim th']) dup_netpair,
@@ -537,7 +543,11 @@
if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
- then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
+ then
+ delSI context th
+ (delSE context th
+ (delI context th
+ (delE context th (delSE context th' (delE context th' cs)))))
else (warn_thm context "Undeclared classical rule\n" th; cs)
end;
@@ -774,24 +784,24 @@
(*Dumb but fast*)
fun fast_tac ctxt =
- Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
+ Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
(*Slower but smarter than fast_tac*)
fun best_tac ctxt =
- Object_Logic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
(*even a bit smarter than best_tac*)
fun first_best_tac ctxt =
- Object_Logic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
fun slow_tac ctxt =
- Object_Logic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
fun slow_best_tac ctxt =
- Object_Logic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
@@ -800,13 +810,13 @@
val weight_ASTAR = 5;
fun astar_tac ctxt =
- Object_Logic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
SELECT_GOAL
(ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
(step_tac ctxt 1));
fun slow_astar_tac ctxt =
- Object_Logic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
SELECT_GOAL
(ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
(slow_step_tac ctxt 1));
@@ -901,12 +911,12 @@
in
fn st => Seq.maps (fn rule => rtac rule i st) ruleq
end)
- THEN_ALL_NEW Goal.norm_hhf_tac;
+ THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
in
fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
- | rule_tac _ rules facts = Method.rule_tac rules facts;
+ | rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts;
fun default_tac ctxt rules facts =
HEADGOAL (rule_tac ctxt rules facts) ORELSE
@@ -941,7 +951,7 @@
(Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
"apply some intro/elim rule (potentially classical)" #>
Method.setup @{binding contradiction}
- (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])))
+ (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
"proof by contradiction" #>
Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
"repeatedly apply safe steps" #>
--- a/src/Provers/splitter.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Provers/splitter.ML Sun Dec 15 05:11:46 2013 +0100
@@ -100,7 +100,7 @@
val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
[Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
(Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
- (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1)
+ (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1)
val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
--- a/src/Pure/Isar/class.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/class.ML Sun Dec 15 05:11:46 2013 +0100
@@ -656,7 +656,7 @@
| default_intro_tac _ _ = no_tac;
fun default_tac rules ctxt facts =
- HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
+ HEADGOAL (Method.some_rule_tac ctxt rules facts) ORELSE
default_intro_tac ctxt facts;
val _ = Theory.setup
--- a/src/Pure/Isar/class_declaration.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/class_declaration.ML Sun Dec 15 05:11:46 2013 +0100
@@ -58,7 +58,7 @@
(_, NONE) => all_tac
| (_, SOME intro) => ALLGOALS (rtac intro));
val tac = loc_intro_tac
- THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
+ THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
in Element.prove_witness empty_ctxt prop tac end) some_prop;
val some_axiom = Option.map Element.conclude_witness some_witn;
@@ -77,8 +77,10 @@
SOME eq_morph => const_morph $> eq_morph
| NONE => const_morph);
val thm'' = Morphism.thm const_eq_morph thm';
- val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
- in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+ in
+ Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'')
+ (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm'']))
+ end;
val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
(* of_class *)
--- a/src/Pure/Isar/code.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/code.ML Sun Dec 15 05:11:46 2013 +0100
@@ -1130,9 +1130,12 @@
fun mk_prem z = Free (z, T_cong);
fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
- fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
- THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
- in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end;
+ in
+ Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl
+ (fn {context = ctxt', prems} =>
+ Simplifier.rewrite_goals_tac ctxt' prems
+ THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm]))
+ end;
fun add_case thm thy =
let
--- a/src/Pure/Isar/element.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/element.ML Sun Dec 15 05:11:46 2013 +0100
@@ -456,11 +456,16 @@
fun eq_morphism _ [] = NONE
| eq_morphism thy thms =
- SOME (Morphism.morphism "Element.eq_morphism"
- {binding = [],
- typ = [],
- term = [Raw_Simplifier.rewrite_term thy thms []],
- fact = [map (rewrite_rule thms)]});
+ let
+ (* FIXME proper context!? *)
+ fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th;
+ val phi =
+ Morphism.morphism "Element.eq_morphism"
+ {binding = [],
+ typ = [],
+ term = [Raw_Simplifier.rewrite_term thy thms []],
+ fact = [map rewrite]};
+ in SOME phi end;
--- a/src/Pure/Isar/expression.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/expression.ML Sun Dec 15 05:11:46 2013 +0100
@@ -619,7 +619,7 @@
val bodyT = Term.fastype_of body;
in
if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
- else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
+ else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t))
end;
(* achieve plain syntax for locale predicates (without "PROP") *)
@@ -669,20 +669,22 @@
val cert = Thm.cterm_of defs_thy;
- val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
- rewrite_goals_tac [pred_def] THEN
- compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
- compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+ val intro = Goal.prove_global defs_thy [] norm_ts statement
+ (fn {context = ctxt, ...} =>
+ rewrite_goals_tac ctxt [pred_def] THEN
+ compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
+ compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
val conjuncts =
- (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
+ (Drule.equal_elim_rule2 OF
+ [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
|> Conjunction.elim_balanced (length ts);
val (_, axioms_ctxt) = defs_ctxt
|> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
Element.prove_witness axioms_ctxt t
- (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
+ (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
in ((statement, intro, axioms), defs_thy) end;
in
@@ -849,7 +851,7 @@
val dep_morphs = map2 (fn (dep, morph) => fn wits =>
(dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
fun activate' dep_morph ctxt = activate dep_morph
- (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
+ (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
in
ctxt'
|> fold activate' dep_morphs
--- a/src/Pure/Isar/generic_target.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/generic_target.ML Sun Dec 15 05:11:46 2013 +0100
@@ -104,7 +104,7 @@
(*result*)
val def =
Thm.transitive local_def global_def
- |> Local_Defs.contract defs
+ |> Local_Defs.contract lthy3 defs
(Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
val ([(res_name, [res])], lthy4) = lthy3
|> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
@@ -125,7 +125,7 @@
(*export assumes/defines*)
val th = Goal.norm_result raw_th;
val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
- val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
+ val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
(*export fixes*)
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
@@ -153,7 +153,7 @@
val result'' =
(fold (curry op COMP) asms' result'
handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
- |> Local_Defs.contract defs (Thm.cprop_of th)
+ |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
|> Goal.norm_result
|> Global_Theory.name_thm false false name;
--- a/src/Pure/Isar/local_defs.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/local_defs.ML Sun Dec 15 05:11:46 2013 +0100
@@ -17,7 +17,7 @@
(term * term) * Proof.context
val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm
val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm
- val contract: thm list -> cterm -> thm -> thm
+ val contract: Proof.context -> thm list -> cterm -> thm -> thm
val print_rules: Proof.context -> unit
val defn_add: attribute
val defn_del: attribute
@@ -162,8 +162,8 @@
fun export_cterm inner outer ct =
export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
-fun contract defs ct th =
- th COMP (Raw_Simplifier.rewrite true defs ct COMP_INCR Drule.equal_elim_rule2);
+fun contract ctxt defs ct th =
+ th COMP (Raw_Simplifier.rewrite ctxt true defs ct COMP_INCR Drule.equal_elim_rule2);
@@ -200,7 +200,7 @@
(* rewriting with object-level rules *)
-fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
+fun meta f ctxt = f ctxt o map (meta_rewrite_rule ctxt);
val unfold = meta Raw_Simplifier.rewrite_rule;
val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule;
@@ -220,10 +220,12 @@
|> conditional ? Logic.strip_imp_concl
|> (abs_def o #2 o cert_def ctxt);
fun prove ctxt' def =
- Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop (K (ALLGOALS
- (CONVERSION (meta_rewrite_conv ctxt') THEN'
- rewrite_goal_tac [def] THEN'
- resolve_tac [Drule.reflexive_thm])))
+ Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop
+ (fn {context = ctxt'', ...} =>
+ ALLGOALS
+ (CONVERSION (meta_rewrite_conv ctxt'') THEN'
+ rewrite_goal_tac ctxt'' [def] THEN'
+ resolve_tac [Drule.reflexive_thm]))
handle ERROR msg => cat_error msg "Failed to prove definitional specification";
in (((c, T), rhs), prove) end;
--- a/src/Pure/Isar/method.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/method.ML Sun Dec 15 05:11:46 2013 +0100
@@ -25,7 +25,7 @@
val elim: thm list -> method
val unfold: thm list -> Proof.context -> method
val fold: thm list -> Proof.context -> method
- val atomize: bool -> method
+ val atomize: bool -> Proof.context -> method
val this: method
val fact: thm list -> Proof.context -> method
val assm_tac: Proof.context -> int -> tactic
@@ -33,14 +33,14 @@
val assumption: Proof.context -> method
val rule_trace: bool Config.T
val trace: Proof.context -> thm list -> unit
- val rule_tac: thm list -> thm list -> int -> tactic
- val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
+ val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
+ val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
val intros_tac: thm list -> thm list -> tactic
val try_intros_tac: thm list -> thm list -> tactic
- val rule: thm list -> method
- val erule: int -> thm list -> method
- val drule: int -> thm list -> method
- val frule: int -> thm list -> method
+ val rule: Proof.context -> thm list -> method
+ val erule: Proof.context -> int -> thm list -> method
+ val drule: Proof.context -> int -> thm list -> method
+ val frule: Proof.context -> int -> thm list -> method
val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
val tactic: string * Position.T -> Proof.context -> method
val raw_tactic: string * Position.T -> Proof.context -> method
@@ -147,8 +147,10 @@
(* atomize rule statements *)
-fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
- | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
+fun atomize false ctxt =
+ SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
+ | atomize true ctxt =
+ RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)));
(* this -- resolve facts directly *)
@@ -159,7 +161,7 @@
(* fact -- composition by facts from context *)
fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt)
- | fact rules _ = SIMPLE_METHOD' (Proof_Context.fact_tac rules);
+ | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules);
(* assumption *)
@@ -208,31 +210,31 @@
local
-fun gen_rule_tac tac rules facts =
+fun gen_rule_tac tac ctxt rules facts =
(fn i => fn st =>
if null facts then tac rules i st
else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
- THEN_ALL_NEW Goal.norm_hhf_tac;
+ THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
-fun gen_arule_tac tac j rules facts =
- EVERY' (gen_rule_tac tac rules facts :: replicate j assume_tac);
+fun gen_arule_tac tac ctxt j rules facts =
+ EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac);
-fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
+fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) =>
let
val rules =
if not (null arg_rules) then arg_rules
else flat (Context_Rules.find_rules false facts goal ctxt)
- in trace ctxt rules; tac rules facts i end);
+ in trace ctxt rules; tac ctxt rules facts i end);
-fun meth tac x = METHOD (HEADGOAL o tac x);
-fun meth' tac x y = METHOD (HEADGOAL o tac x y);
+fun meth tac x y = METHOD (HEADGOAL o tac x y);
+fun meth' tac x y z = METHOD (HEADGOAL o tac x y z);
in
val rule_tac = gen_rule_tac resolve_tac;
val rule = meth rule_tac;
val some_rule_tac = gen_some_rule_tac rule_tac;
-val some_rule = meth' some_rule_tac;
+val some_rule = meth some_rule_tac;
val erule = meth' (gen_arule_tac eresolve_tac);
val drule = meth' (gen_arule_tac dresolve_tac);
@@ -390,9 +392,9 @@
(* extra rule methods *)
-fun xrule_meth m =
+fun xrule_meth meth =
Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
- (fn (n, ths) => K (m n ths));
+ (fn (n, ths) => fn ctxt => meth ctxt n ths);
(* outer parser *)
@@ -451,9 +453,10 @@
"repeatedly apply elimination rules" #>
setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
- setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> (K o atomize))
+ setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> atomize)
"present local premises as object-level statements" #>
- setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
+ setup (Binding.name "rule") (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
+ "apply some intro/elim rule" #>
setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
--- a/src/Pure/Isar/object_logic.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/object_logic.ML Sun Dec 15 05:11:46 2013 +0100
@@ -21,14 +21,14 @@
val declare_atomize: attribute
val declare_rulify: attribute
val atomize_term: theory -> term -> term
- val atomize: conv
- val atomize_prems: conv
- val atomize_prems_tac: int -> tactic
- val full_atomize_tac: int -> tactic
+ val atomize: Proof.context -> conv
+ val atomize_prems: Proof.context -> conv
+ val atomize_prems_tac: Proof.context -> int -> tactic
+ val full_atomize_tac: Proof.context -> int -> tactic
val rulify_term: theory -> term -> term
- val rulify_tac: int -> tactic
- val rulify: thm -> thm
- val rulify_no_asm: thm -> thm
+ val rulify_tac: Proof.context -> int -> tactic
+ val rulify: Proof.context -> thm -> thm
+ val rulify_no_asm: Proof.context -> thm -> thm
val rule_format: attribute
val rule_format_no_asm: attribute
end;
@@ -182,32 +182,31 @@
fun atomize_term thy =
drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
-fun atomize ct =
- Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
+fun atomize ctxt =
+ Raw_Simplifier.rewrite ctxt true (get_atomize (Proof_Context.theory_of ctxt));
-fun atomize_prems ct =
+fun atomize_prems ctxt ct =
if Logic.has_meta_prems (Thm.term_of ct) then
- Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
- (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct
+ Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize) ctxt ct
else Conv.all_conv ct;
-val atomize_prems_tac = CONVERSION atomize_prems;
-val full_atomize_tac = CONVERSION atomize;
+val atomize_prems_tac = CONVERSION o atomize_prems;
+val full_atomize_tac = CONVERSION o atomize;
(* rulify *)
fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
-fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
+fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
-fun gen_rulify full thm =
- Conv.fconv_rule (Raw_Simplifier.rewrite full (get_rulify (Thm.theory_of_thm thm))) thm
- |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
+fun gen_rulify full ctxt =
+ Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
+ #> Drule.gen_all #> Thm.strip_shyps #> Drule.zero_var_indexes;
val rulify = gen_rulify true;
val rulify_no_asm = gen_rulify false;
-val rule_format = Thm.rule_attribute (K rulify);
-val rule_format_no_asm = Thm.rule_attribute (K rulify_no_asm);
+val rule_format = Thm.rule_attribute (rulify o Context.proof_of);
+val rule_format_no_asm = Thm.rule_attribute (rulify_no_asm o Context.proof_of);
end;
--- a/src/Pure/Isar/proof.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/proof.ML Sun Dec 15 05:11:46 2013 +0100
@@ -443,18 +443,18 @@
local
-fun finish_tac 0 = K all_tac
- | finish_tac n =
- Goal.norm_hhf_tac THEN'
+fun finish_tac _ 0 = K all_tac
+ | finish_tac ctxt n =
+ Goal.norm_hhf_tac ctxt THEN'
SUBGOAL (fn (goal, i) =>
if can Logic.unprotect (Logic.strip_assums_concl goal) then
- etac Drule.protectI i THEN finish_tac (n - 1) i
- else finish_tac (n - 1) (i + 1));
+ etac Drule.protectI i THEN finish_tac ctxt (n - 1) i
+ else finish_tac ctxt (n - 1) (i + 1));
-fun goal_tac rule =
- Goal.norm_hhf_tac THEN'
+fun goal_tac ctxt rule =
+ Goal.norm_hhf_tac ctxt THEN'
rtac rule THEN'
- finish_tac (Thm.nprems_of rule);
+ finish_tac ctxt (Thm.nprems_of rule);
fun FINDGOAL tac st =
let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
@@ -465,7 +465,7 @@
fun refine_goals print_rule inner raw_rules state =
let
val (outer, (_, goal)) = get_goal state;
- fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st);
+ fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st);
in
raw_rules
|> Proof_Context.goal_export inner outer
--- a/src/Pure/Isar/proof_context.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/proof_context.ML Sun Dec 15 05:11:46 2013 +0100
@@ -110,7 +110,7 @@
(term list list * (Proof.context -> Proof.context)) * Proof.context
val bind_propp_schematic_i: (term * term list) list list -> Proof.context ->
(term list list * (Proof.context -> Proof.context)) * Proof.context
- val fact_tac: thm list -> int -> tactic
+ val fact_tac: Proof.context -> thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
val get_fact: Proof.context -> Facts.ref -> thm list
val get_fact_single: Proof.context -> Facts.ref -> thm
@@ -889,12 +889,12 @@
in
-fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
+fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts;
fun potential_facts ctxt prop =
Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
-fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
+fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i);
end;
@@ -913,7 +913,7 @@
val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
fun prove_fact th =
- Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac [th])));
+ Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
val results = map_filter (try prove_fact) (potential_facts ctxt prop');
val res =
(case distinct Thm.eq_thm_prop results of
--- a/src/Pure/Isar/rule_cases.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Isar/rule_cases.ML Sun Dec 15 05:11:46 2013 +0100
@@ -31,7 +31,7 @@
val make_nested: term -> theory * term ->
((string * string list) * string list) list -> cases
val apply: term list -> T -> T
- val consume: thm list -> thm list -> ('a * int) * thm ->
+ val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
(('a * (int * thm list)) * thm) Seq.seq
val get_consumes: thm -> int
val put_consumes: int option -> thm -> thm
@@ -203,24 +203,24 @@
local
-fun unfold_prems n defs th =
+fun unfold_prems ctxt n defs th =
if null defs then th
- else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th;
+ else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite ctxt true defs)) th;
-fun unfold_prems_concls defs th =
+fun unfold_prems_concls ctxt defs th =
if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
else
Conv.fconv_rule
(Conv.concl_conv ~1 (Conjunction.convs
- (Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th;
+ (Conv.prems_conv ~1 (Raw_Simplifier.rewrite ctxt true defs)))) th;
in
-fun consume defs facts ((xx, n), th) =
+fun consume ctxt defs facts ((xx, n), th) =
let val m = Int.min (length facts, n) in
th
- |> unfold_prems n defs
- |> unfold_prems_concls defs
+ |> unfold_prems ctxt n defs
+ |> unfold_prems_concls ctxt defs
|> Drule.multi_resolve (take m facts)
|> Seq.map (pair (xx, (n - m, drop m facts)))
end;
--- a/src/Pure/Tools/find_theorems.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/Tools/find_theorems.ML Sun Dec 15 05:11:46 2013 +0100
@@ -237,7 +237,9 @@
Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
fun try_thm thm =
if Thm.no_prems thm then rtac thm 1 goal'
- else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
+ else
+ (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
+ 1 goal';
in
fn Internal (_, thm) =>
if is_some (Seq.pull (try_thm thm))
--- a/src/Pure/axclass.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/axclass.ML Sun Dec 15 05:11:46 2013 +0100
@@ -291,11 +291,17 @@
fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
-fun unoverload thy = rewrite_rule (inst_thms thy);
-fun overload thy = rewrite_rule (map Thm.symmetric (inst_thms thy));
+fun unoverload thy =
+ rewrite_rule (Proof_Context.init_global thy) (inst_thms thy);
+
+fun overload thy =
+ rewrite_rule (Proof_Context.init_global thy) (map Thm.symmetric (inst_thms thy));
-fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
-fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
+fun unoverload_conv thy =
+ Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (inst_thms thy);
+
+fun overload_conv thy =
+ Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (map Thm.symmetric (inst_thms thy));
fun lookup_inst_param consts params (c, T) =
(case get_inst_tyco consts (c, T) of
--- a/src/Pure/goal.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/goal.ML Sun Dec 15 05:11:46 2013 +0100
@@ -49,7 +49,7 @@
val conjunction_tac: int -> tactic
val precise_conjunction_tac: int -> int -> tactic
val recover_conjunction_tac: tactic
- val norm_hhf_tac: int -> tactic
+ val norm_hhf_tac: Proof.context -> int -> tactic
val assume_rule_tac: Proof.context -> int -> tactic
end;
@@ -317,11 +317,11 @@
(* hhf normal form *)
-val norm_hhf_tac =
+fun norm_hhf_tac ctxt =
rtac Drule.asm_rl (*cheap approximation -- thanks to builtin Logic.flatten_params*)
THEN' SUBGOAL (fn (t, i) =>
if Drule.is_norm_hhf t then all_tac
- else rewrite_goal_tac Drule.norm_hhf_eqs i);
+ else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
(* non-atomic goal assumptions *)
@@ -330,7 +330,7 @@
| non_atomic (Const ("all", _) $ _) = true
| non_atomic _ = false;
-fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
+fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
let
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
--- a/src/Pure/raw_simplifier.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Pure/raw_simplifier.ML Sun Dec 15 05:11:46 2013 +0100
@@ -57,13 +57,13 @@
val setSolver: Proof.context * solver -> Proof.context
val addSolver: Proof.context * solver -> Proof.context
- val rewrite_rule: thm list -> thm -> thm
- val rewrite_goals_rule: thm list -> thm -> thm
- val rewrite_goals_tac: thm list -> tactic
- val rewrite_goal_tac: thm list -> int -> tactic
- val prune_params_tac: tactic
- val fold_rule: thm list -> thm -> thm
- val fold_goals_tac: thm list -> tactic
+ val rewrite_rule: Proof.context -> thm list -> thm -> thm
+ val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm
+ val rewrite_goals_tac: Proof.context -> thm list -> tactic
+ val rewrite_goal_tac: Proof.context -> thm list -> int -> tactic
+ val prune_params_tac: Proof.context -> tactic
+ val fold_rule: Proof.context -> thm list -> thm -> thm
+ val fold_goals_tac: Proof.context -> thm list -> tactic
val norm_hhf: thm -> thm
val norm_hhf_protect: thm -> thm
end;
@@ -126,7 +126,7 @@
(Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm
val generic_rewrite_goal_tac: bool * bool * bool ->
(Proof.context -> tactic) -> Proof.context -> int -> tactic
- val rewrite: bool -> thm list -> conv
+ val rewrite: Proof.context -> bool -> thm list -> conv
end;
structure Raw_Simplifier: RAW_SIMPLIFIER =
@@ -1366,12 +1366,12 @@
val simple_prover =
SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
-fun rewrite _ [] ct = Thm.reflexive ct
- | rewrite full thms ct =
+fun rewrite _ _ [] = Thm.reflexive
+ | rewrite ctxt full thms =
rewrite_cterm (full, false, false) simple_prover
- (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
+ (empty_simpset ctxt addsimps thms);
-val rewrite_rule = Conv.fconv_rule o rewrite true;
+fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
(*simple term rewriting -- no proof*)
fun rewrite_term thy rules procs =
@@ -1380,15 +1380,15 @@
fun rewrite_thm mode prover ctxt = Conv.fconv_rule (rewrite_cterm mode prover ctxt);
(*Rewrite the subgoals of a proof state (represented by a theorem)*)
-fun rewrite_goals_rule thms th =
+fun rewrite_goals_rule ctxt thms th =
Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
- (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
+ (empty_simpset ctxt addsimps thms))) th;
(** meta-rewriting tactics **)
(*Rewrite all subgoals*)
-fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
+fun rewrite_goals_tac ctxt defs = PRIMITIVE (rewrite_goals_rule ctxt defs);
(*Rewrite one subgoal*)
fun generic_rewrite_goal_tac mode prover_tac ctxt i thm =
@@ -1396,12 +1396,12 @@
Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
else Seq.empty;
-fun rewrite_goal_tac rews i st =
+fun rewrite_goal_tac ctxt rews =
generic_rewrite_goal_tac (true, false, false) (K no_tac)
- (global_context (Thm.theory_of_thm st) empty_ss addsimps rews) i st;
+ (empty_simpset ctxt addsimps rews);
(*Prunes all redundant parameters from the proof state by rewriting.*)
-val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
+fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
(* for folding definitions, handling critical pairs *)
@@ -1422,8 +1422,8 @@
val rev_defs = sort_lhs_depths o map Thm.symmetric;
-fun fold_rule defs = fold rewrite_rule (rev_defs defs);
-fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
+fun fold_rule ctxt defs = fold (rewrite_rule ctxt) (rev_defs defs);
+fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs));
(* HHF normal form: !! before ==>, outermost !! generalized *)
--- a/src/Sequents/S4.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Sequents/S4.thy Sun Dec 15 05:11:46 2013 +0100
@@ -43,7 +43,8 @@
)
*}
-method_setup S4_solve = {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *}
+method_setup S4_solve =
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2)) *}
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
--- a/src/Sequents/S43.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Sequents/S43.thy Sun Dec 15 05:11:46 2013 +0100
@@ -90,8 +90,8 @@
method_setup S43_solve = {*
- Scan.succeed (K (SIMPLE_METHOD
- (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
+ Scan.succeed (fn ctxt => SIMPLE_METHOD
+ (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3))
*}
--- a/src/Sequents/T.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Sequents/T.thy Sun Dec 15 05:11:46 2013 +0100
@@ -42,7 +42,7 @@
)
*}
-method_setup T_solve = {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *}
+method_setup T_solve = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (T_Prover.solve_tac ctxt 2)) *}
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
--- a/src/Sequents/modal.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Sequents/modal.ML Sun Dec 15 05:11:46 2013 +0100
@@ -19,7 +19,7 @@
val rule_tac : thm list -> int ->tactic
val step_tac : int -> tactic
val solven_tac : int -> int -> tactic
- val solve_tac : int -> tactic
+ val solve_tac : Proof.context -> int -> tactic
end;
functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER =
@@ -78,7 +78,7 @@
((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND
(fres_bound_tac n THEN UPTOGOAL n (solven_tac (d-1)))));
-fun solve_tac d = rewrite_goals_tac Modal_Rule.rewrite_rls THEN solven_tac d 1;
+fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac d 1;
fun step_tac n =
COND (has_fewer_prems 1) all_tac
--- a/src/Tools/atomize_elim.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/atomize_elim.ML Sun Dec 15 05:11:46 2013 +0100
@@ -59,8 +59,8 @@
(EX x y z. ...) | ... | (EX a b c. ...)
*)
fun atomize_elim_conv ctxt ct =
- (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
- then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
+ (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
+ then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt)
then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
then all_conv ct'
else raise CTERM ("atomize_elim", [ct', ct])))
--- a/src/Tools/case_product.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/case_product.ML Sun Dec 15 05:11:46 2013 +0100
@@ -65,14 +65,14 @@
(concl, prems)
end
-fun case_product_tac prems struc thm1 thm2 =
+fun case_product_tac ctxt prems struc thm1 thm2 =
let
val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
val thm2' = thm2 OF p_cons2
in
rtac (thm1 OF p_cons1)
THEN' EVERY' (map (fn p =>
- rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
+ rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
end
fun combine ctxt thm1 thm2 =
@@ -80,8 +80,9 @@
val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
in
- Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
- case_product_tac prems prems_rich i_thm1 i_thm2 1)
+ Goal.prove ctxt' [] (flat prems_rich) concl
+ (fn {context = ctxt'', prems} =>
+ case_product_tac ctxt'' prems prems_rich i_thm1 i_thm2 1)
|> singleton (Variable.export ctxt' ctxt)
end
--- a/src/Tools/coherent.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/coherent.ML Sun Dec 15 05:11:46 2013 +0100
@@ -41,14 +41,14 @@
val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
-fun rulify_elim_conv ct =
+fun rulify_elim_conv ctxt ct =
if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct
else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct)))
(Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
- Raw_Simplifier.rewrite true (map Thm.symmetric
+ Raw_Simplifier.rewrite ctxt true (map Thm.symmetric
[Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
-fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
+fun rulify_elim ctxt th = Simplifier.norm_hhf (Conv.fconv_rule (rulify_elim_conv ctxt) th);
(* Decompose elimination rule of the form
A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
@@ -66,9 +66,9 @@
(map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
end;
-fun mk_rule th =
+fun mk_rule ctxt th =
let
- val th' = rulify_elim th;
+ val th' = rulify_elim ctxt th;
val (prems, cases) = dest_elim (prop_of th')
in (th', prems, cases) end;
@@ -208,19 +208,19 @@
(** external interface **)
-fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
- rtac (rulify_elim_conv concl RS Drule.equal_elim_rule2) 1 THEN
- SUBPROOF (fn {prems = prems', concl, context, ...} =>
+fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
+ rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
+ SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
let val xs = map (term_of o #2) params @
- map (fn (_, s) => Free (s, the (Variable.default_type context s)))
- (rev (Variable.dest_fixes context)) (* FIXME !? *)
+ map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
+ (rev (Variable.dest_fixes ctxt'')) (* FIXME !? *)
in
- case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
+ case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
(mk_dom xs) Net.empty 0 0 of
NONE => no_tac
| SOME prf =>
- rtac (thm_of_cl_prf (Proof_Context.theory_of context) concl [] prf) 1
- end) context 1) ctxt;
+ rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1
+ end) ctxt' 1) ctxt;
val setup = Method.setup @{binding coherent}
(Attrib.thms >> (fn rules => fn ctxt =>
--- a/src/Tools/eqsubst.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/eqsubst.ML Sun Dec 15 05:11:46 2013 +0100
@@ -328,7 +328,7 @@
val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
val preelimrule =
RW_Inst.rw ctxt m rule pth
- |> (Seq.hd o prune_params_tac)
+ |> (Seq.hd o prune_params_tac ctxt)
|> Thm.permute_prems 0 ~1 (* put old asm first *)
|> unfix_frees cfvs (* unfix any global params *)
|> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
--- a/src/Tools/induct.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/induct.ML Sun Dec 15 05:11:46 2013 +0100
@@ -60,16 +60,16 @@
val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
(term option list * thm list) * Proof.context
val atomize_term: theory -> term -> term
- val atomize_cterm: conv
- val atomize_tac: int -> tactic
- val inner_atomize_tac: int -> tactic
+ val atomize_cterm: Proof.context -> conv
+ val atomize_tac: Proof.context -> int -> tactic
+ val inner_atomize_tac: Proof.context -> int -> tactic
val rulified_term: thm -> theory * term
- val rulify_tac: int -> tactic
+ val rulify_tac: Proof.context -> int -> tactic
val simplified_rule: Proof.context -> thm -> thm
val simplify_tac: Proof.context -> int -> tactic
val trivial_tac: int -> tactic
val rotate_tac: int -> int -> int -> tactic
- val internalize: int -> thm -> thm
+ val internalize: Proof.context -> int -> thm -> thm
val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
thm list -> int -> cases_tactic
@@ -433,10 +433,10 @@
fun mark_constraints n ctxt = Conv.fconv_rule
(Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
- (Raw_Simplifier.rewrite false [equal_def']))) ctxt));
+ (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
-val unmark_constraints = Conv.fconv_rule
- (Raw_Simplifier.rewrite true [Induct_Args.equal_def]);
+fun unmark_constraints ctxt =
+ Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
(* simplify *)
@@ -504,11 +504,11 @@
in
fn i => fn st =>
ruleq
- |> Seq.maps (Rule_Cases.consume [] facts)
+ |> Seq.maps (Rule_Cases.consume ctxt [] facts)
|> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
let
val rule' = rule
- |> simp ? (simplified_rule' ctxt #> unmark_constraints);
+ |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
in
CASES (Rule_Cases.make_common (thy,
Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
@@ -532,12 +532,12 @@
Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
#> Object_Logic.drop_judgment thy;
-val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
+fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
-val atomize_tac = rewrite_goal_tac Induct_Args.atomize;
+fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
-val inner_atomize_tac =
- rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
+fun inner_atomize_tac ctxt =
+ rewrite_goal_tac ctxt (map Thm.symmetric conjunction_congs) THEN' atomize_tac ctxt;
(* rulify *)
@@ -553,11 +553,11 @@
val (As, B) = Logic.strip_horn (Thm.prop_of thm);
in (thy, Logic.list_implies (map rulify As, rulify B)) end;
-val rulify_tac =
- rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
- rewrite_goal_tac Induct_Args.rulify_fallback THEN'
+fun rulify_tac ctxt =
+ rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
+ rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
Goal.conjunction_tac THEN_ALL_NEW
- (rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
+ (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
(* prepare rule *)
@@ -565,9 +565,9 @@
fun rule_instance ctxt inst rule =
Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
-fun internalize k th =
+fun internalize ctxt k th =
th |> Thm.permute_prems 0 k
- |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
+ |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) (atomize_cterm ctxt));
(* guess rule instantiation -- cannot handle pending goal parameters *)
@@ -683,8 +683,10 @@
| NONE => all_tac)
end);
-fun miniscope_tac p = CONVERSION o
- Conv.params_conv p (K (Raw_Simplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
+fun miniscope_tac p =
+ CONVERSION o
+ Conv.params_conv p (fn ctxt =>
+ Raw_Simplifier.rewrite ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
in
@@ -743,7 +745,7 @@
val thy = Proof_Context.theory_of ctxt;
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
- val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs;
+ val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
fun inst_rule (concls, r) =
(if null insts then `Rule_Cases.get r
@@ -774,7 +776,7 @@
in
(fn i => fn st =>
ruleq
- |> Seq.maps (Rule_Cases.consume (flat defs) facts)
+ |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
|> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
(CONJUNCTS (ALLGOALS
@@ -791,9 +793,9 @@
else
arbitrary_tac defs_ctxt k xs)
end)
- THEN' inner_atomize_tac) j))
- THEN' atomize_tac) i st |> Seq.maps (fn st' =>
- guess_instance ctxt (internalize more_consumes rule) i st'
+ THEN' inner_atomize_tac defs_ctxt) j))
+ THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
+ guess_instance ctxt (internalize ctxt more_consumes rule) i st'
|> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
CASES (rule_cases ctxt rule' cases)
@@ -802,7 +804,7 @@
THEN_ALL_NEW_CASES
((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
else K all_tac)
- THEN_ALL_NEW rulify_tac)
+ THEN_ALL_NEW rulify_tac ctxt)
end;
val induct_tac = gen_induct_tac (K I);
@@ -849,7 +851,7 @@
in
SUBGOAL_CASES (fn (goal, i) => fn st =>
ruleq goal
- |> Seq.maps (Rule_Cases.consume [] facts)
+ |> Seq.maps (Rule_Cases.consume ctxt [] facts)
|> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
guess_instance ctxt rule i st
|> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
--- a/src/Tools/induct_tacs.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/induct_tacs.ML Sun Dec 15 05:11:46 2013 +0100
@@ -98,7 +98,7 @@
(_, rule) :: _ => rule
| [] => raise THM ("No induction rules", 0, [])));
- val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
+ val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 (Object_Logic.atomize ctxt));
val _ = Method.trace ctxt [rule'];
val concls = Logic.dest_conjunctions (Thm.concl_of rule);
--- a/src/Tools/intuitionistic.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/Tools/intuitionistic.ML Sun Dec 15 05:11:46 2013 +0100
@@ -89,7 +89,7 @@
Method.setup name
(Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
(fn opt_lim => fn ctxt =>
- SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
+ SIMPLE_METHOD' (Object_Logic.atomize_prems_tac ctxt THEN' prover_tac ctxt opt_lim)))
"intuitionistic proof search";
end;
--- a/src/ZF/Tools/cartprod.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/cartprod.ML Sun Dec 15 05:11:46 2013 +0100
@@ -51,9 +51,9 @@
val mk_prod : typ * typ -> typ
val mk_tuple : term -> typ -> term list -> term
val pseudo_type : term -> typ
- val remove_split : thm -> thm
+ val remove_split : Proof.context -> thm -> thm
val split_const : typ -> term
- val split_rule_var : term * typ * thm -> thm
+ val split_rule_var : Proof.context -> term * typ * thm -> thm
end;
@@ -100,18 +100,18 @@
| mk_tuple pair T (t::_) = t;
(*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [Pr.split_eq];
+fun remove_split ctxt = rewrite_rule ctxt [Pr.split_eq];
(*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
-fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
+fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) =
let val T' = factors T1 ---> T2
val newt = ap_split T1 T2 (Var(v,T'))
val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
in
- remove_split (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
+ remove_split ctxt (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
cterm newt)]) rl)
end
- | split_rule_var (t,T,rl) = rl;
+ | split_rule_var _ (t,T,rl) = rl;
end;
--- a/src/ZF/Tools/datatype_package.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/datatype_package.ML Sun Dec 15 05:11:46 2013 +0100
@@ -288,8 +288,8 @@
Goal.prove_global thy1 [] []
(Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
(*Proves a single case equation. Could use simp_tac, but it's slower!*)
- (fn _ => EVERY
- [rewrite_goals_tac [con_def],
+ (fn {context = ctxt, ...} => EVERY
+ [rewrite_goals_tac ctxt [con_def],
rtac case_trans 1,
REPEAT
(resolve_tac [@{thm refl}, split_trans,
@@ -353,9 +353,9 @@
val ctxt = Proof_Context.init_global thy;
in
Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
- (fn _ => EVERY
- [rewrite_goals_tac con_defs,
- fast_tac (put_claset ZF_cs ctxt addSEs free_SEs @ Su.free_SEs) 1])
+ (fn {context = ctxt', ...} => EVERY
+ [rewrite_goals_tac ctxt' con_defs,
+ fast_tac (put_claset ZF_cs ctxt' addSEs free_SEs @ Su.free_SEs) 1])
end;
val simps = case_eqns @ recursor_eqns;
--- a/src/ZF/Tools/ind_cases.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/ind_cases.ML Sun Dec 15 05:11:46 2013 +0100
@@ -58,7 +58,7 @@
val setup =
Method.setup @{binding "ind_cases"}
(Scan.lift (Scan.repeat1 Args.name_source) >>
- (fn props => fn ctxt => Method.erule 0 (map (smart_cases ctxt) props)))
+ (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
"dynamic case analysis on sets";
--- a/src/ZF/Tools/inductive_package.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/inductive_package.ML Sun Dec 15 05:11:46 2013 +0100
@@ -214,7 +214,7 @@
(*Type-checking is hardest aspect of proof;
disjIn selects the correct disjunct after unfolding*)
- fun intro_tacsf disjIn =
+ fun intro_tacsf disjIn ctxt =
[DETERM (stac unfold 1),
REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
(*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
@@ -223,7 +223,7 @@
backtracking may occur if the premises have extra variables!*)
DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
- rewrite_goals_tac con_defs,
+ rewrite_goals_tac ctxt con_defs,
REPEAT (rtac @{thm refl} 2),
(*Typechecking; this can fail*)
if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
@@ -246,7 +246,7 @@
(intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
|> ListPair.map (fn (t, tacs) =>
Goal.prove_global thy1 [] [] t
- (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
+ (fn {context = ctxt, ...} => EVERY (rewrite_goals_tac ctxt part_rec_defs :: tacs ctxt)));
(********)
val dummy = writeln " Proving the elimination rule...";
@@ -255,9 +255,9 @@
fun basic_elim_tac ctxt =
REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
ORELSE' bound_hyp_subst_tac ctxt))
- THEN prune_params_tac
+ THEN prune_params_tac ctxt
(*Mutual recursion: collapse references to Part(D,h)*)
- THEN (PRIMITIVE (fold_rule part_rec_defs));
+ THEN (PRIMITIVE (fold_rule ctxt part_rec_defs));
(*Elimination*)
val elim =
@@ -337,8 +337,8 @@
val quant_induct =
Goal.prove_global thy1 [] ind_prems
(FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
- (fn {prems, ...} => EVERY
- [rewrite_goals_tac part_rec_defs,
+ (fn {context = ctxt, prems} => EVERY
+ [rewrite_goals_tac ctxt part_rec_defs,
rtac (@{thm impI} RS @{thm allI}) 1,
DETERM (etac raw_induct 1),
(*Push Part inside Collect*)
@@ -349,7 +349,7 @@
some premise involves disjunction.*)
REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
ORELSE' (bound_hyp_subst_tac ctxt1))),
- ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
+ ind_tac (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
val dummy =
if ! Ind_Syntax.trace then
@@ -422,9 +422,9 @@
(writeln " Proving the mutual induction rule...";
Goal.prove_global thy1 [] []
(Logic.mk_implies (induct_concl, mutual_induct_concl))
- (fn _ => EVERY
- [rewrite_goals_tac part_rec_defs,
- REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
+ (fn {context = ctxt, ...} => EVERY
+ [rewrite_goals_tac ctxt part_rec_defs,
+ REPEAT (rewrite_goals_tac ctxt [Pr.split_eq] THEN lemma_tac 1)]))
else (writeln " [ No mutual induction rule needed ]"; @{thm TrueI});
val dummy =
@@ -452,15 +452,15 @@
RLN (2,[@{thm rev_subsetD}]);
(*Minimizes backtracking by delivering the correct premise to each goal*)
- fun mutual_ind_tac [] 0 = all_tac
- | mutual_ind_tac(prem::prems) i =
+ fun mutual_ind_tac _ [] 0 = all_tac
+ | mutual_ind_tac ctxt (prem::prems) i =
DETERM
(SELECT_GOAL
(
(*Simplify the assumptions and goal by unfolding Part and
using freeness of the Sum constructors; proves all but one
conjunct by contradiction*)
- rewrite_goals_tac all_defs THEN
+ rewrite_goals_tac ctxt all_defs THEN
simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1 THEN
IF_UNSOLVED (*simp_tac may have finished it off!*)
((*simplify assumptions*)
@@ -471,20 +471,20 @@
THEN
(*unpackage and use "prem" in the corresponding place*)
REPEAT (rtac @{thm impI} 1) THEN
- rtac (rewrite_rule all_defs prem) 1 THEN
+ rtac (rewrite_rule ctxt all_defs prem) 1 THEN
(*prem must not be REPEATed below: could loop!*)
DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
) i)
- THEN mutual_ind_tac prems (i-1);
+ THEN mutual_ind_tac ctxt prems (i-1);
val mutual_induct_fsplit =
if need_mutual then
Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
mutual_induct_concl
- (fn {prems, ...} => EVERY
+ (fn {context = ctxt, prems} => EVERY
[rtac (quant_induct RS lemma) 1,
- mutual_ind_tac (rev prems) (length prems)])
+ mutual_ind_tac ctxt (rev prems) (length prems)])
else @{thm TrueI};
(** Uncurrying the predicate in the ordinary induction rule **)
@@ -502,9 +502,11 @@
val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
- val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
- |> Drule.export_without_context
- and mutual_induct = CP.remove_split mutual_induct_fsplit
+ val induct =
+ CP.split_rule_var (Proof_Context.init_global thy)
+ (pred_var, elem_type-->FOLogic.oT, induct0)
+ |> Drule.export_without_context
+ and mutual_induct = CP.remove_split (Proof_Context.init_global thy) mutual_induct_fsplit
val ([induct', mutual_induct'], thy') =
thy
--- a/src/ZF/Tools/primrec_package.ML Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/Tools/primrec_package.ML Sun Dec 15 05:11:46 2013 +0100
@@ -176,7 +176,7 @@
val eqn_thms =
eqn_terms |> map (fn t =>
Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
- (fn _ => EVERY [rewrite_goals_tac rewrites, rtac @{thm refl} 1]));
+ (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
val (eqn_thms', thy2) =
thy1
--- a/src/ZF/UNITY/Constrains.thy Sat Dec 14 07:45:30 2013 +0800
+++ b/src/ZF/UNITY/Constrains.thy Sun Dec 15 05:11:46 2013 +0100
@@ -479,7 +479,7 @@
@{thm constrains_imp_Constrains}] 1),
rtac @{thm constrainsI} 1,
(* Three subgoals *)
- rewrite_goal_tac [@{thm st_set_def}] 3,
+ rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
REPEAT (force_tac ctxt 2),
full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1,
ALLGOALS (clarify_tac ctxt),