proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
1.1 --- a/NEWS Fri Dec 13 23:53:02 2013 +0100
1.2 +++ b/NEWS Sat Dec 14 17:28:05 2013 +0100
1.3 @@ -115,6 +115,11 @@
1.4 Note that 'ML_file' is the canonical command to load ML files into the
1.5 formal context.
1.6
1.7 +* Proper context for basic Simplifier operations: rewrite_rule,
1.8 +rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
1.9 +pass runtime Proof.context (and ensure that the simplified entity
1.10 +actually belongs to it).
1.11 +
1.12
1.13 *** System ***
1.14
2.1 --- a/src/CCL/CCL.thy Fri Dec 13 23:53:02 2013 +0100
2.2 +++ b/src/CCL/CCL.thy Sat Dec 14 17:28:05 2013 +0100
2.3 @@ -280,7 +280,7 @@
2.4 fun mk_dstnct_thm rls s =
2.5 Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
2.6 (fn _ =>
2.7 - rewrite_goals_tac defs THEN
2.8 + rewrite_goals_tac ctxt defs THEN
2.9 simp_tac (ctxt addsimps (rls @ inj_rls)) 1)
2.10 in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
2.11
3.1 --- a/src/Doc/IsarImplementation/Eq.thy Fri Dec 13 23:53:02 2013 +0100
3.2 +++ b/src/Doc/IsarImplementation/Eq.thy Sat Dec 14 17:28:05 2013 +0100
3.3 @@ -91,30 +91,30 @@
3.4
3.5 text %mlref {*
3.6 \begin{mldecls}
3.7 - @{index_ML rewrite_rule: "thm list -> thm -> thm"} \\
3.8 - @{index_ML rewrite_goals_rule: "thm list -> thm -> thm"} \\
3.9 - @{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\
3.10 - @{index_ML rewrite_goals_tac: "thm list -> tactic"} \\
3.11 - @{index_ML fold_goals_tac: "thm list -> tactic"} \\
3.12 + @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
3.13 + @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
3.14 + @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
3.15 + @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
3.16 + @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
3.17 \end{mldecls}
3.18
3.19 \begin{description}
3.20
3.21 - \item @{ML rewrite_rule}~@{text "rules thm"} rewrites the whole
3.22 + \item @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole
3.23 theorem by the given rules.
3.24
3.25 - \item @{ML rewrite_goals_rule}~@{text "rules thm"} rewrites the
3.26 + \item @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the
3.27 outer premises of the given theorem. Interpreting the same as a
3.28 goal state (\secref{sec:tactical-goals}) it means to rewrite all
3.29 subgoals (in the same manner as @{ML rewrite_goals_tac}).
3.30
3.31 - \item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal
3.32 + \item @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal
3.33 @{text "i"} by the given rewrite rules.
3.34
3.35 - \item @{ML rewrite_goals_tac}~@{text "rules"} rewrites all subgoals
3.36 + \item @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals
3.37 by the given rewrite rules.
3.38
3.39 - \item @{ML fold_goals_tac}~@{text "rules"} essentially uses @{ML
3.40 + \item @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML
3.41 rewrite_goals_tac} with the symmetric form of each member of @{text
3.42 "rules"}, re-ordered to fold longer expression first. This supports
3.43 to idea to fold primitive definitions that appear in expended form
4.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Dec 13 23:53:02 2013 +0100
4.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Sat Dec 14 17:28:05 2013 +0100
4.3 @@ -590,10 +590,10 @@
4.4 fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
4.5 val expand_rels =
4.6 fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
4.7 - val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
4.8 - val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
4.9 - val unfold_rels = unfold_thms lthy rel_unfolds;
4.10 - val unfold_all = unfold_sets o unfold_maps o unfold_rels;
4.11 + fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
4.12 + fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
4.13 + fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
4.14 + fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
4.15 val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
4.16 val bnf_sets = map (expand_maps o expand_sets)
4.17 (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
4.18 @@ -627,7 +627,7 @@
4.19 map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
4.20
4.21 fun mk_tac thm {context = ctxt, prems = _} =
4.22 - (rtac (unfold_all thm) THEN'
4.23 + (rtac (unfold_all ctxt thm) THEN'
4.24 SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
4.25
4.26 val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
4.27 @@ -638,7 +638,8 @@
4.28
4.29 val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
4.30
4.31 - fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
4.32 + fun wit_tac {context = ctxt, prems = _} =
4.33 + mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
4.34
4.35 val (bnf', lthy') =
4.36 bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
5.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Fri Dec 13 23:53:02 2013 +0100
5.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Sat Dec 14 17:28:05 2013 +0100
5.3 @@ -130,7 +130,7 @@
5.4 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN
5.5 EVERY [REPEAT_DETERM_N r
5.6 (HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
5.7 - if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, HEADGOAL atac,
5.8 + if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac,
5.9 mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs]
5.10 end;
5.11
6.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML Fri Dec 13 23:53:02 2013 +0100
6.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML Sat Dec 14 17:28:05 2013 +0100
6.3 @@ -168,7 +168,7 @@
6.4 cterm_instantiate_pos cts rel_xtor_co_induct_thm
6.5 |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
6.6 |> funpow (2 * n) (fn thm => thm RS spec)
6.7 - |> Conv.fconv_rule Object_Logic.atomize
6.8 + |> Conv.fconv_rule (Object_Logic.atomize lthy)
6.9 |> funpow n (fn thm => thm RS mp)
6.10 end);
6.11
7.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Dec 13 23:53:02 2013 +0100
7.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sat Dec 14 17:28:05 2013 +0100
7.3 @@ -567,7 +567,7 @@
7.4 EVERY' [rtac allI, fo_rtac induct ctxt,
7.5 select_prem_tac n (dtac @{thm meta_spec2}) i,
7.6 REPEAT_DETERM_N n o
7.7 - EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac,
7.8 + EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt,
7.9 REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac],
7.10 atac];
7.11 in
8.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML Fri Dec 13 23:53:02 2013 +0100
8.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Sat Dec 14 17:28:05 2013 +0100
8.3 @@ -45,7 +45,7 @@
8.4 rtac (Drule.instantiate_normalize insts thm) 1
8.5 end);
8.6
8.7 -fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
8.8 +fun mk_unfold_thms_then_tac ctxt defs tac x = unfold_thms_tac ctxt defs THEN tac x;
8.9
8.10 (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
8.11 fun mk_pointfree ctxt thm = thm
9.1 --- a/src/HOL/Bali/Example.thy Fri Dec 13 23:53:02 2013 +0100
9.2 +++ b/src/HOL/Bali/Example.thy Sat Dec 14 17:28:05 2013 +0100
9.3 @@ -894,7 +894,7 @@
9.4
9.5 declare member_is_static_simp [simp]
9.6 declare wt.Skip [rule del] wt.Init [rule del]
9.7 -ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
9.8 +ML {* bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
9.9 lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
9.10 lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
9.11
9.12 @@ -1189,7 +1189,7 @@
9.13
9.14 ML {* bind_thms ("eval_intros", map
9.15 (simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o
9.16 - rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
9.17 + rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
9.18 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
9.19
9.20 axiomatization
10.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Dec 13 23:53:02 2013 +0100
10.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Dec 14 17:28:05 2013 +0100
10.3 @@ -2920,7 +2920,7 @@
10.4 struct
10.5
10.6 fun tactic ctxt alternative T ps =
10.7 - Object_Logic.full_atomize_tac
10.8 + Object_Logic.full_atomize_tac ctxt
10.9 THEN' CSUBGOAL (fn (g, i) =>
10.10 let
10.11 val th = frpar_oracle (ctxt, alternative, T, ps, g)
11.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Dec 13 23:53:02 2013 +0100
11.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Dec 14 17:28:05 2013 +0100
11.3 @@ -62,7 +62,7 @@
11.4 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
11.5
11.6
11.7 -fun linz_tac ctxt q = Object_Logic.atomize_prems_tac THEN' SUBGOAL (fn (g, i) =>
11.8 +fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) =>
11.9 let
11.10 val thy = Proof_Context.theory_of ctxt
11.11 (* Transform the term*)
12.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Dec 13 23:53:02 2013 +0100
12.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sat Dec 14 17:28:05 2013 +0100
12.3 @@ -66,7 +66,7 @@
12.4
12.5
12.6 fun linr_tac ctxt q =
12.7 - Object_Logic.atomize_prems_tac
12.8 + Object_Logic.atomize_prems_tac ctxt
12.9 THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
12.10 THEN' SUBGOAL (fn (g, i) =>
12.11 let
13.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Dec 13 23:53:02 2013 +0100
13.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sat Dec 14 17:28:05 2013 +0100
13.3 @@ -224,7 +224,7 @@
13.4 (case dlo_instance ctxt p of
13.5 NONE => no_tac
13.6 | SOME instance =>
13.7 - Object_Logic.full_atomize_tac i THEN
13.8 + Object_Logic.full_atomize_tac ctxt i THEN
13.9 simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN (* FIXME already part of raw_ferrack_qe_conv? *)
13.10 CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
13.11 simp_tac ctxt i)); (* FIXME really? *)
14.1 --- a/src/HOL/Decision_Procs/langford.ML Fri Dec 13 23:53:02 2013 +0100
14.2 +++ b/src/HOL/Decision_Procs/langford.ML Sat Dec 14 17:28:05 2013 +0100
14.3 @@ -237,11 +237,11 @@
14.4 (case dlo_instance ctxt p of
14.5 (ss, NONE) => simp_tac (put_simpset ss ctxt) i
14.6 | (ss, SOME instance) =>
14.7 - Object_Logic.full_atomize_tac i THEN
14.8 + Object_Logic.full_atomize_tac ctxt i THEN
14.9 simp_tac (put_simpset ss ctxt) i
14.10 THEN (CONVERSION Thm.eta_long_conversion) i
14.11 THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
14.12 - THEN Object_Logic.full_atomize_tac i
14.13 + THEN Object_Logic.full_atomize_tac ctxt i
14.14 THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ctxt ss instance)) i
14.15 THEN (simp_tac (put_simpset ss ctxt) i)));
14.16 end;
14.17 \ No newline at end of file
15.1 --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Dec 13 23:53:02 2013 +0100
15.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Dec 14 17:28:05 2013 +0100
15.3 @@ -82,7 +82,7 @@
15.4
15.5
15.6 fun mir_tac ctxt q =
15.7 - Object_Logic.atomize_prems_tac
15.8 + Object_Logic.atomize_prems_tac ctxt
15.9 THEN' simp_tac (put_simpset HOL_basic_ss ctxt
15.10 addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
15.11 THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
16.1 --- a/src/HOL/HOL.thy Fri Dec 13 23:53:02 2013 +0100
16.2 +++ b/src/HOL/HOL.thy Sat Dec 14 17:28:05 2013 +0100
16.3 @@ -1496,8 +1496,9 @@
16.4 | is_conj _ = false
16.5 in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
16.6 | _ => NONE))]
16.7 - |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
16.8 - map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback})))))
16.9 + |> Simplifier.set_mksimps (fn ctxt =>
16.10 + Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
16.11 + map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
16.12 *}
16.13
16.14 text {* Pre-simplification of induction and cases rules *}
17.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Fri Dec 13 23:53:02 2013 +0100
17.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Sat Dec 14 17:28:05 2013 +0100
17.3 @@ -208,29 +208,29 @@
17.4 txt {* 10 - 7 *}
17.5 apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
17.6 txt {* 6 *}
17.7 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
17.8 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
17.9 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
17.10
17.11 txt {* 6 - 5 *}
17.12 apply (tactic "EVERY1 [tac2,tac2]")
17.13
17.14 txt {* 4 *}
17.15 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
17.16 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
17.17 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
17.18 apply (tactic "tac2 1")
17.19
17.20 txt {* 3 *}
17.21 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
17.22 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
17.23 (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
17.24
17.25 apply (tactic "tac2 1")
17.26 - apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
17.27 + apply (tactic {* fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
17.28 (@{thm Impl.hdr_sum_def})] *})
17.29 apply arith
17.30
17.31 txt {* 2 *}
17.32 apply (tactic "tac2 1")
17.33 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
17.34 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
17.35 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
17.36 apply (intro strip)
17.37 apply (erule conjE)+
17.38 @@ -238,11 +238,12 @@
17.39
17.40 txt {* 1 *}
17.41 apply (tactic "tac2 1")
17.42 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
17.43 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
17.44 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
17.45 apply (intro strip)
17.46 apply (erule conjE)+
17.47 - apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
17.48 + apply (tactic {* fold_goals_tac @{context}
17.49 + [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
17.50 apply simp
17.51
17.52 done
17.53 @@ -286,13 +287,13 @@
17.54 apply (intro strip, (erule conjE)+)
17.55 apply (rule imp_disjL [THEN iffD1])
17.56 apply (rule impI)
17.57 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
17.58 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
17.59 (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
17.60 apply simp
17.61 apply (erule conjE)+
17.62 apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
17.63 k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
17.64 - apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
17.65 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm inv1_def}]
17.66 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
17.67 apply (simp add: hdr_sum_def Multiset.count_def)
17.68 apply (rule add_le_mono)
17.69 @@ -307,7 +308,7 @@
17.70 apply (intro strip, (erule conjE)+)
17.71 apply (rule imp_disjL [THEN iffD1])
17.72 apply (rule impI)
17.73 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
17.74 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
17.75 (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
17.76 apply simp
17.77 done
17.78 @@ -333,7 +334,7 @@
17.79 txt {* 2 b *}
17.80
17.81 apply (intro strip, (erule conjE)+)
17.82 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
17.83 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
17.84 (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
17.85 apply simp
17.86
17.87 @@ -341,9 +342,9 @@
17.88 apply (tactic "tac4 1")
17.89 apply (intro strip, (erule conjE)+)
17.90 apply (rule ccontr)
17.91 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
17.92 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
17.93 (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
17.94 - apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
17.95 + apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
17.96 (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
17.97 apply simp
17.98 apply (erule_tac x = "m" in allE)
18.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Dec 13 23:53:02 2013 +0100
18.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sat Dec 14 17:28:05 2013 +0100
18.3 @@ -101,8 +101,8 @@
18.4 : thm =
18.5 let
18.6 fun tac {prems, context} =
18.7 - rewrite_goals_tac defs THEN
18.8 - EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
18.9 + rewrite_goals_tac context defs THEN
18.10 + EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
18.11 in
18.12 Goal.prove_global thy [] [] goal tac
18.13 end
18.14 @@ -213,8 +213,10 @@
18.15 in (n2, mk_ssumT (t1, t2)) end
18.16 val ct = ctyp_of thy (snd (cons2typ 1 spec'))
18.17 val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
18.18 - val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
18.19 - val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2
18.20 + val thm2 = rewrite_rule (Proof_Context.init_global thy)
18.21 + (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
18.22 + val thm3 = rewrite_rule (Proof_Context.init_global thy)
18.23 + [mk_meta_eq @{thm conj_assoc}] thm2
18.24
18.25 val y = Free ("y", lhsT)
18.26 fun one_con (con, args) =
18.27 @@ -225,15 +227,15 @@
18.28 in Library.foldr mk_ex (vs, conj) end
18.29 val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
18.30 (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
18.31 - val tacs = [
18.32 + fun tacs {context = ctxt, prems} = [
18.33 rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
18.34 - rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
18.35 + rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
18.36 rtac thm3 1]
18.37 in
18.38 - val nchotomy = prove thy con_betas goal (K tacs)
18.39 + val nchotomy = prove thy con_betas goal tacs
18.40 val exhaust =
18.41 (nchotomy RS @{thm exh_casedist0})
18.42 - |> rewrite_rule @{thms exh_casedists}
18.43 + |> rewrite_rule (Proof_Context.init_global thy) @{thms exh_casedists}
18.44 |> Drule.zero_var_indexes
18.45 end
18.46
19.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Dec 13 23:53:02 2013 +0100
19.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Dec 14 17:28:05 2013 +0100
19.3 @@ -161,12 +161,12 @@
19.4 val simplify = asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules)
19.5 fun arg_tac (lazy, _) =
19.6 rtac (if lazy then allI else case_UU_allI) 1
19.7 - val tacs =
19.8 - rewrite_goals_tac @{thms atomize_all atomize_imp} ::
19.9 + fun tacs ctxt =
19.10 + rewrite_goals_tac ctxt @{thms atomize_all atomize_imp} ::
19.11 map arg_tac args @
19.12 [REPEAT (rtac impI 1), ALLGOALS simplify]
19.13 in
19.14 - Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
19.15 + Goal.prove ctxt [] [] subgoal (EVERY o tacs o #context)
19.16 end
19.17 fun eq_thms (p, cons) = map (con_thm p) cons
19.18 val conss = map #con_specs constr_infos
19.19 @@ -321,7 +321,7 @@
19.20 val rules = @{thm Rep_cfun_strict1} :: take_0_thms
19.21 fun tacf {prems, context = ctxt} =
19.22 let
19.23 - val prem' = rewrite_rule [bisim_def_thm] (hd prems)
19.24 + val prem' = rewrite_rule ctxt [bisim_def_thm] (hd prems)
19.25 val prems' = Project_Rule.projections ctxt prem'
19.26 val dests = map (fn th => th RS spec RS spec RS mp) prems'
19.27 fun one_tac (dest, rews) =
20.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Dec 13 23:53:02 2013 +0100
20.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Dec 14 17:28:05 2013 +0100
20.3 @@ -157,10 +157,10 @@
20.4 (* prove applied version of definitions *)
20.5 fun prove_proj (lhs, rhs) =
20.6 let
20.7 - val tac = rewrite_goals_tac fixdef_thms THEN
20.8 + fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN
20.9 (simp_tac (Simplifier.global_context thy beta_ss)) 1
20.10 val goal = Logic.mk_equals (lhs, rhs)
20.11 - in Goal.prove_global thy [] [] goal (K tac) end
20.12 + in Goal.prove_global thy [] [] goal (tac o #context) end
20.13 val proj_thms = map prove_proj projs
20.14
20.15 (* mk_tuple lhss == fixpoint *)
20.16 @@ -328,7 +328,7 @@
20.17 in
20.18 Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
20.19 EVERY
20.20 - [rewrite_goals_tac map_apply_thms,
20.21 + [rewrite_goals_tac ctxt map_apply_thms,
20.22 rtac (map_cont_thm RS @{thm cont_fix_ind}) 1,
20.23 REPEAT (resolve_tac adm_rules 1),
20.24 simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
20.25 @@ -533,11 +533,11 @@
20.26 let
20.27 val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
20.28 val DEFL_simps = RepData.get (Proof_Context.init_global thy)
20.29 - val tac =
20.30 - rewrite_goals_tac (map mk_meta_eq DEFL_simps)
20.31 + fun tac ctxt =
20.32 + rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
20.33 THEN TRY (resolve_tac defl_unfold_thms 1)
20.34 in
20.35 - Goal.prove_global thy [] [] goal (K tac)
20.36 + Goal.prove_global thy [] [] goal (tac o #context)
20.37 end
20.38 val DEFL_eq_thms = map mk_DEFL_eq_thm dom_eqns
20.39
20.40 @@ -641,7 +641,7 @@
20.41 in
20.42 Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
20.43 EVERY
20.44 - [rewrite_goals_tac (defl_apply_thms @ map_apply_thms),
20.45 + [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms),
20.46 rtac (@{thm cont_parallel_fix_ind}
20.47 OF [defl_cont_thm, map_cont_thm]) 1,
20.48 REPEAT (resolve_tac adm_rules 1),
21.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Dec 13 23:53:02 2013 +0100
21.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Dec 14 17:28:05 2013 +0100
21.3 @@ -470,15 +470,15 @@
21.4 fun prove_finite_thm (absT, finite_const) =
21.5 let
21.6 val goal = mk_trp (finite_const $ Free ("x", absT))
21.7 - val tac =
21.8 + fun tac ctxt =
21.9 EVERY [
21.10 - rewrite_goals_tac finite_defs,
21.11 + rewrite_goals_tac ctxt finite_defs,
21.12 rtac @{thm lub_ID_finite} 1,
21.13 resolve_tac chain_take_thms 1,
21.14 resolve_tac lub_take_thms 1,
21.15 resolve_tac decisive_thms 1]
21.16 in
21.17 - Goal.prove_global thy [] [] goal (K tac)
21.18 + Goal.prove_global thy [] [] goal (tac o #context)
21.19 end
21.20 val finite_thms =
21.21 map prove_finite_thm (absTs ~~ finite_consts)
22.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 13 23:53:02 2013 +0100
22.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sat Dec 14 17:28:05 2013 +0100
22.3 @@ -411,8 +411,8 @@
22.4 : thm =
22.5 let
22.6 fun tac {prems, context} =
22.7 - rewrite_goals_tac defs THEN
22.8 - EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
22.9 + rewrite_goals_tac context defs THEN
22.10 + EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
22.11 in
22.12 Goal.prove_global thy [] [] goal tac
22.13 end;
23.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Fri Dec 13 23:53:02 2013 +0100
23.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sat Dec 14 17:28:05 2013 +0100
23.3 @@ -938,7 +938,7 @@
23.4 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
23.5
23.6 fun sos_tac print_cert prover ctxt =
23.7 - Object_Logic.full_atomize_tac THEN'
23.8 + Object_Logic.full_atomize_tac ctxt THEN'
23.9 elim_denom_tac ctxt THEN'
23.10 core_sos_tac print_cert prover ctxt;
23.11
24.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy Fri Dec 13 23:53:02 2013 +0100
24.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sat Dec 14 17:28:05 2013 +0100
24.3 @@ -325,7 +325,7 @@
24.4 apply( fast intro: hext_trans)
24.5
24.6
24.7 -apply( tactic prune_params_tac)
24.8 +apply( tactic "prune_params_tac @{context}")
24.9 -- "Level 52"
24.10
24.11 -- "1 Call"
25.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML Fri Dec 13 23:53:02 2013 +0100
25.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat Dec 14 17:28:05 2013 +0100
25.3 @@ -399,7 +399,7 @@
25.4
25.5 fun norm_arith_tac ctxt =
25.6 clarify_tac (put_claset HOL_cs ctxt) THEN'
25.7 - Object_Logic.full_atomize_tac THEN'
25.8 + Object_Logic.full_atomize_tac ctxt THEN'
25.9 CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
25.10
25.11 end;
26.1 --- a/src/HOL/NSA/transfer.ML Fri Dec 13 23:53:02 2013 +0100
26.2 +++ b/src/HOL/NSA/transfer.ML Sat Dec 14 17:28:05 2013 +0100
26.3 @@ -58,11 +58,11 @@
26.4 val meta = Local_Defs.meta_rewrite_rule ctxt;
26.5 val ths' = map meta ths;
26.6 val unfolds' = map meta unfolds and refolds' = map meta refolds;
26.7 - val (_$_$t') = concl_of (Raw_Simplifier.rewrite true unfolds' (cterm_of thy t))
26.8 + val (_$_$t') = concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (cterm_of thy t))
26.9 val u = unstar_term consts t'
26.10 val tac =
26.11 - rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
26.12 - ALLGOALS Object_Logic.full_atomize_tac THEN
26.13 + rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
26.14 + ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
26.15 match_tac [transitive_thm] 1 THEN
26.16 resolve_tac [@{thm transfer_start}] 1 THEN
26.17 REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
26.18 @@ -76,7 +76,7 @@
26.19 val tr = transfer_thm_of ctxt ths t
26.20 val (_$l$r) = concl_of tr;
26.21 val trs = if l aconv r then [] else [tr];
26.22 - in rewrite_goals_tac trs th end))
26.23 + in rewrite_goals_tac ctxt trs th end))
26.24
26.25 local
26.26
27.1 --- a/src/HOL/Nat.thy Fri Dec 13 23:53:02 2013 +0100
27.2 +++ b/src/HOL/Nat.thy Sat Dec 14 17:28:05 2013 +0100
27.3 @@ -1536,19 +1536,19 @@
27.4
27.5 simproc_setup nateq_cancel_sums
27.6 ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
27.7 - {* fn phi => fn ss => try Nat_Arith.cancel_eq_conv *}
27.8 + {* fn phi => try o Nat_Arith.cancel_eq_conv *}
27.9
27.10 simproc_setup natless_cancel_sums
27.11 ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
27.12 - {* fn phi => fn ss => try Nat_Arith.cancel_less_conv *}
27.13 + {* fn phi => try o Nat_Arith.cancel_less_conv *}
27.14
27.15 simproc_setup natle_cancel_sums
27.16 ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
27.17 - {* fn phi => fn ss => try Nat_Arith.cancel_le_conv *}
27.18 + {* fn phi => try o Nat_Arith.cancel_le_conv *}
27.19
27.20 simproc_setup natdiff_cancel_sums
27.21 ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
27.22 - {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
27.23 + {* fn phi => try o Nat_Arith.cancel_diff_conv *}
27.24
27.25 ML_file "Tools/lin_arith.ML"
27.26 setup {* Lin_Arith.global_setup *}
28.1 --- a/src/HOL/Nominal/nominal_atoms.ML Fri Dec 13 23:53:02 2013 +0100
28.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Dec 14 17:28:05 2013 +0100
28.3 @@ -829,6 +829,7 @@
28.4 (* instantiations. *)
28.5 val (_, thy33) =
28.6 let
28.7 + val ctxt32 = Proof_Context.init_global thy32;
28.8
28.9 (* takes a theorem thm and a list of theorems [t1,..,tn] *)
28.10 (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *)
28.11 @@ -918,7 +919,7 @@
28.12 ||>> add_thmss_string
28.13 let
28.14 val thms1 = inst_pt_at [all_eqvt];
28.15 - val thms2 = map (fold_rule [inductive_forall_def]) thms1
28.16 + val thms2 = map (fold_rule ctxt32 [inductive_forall_def]) thms1
28.17 in
28.18 [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
28.19 end
29.1 --- a/src/HOL/Nominal/nominal_datatype.ML Fri Dec 13 23:53:02 2013 +0100
29.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Dec 14 17:28:05 2013 +0100
29.3 @@ -134,7 +134,7 @@
29.4 val at_fin_set_fresh = @{thm at_fin_set_fresh};
29.5 val abs_fun_eq1 = @{thm abs_fun_eq1};
29.6
29.7 -val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
29.8 +fun collect_simp ctxt = rewrite_rule ctxt [mk_meta_eq mem_Collect_eq];
29.9
29.10 fun mk_perm Ts t u =
29.11 let
29.12 @@ -595,10 +595,12 @@
29.13 end))
29.14 (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
29.15
29.16 + val ctxt6 = Proof_Context.init_global thy6;
29.17 +
29.18 val perm_defs = map snd typedefs;
29.19 - val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
29.20 + val Abs_inverse_thms = map (collect_simp ctxt6 o #Abs_inverse o snd o fst) typedefs;
29.21 val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
29.22 - val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
29.23 + val Rep_thms = map (collect_simp ctxt6 o #Rep o snd o fst) typedefs;
29.24
29.25
29.26 (** prove that new types are in class pt_<name> **)
29.27 @@ -616,7 +618,7 @@
29.28 (Sign.intern_type thy name,
29.29 map (inter_sort thy sort o snd) tvs, [pt_class])
29.30 (fn ctxt => EVERY [Class.intro_classes_tac [],
29.31 - rewrite_goals_tac [perm_def],
29.32 + rewrite_goals_tac ctxt [perm_def],
29.33 asm_full_simp_tac (ctxt addsimps [Rep_inverse]) 1,
29.34 asm_full_simp_tac (ctxt addsimps
29.35 [Rep RS perm_closed RS Abs_inverse]) 1,
29.36 @@ -645,7 +647,7 @@
29.37 (Sign.intern_type thy name,
29.38 map (inter_sort thy sort o snd) tvs, [cp_class])
29.39 (fn ctxt => EVERY [Class.intro_classes_tac [],
29.40 - rewrite_goals_tac [perm_def],
29.41 + rewrite_goals_tac ctxt [perm_def],
29.42 asm_full_simp_tac (ctxt addsimps
29.43 ((Rep RS perm_closed1 RS Abs_inverse) ::
29.44 (if atom1 = atom2 then []
29.45 @@ -783,7 +785,7 @@
29.46 new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
29.47 (thy7, [], [], []);
29.48
29.49 - val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
29.50 + val abs_inject_thms = map (collect_simp ctxt6 o #Abs_inject o snd o fst) typedefs
29.51 val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
29.52
29.53 (* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *)
29.54 @@ -792,9 +794,9 @@
29.55 let
29.56 val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
29.57 val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
29.58 - in Goal.prove_global_future thy8 [] [] eqn (fn _ => EVERY
29.59 + in Goal.prove_global_future thy8 [] [] eqn (fn {context = ctxt, ...} => EVERY
29.60 [resolve_tac inj_thms 1,
29.61 - rewrite_goals_tac rewrites,
29.62 + rewrite_goals_tac ctxt rewrites,
29.63 rtac refl 3,
29.64 resolve_tac rep_intrs 2,
29.65 REPEAT (resolve_tac Rep_thms 1)])
29.66 @@ -1043,7 +1045,7 @@
29.67 (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
29.68 (fn {prems, context = ctxt} => EVERY
29.69 [rtac indrule_lemma' 1,
29.70 - (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
29.71 + (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
29.72 EVERY (map (fn (prem, r) => (EVERY
29.73 [REPEAT (eresolve_tac Abs_inverse_thms' 1),
29.74 simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
29.75 @@ -2017,8 +2019,8 @@
29.76 Goal.prove_global_future thy12 []
29.77 (map (augment_sort thy12 fs_cp_sort) prems')
29.78 (augment_sort thy12 fs_cp_sort concl')
29.79 - (fn {prems, ...} => EVERY
29.80 - [rewrite_goals_tac reccomb_defs,
29.81 + (fn {context = ctxt, prems} => EVERY
29.82 + [rewrite_goals_tac ctxt reccomb_defs,
29.83 rtac @{thm the1_equality} 1,
29.84 solve rec_unique_thms prems 1,
29.85 resolve_tac rec_intrs 1,
30.1 --- a/src/HOL/Nominal/nominal_induct.ML Fri Dec 13 23:53:02 2013 +0100
30.2 +++ b/src/HOL/Nominal/nominal_induct.ML Sat Dec 14 17:28:05 2013 +0100
30.3 @@ -87,7 +87,7 @@
30.4 val cert = Thm.cterm_of thy;
30.5
30.6 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
30.7 - val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
30.8 + val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm ctxt))) defs;
30.9
30.10 val finish_rule =
30.11 split_all_tuples defs_ctxt
30.12 @@ -101,7 +101,7 @@
30.13 (fn i => fn st =>
30.14 rules
30.15 |> inst_mutual_rule ctxt insts avoiding
30.16 - |> Rule_Cases.consume (flat defs) facts
30.17 + |> Rule_Cases.consume ctxt (flat defs) facts
30.18 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
30.19 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
30.20 (CONJUNCTS (ALLGOALS
30.21 @@ -118,10 +118,10 @@
30.22 else
30.23 Induct.arbitrary_tac defs_ctxt k xs)
30.24 end)
30.25 - THEN' Induct.inner_atomize_tac) j))
30.26 - THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
30.27 + THEN' Induct.inner_atomize_tac defs_ctxt) j))
30.28 + THEN' Induct.atomize_tac ctxt) i st |> Seq.maps (fn st' =>
30.29 Induct.guess_instance ctxt
30.30 - (finish_rule (Induct.internalize more_consumes rule)) i st'
30.31 + (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
30.32 |> Seq.maps (fn rule' =>
30.33 CASES (rule_cases ctxt rule' cases)
30.34 (rtac (rename_params_rule false [] rule') i THEN
30.35 @@ -129,7 +129,7 @@
30.36 THEN_ALL_NEW_CASES
30.37 ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
30.38 else K all_tac)
30.39 - THEN_ALL_NEW Induct.rulify_tac)
30.40 + THEN_ALL_NEW Induct.rulify_tac ctxt)
30.41 end;
30.42
30.43
31.1 --- a/src/HOL/Nominal/nominal_primrec.ML Fri Dec 13 23:53:02 2013 +0100
31.2 +++ b/src/HOL/Nominal/nominal_primrec.ML Sat Dec 14 17:28:05 2013 +0100
31.3 @@ -373,8 +373,8 @@
31.4 |> snd
31.5 end)
31.6 [goals] |>
31.7 - Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
31.8 - rewrite_goals_tac defs_thms THEN
31.9 + Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ =>
31.10 + rewrite_goals_tac ctxt defs_thms THEN
31.11 compose_tac (false, rule, length rule_prems) 1))) |>
31.12 Seq.hd
31.13 end;
32.1 --- a/src/HOL/TLA/Action.thy Fri Dec 13 23:53:02 2013 +0100
32.2 +++ b/src/HOL/TLA/Action.thy Sat Dec 14 17:28:05 2013 +0100
32.3 @@ -108,23 +108,26 @@
32.4 "world" parameter of the form (s,t) and apply additional rewrites.
32.5 *)
32.6
32.7 -fun action_unlift th =
32.8 - (rewrite_rule @{thms action_rews} (th RS @{thm actionD}))
32.9 - handle THM _ => int_unlift th;
32.10 +fun action_unlift ctxt th =
32.11 + (rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD}))
32.12 + handle THM _ => int_unlift ctxt th;
32.13
32.14 (* Turn |- A = B into meta-level rewrite rule A == B *)
32.15 val action_rewrite = int_rewrite
32.16
32.17 -fun action_use th =
32.18 +fun action_use ctxt th =
32.19 case (concl_of th) of
32.20 Const _ $ (Const ("Intensional.Valid", _) $ _) =>
32.21 - (flatten (action_unlift th) handle THM _ => th)
32.22 + (flatten (action_unlift ctxt th) handle THM _ => th)
32.23 | _ => th;
32.24 *}
32.25
32.26 -attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *}
32.27 -attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *}
32.28 -attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *}
32.29 +attribute_setup action_unlift =
32.30 + {* Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of)) *}
32.31 +attribute_setup action_rewrite =
32.32 + {* Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of)) *}
32.33 +attribute_setup action_use =
32.34 + {* Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of)) *}
32.35
32.36
32.37 (* =========================== square / angle brackets =========================== *)
32.38 @@ -258,11 +261,11 @@
32.39 should plug in only "very safe" rules that can be applied blindly.
32.40 Note that it applies whatever simplifications are currently active.
32.41 *)
32.42 -fun action_simp_tac ss intros elims =
32.43 +fun action_simp_tac ctxt intros elims =
32.44 asm_full_simp_tac
32.45 - (ss setloop (fn _ => (resolve_tac ((map action_use intros)
32.46 + (ctxt setloop (fn _ => (resolve_tac ((map (action_use ctxt) intros)
32.47 @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
32.48 - ORELSE' (eresolve_tac ((map action_use elims)
32.49 + ORELSE' (eresolve_tac ((map (action_use ctxt) elims)
32.50 @ [conjE,disjE,exE]))));
32.51 *}
32.52
33.1 --- a/src/HOL/TLA/Intensional.thy Fri Dec 13 23:53:02 2013 +0100
33.2 +++ b/src/HOL/TLA/Intensional.thy Sat Dec 14 17:28:05 2013 +0100
33.3 @@ -243,12 +243,12 @@
33.4 |- F --> G becomes F w --> G w
33.5 *)
33.6
33.7 -fun int_unlift th =
33.8 - rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
33.9 +fun int_unlift ctxt th =
33.10 + rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
33.11
33.12 (* Turn |- F = G into meta-level rewrite rule F == G *)
33.13 -fun int_rewrite th =
33.14 - zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection}))
33.15 +fun int_rewrite ctxt th =
33.16 + zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))
33.17
33.18 (* flattening turns "-->" into "==>" and eliminates conjunctions in the
33.19 antecedent. For example,
33.20 @@ -282,17 +282,20 @@
33.21 hflatten t
33.22 end
33.23
33.24 -fun int_use th =
33.25 +fun int_use ctxt th =
33.26 case (concl_of th) of
33.27 Const _ $ (Const ("Intensional.Valid", _) $ _) =>
33.28 - (flatten (int_unlift th) handle THM _ => th)
33.29 + (flatten (int_unlift ctxt th) handle THM _ => th)
33.30 | _ => th
33.31 *}
33.32
33.33 -attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *}
33.34 -attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *}
33.35 +attribute_setup int_unlift =
33.36 + {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}
33.37 +attribute_setup int_rewrite =
33.38 + {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}
33.39 attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
33.40 -attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *}
33.41 +attribute_setup int_use =
33.42 + {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
33.43
33.44 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
33.45 by (simp add: Valid_def)
34.1 --- a/src/HOL/TLA/Memory/Memory.thy Fri Dec 13 23:53:02 2013 +0100
34.2 +++ b/src/HOL/TLA/Memory/Memory.thy Sat Dec 14 17:28:05 2013 +0100
34.3 @@ -223,11 +223,11 @@
34.4 apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
34.5 apply (case_tac "arg (ch w p)")
34.6 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Read_def},
34.7 - temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
34.8 + temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
34.9 apply (force dest: base_pair [temp_use])
34.10 apply (erule contrapos_np)
34.11 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Write_def},
34.12 - temp_rewrite @{thm enabled_ex}])
34.13 + temp_rewrite @{context} @{thm enabled_ex}])
34.14 [@{thm WriteInner_enabled}, exI] [] 1 *})
34.15 done
34.16
35.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Dec 13 23:53:02 2013 +0100
35.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sat Dec 14 17:28:05 2013 +0100
35.3 @@ -233,7 +233,7 @@
35.4
35.5 setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
35.6
35.7 -ML {* val temp_elim = make_elim o temp_use *}
35.8 +ML {* val temp_elim = make_elim oo temp_use *}
35.9
35.10
35.11
35.12 @@ -352,7 +352,7 @@
35.13 --> unchanged (rmhist!p)"
35.14 by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
35.15 @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
35.16 - @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
35.17 + @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1 *})
35.18
35.19
35.20 (* ------------------------------ State S2 ---------------------------------------- *)
35.21 @@ -566,7 +566,8 @@
35.22 & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p
35.23 --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
35.24 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
35.25 - (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
35.26 + (map (temp_elim @{context})
35.27 + [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
35.28 using [[fast_solver]]
35.29 apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
35.30 done
35.31 @@ -576,7 +577,8 @@
35.32 --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
35.33 & unchanged (e p, r p, m p, rmhist!p)"
35.34 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
35.35 - (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
35.36 + (map (temp_elim @{context})
35.37 + [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
35.38 using [[fast_solver]]
35.39 apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
35.40 done
35.41 @@ -586,9 +588,10 @@
35.42 --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
35.43 | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
35.44 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
35.45 - (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
35.46 + (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
35.47 apply (tactic {* action_simp_tac @{context} []
35.48 - (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
35.49 + (@{thm squareE} ::
35.50 + map (temp_elim @{context}) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
35.51 apply (auto dest!: S3Hist [temp_use])
35.52 done
35.53
35.54 @@ -599,9 +602,10 @@
35.55 | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
35.56 | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
35.57 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
35.58 - (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
35.59 + (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
35.60 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
35.61 - (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
35.62 + (@{thm squareE} ::
35.63 + map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
35.64 apply (auto dest!: S4Hist [temp_use])
35.65 done
35.66
35.67 @@ -610,8 +614,8 @@
35.68 --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
35.69 | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
35.70 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
35.71 - (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
35.72 - apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
35.73 + (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
35.74 + apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
35.75 using [[fast_solver]]
35.76 apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
35.77 done
35.78 @@ -621,9 +625,9 @@
35.79 --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
35.80 | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
35.81 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
35.82 - (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
35.83 + (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
35.84 apply (tactic {* action_simp_tac @{context} []
35.85 - (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
35.86 + (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
35.87 apply (auto dest: S6Hist [temp_use])
35.88 done
35.89
35.90 @@ -795,8 +799,8 @@
35.91 SELECT_GOAL
35.92 (TRY (rtac @{thm actionI} 1) THEN
35.93 Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
35.94 - rewrite_goals_tac @{thms action_rews} THEN
35.95 - forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
35.96 + rewrite_goals_tac ctxt @{thms action_rews} THEN
35.97 + forward_tac [temp_use ctxt @{thm Step1_4_7}] 1 THEN
35.98 asm_full_simp_tac ctxt 1);
35.99 *}
35.100
35.101 @@ -898,7 +902,7 @@
35.102 lemma S1_RNextdisabled: "|- S1 rmhist p -->
35.103 ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
35.104 apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
35.105 - @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
35.106 + @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
35.107 apply force
35.108 done
35.109
35.110 @@ -1103,7 +1107,7 @@
35.111 apply (erule InfiniteEnsures)
35.112 apply assumption
35.113 apply (tactic {* action_simp_tac @{context} []
35.114 - (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
35.115 + (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
35.116 apply (auto simp: SF_def)
35.117 apply (erule contrapos_np)
35.118 apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
35.119 @@ -1190,7 +1194,7 @@
35.120 ==> sigma |= []<>S1 rmhist p"
35.121 apply (rule classical)
35.122 apply (tactic {* asm_lr_simp_tac (@{context} addsimps
35.123 - [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
35.124 + [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
35.125 apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
35.126 done
35.127
36.1 --- a/src/HOL/TLA/TLA.thy Fri Dec 13 23:53:02 2013 +0100
36.2 +++ b/src/HOL/TLA/TLA.thy Sat Dec 14 17:28:05 2013 +0100
36.3 @@ -118,25 +118,30 @@
36.4 functions defined in theory Intensional in that they introduce a
36.5 "world" parameter of type "behavior".
36.6 *)
36.7 -fun temp_unlift th =
36.8 - (rewrite_rule @{thms action_rews} (th RS @{thm tempD})) handle THM _ => action_unlift th;
36.9 +fun temp_unlift ctxt th =
36.10 + (rewrite_rule ctxt @{thms action_rews} (th RS @{thm tempD}))
36.11 + handle THM _ => action_unlift ctxt th;
36.12
36.13 (* Turn |- F = G into meta-level rewrite rule F == G *)
36.14 val temp_rewrite = int_rewrite
36.15
36.16 -fun temp_use th =
36.17 +fun temp_use ctxt th =
36.18 case (concl_of th) of
36.19 Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) =>
36.20 - ((flatten (temp_unlift th)) handle THM _ => th)
36.21 + ((flatten (temp_unlift ctxt th)) handle THM _ => th)
36.22 | _ => th;
36.23
36.24 -fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
36.25 +fun try_rewrite ctxt th = temp_rewrite ctxt th handle THM _ => temp_use ctxt th;
36.26 *}
36.27
36.28 -attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *}
36.29 -attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *}
36.30 -attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *}
36.31 -attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *}
36.32 +attribute_setup temp_unlift =
36.33 + {* Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of)) *}
36.34 +attribute_setup temp_rewrite =
36.35 + {* Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of)) *}
36.36 +attribute_setup temp_use =
36.37 + {* Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of)) *}
36.38 +attribute_setup try_rewrite =
36.39 + {* Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of)) *}
36.40
36.41
36.42 (* ------------------------------------------------------------------------- *)
36.43 @@ -584,7 +589,7 @@
36.44 (EVERY
36.45 [auto_tac ctxt,
36.46 TRY (merge_box_tac 1),
36.47 - rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
36.48 + rtac (temp_use ctxt @{thm INV1}) 1, (* fail if the goal is not a box *)
36.49 TRYALL (etac @{thm Stable})]);
36.50
36.51 (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
37.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Fri Dec 13 23:53:02 2013 +0100
37.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Sat Dec 14 17:28:05 2013 +0100
37.3 @@ -40,7 +40,7 @@
37.4 in
37.5 thms
37.6 |> Conjunction.intr_balanced
37.7 - |> rewrite_rule [Thm.symmetric (Thm.assume assum)]
37.8 + |> rewrite_rule (Proof_Context.init_global thy) [Thm.symmetric (Thm.assume assum)]
37.9 |> Thm.implies_intr assum
37.10 |> Thm.generalize ([], params) 0
37.11 |> Axclass.unoverload thy
37.12 @@ -94,14 +94,14 @@
37.13 (def, lthy')
37.14 end;
37.15
37.16 - fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
37.17 + fun tac ctxt thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms);
37.18
37.19 val qualify =
37.20 Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
37.21 in
37.22 Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
37.23 #> add_def
37.24 - #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single
37.25 + #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single
37.26 #-> fold Code.del_eqn
37.27 #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
37.28 #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
38.1 --- a/src/HOL/Tools/Datatype/datatype.ML Fri Dec 13 23:53:02 2013 +0100
38.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Sat Dec 14 17:28:05 2013 +0100
38.3 @@ -32,8 +32,6 @@
38.4 val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover};
38.5 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
38.6
38.7 -val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
38.8 -
38.9 fun exh_thm_of (dt_info : Datatype_Aux.info Symtab.table) tname =
38.10 #exhaust (the (Symtab.lookup dt_info tname));
38.11
38.12 @@ -271,6 +269,8 @@
38.13
38.14 val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
38.15
38.16 + val collect_simp = rewrite_rule (Proof_Context.init_global thy4) [mk_meta_eq mem_Collect_eq];
38.17 +
38.18 val newT_iso_axms = typedefs |> map (fn (_, (_, {Abs_inverse, Rep_inverse, Rep, ...})) =>
38.19 (collect_simp Abs_inverse, Rep_inverse, collect_simp Rep));
38.20
38.21 @@ -355,7 +355,7 @@
38.22 val rewrites = def_thms @ map mk_meta_eq rec_rewrites;
38.23 val char_thms' =
38.24 map (fn eqn => Goal.prove_sorry_global thy' [] [] eqn
38.25 - (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
38.26 + (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac refl 1])) eqns;
38.27
38.28 in (thy', char_thms' @ char_thms) end;
38.29
38.30 @@ -418,13 +418,13 @@
38.31 Goal.prove_sorry_global thy5 [] []
38.32 (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1))
38.33 (fn {context = ctxt, ...} => EVERY
38.34 - [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
38.35 + [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
38.36 REPEAT (EVERY
38.37 [rtac allI 1, rtac impI 1,
38.38 Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
38.39 REPEAT (EVERY
38.40 [hyp_subst_tac ctxt 1,
38.41 - rewrite_goals_tac rewrites,
38.42 + rewrite_goals_tac ctxt rewrites,
38.43 REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
38.44 (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
38.45 ORELSE (EVERY
38.46 @@ -443,9 +443,10 @@
38.47 val elem_thm =
38.48 Goal.prove_sorry_global thy5 [] []
38.49 (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
38.50 - (fn _ =>
38.51 - EVERY [(Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
38.52 - rewrite_goals_tac rewrites,
38.53 + (fn {context = ctxt, ...} =>
38.54 + EVERY [
38.55 + (Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
38.56 + rewrite_goals_tac ctxt rewrites,
38.57 REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
38.58 ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
38.59
38.60 @@ -480,11 +481,11 @@
38.61 else
38.62 drop (length newTs) (Datatype_Aux.split_conj_thm
38.63 (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY
38.64 - [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
38.65 + [(Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
38.66 REPEAT (rtac TrueI 1),
38.67 - rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
38.68 + rewrite_goals_tac ctxt (mk_meta_eq @{thm choice_eq} ::
38.69 Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
38.70 - rewrite_goals_tac (map Thm.symmetric range_eqs),
38.71 + rewrite_goals_tac ctxt (map Thm.symmetric range_eqs),
38.72 REPEAT (EVERY
38.73 [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
38.74 maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
38.75 @@ -511,9 +512,9 @@
38.76 val rewrites = @{thm o_def} :: constr_defs @ map (mk_meta_eq o #2) newT_iso_axms;
38.77 in
38.78 Goal.prove_sorry_global thy5 [] [] eqn
38.79 - (fn _ => EVERY
38.80 + (fn {context = ctxt, ...} => EVERY
38.81 [resolve_tac inj_thms 1,
38.82 - rewrite_goals_tac rewrites,
38.83 + rewrite_goals_tac ctxt rewrites,
38.84 rtac refl 3,
38.85 resolve_tac rep_intrs 2,
38.86 REPEAT (resolve_tac iso_elem_thms 1)])
38.87 @@ -634,7 +635,7 @@
38.88 (fn {context = ctxt, prems, ...} =>
38.89 EVERY
38.90 [rtac indrule_lemma' 1,
38.91 - (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
38.92 + (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
38.93 EVERY (map (fn (prem, r) => (EVERY
38.94 [REPEAT (eresolve_tac Abs_inverse_thms 1),
38.95 simp_tac (put_simpset HOL_basic_ss ctxt
39.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Dec 13 23:53:02 2013 +0100
39.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Dec 14 17:28:05 2013 +0100
39.3 @@ -27,6 +27,9 @@
39.4
39.5 fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype.info) is thy =
39.6 let
39.7 + val ctxt = Proof_Context.init_global thy;
39.8 + val cert = cterm_of thy;
39.9 +
39.10 val recTs = Datatype_Aux.get_rec_types descr;
39.11 val pnames =
39.12 if length descr = 1 then ["P"]
39.13 @@ -104,7 +107,6 @@
39.14 (map (fn ((((i, _), T), U), tname) =>
39.15 make_pred i U T (mk_proj i is r) (Free (tname, T)))
39.16 (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
39.17 - val cert = cterm_of thy;
39.18 val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
39.19 (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
39.20
39.21 @@ -112,10 +114,10 @@
39.22 Goal.prove_internal (map cert prems) (cert concl)
39.23 (fn prems =>
39.24 EVERY [
39.25 - rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
39.26 + rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
39.27 rtac (cterm_instantiate inst induct) 1,
39.28 - ALLGOALS Object_Logic.atomize_prems_tac,
39.29 - rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
39.30 + ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
39.31 + rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
39.32 REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
39.33 REPEAT (etac allE i) THEN atac i)) 1)])
39.34 |> Drule.export_without_context;
40.1 --- a/src/HOL/Tools/Datatype/primrec.ML Fri Dec 13 23:53:02 2013 +0100
40.2 +++ b/src/HOL/Tools/Datatype/primrec.ML Sat Dec 14 17:28:05 2013 +0100
40.3 @@ -245,8 +245,10 @@
40.4 let
40.5 val frees = fold (Variable.add_free_names ctxt) eqs [];
40.6 val rewrites = rec_rewrites' @ map (snd o snd) defs;
40.7 - fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
40.8 - in map (fn eq => Goal.prove ctxt frees [] eq tac) eqs end;
40.9 + in
40.10 + map (fn eq => Goal.prove ctxt frees [] eq
40.11 + (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs
40.12 + end;
40.13 in ((prefix, (fs, defs)), prove) end
40.14 handle PrimrecError (msg, some_eqn) =>
40.15 error ("Primrec definition error:\n" ^ msg ^
41.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Dec 13 23:53:02 2013 +0100
41.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Sat Dec 14 17:28:05 2013 +0100
41.3 @@ -207,8 +207,8 @@
41.4 (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts))
41.5 (fn {context = ctxt, ...} =>
41.6 #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
41.7 - (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1 THEN
41.8 - rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
41.9 + (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
41.10 + rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
41.11 end;
41.12
41.13 val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
41.14 @@ -247,8 +247,8 @@
41.15 val rec_thms =
41.16 map (fn t =>
41.17 Goal.prove_sorry_global thy2 [] [] t
41.18 - (fn _ => EVERY
41.19 - [rewrite_goals_tac reccomb_defs,
41.20 + (fn {context = ctxt, ...} => EVERY
41.21 + [rewrite_goals_tac ctxt reccomb_defs,
41.22 rtac @{thm the1_equality} 1,
41.23 resolve_tac rec_unique_thms 1,
41.24 resolve_tac rec_intrs 1,
41.25 @@ -327,8 +327,8 @@
41.26 val case_thms =
41.27 (map o map) (fn t =>
41.28 Goal.prove_sorry_global thy2 [] [] t
41.29 - (fn _ =>
41.30 - EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
41.31 + (fn {context = ctxt, ...} =>
41.32 + EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
41.33 (Datatype_Prop.make_cases case_names descr thy2);
41.34 in
41.35 thy2
42.1 --- a/src/HOL/Tools/Function/function_lib.ML Fri Dec 13 23:53:02 2013 +0100
42.2 +++ b/src/HOL/Tools/Function/function_lib.ML Sat Dec 14 17:28:05 2013 +0100
42.3 @@ -107,12 +107,14 @@
42.4
42.5 fun regroup_conv neu cn ac is ct =
42.6 let
42.7 + val thy = theory_of_cterm ct
42.8 + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
42.9 +
42.10 val mk = HOLogic.mk_binop cn
42.11 val t = term_of ct
42.12 val xs = dest_binop_list cn t
42.13 val js = subtract (op =) is (0 upto (length xs) - 1)
42.14 val ty = fastype_of t
42.15 - val thy = theory_of_cterm ct
42.16 in
42.17 Goal.prove_internal []
42.18 (cterm_of thy
42.19 @@ -122,7 +124,7 @@
42.20 else if null js
42.21 then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
42.22 else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
42.23 - (K (rewrite_goals_tac ac
42.24 + (K (rewrite_goals_tac ctxt ac
42.25 THEN rtac Drule.reflexive_thm 1))
42.26 end
42.27
43.1 --- a/src/HOL/Tools/Function/induction_schema.ML Fri Dec 13 23:53:02 2013 +0100
43.2 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat Dec 14 17:28:05 2013 +0100
43.3 @@ -38,12 +38,12 @@
43.4 branches: scheme_branch list,
43.5 cases: scheme_case list}
43.6
43.7 -val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
43.8 -val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
43.9 +fun ind_atomize ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_atomize}
43.10 +fun ind_rulify ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_rulify}
43.11
43.12 fun meta thm = thm RS eq_reflection
43.13
43.14 -val sum_prod_conv = Raw_Simplifier.rewrite true
43.15 +fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
43.16 (map meta (@{thm split_conv} :: @{thms sum.cases}))
43.17
43.18 fun term_conv thy cv t =
43.19 @@ -187,13 +187,15 @@
43.20 end
43.21
43.22
43.23 -fun mk_ind_goal thy branches =
43.24 +fun mk_ind_goal ctxt branches =
43.25 let
43.26 + val thy = Proof_Context.theory_of ctxt
43.27 +
43.28 fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
43.29 HOLogic.mk_Trueprop (list_comb (P, map Free xs))
43.30 |> fold_rev (curry Logic.mk_implies) Cs
43.31 |> fold_rev (Logic.all o Free) ws
43.32 - |> term_conv thy ind_atomize
43.33 + |> term_conv thy (ind_atomize ctxt)
43.34 |> Object_Logic.drop_judgment thy
43.35 |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
43.36 in
43.37 @@ -203,6 +205,9 @@
43.38 fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
43.39 (IndScheme {T, cases=scases, branches}) =
43.40 let
43.41 + val thy = Proof_Context.theory_of ctxt
43.42 + val cert = cterm_of thy
43.43 +
43.44 val n = length branches
43.45 val scases_idx = map_index I scases
43.46
43.47 @@ -210,10 +215,7 @@
43.48 SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
43.49 val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
43.50
43.51 - val thy = Proof_Context.theory_of ctxt
43.52 - val cert = cterm_of thy
43.53 -
43.54 - val P_comp = mk_ind_goal thy branches
43.55 + val P_comp = mk_ind_goal ctxt branches
43.56
43.57 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
43.58 val ihyp = Logic.all_const T $ Abs ("z", T,
43.59 @@ -270,8 +272,8 @@
43.60 sih
43.61 |> Thm.forall_elim (cert (inject idx rcargs))
43.62 |> Thm.elim_implies (import ineq) (* Psum rcargs *)
43.63 - |> Conv.fconv_rule sum_prod_conv
43.64 - |> Conv.fconv_rule ind_rulify
43.65 + |> Conv.fconv_rule (sum_prod_conv ctxt)
43.66 + |> Conv.fconv_rule (ind_rulify ctxt)
43.67 |> (fn th => th COMP ipres) (* P rs *)
43.68 |> fold_rev (Thm.implies_intr o cprop_of) cGas
43.69 |> fold_rev Thm.forall_intr cGvs
43.70 @@ -312,8 +314,9 @@
43.71
43.72 val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
43.73 |> Goal.init
43.74 - |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
43.75 - THEN CONVERSION ind_rulify 1)
43.76 + |> (Simplifier.rewrite_goals_tac ctxt
43.77 + (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
43.78 + THEN CONVERSION (ind_rulify ctxt) 1)
43.79 |> Seq.hd
43.80 |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
43.81 |> Goal.finish ctxt
43.82 @@ -375,7 +378,7 @@
43.83 indthm
43.84 |> Drule.instantiate' [] [SOME inst]
43.85 |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
43.86 - |> Conv.fconv_rule ind_rulify
43.87 + |> Conv.fconv_rule (ind_rulify ctxt'')
43.88 end
43.89
43.90 val res = Conjunction.intr_balanced (map_index project branches)
44.1 --- a/src/HOL/Tools/Function/partial_function.ML Fri Dec 13 23:53:02 2013 +0100
44.2 +++ b/src/HOL/Tools/Function/partial_function.ML Sat Dec 14 17:28:05 2013 +0100
44.3 @@ -180,6 +180,7 @@
44.4 val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
44.5 val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
44.6 in
44.7 + (* FIXME ctxt vs. ctxt' (!?) *)
44.8 rule
44.9 |> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
44.10 |> Tactic.rule_by_tactic ctxt
44.11 @@ -188,7 +189,7 @@
44.12 THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
44.13 |> (fn thm => thm OF [mono_thm, f_def])
44.14 |> Conv.fconv_rule (Conv.concl_conv ~1 (* simplify conclusion *)
44.15 - (Raw_Simplifier.rewrite false [mk_meta_eq @{thm Product_Type.curry_split}]))
44.16 + (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_split}]))
44.17 |> singleton (Variable.export ctxt' ctxt)
44.18 end
44.19
45.1 --- a/src/HOL/Tools/Function/termination.ML Fri Dec 13 23:53:02 2013 +0100
45.2 +++ b/src/HOL/Tools/Function/termination.ML Sat Dec 14 17:28:05 2013 +0100
45.3 @@ -305,7 +305,7 @@
45.4 in
45.5 (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
45.6 THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
45.7 - THEN rewrite_goal_tac Un_aci_simps 1) st (* eliminate duplicates *)
45.8 + THEN rewrite_goal_tac ctxt Un_aci_simps 1) st (* eliminate duplicates *)
45.9 end
45.10
45.11 end
46.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Dec 13 23:53:02 2013 +0100
46.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Sat Dec 14 17:28:05 2013 +0100
46.3 @@ -85,7 +85,7 @@
46.4 in
46.5 Conv.fconv_rule
46.6 ((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
46.7 - (Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm
46.8 + (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
46.9 end
46.10
46.11 fun inst_relcomppI thy ant1 ant2 =
46.12 @@ -482,7 +482,7 @@
46.13 val eq_thm =
46.14 (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
46.15 in
46.16 - Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
46.17 + Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
46.18 end
46.19
46.20 fun rename_to_tnames ctxt term =
46.21 @@ -533,7 +533,8 @@
46.22 fun after_qed' thm_list lthy =
46.23 let
46.24 val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm
46.25 - (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac (hd thm_list) 1)
46.26 + (fn {context = ctxt, ...} =>
46.27 + rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1)
46.28 in
46.29 after_qed internal_rsp_thm lthy
46.30 end
47.1 --- a/src/HOL/Tools/Meson/meson.ML Fri Dec 13 23:53:02 2013 +0100
47.2 +++ b/src/HOL/Tools/Meson/meson.ML Sat Dec 14 17:28:05 2013 +0100
47.3 @@ -552,9 +552,9 @@
47.4 @{const_name Let}]
47.5
47.6 fun presimplify ctxt =
47.7 - rewrite_rule (map safe_mk_meta_eq nnf_simps)
47.8 + rewrite_rule ctxt (map safe_mk_meta_eq nnf_simps)
47.9 #> simplify (put_simpset nnf_ss ctxt)
47.10 - #> rewrite_rule @{thms Let_def [abs_def]}
47.11 + #> rewrite_rule ctxt @{thms Let_def [abs_def]}
47.12
47.13 fun make_nnf ctxt th = case prems_of th of
47.14 [] => th |> presimplify ctxt |> make_nnf1 ctxt
47.15 @@ -706,7 +706,7 @@
47.16 Function mkcl converts theorems to clauses.*)
47.17 fun MESON preskolem_tac mkcl cltac ctxt i st =
47.18 SELECT_GOAL
47.19 - (EVERY [Object_Logic.atomize_prems_tac 1,
47.20 + (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
47.21 rtac ccontr 1,
47.22 preskolem_tac,
47.23 Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
48.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Dec 13 23:53:02 2013 +0100
48.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Dec 14 17:28:05 2013 +0100
48.3 @@ -193,6 +193,8 @@
48.4 Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
48.5 fun old_skolem_theorem_of_def thy rhs0 =
48.6 let
48.7 + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
48.8 +
48.9 val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
48.10 val rhs' = rhs |> Thm.dest_comb |> snd
48.11 val (ch, frees) = c_variant_abs_multi (rhs', [])
48.12 @@ -208,8 +210,8 @@
48.13 Drule.list_comb (rhs, frees)
48.14 |> Drule.beta_conv cabs |> Thm.apply cTrueprop
48.15 fun tacf [prem] =
48.16 - rewrite_goals_tac @{thms skolem_def [abs_def]}
48.17 - THEN rtac ((prem |> rewrite_rule @{thms skolem_def [abs_def]})
48.18 + rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
48.19 + THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
48.20 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
48.21 in
48.22 Goal.prove_internal [ex_tm] conc tacf
48.23 @@ -308,7 +310,7 @@
48.24 |> zero_var_indexes
48.25 |> new_skolem ? forall_intr_vars
48.26 val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
48.27 - val th = th |> Conv.fconv_rule Object_Logic.atomize
48.28 + val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
48.29 |> cong_extensionalize_thm thy
48.30 |> abs_extensionalize_thm ctxt
48.31 |> make_nnf ctxt
49.1 --- a/src/HOL/Tools/Metis/metis_generate.ML Fri Dec 13 23:53:02 2013 +0100
49.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML Sat Dec 14 17:28:05 2013 +0100
49.3 @@ -135,8 +135,8 @@
49.4 Isa_Raw of thm
49.5
49.6 val proxy_defs = map (fst o snd o snd) proxy_table
49.7 -val prepare_helper =
49.8 - Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
49.9 +fun prepare_helper ctxt =
49.10 + Meson.make_meta_clause #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
49.11
49.12 fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
49.13 if is_tptp_variable s then
49.14 @@ -160,7 +160,7 @@
49.15 fun metis_literals_of_atp type_enc (AConn (AOr, phis)) =
49.16 maps (metis_literals_of_atp type_enc) phis
49.17 | metis_literals_of_atp type_enc phi = [metis_literal_of_atp type_enc phi]
49.18 -fun metis_axiom_of_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
49.19 +fun metis_axiom_of_atp ctxt type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
49.20 let
49.21 fun some isa =
49.22 SOME (phi |> metis_literals_of_atp type_enc
49.23 @@ -178,7 +178,7 @@
49.24 nth (AList.lookup (op =) helper_table (const, needs_fairly_sound)
49.25 |> the)
49.26 (the (Int.fromString j) - 1)
49.27 - |> snd |> prepare_helper
49.28 + |> snd |> prepare_helper ctxt
49.29 |> Isa_Raw |> some
49.30 | _ => raise Fail ("malformed helper identifier " ^ quote ident)
49.31 else case try (unprefix fact_prefix) ident of
49.32 @@ -196,7 +196,7 @@
49.33 end
49.34 | NONE => TrueI |> Isa_Raw |> some
49.35 end
49.36 - | metis_axiom_of_atp _ _ _ = raise Fail "not CNF -- expected formula"
49.37 + | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
49.38
49.39 fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
49.40 eliminate_lam_wrappers t
49.41 @@ -249,7 +249,7 @@
49.42 (* "rev" is for compatibility with existing proof scripts. *)
49.43 val axioms =
49.44 atp_problem
49.45 - |> maps (map_filter (metis_axiom_of_atp type_enc clauses) o snd) |> rev
49.46 + |> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev
49.47 fun ord_info () = atp_problem_term_order_info atp_problem
49.48 in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
49.49
50.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Dec 13 23:53:02 2013 +0100
50.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Dec 14 17:28:05 2013 +0100
50.3 @@ -249,16 +249,16 @@
50.4 "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
50.5 don't use this trick in general because it makes the proof object uglier than
50.6 necessary. FIXME. *)
50.7 -fun negate_head th =
50.8 +fun negate_head ctxt th =
50.9 if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
50.10 (th RS @{thm select_FalseI})
50.11 - |> fold (rewrite_rule o single)
50.12 + |> fold (rewrite_rule ctxt o single)
50.13 @{thms not_atomize_select atomize_not_select}
50.14 else
50.15 - th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
50.16 + th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not}
50.17
50.18 (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
50.19 -val select_literal = negate_head oo make_last
50.20 +fun select_literal ctxt = negate_head ctxt oo make_last
50.21
50.22 fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
50.23 let
50.24 @@ -293,7 +293,7 @@
50.25 i_th2)
50.26 | j2 =>
50.27 (trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2);
50.28 - resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
50.29 + resolve_inc_tyvars thy (select_literal ctxt j1 i_th1) j2 i_th2
50.30 handle TERM (s, _) =>
50.31 raise METIS_RECONSTRUCT ("resolve_inference", s)))
50.32 end
50.33 @@ -448,7 +448,7 @@
50.34 |> distinct Term.aconv_untyped
50.35 val goal = Logic.list_implies (prems, concl)
50.36 val tac = cut_tac th 1
50.37 - THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
50.38 + THEN rewrite_goals_tac ctxt @{thms not_not [THEN eq_reflection]}
50.39 THEN ALLGOALS assume_tac
50.40 in
50.41 if length prems = length prems0 then
51.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Dec 13 23:53:02 2013 +0100
51.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Sat Dec 14 17:28:05 2013 +0100
51.3 @@ -65,7 +65,7 @@
51.4 fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
51.5 let
51.6 val thy = Proof_Context.theory_of ctxt
51.7 - val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
51.8 + val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
51.9 val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
51.10 val ct = cterm_of thy (HOLogic.mk_Trueprop t)
51.11 in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
52.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Dec 13 23:53:02 2013 +0100
52.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Dec 14 17:28:05 2013 +0100
52.3 @@ -219,8 +219,8 @@
52.4 |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
52.5 val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
52.6 val case_th =
52.7 - rewrite_rule (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
52.8 - val prems' = maps (dest_conjunct_prem o rewrite_rule tuple_rew_rules) prems
52.9 + rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
52.10 + val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems
52.11 val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
52.12 val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
52.13 OF (replicate nargs @{thm refl})
52.14 @@ -236,7 +236,7 @@
52.15 (PEEK nprems_of
52.16 (fn n =>
52.17 ALLGOALS (fn i =>
52.18 - rewrite_goal_tac [@{thm split_paired_all}] i
52.19 + rewrite_goal_tac ctxt [@{thm split_paired_all}] i
52.20 THEN (SUBPROOF (instantiate i n) ctxt i))))
52.21 in
52.22 Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
53.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Dec 13 23:53:02 2013 +0100
53.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Dec 14 17:28:05 2013 +0100
53.3 @@ -1017,8 +1017,9 @@
53.4
53.5 fun peephole_optimisation thy intro =
53.6 let
53.7 + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
53.8 val process =
53.9 - rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
53.10 + rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
53.11 fun process_False intro_t =
53.12 if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
53.13 fun process_True intro_t =
54.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Dec 13 23:53:02 2013 +0100
54.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Dec 14 17:28:05 2013 +0100
54.3 @@ -203,7 +203,7 @@
54.4 SOME specss => (specss, thy)
54.5 | NONE =>*)
54.6 let
54.7 - val ctxt = Proof_Context.init_global thy
54.8 + val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
54.9 val intros =
54.10 if forall is_pred_equation specs then
54.11 map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
54.12 @@ -213,7 +213,7 @@
54.13 error ("unexpected specification for constant " ^ quote constname ^ ":\n"
54.14 ^ commas (map (quote o Display.string_of_thm_global thy) specs))
54.15 val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
54.16 - val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros
54.17 + val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros
54.18 val _ = print_specs options thy "normalized intros" intros
54.19 (*val intros = maps (split_cases thy) intros*)
54.20 val (intros', (local_defs, thy')) = flatten_intros constname intros thy
55.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Dec 13 23:53:02 2013 +0100
55.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sat Dec 14 17:28:05 2013 +0100
55.3 @@ -79,11 +79,11 @@
55.4 @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
55.5 @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
55.6 | Free _ =>
55.7 - Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} =>
55.8 + Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
55.9 let
55.10 val prems' = maps dest_conjunct_prem (take nargs prems)
55.11 in
55.12 - rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
55.13 + rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
55.14 end) ctxt 1
55.15 | Abs _ => raise Fail "prove_param: No valid parameter term"
55.16 in
55.17 @@ -118,7 +118,7 @@
55.18 end
55.19 | (Free _, _) =>
55.20 print_tac options "proving parameter call.."
55.21 - THEN Subgoal.FOCUS_PREMS (fn {context, params, prems, asms, concl, schematics} =>
55.22 + THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
55.23 let
55.24 val param_prem = nth prems premposition
55.25 val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
55.26 @@ -126,7 +126,7 @@
55.27 fun param_rewrite prem =
55.28 param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
55.29 val SOME rew_eq = find_first param_rewrite prems'
55.30 - val param_prem' = rewrite_rule
55.31 + val param_prem' = rewrite_rule ctxt'
55.32 (map (fn th => th RS @{thm eq_reflection})
55.33 [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
55.34 param_prem
55.35 @@ -168,7 +168,7 @@
55.36 let
55.37 val prems' = maps dest_conjunct_prem (take nargs prems)
55.38 in
55.39 - rewrite_goal_tac
55.40 + rewrite_goal_tac ctxt
55.41 (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
55.42 end
55.43 THEN REPEAT_DETERM (rtac @{thm refl} 1))
55.44 @@ -205,12 +205,12 @@
55.45 THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
55.46 THEN print_tac options "before single intro rule"
55.47 THEN Subgoal.FOCUS_PREMS
55.48 - (fn {context, params, prems, asms, concl, schematics} =>
55.49 - let
55.50 - val prems' = maps dest_conjunct_prem (take nargs prems)
55.51 - in
55.52 - rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
55.53 - end) ctxt 1
55.54 + (fn {context = ctxt', params, prems, asms, concl, schematics} =>
55.55 + let
55.56 + val prems' = maps dest_conjunct_prem (take nargs prems)
55.57 + in
55.58 + rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
55.59 + end) ctxt 1
55.60 THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
55.61 | prove_prems out_ts ((p, deriv) :: ps) =
55.62 let
55.63 @@ -293,7 +293,7 @@
55.64 val nargs = length (binder_types T)
55.65 val pred_case_rule = the_elim_of ctxt pred
55.66 in
55.67 - REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))
55.68 + REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
55.69 THEN print_tac options "before applying elim rule"
55.70 THEN etac (predfun_elim_of ctxt pred mode) 1
55.71 THEN etac pred_case_rule 1
55.72 @@ -370,7 +370,7 @@
55.73 val ho_args = ho_args_of mode args
55.74 in
55.75 etac @{thm bindE} 1
55.76 - THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
55.77 + THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
55.78 THEN print_tac options "prove_expr2-before"
55.79 THEN etac (predfun_elim_of ctxt name mode) 1
55.80 THEN print_tac options "prove_expr2"
55.81 @@ -483,11 +483,11 @@
55.82 THEN (prove_clause2 options ctxt pred mode clause i)
55.83 in
55.84 (DETERM (TRY (rtac @{thm unit.induct} 1)))
55.85 - THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})))
55.86 + THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
55.87 THEN (rtac (predfun_intro_of ctxt pred mode) 1)
55.88 THEN (REPEAT_DETERM (rtac @{thm refl} 2))
55.89 - THEN (if null moded_clauses then
55.90 - etac @{thm botE} 1
55.91 + THEN (
55.92 + if null moded_clauses then etac @{thm botE} 1
55.93 else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
55.94 end;
55.95
56.1 --- a/src/HOL/Tools/Qelim/cooper.ML Fri Dec 13 23:53:02 2013 +0100
56.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Sat Dec 14 17:28:05 2013 +0100
56.3 @@ -865,19 +865,19 @@
56.4 val aprems = Arith_Data.get_arith_facts ctxt
56.5 in
56.6 Method.insert_tac aprems
56.7 - THEN_ALL_NEW Object_Logic.full_atomize_tac
56.8 + THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
56.9 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
56.10 THEN_ALL_NEW simp_tac simpset_ctxt
56.11 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
56.12 - THEN_ALL_NEW Object_Logic.full_atomize_tac
56.13 + THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
56.14 THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
56.15 - THEN_ALL_NEW Object_Logic.full_atomize_tac
56.16 + THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
56.17 THEN_ALL_NEW div_mod_tac ctxt
56.18 THEN_ALL_NEW splits_tac ctxt
56.19 THEN_ALL_NEW simp_tac simpset_ctxt
56.20 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
56.21 THEN_ALL_NEW nat_to_int_tac ctxt
56.22 - THEN_ALL_NEW (core_tac ctxt)
56.23 + THEN_ALL_NEW core_tac ctxt
56.24 THEN_ALL_NEW finish_tac elim
56.25 end 1);
56.26
57.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Dec 13 23:53:02 2013 +0100
57.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Dec 14 17:28:05 2013 +0100
57.3 @@ -107,7 +107,7 @@
57.4 fun tac ctxt =
57.5 ALLGOALS (rtac rule)
57.6 THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
57.7 - THEN (ALLGOALS (Proof_Context.fact_tac eqs2))
57.8 + THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
57.9 val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
57.10 in (simp, lthy') end;
57.11
57.12 @@ -166,7 +166,7 @@
57.13 fun prove_simps proto_simps lthy =
57.14 let
57.15 val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
57.16 - val tac = ALLGOALS (Proof_Context.fact_tac ext_simps);
57.17 + val tac = ALLGOALS (Proof_Context.fact_tac lthy ext_simps);
57.18 in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
57.19 val b = Binding.conceal (Binding.qualify true prfx
57.20 (Binding.qualify true name (Binding.name "simps")));
58.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Dec 13 23:53:02 2013 +0100
58.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Dec 14 17:28:05 2013 +0100
58.3 @@ -129,7 +129,7 @@
58.4 val eq_thm =
58.5 (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
58.6 in
58.7 - Object_Logic.rulify (eq_thm RS Drule.equal_elim_rule2)
58.8 + Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
58.9 end
58.10
58.11
58.12 @@ -187,7 +187,7 @@
58.13 case thm_list of
58.14 [] => the maybe_proven_rsp_thm
58.15 | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
58.16 - (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
58.17 + (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
58.18 in
58.19 snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
58.20 end
59.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Dec 13 23:53:02 2013 +0100
59.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Dec 14 17:28:05 2013 +0100
59.3 @@ -40,10 +40,10 @@
59.4 (* composition of two theorems, used in maps *)
59.5 fun OF1 thm1 thm2 = thm2 RS thm1
59.6
59.7 -fun atomize_thm thm =
59.8 +fun atomize_thm ctxt thm =
59.9 let
59.10 val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
59.11 - val thm'' = Object_Logic.atomize (cprop_of thm')
59.12 + val thm'' = Object_Logic.atomize ctxt (cprop_of thm')
59.13 in
59.14 @{thm equal_elim_rule1} OF [thm'', thm']
59.15 end
59.16 @@ -480,7 +480,7 @@
59.17 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
59.18 val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
59.19 val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
59.20 - val thm3 = rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
59.21 + val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
59.22 val (insp, inst) =
59.23 if ty_c = ty_d
59.24 then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
59.25 @@ -635,7 +635,7 @@
59.26 val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
59.27 in
59.28 full_simp_tac simpset
59.29 - THEN' Object_Logic.full_atomize_tac
59.30 + THEN' Object_Logic.full_atomize_tac ctxt
59.31 THEN' gen_frees_tac ctxt
59.32 THEN' SUBGOAL (fn (goal, i) =>
59.33 let
59.34 @@ -652,7 +652,7 @@
59.35 val mk_tac_raw =
59.36 descend_procedure_tac ctxt simps
59.37 THEN' RANGE
59.38 - [Object_Logic.rulify_tac THEN' (K all_tac),
59.39 + [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
59.40 regularize_tac ctxt,
59.41 all_injection_tac ctxt,
59.42 clean_tac ctxt]
59.43 @@ -685,7 +685,7 @@
59.44 val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
59.45 in
59.46 full_simp_tac simpset
59.47 - THEN' Object_Logic.full_atomize_tac
59.48 + THEN' Object_Logic.full_atomize_tac ctxt
59.49 THEN' gen_frees_tac ctxt
59.50 THEN' SUBGOAL (fn (goal, i) =>
59.51 let
59.52 @@ -702,7 +702,7 @@
59.53 val mk_tac_raw =
59.54 partiality_descend_procedure_tac ctxt simps
59.55 THEN' RANGE
59.56 - [Object_Logic.rulify_tac THEN' (K all_tac),
59.57 + [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
59.58 all_injection_tac ctxt,
59.59 clean_tac ctxt]
59.60 in
59.61 @@ -720,7 +720,7 @@
59.62 val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
59.63 in
59.64 full_simp_tac simpset
59.65 - THEN' Object_Logic.full_atomize_tac
59.66 + THEN' Object_Logic.full_atomize_tac ctxt
59.67 THEN' gen_frees_tac ctxt
59.68 THEN' SUBGOAL (fn (goal, i) =>
59.69 let
59.70 @@ -730,7 +730,7 @@
59.71 rthm |> full_simplify simpset
59.72 |> Drule.eta_contraction_rule
59.73 |> Thm.forall_intr_frees
59.74 - |> atomize_thm
59.75 + |> atomize_thm ctxt
59.76
59.77 val rule = procedure_inst ctxt (prop_of rthm') goal
59.78 in
60.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Dec 13 23:53:02 2013 +0100
60.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Dec 14 17:28:05 2013 +0100
60.3 @@ -193,7 +193,7 @@
60.4 val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name
60.5 val quotient_thm =
60.6 (quot_thm RS @{thm quot_type.Quotient})
60.7 - |> fold_rule [abs_def, rep_def]
60.8 + |> fold_rule lthy3 [abs_def, rep_def]
60.9
60.10 (* name equivalence theorem *)
60.11 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
61.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML Fri Dec 13 23:53:02 2013 +0100
61.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Sat Dec 14 17:28:05 2013 +0100
61.3 @@ -68,7 +68,7 @@
61.4 fun prove_inj_prop ctxt def lhs =
61.5 let
61.6 val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
61.7 - val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
61.8 + val rule = disjE OF [Object_Logic.rulify ctxt (Thm.assume lhs)]
61.9 in
61.10 Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
61.11 |> apply (rtac @{thm injI})
61.12 @@ -94,7 +94,7 @@
61.13
61.14 fun prove_lhs ctxt rhs =
61.15 let
61.16 - val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
61.17 + val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs)))
61.18 val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt
61.19 in
61.20 Z3_Proof_Tools.by_tac (
62.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Dec 13 23:53:02 2013 +0100
62.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat Dec 14 17:28:05 2013 +0100
62.3 @@ -38,16 +38,19 @@
62.4 val merge = Net.merge eq
62.5 )
62.6
62.7 - val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true]
62.8 + fun prep context =
62.9 + `Thm.prop_of o rewrite_rule (Context.proof_of context) [Z3_Proof_Literals.rewrite_true]
62.10
62.11 - fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
62.12 - fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
62.13 + fun ins thm context =
62.14 + context |> Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net)
62.15 + fun rem thm context =
62.16 + context |> Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net)
62.17
62.18 - val add = Thm.declaration_attribute (Z3_Rules.map o ins)
62.19 - val del = Thm.declaration_attribute (Z3_Rules.map o del)
62.20 + val add = Thm.declaration_attribute ins
62.21 + val del = Thm.declaration_attribute rem
62.22 in
62.23
62.24 -val add_z3_rule = Z3_Rules.map o ins
62.25 +val add_z3_rule = ins
62.26
62.27 fun by_schematic_rule ctxt ct =
62.28 the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
63.1 --- a/src/HOL/Tools/TFL/post.ML Fri Dec 13 23:53:02 2013 +0100
63.2 +++ b/src/HOL/Tools/TFL/post.ML Sat Dec 14 17:28:05 2013 +0100
63.3 @@ -68,10 +68,11 @@
63.4 | _ => r RS P_imp_P_eq_True
63.5
63.6 (*Is this the best way to invoke the simplifier??*)
63.7 -fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L))
63.8 +fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
63.9
63.10 fun join_assums th =
63.11 let val thy = Thm.theory_of_thm th
63.12 + val ctxt = Proof_Context.init_global thy
63.13 val tych = cterm_of thy
63.14 val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
63.15 val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *)
63.16 @@ -80,7 +81,7 @@
63.17 in
63.18 Rules.GEN_ALL
63.19 (Rules.DISCH_ALL
63.20 - (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
63.21 + (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
63.22 end
63.23 val gen_all = USyntax.gen_all
63.24 in
63.25 @@ -139,7 +140,7 @@
63.26 let
63.27 val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
63.28 val {rules,rows,TCs,full_pats_TCs} =
63.29 - Prim.post_definition congs (thy, (def, pats))
63.30 + Prim.post_definition congs thy ctxt (def, pats)
63.31 val {lhs=f,rhs} = USyntax.dest_eq (concl def)
63.32 val (_,[R,_]) = USyntax.strip_comb rhs
63.33 val dummy = Prim.trace_thms "congs =" congs
63.34 @@ -149,9 +150,9 @@
63.35 {f = f, R = R, rules = rules,
63.36 full_pats_TCs = full_pats_TCs,
63.37 TCs = TCs}
63.38 - val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
63.39 + val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
63.40 (Rules.CONJUNCTS rules)
63.41 - in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
63.42 + in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
63.43 rules = ListPair.zip(rules', rows),
63.44 tcs = (termination_goals rules') @ tcs}
63.45 end
63.46 @@ -170,7 +171,7 @@
63.47 | solve_eq _ (th, [a], i) = [(a, i)]
63.48 | solve_eq ctxt (th, splitths, i) =
63.49 (writeln "Proving unsplit equation...";
63.50 - [((Drule.export_without_context o Object_Logic.rulify_no_asm)
63.51 + [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
63.52 (CaseSplit.splitto ctxt splitths th), i)])
63.53 handle ERROR s =>
63.54 (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
64.1 --- a/src/HOL/Tools/TFL/rules.ML Fri Dec 13 23:53:02 2013 +0100
64.2 +++ b/src/HOL/Tools/TFL/rules.ML Sat Dec 14 17:28:05 2013 +0100
64.3 @@ -42,14 +42,14 @@
64.4 val DISJ_CASESL: thm -> thm list -> thm
64.5
64.6 val list_beta_conv: cterm -> cterm list -> thm
64.7 - val SUBS: thm list -> thm -> thm
64.8 + val SUBS: Proof.context -> thm list -> thm -> thm
64.9 val simpl_conv: Proof.context -> thm list -> cterm -> thm
64.10
64.11 val rbeta: thm -> thm
64.12 val tracing: bool Unsynchronized.ref
64.13 val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
64.14 -> thm -> thm * term list
64.15 - val RIGHT_ASSOC: thm -> thm
64.16 + val RIGHT_ASSOC: Proof.context -> thm -> thm
64.17
64.18 val prove: bool -> cterm * tactic -> thm
64.19 end;
64.20 @@ -417,8 +417,8 @@
64.21 * Rewriting
64.22 *---------------------------------------------------------------------------*)
64.23
64.24 -fun SUBS thl =
64.25 - rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
64.26 +fun SUBS ctxt thl =
64.27 + rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
64.28
64.29 val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
64.30
64.31 @@ -426,7 +426,7 @@
64.32 rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
64.33
64.34
64.35 -val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];
64.36 +fun RIGHT_ASSOC ctxt = rewrite_rule ctxt [Thms.disj_assoc];
64.37
64.38
64.39
64.40 @@ -602,24 +602,24 @@
64.41 * the wrong word to use).
64.42 *---------------------------------------------------------------------------*)
64.43
64.44 -fun VSTRUCT_ELIM tych a vstr th =
64.45 +fun VSTRUCT_ELIM ctxt tych a vstr th =
64.46 let val L = USyntax.free_vars_lr vstr
64.47 val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
64.48 - val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
64.49 + val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
64.50 val thm2 = forall_intr_list (map tych L) thm1
64.51 val thm3 = forall_elim_list (XFILL tych a vstr) thm2
64.52 in refl RS
64.53 - rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
64.54 + rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
64.55 end;
64.56
64.57 -fun PGEN tych a vstr th =
64.58 +fun PGEN ctxt tych a vstr th =
64.59 let val a1 = tych a
64.60 val vstr1 = tych vstr
64.61 in
64.62 Thm.forall_intr a1
64.63 (if (is_Free vstr)
64.64 then cterm_instantiate [(vstr1,a1)] th
64.65 - else VSTRUCT_ELIM tych a vstr th)
64.66 + else VSTRUCT_ELIM ctxt tych a vstr th)
64.67 end;
64.68
64.69
64.70 @@ -701,7 +701,7 @@
64.71 val impth = implies_intr_list ants1 QeeqQ3
64.72 val impth1 = impth RS meta_eq_to_obj_eq
64.73 (* Need to abstract *)
64.74 - val ant_th = Utils.itlist2 (PGEN tych) args vstrl impth1
64.75 + val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
64.76 in ant_th COMP thm
64.77 end
64.78 fun q_eliminate (thm,imp,thy) =
65.1 --- a/src/HOL/Tools/TFL/tfl.ML Fri Dec 13 23:53:02 2013 +0100
65.2 +++ b/src/HOL/Tools/TFL/tfl.ML Sat Dec 14 17:28:05 2013 +0100
65.3 @@ -12,7 +12,7 @@
65.4 type pattern
65.5 val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
65.6 val wfrec_definition0: theory -> string -> term -> term -> theory * thm
65.7 - val post_definition: thm list -> theory * (thm * pattern list) ->
65.8 + val post_definition: thm list -> theory -> Proof.context -> thm * pattern list ->
65.9 {rules: thm,
65.10 rows: int list,
65.11 TCs: term list list,
65.12 @@ -415,7 +415,7 @@
65.13
65.14 fun givens pats = map pat_of (filter given pats);
65.15
65.16 -fun post_definition meta_tflCongs (theory, (def, pats)) =
65.17 +fun post_definition meta_tflCongs theory ctxt (def, pats) =
65.18 let val tych = Thry.typecheck theory
65.19 val f = #lhs(USyntax.dest_eq(concl def))
65.20 val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
65.21 @@ -440,7 +440,7 @@
65.22 val extract = Rules.CONTEXT_REWRITE_RULE
65.23 (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
65.24 val (rules, TCs) = ListPair.unzip (map extract corollaries')
65.25 - val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
65.26 + val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
65.27 val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
65.28 val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
65.29 in
65.30 @@ -460,7 +460,8 @@
65.31 *---------------------------------------------------------------------------*)
65.32
65.33 fun wfrec_eqns thy fid tflCongs eqns =
65.34 - let val {lhs,rhs} = USyntax.dest_eq (hd eqns)
65.35 + let val ctxt = Proof_Context.init_global thy
65.36 + val {lhs,rhs} = USyntax.dest_eq (hd eqns)
65.37 val (f,args) = USyntax.strip_comb lhs
65.38 val (fname,fty) = dest_atom f
65.39 val (SV,a) = front_last args (* SV = schematic variables *)
65.40 @@ -493,7 +494,7 @@
65.41 val R1 = USyntax.rand WFR
65.42 val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
65.43 val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
65.44 - val corollaries' = map (rewrite_rule case_rewrites) corollaries
65.45 + val corollaries' = map (rewrite_rule ctxt case_rewrites) corollaries
65.46 fun extract X = Rules.CONTEXT_REWRITE_RULE
65.47 (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
65.48 in {proto_def = proto_def,
65.49 @@ -625,6 +626,7 @@
65.50
65.51 fun mk_case ty_info usednames thy =
65.52 let
65.53 + val ctxt = Proof_Context.init_global thy
65.54 val divide = ipartition (gvvariant usednames)
65.55 val tych = Thry.typecheck thy
65.56 fun tych_binding(x,y) = (tych x, tych y)
65.57 @@ -657,7 +659,7 @@
65.58 (new_formals, disjuncts)
65.59 val constraints = map #1 existentials
65.60 val vexl = map #2 existentials
65.61 - fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS [Rules.ASSUME (tych tm)] th, b))
65.62 + fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
65.63 val news = map (fn (nf,rows,c) => {path = nf@rstp,
65.64 rows = map (expnd c) rows})
65.65 (Utils.zip3 new_formals groups constraints)
65.66 @@ -675,7 +677,8 @@
65.67
65.68
65.69 fun complete_cases thy =
65.70 - let val tych = Thry.typecheck thy
65.71 + let val ctxt = Proof_Context.init_global thy
65.72 + val tych = Thry.typecheck thy
65.73 val ty_info = Thry.induct_info thy
65.74 in fn pats =>
65.75 let val names = List.foldr Misc_Legacy.add_term_names [] pats
65.76 @@ -691,7 +694,7 @@
65.77 val rows = map (fn x => ([x], (th0,[]))) pats
65.78 in
65.79 Rules.GEN (tych a)
65.80 - (Rules.RIGHT_ASSOC
65.81 + (Rules.RIGHT_ASSOC ctxt
65.82 (Rules.CHOOSE(tych v, ex_th0)
65.83 (mk_case ty_info (vname::aname::names)
65.84 thy {path=[v], rows=rows})))
65.85 @@ -826,7 +829,8 @@
65.86 * the antecedent of Rinduct.
65.87 *---------------------------------------------------------------------------*)
65.88 fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
65.89 -let val tych = Thry.typecheck thy
65.90 +let val ctxt = Proof_Context.init_global thy
65.91 + val tych = Thry.typecheck thy
65.92 val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
65.93 val (pats,TCsl) = ListPair.unzip pat_TCs_list
65.94 val case_thm = complete_cases thy pats
65.95 @@ -848,7 +852,7 @@
65.96 domain)
65.97 val vtyped = tych v
65.98 val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
65.99 - val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
65.100 + val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
65.101 (substs, proved_cases)
65.102 val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
65.103 val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
66.1 --- a/src/HOL/Tools/choice_specification.ML Fri Dec 13 23:53:02 2013 +0100
66.2 +++ b/src/HOL/Tools/choice_specification.ML Sat Dec 14 17:28:05 2013 +0100
66.3 @@ -113,6 +113,8 @@
66.4
66.5 fun process_spec axiomatic cos alt_props thy =
66.6 let
66.7 + val ctxt = Proof_Context.init_global thy
66.8 +
66.9 fun zip3 [] [] [] = []
66.10 | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
66.11 | zip3 _ _ _ = error "Choice_Specification.process_spec internal error"
66.12 @@ -122,7 +124,7 @@
66.13 | myfoldr f [] = error "Choice_Specification.process_spec internal error"
66.14
66.15 val rew_imps = alt_props |>
66.16 - map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
66.17 + map (Object_Logic.atomize ctxt o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
66.18 val props' = rew_imps |>
66.19 map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
66.20
67.1 --- a/src/HOL/Tools/coinduction.ML Fri Dec 13 23:53:02 2013 +0100
67.2 +++ b/src/HOL/Tools/coinduction.ML Sat Dec 14 17:28:05 2013 +0100
67.3 @@ -53,9 +53,9 @@
67.4 val cases = Rule_Cases.get raw_thm |> fst
67.5 in
67.6 NO_CASES (HEADGOAL (
67.7 - Object_Logic.rulify_tac THEN'
67.8 + Object_Logic.rulify_tac ctxt THEN'
67.9 Method.insert_tac prems THEN'
67.10 - Object_Logic.atomize_prems_tac THEN'
67.11 + Object_Logic.atomize_prems_tac ctxt THEN'
67.12 DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
67.13 let
67.14 val vars = raw_vars @ map (term_of o snd) params;
67.15 @@ -110,7 +110,7 @@
67.16 unfold_thms_tac ctxt eqs
67.17 end)) ctxt)))])
67.18 end) ctxt) THEN'
67.19 - K (prune_params_tac))) st
67.20 + K (prune_params_tac ctxt))) st
67.21 |> Seq.maps (fn (_, st) =>
67.22 CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
67.23 end;
68.1 --- a/src/HOL/Tools/groebner.ML Fri Dec 13 23:53:02 2013 +0100
68.2 +++ b/src/HOL/Tools/groebner.ML Sat Dec 14 17:28:05 2013 +0100
68.3 @@ -928,7 +928,7 @@
68.4 delsimps del_thms addsimps add_thms);
68.5
68.6 fun ring_tac add_ths del_ths ctxt =
68.7 - Object_Logic.full_atomize_tac
68.8 + Object_Logic.full_atomize_tac ctxt
68.9 THEN' presimplify ctxt add_ths del_ths
68.10 THEN' CSUBGOAL (fn (p, i) =>
68.11 rtac (let val form = Object_Logic.dest_judgment p
68.12 @@ -970,7 +970,7 @@
68.13 end
68.14 in
68.15 clarify_tac (put_claset claset ctxt) i
68.16 - THEN Object_Logic.full_atomize_tac i
68.17 + THEN Object_Logic.full_atomize_tac ctxt i
68.18 THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i
68.19 THEN clarify_tac (put_claset claset ctxt) i
68.20 THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i))
69.1 --- a/src/HOL/Tools/inductive.ML Fri Dec 13 23:53:02 2013 +0100
69.2 +++ b/src/HOL/Tools/inductive.ML Sat Dec 14 17:28:05 2013 +0100
69.3 @@ -396,7 +396,7 @@
69.4
69.5 val intrs = map_index (fn (i, intr) =>
69.6 Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
69.7 - [rewrite_goals_tac rec_preds_defs,
69.8 + [rewrite_goals_tac ctxt rec_preds_defs,
69.9 rtac (unfold RS iffD2) 1,
69.10 EVERY1 (select_disj (length intr_ts) (i + 1)),
69.11 (*Not ares_tac, since refl must be tried before any equality assumptions;
69.12 @@ -440,14 +440,15 @@
69.13 map mk_elim_prem (map #1 c_intrs)
69.14 in
69.15 (Goal.prove_sorry ctxt'' [] prems P
69.16 - (fn {prems, ...} => EVERY
69.17 + (fn {context = ctxt4, prems} => EVERY
69.18 [cut_tac (hd prems) 1,
69.19 - rewrite_goals_tac rec_preds_defs,
69.20 + rewrite_goals_tac ctxt4 rec_preds_defs,
69.21 dtac (unfold RS iffD1) 1,
69.22 REPEAT (FIRSTGOAL (eresolve_tac rules1)),
69.23 REPEAT (FIRSTGOAL (eresolve_tac rules2)),
69.24 EVERY (map (fn prem =>
69.25 - DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
69.26 + DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
69.27 + (tl prems))])
69.28 |> singleton (Proof_Context.export ctxt'' ctxt'''),
69.29 map #2 c_intrs, length Ts)
69.30 end
69.31 @@ -503,12 +504,12 @@
69.32 (if null ts andalso null us then rtac intr 1
69.33 else
69.34 EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
69.35 - Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
69.36 + Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
69.37 let
69.38 val (eqs, prems') = chop (length us) prems;
69.39 val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
69.40 in
69.41 - rewrite_goal_tac rew_thms 1 THEN
69.42 + rewrite_goal_tac ctxt'' rew_thms 1 THEN
69.43 rtac intr 1 THEN
69.44 EVERY (map (fn p => rtac p 1) prems')
69.45 end) ctxt' 1);
69.46 @@ -545,7 +546,7 @@
69.47
69.48 in
69.49
69.50 -fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
69.51 +fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac ctxt;
69.52
69.53 fun mk_cases ctxt prop =
69.54 let
69.55 @@ -598,7 +599,7 @@
69.56 val props = Syntax.read_props ctxt' raw_props;
69.57 val ctxt'' = fold Variable.declare_term props ctxt';
69.58 val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
69.59 - in Method.erule 0 rules end))
69.60 + in Method.erule ctxt 0 rules end))
69.61 "dynamic case analysis on predicates";
69.62
69.63
69.64 @@ -724,30 +725,30 @@
69.65 val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct});
69.66
69.67 val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
69.68 - (fn {prems, ...} => EVERY
69.69 - [rewrite_goals_tac [inductive_conj_def],
69.70 + (fn {context = ctxt3, prems} => EVERY
69.71 + [rewrite_goals_tac ctxt3 [inductive_conj_def],
69.72 DETERM (rtac raw_fp_induct 1),
69.73 REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
69.74 - rewrite_goals_tac simp_thms2,
69.75 + rewrite_goals_tac ctxt3 simp_thms2,
69.76 (*This disjE separates out the introduction rules*)
69.77 REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
69.78 (*Now break down the individual cases. No disjE here in case
69.79 some premise involves disjunction.*)
69.80 - REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
69.81 + REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)),
69.82 REPEAT (FIRSTGOAL
69.83 (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
69.84 - EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
69.85 + EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
69.86 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
69.87 conjI, refl] 1)) prems)]);
69.88
69.89 val lemma = Goal.prove_sorry ctxt'' [] []
69.90 - (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
69.91 - [rewrite_goals_tac rec_preds_defs,
69.92 + (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
69.93 + [rewrite_goals_tac ctxt3 rec_preds_defs,
69.94 REPEAT (EVERY
69.95 [REPEAT (resolve_tac [conjI, impI] 1),
69.96 REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
69.97 atac 1,
69.98 - rewrite_goals_tac simp_thms1,
69.99 + rewrite_goals_tac ctxt3 simp_thms1,
69.100 atac 1])]);
69.101
69.102 in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
69.103 @@ -961,9 +962,9 @@
69.104 (if no_ind then Drule.asm_rl
69.105 else if coind then
69.106 singleton (Proof_Context.export lthy2 lthy1)
69.107 - (rotate_prems ~1 (Object_Logic.rulify
69.108 - (fold_rule rec_preds_defs
69.109 - (rewrite_rule simp_thms3
69.110 + (rotate_prems ~1 (Object_Logic.rulify lthy2
69.111 + (fold_rule lthy2 rec_preds_defs
69.112 + (rewrite_rule lthy2 simp_thms3
69.113 (mono RS (fp_def RS @{thm def_coinduct}))))))
69.114 else
69.115 prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
70.1 --- a/src/HOL/Tools/inductive_realizer.ML Fri Dec 13 23:53:02 2013 +0100
70.2 +++ b/src/HOL/Tools/inductive_realizer.ML Sat Dec 14 17:28:05 2013 +0100
70.3 @@ -393,11 +393,11 @@
70.4 val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
70.5 val thm = Goal.prove_global thy []
70.6 (map attach_typeS prems) (attach_typeS concl)
70.7 - (fn {prems, ...} => EVERY
70.8 + (fn {context = ctxt, prems} => EVERY
70.9 [rtac (#raw_induct ind_info) 1,
70.10 - rewrite_goals_tac rews,
70.11 + rewrite_goals_tac ctxt rews,
70.12 REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
70.13 - [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
70.14 + [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
70.15 DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
70.16 val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
70.17 (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
70.18 @@ -459,8 +459,8 @@
70.19 [cut_tac (hd prems) 1,
70.20 etac elimR 1,
70.21 ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
70.22 - rewrite_goals_tac rews,
70.23 - REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
70.24 + rewrite_goals_tac ctxt rews,
70.25 + REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
70.26 DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
70.27 val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
70.28 (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
71.1 --- a/src/HOL/Tools/lin_arith.ML Fri Dec 13 23:53:02 2013 +0100
71.2 +++ b/src/HOL/Tools/lin_arith.ML Sat Dec 14 17:28:05 2013 +0100
71.3 @@ -871,8 +871,9 @@
71.4
71.5 in
71.6
71.7 -fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
71.8 - Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
71.9 +fun gen_tac ex ctxt =
71.10 + FIRST' [simple_tac ctxt,
71.11 + Object_Logic.full_atomize_tac ctxt THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
71.12
71.13 val tac = gen_tac true;
71.14
72.1 --- a/src/HOL/Tools/nat_arith.ML Fri Dec 13 23:53:02 2013 +0100
72.2 +++ b/src/HOL/Tools/nat_arith.ML Sat Dec 14 17:28:05 2013 +0100
72.3 @@ -6,10 +6,10 @@
72.4
72.5 signature NAT_ARITH =
72.6 sig
72.7 - val cancel_diff_conv: conv
72.8 - val cancel_eq_conv: conv
72.9 - val cancel_le_conv: conv
72.10 - val cancel_less_conv: conv
72.11 + val cancel_diff_conv: Proof.context -> conv
72.12 + val cancel_eq_conv: Proof.context -> conv
72.13 + val cancel_le_conv: Proof.context -> conv
72.14 + val cancel_less_conv: Proof.context -> conv
72.15 end;
72.16
72.17 structure Nat_Arith: NAT_ARITH =
72.18 @@ -26,9 +26,9 @@
72.19
72.20 val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
72.21
72.22 -fun move_to_front path = Conv.every_conv
72.23 +fun move_to_front ctxt path = Conv.every_conv
72.24 [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
72.25 - Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
72.26 + Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
72.27
72.28 fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
72.29 add_atoms (add1::path) x #> add_atoms (add2::path) y
72.30 @@ -54,12 +54,12 @@
72.31 find (sort ord' xs) (sort ord' ys)
72.32 end
72.33
72.34 -fun cancel_conv rule ct =
72.35 +fun cancel_conv rule ctxt ct =
72.36 let
72.37 val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
72.38 val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
72.39 - val lconv = move_to_front lpath
72.40 - val rconv = move_to_front rpath
72.41 + val lconv = move_to_front ctxt lpath
72.42 + val rconv = move_to_front ctxt rpath
72.43 val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
72.44 val conv = conv1 then_conv Conv.rewr_conv rule
72.45 in conv ct end
73.1 --- a/src/HOL/Tools/record.ML Fri Dec 13 23:53:02 2013 +0100
73.2 +++ b/src/HOL/Tools/record.ML Sat Dec 14 17:28:05 2013 +0100
73.3 @@ -1616,9 +1616,9 @@
73.4
73.5 val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
73.6 Goal.prove_sorry_global defs_thy [] [] split_meta_prop
73.7 - (fn _ =>
73.8 + (fn {context = ctxt, ...} =>
73.9 EVERY1
73.10 - [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
73.11 + [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
73.12 etac @{thm meta_allE}, atac,
73.13 rtac (@{thm prop_subst} OF [surject]),
73.14 REPEAT o etac @{thm meta_allE}, atac]));
73.15 @@ -1742,12 +1742,13 @@
73.16 HOLogic.mk_Trueprop (HOLogic.mk_eq
73.17 (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
73.18 Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
73.19 - fun tac eq_def =
73.20 + fun tac ctxt eq_def =
73.21 Class.intro_classes_tac []
73.22 - THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
73.23 + THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
73.24 THEN ALLGOALS (rtac @{thm refl});
73.25 fun mk_eq thy eq_def =
73.26 - rewrite_rule [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
73.27 + rewrite_rule (Proof_Context.init_global thy)
73.28 + [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
73.29 fun mk_eq_refl thy =
73.30 @{thm equal_refl}
73.31 |> Thm.instantiate
73.32 @@ -1765,8 +1766,7 @@
73.33 |-> (fn eq => Specification.definition
73.34 (NONE, (Attrib.empty_binding, eq)))
73.35 |-> (fn (_, (_, eq_def)) =>
73.36 - Class.prove_instantiation_exit_result Morphism.thm
73.37 - (fn _ => fn eq_def => tac eq_def) eq_def)
73.38 + Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
73.39 |-> (fn eq_def => fn thy =>
73.40 thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
73.41 |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
73.42 @@ -2139,18 +2139,18 @@
73.43
73.44 val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
73.45 Goal.prove_sorry_global defs_thy [] [] split_meta_prop
73.46 - (fn _ =>
73.47 + (fn {context = ctxt', ...} =>
73.48 EVERY1
73.49 - [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
73.50 + [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
73.51 etac @{thm meta_allE}, atac,
73.52 rtac (@{thm prop_subst} OF [surjective]),
73.53 REPEAT o etac @{thm meta_allE}, atac]));
73.54
73.55 val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
73.56 Goal.prove_sorry_global defs_thy [] [] split_object_prop
73.57 - (fn _ =>
73.58 + (fn {context = ctxt, ...} =>
73.59 rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
73.60 - rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
73.61 + rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN
73.62 rtac split_meta 1));
73.63
73.64 val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
74.1 --- a/src/HOL/Tools/sat_funcs.ML Fri Dec 13 23:53:02 2013 +0100
74.2 +++ b/src/HOL/Tools/sat_funcs.ML Sat Dec 14 17:28:05 2013 +0100
74.3 @@ -427,9 +427,9 @@
74.4 (* subgoal *)
74.5 (* ------------------------------------------------------------------------- *)
74.6
74.7 -val pre_cnf_tac =
74.8 +fun pre_cnf_tac ctxt =
74.9 rtac ccontr THEN'
74.10 - Object_Logic.atomize_prems_tac THEN'
74.11 + Object_Logic.atomize_prems_tac ctxt THEN'
74.12 CONVERSION Drule.beta_eta_conversion;
74.13
74.14 (* ------------------------------------------------------------------------- *)
74.15 @@ -460,7 +460,7 @@
74.16 (* ------------------------------------------------------------------------- *)
74.17
74.18 fun sat_tac ctxt i =
74.19 - pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
74.20 + pre_cnf_tac ctxt i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
74.21
74.22 (* ------------------------------------------------------------------------- *)
74.23 (* satx_tac: tactic for calling an external SAT solver, taking as input an *)
74.24 @@ -469,6 +469,6 @@
74.25 (* ------------------------------------------------------------------------- *)
74.26
74.27 fun satx_tac ctxt i =
74.28 - pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
74.29 + pre_cnf_tac ctxt i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
74.30
74.31 end;
75.1 --- a/src/HOL/Tools/simpdata.ML Fri Dec 13 23:53:02 2013 +0100
75.2 +++ b/src/HOL/Tools/simpdata.ML Sat Dec 14 17:28:05 2013 +0100
75.3 @@ -71,10 +71,10 @@
75.4 Goal.prove_global (Thm.theory_of_thm st) []
75.5 [mk_simp_implies @{prop "(x::'a) == y"}]
75.6 (mk_simp_implies @{prop "(x::'a) = y"})
75.7 - (fn {prems, ...} => EVERY
75.8 - [rewrite_goals_tac @{thms simp_implies_def},
75.9 + (fn {context = ctxt, prems} => EVERY
75.10 + [rewrite_goals_tac ctxt @{thms simp_implies_def},
75.11 REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
75.12 - map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
75.13 + map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
75.14 end
75.15 end;
75.16
76.1 --- a/src/HOL/Tools/transfer.ML Fri Dec 13 23:53:02 2013 +0100
76.2 +++ b/src/HOL/Tools/transfer.ML Sat Dec 14 17:28:05 2013 +0100
76.3 @@ -193,7 +193,7 @@
76.4 by (unfold is_equality_def, rule, drule meta_spec,
76.5 erule meta_mp, rule refl, simp)}
76.6
76.7 -fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
76.8 +fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
76.9 let
76.10 val thy = Thm.theory_of_thm thm
76.11 val prop = Thm.prop_of thm
76.12 @@ -212,7 +212,7 @@
76.13 val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
76.14 val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
76.15 val cprop = Thm.cterm_of thy prop2
76.16 - val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop
76.17 + val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
76.18 fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
76.19 in
76.20 forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
76.21 @@ -234,11 +234,11 @@
76.22 Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
76.23 handle CTERM _ => thm
76.24 in
76.25 - gen_abstract_equalities dest contracted_eq_thm
76.26 + gen_abstract_equalities ctxt dest contracted_eq_thm
76.27 end
76.28
76.29 -fun abstract_equalities_relator_eq rel_eq_thm =
76.30 - gen_abstract_equalities (fn x => (x, I))
76.31 +fun abstract_equalities_relator_eq ctxt rel_eq_thm =
76.32 + gen_abstract_equalities ctxt (fn x => (x, I))
76.33 (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
76.34
76.35 fun abstract_equalities_domain ctxt thm =
76.36 @@ -256,7 +256,7 @@
76.37 val contracted_eq_thm =
76.38 Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
76.39 in
76.40 - gen_abstract_equalities dest contracted_eq_thm
76.41 + gen_abstract_equalities ctxt dest contracted_eq_thm
76.42 end
76.43
76.44
76.45 @@ -288,7 +288,7 @@
76.46 | t => t)
76.47 end
76.48
76.49 -fun gen_abstract_domains (dest : term -> term * (term -> term)) thm =
76.50 +fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
76.51 let
76.52 val thy = Thm.theory_of_thm thm
76.53 val prop = Thm.prop_of thm
76.54 @@ -305,14 +305,14 @@
76.55 val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
76.56 val prop2 = Logic.list_rename_params (rev names) prop1
76.57 val cprop = Thm.cterm_of thy prop2
76.58 - val equal_thm = Raw_Simplifier.rewrite false [Domainp_lemma] cprop
76.59 + val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
76.60 fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
76.61 in
76.62 forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
76.63 end
76.64 handle TERM _ => thm
76.65
76.66 -fun abstract_domains_transfer thm =
76.67 +fun abstract_domains_transfer ctxt thm =
76.68 let
76.69 fun dest prop =
76.70 let
76.71 @@ -324,7 +324,7 @@
76.72 Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
76.73 end
76.74 in
76.75 - gen_abstract_domains dest thm
76.76 + gen_abstract_domains ctxt dest thm
76.77 end
76.78
76.79 fun detect_transfer_rules thm =
76.80 @@ -587,11 +587,11 @@
76.81 handle TERM (_, ts) => raise TERM (err_msg, ts)
76.82 in
76.83 EVERY
76.84 - [rewrite_goal_tac pre_simps i THEN
76.85 + [rewrite_goal_tac ctxt pre_simps i THEN
76.86 SUBGOAL main_tac i,
76.87 (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
76.88 - rewrite_goal_tac post_simps i,
76.89 - Goal.norm_hhf_tac i]
76.90 + rewrite_goal_tac ctxt post_simps i,
76.91 + Goal.norm_hhf_tac ctxt i]
76.92 end
76.93
76.94 fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
76.95 @@ -626,7 +626,7 @@
76.96 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
76.97 val thm2 = thm1
76.98 |> Thm.certify_instantiate (instT, [])
76.99 - |> Raw_Simplifier.rewrite_rule pre_simps
76.100 + |> Raw_Simplifier.rewrite_rule ctxt pre_simps
76.101 val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
76.102 val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
76.103 val rule = transfer_rule_of_lhs ctxt' t
76.104 @@ -641,7 +641,7 @@
76.105 val tnames = map (fst o dest_TFree o snd) instT
76.106 in
76.107 thm3
76.108 - |> Raw_Simplifier.rewrite_rule post_simps
76.109 + |> Raw_Simplifier.rewrite_rule ctxt' post_simps
76.110 |> Raw_Simplifier.norm_hhf
76.111 |> Drule.generalize (tnames, [])
76.112 |> Drule.zero_var_indexes
76.113 @@ -662,7 +662,7 @@
76.114 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
76.115 val thm2 = thm1
76.116 |> Thm.certify_instantiate (instT, [])
76.117 - |> Raw_Simplifier.rewrite_rule pre_simps
76.118 + |> Raw_Simplifier.rewrite_rule ctxt pre_simps
76.119 val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
76.120 val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
76.121 val rule = transfer_rule_of_term ctxt' true t
76.122 @@ -677,7 +677,7 @@
76.123 val tnames = map (fst o dest_TFree o snd) instT
76.124 in
76.125 thm3
76.126 - |> Raw_Simplifier.rewrite_rule post_simps
76.127 + |> Raw_Simplifier.rewrite_rule ctxt' post_simps
76.128 |> Raw_Simplifier.norm_hhf
76.129 |> Drule.generalize (tnames, [])
76.130 |> Drule.zero_var_indexes
76.131 @@ -700,8 +700,8 @@
76.132
76.133 (* Attribute for transfer rules *)
76.134
76.135 -fun prep_rule ctxt thm =
76.136 - (abstract_domains_transfer o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv) thm
76.137 +fun prep_rule ctxt =
76.138 + abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
76.139
76.140 val transfer_add =
76.141 Thm.declaration_attribute (fn thm => fn ctxt =>
76.142 @@ -742,10 +742,14 @@
76.143 val relator_eq_setup =
76.144 let
76.145 val name = @{binding relator_eq}
76.146 - fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
76.147 - #> Data.map (map_relator_eq_raw (Item_Net.update (abstract_equalities_relator_eq thm)))
76.148 - fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
76.149 - #> Data.map (map_relator_eq_raw (Item_Net.remove (abstract_equalities_relator_eq thm)))
76.150 + fun add_thm thm context = context
76.151 + |> Data.map (map_relator_eq (Item_Net.update thm))
76.152 + |> Data.map (map_relator_eq_raw
76.153 + (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
76.154 + fun del_thm thm context = context
76.155 + |> Data.map (map_relator_eq (Item_Net.remove thm))
76.156 + |> Data.map (map_relator_eq_raw
76.157 + (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
76.158 val add = Thm.declaration_attribute add_thm
76.159 val del = Thm.declaration_attribute del_thm
76.160 val text = "declaration of relator equality rule (used by transfer method)"
77.1 --- a/src/HOL/Word/Word.thy Fri Dec 13 23:53:02 2013 +0100
77.2 +++ b/src/HOL/Word/Word.thy Sat Dec 14 17:28:05 2013 +0100
77.3 @@ -1463,7 +1463,7 @@
77.4 (put_simpset HOL_ss ctxt
77.5 |> fold Splitter.add_split @{thms uint_splits}
77.6 |> fold Simplifier.add_cong @{thms power_False_cong})),
77.7 - rewrite_goals_tac @{thms word_size},
77.8 + rewrite_goals_tac ctxt @{thms word_size},
77.9 ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN
77.10 REPEAT (etac conjE n) THEN
77.11 REPEAT (dtac @{thm word_of_int_inverse} n
77.12 @@ -1964,7 +1964,7 @@
77.13 (put_simpset HOL_ss ctxt
77.14 |> fold Splitter.add_split @{thms unat_splits}
77.15 |> fold Simplifier.add_cong @{thms power_False_cong})),
77.16 - rewrite_goals_tac @{thms word_size},
77.17 + rewrite_goals_tac ctxt @{thms word_size},
77.18 ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN
77.19 REPEAT (etac conjE n) THEN
77.20 REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
78.1 --- a/src/Provers/blast.ML Fri Dec 13 23:53:02 2013 +0100
78.2 +++ b/src/Provers/blast.ML Sat Dec 14 17:28:05 2013 +0100
78.3 @@ -1265,7 +1265,7 @@
78.4
78.5 fun depth_tac ctxt lim i st =
78.6 SELECT_GOAL
78.7 - (Object_Logic.atomize_prems_tac 1 THEN
78.8 + (Object_Logic.atomize_prems_tac ctxt 1 THEN
78.9 raw_blast (Timing.start ()) ctxt lim) i st;
78.10
78.11 fun blast_tac ctxt i st =
78.12 @@ -1274,7 +1274,7 @@
78.13 val lim = Config.get ctxt depth_limit;
78.14 in
78.15 SELECT_GOAL
78.16 - (Object_Logic.atomize_prems_tac 1 THEN
78.17 + (Object_Logic.atomize_prems_tac ctxt 1 THEN
78.18 DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
78.19 end;
78.20
79.1 --- a/src/Provers/clasimp.ML Fri Dec 13 23:53:02 2013 +0100
79.2 +++ b/src/Provers/clasimp.ML Sat Dec 14 17:28:05 2013 +0100
79.3 @@ -150,7 +150,7 @@
79.4 TRY (Classical.safe_tac ctxt) THEN
79.5 REPEAT_DETERM (FIRSTGOAL main_tac) THEN
79.6 TRY (Classical.safe_tac (addSss ctxt)) THEN
79.7 - prune_params_tac
79.8 + prune_params_tac ctxt
79.9 end;
79.10
79.11 fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
80.1 --- a/src/Provers/classical.ML Fri Dec 13 23:53:02 2013 +0100
80.2 +++ b/src/Provers/classical.ML Sat Dec 14 17:28:05 2013 +0100
80.3 @@ -166,7 +166,13 @@
80.4 else rule;
80.5
80.6 (*flatten nested meta connectives in prems*)
80.7 -val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
80.8 +fun flat_rule opt_context th =
80.9 + let
80.10 + val ctxt =
80.11 + (case opt_context of
80.12 + NONE => Proof_Context.init_global (Thm.theory_of_thm th)
80.13 + | SOME context => Context.proof_of context);
80.14 + in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
80.15
80.16
80.17 (*** Useful tactics for classical reasoning ***)
80.18 @@ -325,7 +331,7 @@
80.19 if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
80.20 else
80.21 let
80.22 - val th' = flat_rule th;
80.23 + val th' = flat_rule context th;
80.24 val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
80.25 List.partition Thm.no_prems [th'];
80.26 val nI = Item_Net.length safeIs + 1;
80.27 @@ -354,7 +360,7 @@
80.28 error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
80.29 else
80.30 let
80.31 - val th' = classical_rule (flat_rule th);
80.32 + val th' = classical_rule (flat_rule context th);
80.33 val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
80.34 List.partition (fn rl => nprems_of rl=1) [th'];
80.35 val nI = Item_Net.length safeIs;
80.36 @@ -386,7 +392,7 @@
80.37 if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
80.38 else
80.39 let
80.40 - val th' = flat_rule th;
80.41 + val th' = flat_rule context th;
80.42 val nI = Item_Net.length hazIs + 1;
80.43 val nE = Item_Net.length hazEs;
80.44 val _ = warn_claset context th cs;
80.45 @@ -415,7 +421,7 @@
80.46 error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
80.47 else
80.48 let
80.49 - val th' = classical_rule (flat_rule th);
80.50 + val th' = classical_rule (flat_rule context th);
80.51 val nI = Item_Net.length hazIs;
80.52 val nE = Item_Net.length hazEs + 1;
80.53 val _ = warn_claset context th cs;
80.54 @@ -443,12 +449,12 @@
80.55 to insert.
80.56 ***)
80.57
80.58 -fun delSI th
80.59 +fun delSI context th
80.60 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
80.61 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
80.62 if Item_Net.member safeIs th then
80.63 let
80.64 - val th' = flat_rule th;
80.65 + val th' = flat_rule context th;
80.66 val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
80.67 in
80.68 CS
80.69 @@ -466,12 +472,12 @@
80.70 end
80.71 else cs;
80.72
80.73 -fun delSE th
80.74 +fun delSE context th
80.75 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
80.76 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
80.77 if Item_Net.member safeEs th then
80.78 let
80.79 - val th' = classical_rule (flat_rule th);
80.80 + val th' = classical_rule (flat_rule context th);
80.81 val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
80.82 in
80.83 CS
80.84 @@ -493,7 +499,7 @@
80.85 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
80.86 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
80.87 if Item_Net.member hazIs th then
80.88 - let val th' = flat_rule th in
80.89 + let val th' = flat_rule context th in
80.90 CS
80.91 {haz_netpair = delete ([th'], []) haz_netpair,
80.92 dup_netpair = delete ([dup_intr th'], []) dup_netpair,
80.93 @@ -511,11 +517,11 @@
80.94 handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *)
80.95 error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
80.96
80.97 -fun delE th
80.98 +fun delE context th
80.99 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
80.100 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
80.101 if Item_Net.member hazEs th then
80.102 - let val th' = classical_rule (flat_rule th) in
80.103 + let val th' = classical_rule (flat_rule context th) in
80.104 CS
80.105 {haz_netpair = delete ([], [th']) haz_netpair,
80.106 dup_netpair = delete ([], [dup_elim th']) dup_netpair,
80.107 @@ -537,7 +543,11 @@
80.108 if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
80.109 Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
80.110 Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
80.111 - then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
80.112 + then
80.113 + delSI context th
80.114 + (delSE context th
80.115 + (delI context th
80.116 + (delE context th (delSE context th' (delE context th' cs)))))
80.117 else (warn_thm context "Undeclared classical rule\n" th; cs)
80.118 end;
80.119
80.120 @@ -774,24 +784,24 @@
80.121
80.122 (*Dumb but fast*)
80.123 fun fast_tac ctxt =
80.124 - Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
80.125 + Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
80.126
80.127 (*Slower but smarter than fast_tac*)
80.128 fun best_tac ctxt =
80.129 - Object_Logic.atomize_prems_tac THEN'
80.130 + Object_Logic.atomize_prems_tac ctxt THEN'
80.131 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
80.132
80.133 (*even a bit smarter than best_tac*)
80.134 fun first_best_tac ctxt =
80.135 - Object_Logic.atomize_prems_tac THEN'
80.136 + Object_Logic.atomize_prems_tac ctxt THEN'
80.137 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
80.138
80.139 fun slow_tac ctxt =
80.140 - Object_Logic.atomize_prems_tac THEN'
80.141 + Object_Logic.atomize_prems_tac ctxt THEN'
80.142 SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
80.143
80.144 fun slow_best_tac ctxt =
80.145 - Object_Logic.atomize_prems_tac THEN'
80.146 + Object_Logic.atomize_prems_tac ctxt THEN'
80.147 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
80.148
80.149
80.150 @@ -800,13 +810,13 @@
80.151 val weight_ASTAR = 5;
80.152
80.153 fun astar_tac ctxt =
80.154 - Object_Logic.atomize_prems_tac THEN'
80.155 + Object_Logic.atomize_prems_tac ctxt THEN'
80.156 SELECT_GOAL
80.157 (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
80.158 (step_tac ctxt 1));
80.159
80.160 fun slow_astar_tac ctxt =
80.161 - Object_Logic.atomize_prems_tac THEN'
80.162 + Object_Logic.atomize_prems_tac ctxt THEN'
80.163 SELECT_GOAL
80.164 (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
80.165 (slow_step_tac ctxt 1));
80.166 @@ -901,12 +911,12 @@
80.167 in
80.168 fn st => Seq.maps (fn rule => rtac rule i st) ruleq
80.169 end)
80.170 - THEN_ALL_NEW Goal.norm_hhf_tac;
80.171 + THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
80.172
80.173 in
80.174
80.175 fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
80.176 - | rule_tac _ rules facts = Method.rule_tac rules facts;
80.177 + | rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts;
80.178
80.179 fun default_tac ctxt rules facts =
80.180 HEADGOAL (rule_tac ctxt rules facts) ORELSE
80.181 @@ -941,7 +951,7 @@
80.182 (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
80.183 "apply some intro/elim rule (potentially classical)" #>
80.184 Method.setup @{binding contradiction}
80.185 - (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])))
80.186 + (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
80.187 "proof by contradiction" #>
80.188 Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
80.189 "repeatedly apply safe steps" #>
81.1 --- a/src/Provers/splitter.ML Fri Dec 13 23:53:02 2013 +0100
81.2 +++ b/src/Provers/splitter.ML Sat Dec 14 17:28:05 2013 +0100
81.3 @@ -100,7 +100,7 @@
81.4 val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
81.5 [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
81.6 (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
81.7 - (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1)
81.8 + (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN rtac reflexive_thm 1)
81.9
81.10 val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = prop_of lift;
81.11
82.1 --- a/src/Pure/Isar/class.ML Fri Dec 13 23:53:02 2013 +0100
82.2 +++ b/src/Pure/Isar/class.ML Sat Dec 14 17:28:05 2013 +0100
82.3 @@ -656,7 +656,7 @@
82.4 | default_intro_tac _ _ = no_tac;
82.5
82.6 fun default_tac rules ctxt facts =
82.7 - HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
82.8 + HEADGOAL (Method.some_rule_tac ctxt rules facts) ORELSE
82.9 default_intro_tac ctxt facts;
82.10
82.11 val _ = Theory.setup
83.1 --- a/src/Pure/Isar/class_declaration.ML Fri Dec 13 23:53:02 2013 +0100
83.2 +++ b/src/Pure/Isar/class_declaration.ML Sat Dec 14 17:28:05 2013 +0100
83.3 @@ -58,7 +58,7 @@
83.4 (_, NONE) => all_tac
83.5 | (_, SOME intro) => ALLGOALS (rtac intro));
83.6 val tac = loc_intro_tac
83.7 - THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
83.8 + THEN ALLGOALS (Proof_Context.fact_tac empty_ctxt (sup_axioms @ the_list assm_axiom));
83.9 in Element.prove_witness empty_ctxt prop tac end) some_prop;
83.10 val some_axiom = Option.map Element.conclude_witness some_witn;
83.11
83.12 @@ -77,8 +77,10 @@
83.13 SOME eq_morph => const_morph $> eq_morph
83.14 | NONE => const_morph);
83.15 val thm'' = Morphism.thm const_eq_morph thm';
83.16 - val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
83.17 - in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (K tac) end;
83.18 + in
83.19 + Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'')
83.20 + (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm'']))
83.21 + end;
83.22 val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
83.23
83.24 (* of_class *)
84.1 --- a/src/Pure/Isar/code.ML Fri Dec 13 23:53:02 2013 +0100
84.2 +++ b/src/Pure/Isar/code.ML Sat Dec 14 17:28:05 2013 +0100
84.3 @@ -1130,9 +1130,12 @@
84.4 fun mk_prem z = Free (z, T_cong);
84.5 fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
84.6 val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
84.7 - fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
84.8 - THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
84.9 - in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end;
84.10 + in
84.11 + Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl
84.12 + (fn {context = ctxt', prems} =>
84.13 + Simplifier.rewrite_goals_tac ctxt' prems
84.14 + THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm]))
84.15 + end;
84.16
84.17 fun add_case thm thy =
84.18 let
85.1 --- a/src/Pure/Isar/element.ML Fri Dec 13 23:53:02 2013 +0100
85.2 +++ b/src/Pure/Isar/element.ML Sat Dec 14 17:28:05 2013 +0100
85.3 @@ -456,11 +456,16 @@
85.4
85.5 fun eq_morphism _ [] = NONE
85.6 | eq_morphism thy thms =
85.7 - SOME (Morphism.morphism "Element.eq_morphism"
85.8 - {binding = [],
85.9 - typ = [],
85.10 - term = [Raw_Simplifier.rewrite_term thy thms []],
85.11 - fact = [map (rewrite_rule thms)]});
85.12 + let
85.13 + (* FIXME proper context!? *)
85.14 + fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th;
85.15 + val phi =
85.16 + Morphism.morphism "Element.eq_morphism"
85.17 + {binding = [],
85.18 + typ = [],
85.19 + term = [Raw_Simplifier.rewrite_term thy thms []],
85.20 + fact = [map rewrite]};
85.21 + in SOME phi end;
85.22
85.23
85.24
86.1 --- a/src/Pure/Isar/expression.ML Fri Dec 13 23:53:02 2013 +0100
86.2 +++ b/src/Pure/Isar/expression.ML Sat Dec 14 17:28:05 2013 +0100
86.3 @@ -619,7 +619,7 @@
86.4 val bodyT = Term.fastype_of body;
86.5 in
86.6 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
86.7 - else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
86.8 + else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t))
86.9 end;
86.10
86.11 (* achieve plain syntax for locale predicates (without "PROP") *)
86.12 @@ -669,20 +669,22 @@
86.13
86.14 val cert = Thm.cterm_of defs_thy;
86.15
86.16 - val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
86.17 - rewrite_goals_tac [pred_def] THEN
86.18 - compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
86.19 - compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
86.20 + val intro = Goal.prove_global defs_thy [] norm_ts statement
86.21 + (fn {context = ctxt, ...} =>
86.22 + rewrite_goals_tac ctxt [pred_def] THEN
86.23 + compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
86.24 + compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
86.25
86.26 val conjuncts =
86.27 - (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
86.28 + (Drule.equal_elim_rule2 OF
86.29 + [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))])
86.30 |> Conjunction.elim_balanced (length ts);
86.31
86.32 val (_, axioms_ctxt) = defs_ctxt
86.33 |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
86.34 val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
86.35 Element.prove_witness axioms_ctxt t
86.36 - (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
86.37 + (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
86.38 in ((statement, intro, axioms), defs_thy) end;
86.39
86.40 in
86.41 @@ -849,7 +851,7 @@
86.42 val dep_morphs = map2 (fn (dep, morph) => fn wits =>
86.43 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
86.44 fun activate' dep_morph ctxt = activate dep_morph
86.45 - (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
86.46 + (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
86.47 in
86.48 ctxt'
86.49 |> fold activate' dep_morphs
87.1 --- a/src/Pure/Isar/generic_target.ML Fri Dec 13 23:53:02 2013 +0100
87.2 +++ b/src/Pure/Isar/generic_target.ML Sat Dec 14 17:28:05 2013 +0100
87.3 @@ -104,7 +104,7 @@
87.4 (*result*)
87.5 val def =
87.6 Thm.transitive local_def global_def
87.7 - |> Local_Defs.contract defs
87.8 + |> Local_Defs.contract lthy3 defs
87.9 (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
87.10 val ([(res_name, [res])], lthy4) = lthy3
87.11 |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
87.12 @@ -125,7 +125,7 @@
87.13 (*export assumes/defines*)
87.14 val th = Goal.norm_result raw_th;
87.15 val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
87.16 - val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
87.17 + val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
87.18
87.19 (*export fixes*)
87.20 val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
87.21 @@ -153,7 +153,7 @@
87.22 val result'' =
87.23 (fold (curry op COMP) asms' result'
87.24 handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
87.25 - |> Local_Defs.contract defs (Thm.cprop_of th)
87.26 + |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
87.27 |> Goal.norm_result
87.28 |> Global_Theory.name_thm false false name;
87.29
88.1 --- a/src/Pure/Isar/local_defs.ML Fri Dec 13 23:53:02 2013 +0100
88.2 +++ b/src/Pure/Isar/local_defs.ML Sat Dec 14 17:28:05 2013 +0100
88.3 @@ -17,7 +17,7 @@
88.4 (term * term) * Proof.context
88.5 val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm
88.6 val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm
88.7 - val contract: thm list -> cterm -> thm -> thm
88.8 + val contract: Proof.context -> thm list -> cterm -> thm -> thm
88.9 val print_rules: Proof.context -> unit
88.10 val defn_add: attribute
88.11 val defn_del: attribute
88.12 @@ -162,8 +162,8 @@
88.13 fun export_cterm inner outer ct =
88.14 export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
88.15
88.16 -fun contract defs ct th =
88.17 - th COMP (Raw_Simplifier.rewrite true defs ct COMP_INCR Drule.equal_elim_rule2);
88.18 +fun contract ctxt defs ct th =
88.19 + th COMP (Raw_Simplifier.rewrite ctxt true defs ct COMP_INCR Drule.equal_elim_rule2);
88.20
88.21
88.22
88.23 @@ -200,7 +200,7 @@
88.24
88.25 (* rewriting with object-level rules *)
88.26
88.27 -fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
88.28 +fun meta f ctxt = f ctxt o map (meta_rewrite_rule ctxt);
88.29
88.30 val unfold = meta Raw_Simplifier.rewrite_rule;
88.31 val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule;
88.32 @@ -220,10 +220,12 @@
88.33 |> conditional ? Logic.strip_imp_concl
88.34 |> (abs_def o #2 o cert_def ctxt);
88.35 fun prove ctxt' def =
88.36 - Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop (K (ALLGOALS
88.37 - (CONVERSION (meta_rewrite_conv ctxt') THEN'
88.38 - rewrite_goal_tac [def] THEN'
88.39 - resolve_tac [Drule.reflexive_thm])))
88.40 + Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop
88.41 + (fn {context = ctxt'', ...} =>
88.42 + ALLGOALS
88.43 + (CONVERSION (meta_rewrite_conv ctxt'') THEN'
88.44 + rewrite_goal_tac ctxt'' [def] THEN'
88.45 + resolve_tac [Drule.reflexive_thm]))
88.46 handle ERROR msg => cat_error msg "Failed to prove definitional specification";
88.47 in (((c, T), rhs), prove) end;
88.48
89.1 --- a/src/Pure/Isar/method.ML Fri Dec 13 23:53:02 2013 +0100
89.2 +++ b/src/Pure/Isar/method.ML Sat Dec 14 17:28:05 2013 +0100
89.3 @@ -25,7 +25,7 @@
89.4 val elim: thm list -> method
89.5 val unfold: thm list -> Proof.context -> method
89.6 val fold: thm list -> Proof.context -> method
89.7 - val atomize: bool -> method
89.8 + val atomize: bool -> Proof.context -> method
89.9 val this: method
89.10 val fact: thm list -> Proof.context -> method
89.11 val assm_tac: Proof.context -> int -> tactic
89.12 @@ -33,14 +33,14 @@
89.13 val assumption: Proof.context -> method
89.14 val rule_trace: bool Config.T
89.15 val trace: Proof.context -> thm list -> unit
89.16 - val rule_tac: thm list -> thm list -> int -> tactic
89.17 - val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
89.18 + val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
89.19 + val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
89.20 val intros_tac: thm list -> thm list -> tactic
89.21 val try_intros_tac: thm list -> thm list -> tactic
89.22 - val rule: thm list -> method
89.23 - val erule: int -> thm list -> method
89.24 - val drule: int -> thm list -> method
89.25 - val frule: int -> thm list -> method
89.26 + val rule: Proof.context -> thm list -> method
89.27 + val erule: Proof.context -> int -> thm list -> method
89.28 + val drule: Proof.context -> int -> thm list -> method
89.29 + val frule: Proof.context -> int -> thm list -> method
89.30 val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
89.31 val tactic: string * Position.T -> Proof.context -> method
89.32 val raw_tactic: string * Position.T -> Proof.context -> method
89.33 @@ -147,8 +147,10 @@
89.34
89.35 (* atomize rule statements *)
89.36
89.37 -fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
89.38 - | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
89.39 +fun atomize false ctxt =
89.40 + SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
89.41 + | atomize true ctxt =
89.42 + RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)));
89.43
89.44
89.45 (* this -- resolve facts directly *)
89.46 @@ -159,7 +161,7 @@
89.47 (* fact -- composition by facts from context *)
89.48
89.49 fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt)
89.50 - | fact rules _ = SIMPLE_METHOD' (Proof_Context.fact_tac rules);
89.51 + | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules);
89.52
89.53
89.54 (* assumption *)
89.55 @@ -208,31 +210,31 @@
89.56
89.57 local
89.58
89.59 -fun gen_rule_tac tac rules facts =
89.60 +fun gen_rule_tac tac ctxt rules facts =
89.61 (fn i => fn st =>
89.62 if null facts then tac rules i st
89.63 else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
89.64 - THEN_ALL_NEW Goal.norm_hhf_tac;
89.65 + THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
89.66
89.67 -fun gen_arule_tac tac j rules facts =
89.68 - EVERY' (gen_rule_tac tac rules facts :: replicate j assume_tac);
89.69 +fun gen_arule_tac tac ctxt j rules facts =
89.70 + EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac);
89.71
89.72 -fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
89.73 +fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) =>
89.74 let
89.75 val rules =
89.76 if not (null arg_rules) then arg_rules
89.77 else flat (Context_Rules.find_rules false facts goal ctxt)
89.78 - in trace ctxt rules; tac rules facts i end);
89.79 + in trace ctxt rules; tac ctxt rules facts i end);
89.80
89.81 -fun meth tac x = METHOD (HEADGOAL o tac x);
89.82 -fun meth' tac x y = METHOD (HEADGOAL o tac x y);
89.83 +fun meth tac x y = METHOD (HEADGOAL o tac x y);
89.84 +fun meth' tac x y z = METHOD (HEADGOAL o tac x y z);
89.85
89.86 in
89.87
89.88 val rule_tac = gen_rule_tac resolve_tac;
89.89 val rule = meth rule_tac;
89.90 val some_rule_tac = gen_some_rule_tac rule_tac;
89.91 -val some_rule = meth' some_rule_tac;
89.92 +val some_rule = meth some_rule_tac;
89.93
89.94 val erule = meth' (gen_arule_tac eresolve_tac);
89.95 val drule = meth' (gen_arule_tac dresolve_tac);
89.96 @@ -390,9 +392,9 @@
89.97
89.98 (* extra rule methods *)
89.99
89.100 -fun xrule_meth m =
89.101 +fun xrule_meth meth =
89.102 Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
89.103 - (fn (n, ths) => K (m n ths));
89.104 + (fn (n, ths) => fn ctxt => meth ctxt n ths);
89.105
89.106
89.107 (* outer parser *)
89.108 @@ -451,9 +453,10 @@
89.109 "repeatedly apply elimination rules" #>
89.110 setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
89.111 setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
89.112 - setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> (K o atomize))
89.113 + setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> atomize)
89.114 "present local premises as object-level statements" #>
89.115 - setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
89.116 + setup (Binding.name "rule") (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
89.117 + "apply some intro/elim rule" #>
89.118 setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
89.119 setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
89.120 setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
90.1 --- a/src/Pure/Isar/object_logic.ML Fri Dec 13 23:53:02 2013 +0100
90.2 +++ b/src/Pure/Isar/object_logic.ML Sat Dec 14 17:28:05 2013 +0100
90.3 @@ -21,14 +21,14 @@
90.4 val declare_atomize: attribute
90.5 val declare_rulify: attribute
90.6 val atomize_term: theory -> term -> term
90.7 - val atomize: conv
90.8 - val atomize_prems: conv
90.9 - val atomize_prems_tac: int -> tactic
90.10 - val full_atomize_tac: int -> tactic
90.11 + val atomize: Proof.context -> conv
90.12 + val atomize_prems: Proof.context -> conv
90.13 + val atomize_prems_tac: Proof.context -> int -> tactic
90.14 + val full_atomize_tac: Proof.context -> int -> tactic
90.15 val rulify_term: theory -> term -> term
90.16 - val rulify_tac: int -> tactic
90.17 - val rulify: thm -> thm
90.18 - val rulify_no_asm: thm -> thm
90.19 + val rulify_tac: Proof.context -> int -> tactic
90.20 + val rulify: Proof.context -> thm -> thm
90.21 + val rulify_no_asm: Proof.context -> thm -> thm
90.22 val rule_format: attribute
90.23 val rule_format_no_asm: attribute
90.24 end;
90.25 @@ -182,32 +182,31 @@
90.26 fun atomize_term thy =
90.27 drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
90.28
90.29 -fun atomize ct =
90.30 - Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
90.31 +fun atomize ctxt =
90.32 + Raw_Simplifier.rewrite ctxt true (get_atomize (Proof_Context.theory_of ctxt));
90.33
90.34 -fun atomize_prems ct =
90.35 +fun atomize_prems ctxt ct =
90.36 if Logic.has_meta_prems (Thm.term_of ct) then
90.37 - Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
90.38 - (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct
90.39 + Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize) ctxt ct
90.40 else Conv.all_conv ct;
90.41
90.42 -val atomize_prems_tac = CONVERSION atomize_prems;
90.43 -val full_atomize_tac = CONVERSION atomize;
90.44 +val atomize_prems_tac = CONVERSION o atomize_prems;
90.45 +val full_atomize_tac = CONVERSION o atomize;
90.46
90.47
90.48 (* rulify *)
90.49
90.50 fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
90.51 -fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
90.52 +fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
90.53
90.54 -fun gen_rulify full thm =
90.55 - Conv.fconv_rule (Raw_Simplifier.rewrite full (get_rulify (Thm.theory_of_thm thm))) thm
90.56 - |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
90.57 +fun gen_rulify full ctxt =
90.58 + Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
90.59 + #> Drule.gen_all #> Thm.strip_shyps #> Drule.zero_var_indexes;
90.60
90.61 val rulify = gen_rulify true;
90.62 val rulify_no_asm = gen_rulify false;
90.63
90.64 -val rule_format = Thm.rule_attribute (K rulify);
90.65 -val rule_format_no_asm = Thm.rule_attribute (K rulify_no_asm);
90.66 +val rule_format = Thm.rule_attribute (rulify o Context.proof_of);
90.67 +val rule_format_no_asm = Thm.rule_attribute (rulify_no_asm o Context.proof_of);
90.68
90.69 end;
91.1 --- a/src/Pure/Isar/proof.ML Fri Dec 13 23:53:02 2013 +0100
91.2 +++ b/src/Pure/Isar/proof.ML Sat Dec 14 17:28:05 2013 +0100
91.3 @@ -443,18 +443,18 @@
91.4
91.5 local
91.6
91.7 -fun finish_tac 0 = K all_tac
91.8 - | finish_tac n =
91.9 - Goal.norm_hhf_tac THEN'
91.10 +fun finish_tac _ 0 = K all_tac
91.11 + | finish_tac ctxt n =
91.12 + Goal.norm_hhf_tac ctxt THEN'
91.13 SUBGOAL (fn (goal, i) =>
91.14 if can Logic.unprotect (Logic.strip_assums_concl goal) then
91.15 - etac Drule.protectI i THEN finish_tac (n - 1) i
91.16 - else finish_tac (n - 1) (i + 1));
91.17 + etac Drule.protectI i THEN finish_tac ctxt (n - 1) i
91.18 + else finish_tac ctxt (n - 1) (i + 1));
91.19
91.20 -fun goal_tac rule =
91.21 - Goal.norm_hhf_tac THEN'
91.22 +fun goal_tac ctxt rule =
91.23 + Goal.norm_hhf_tac ctxt THEN'
91.24 rtac rule THEN'
91.25 - finish_tac (Thm.nprems_of rule);
91.26 + finish_tac ctxt (Thm.nprems_of rule);
91.27
91.28 fun FINDGOAL tac st =
91.29 let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
91.30 @@ -465,7 +465,7 @@
91.31 fun refine_goals print_rule inner raw_rules state =
91.32 let
91.33 val (outer, (_, goal)) = get_goal state;
91.34 - fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st);
91.35 + fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st);
91.36 in
91.37 raw_rules
91.38 |> Proof_Context.goal_export inner outer
92.1 --- a/src/Pure/Isar/proof_context.ML Fri Dec 13 23:53:02 2013 +0100
92.2 +++ b/src/Pure/Isar/proof_context.ML Sat Dec 14 17:28:05 2013 +0100
92.3 @@ -110,7 +110,7 @@
92.4 (term list list * (Proof.context -> Proof.context)) * Proof.context
92.5 val bind_propp_schematic_i: (term * term list) list list -> Proof.context ->
92.6 (term list list * (Proof.context -> Proof.context)) * Proof.context
92.7 - val fact_tac: thm list -> int -> tactic
92.8 + val fact_tac: Proof.context -> thm list -> int -> tactic
92.9 val some_fact_tac: Proof.context -> int -> tactic
92.10 val get_fact: Proof.context -> Facts.ref -> thm list
92.11 val get_fact_single: Proof.context -> Facts.ref -> thm
92.12 @@ -889,12 +889,12 @@
92.13
92.14 in
92.15
92.16 -fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
92.17 +fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts;
92.18
92.19 fun potential_facts ctxt prop =
92.20 Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
92.21
92.22 -fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
92.23 +fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i);
92.24
92.25 end;
92.26
92.27 @@ -913,7 +913,7 @@
92.28
92.29 val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
92.30 fun prove_fact th =
92.31 - Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac [th])));
92.32 + Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
92.33 val results = map_filter (try prove_fact) (potential_facts ctxt prop');
92.34 val res =
92.35 (case distinct Thm.eq_thm_prop results of
93.1 --- a/src/Pure/Isar/rule_cases.ML Fri Dec 13 23:53:02 2013 +0100
93.2 +++ b/src/Pure/Isar/rule_cases.ML Sat Dec 14 17:28:05 2013 +0100
93.3 @@ -31,7 +31,7 @@
93.4 val make_nested: term -> theory * term ->
93.5 ((string * string list) * string list) list -> cases
93.6 val apply: term list -> T -> T
93.7 - val consume: thm list -> thm list -> ('a * int) * thm ->
93.8 + val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
93.9 (('a * (int * thm list)) * thm) Seq.seq
93.10 val get_consumes: thm -> int
93.11 val put_consumes: int option -> thm -> thm
93.12 @@ -203,24 +203,24 @@
93.13
93.14 local
93.15
93.16 -fun unfold_prems n defs th =
93.17 +fun unfold_prems ctxt n defs th =
93.18 if null defs then th
93.19 - else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th;
93.20 + else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite ctxt true defs)) th;
93.21
93.22 -fun unfold_prems_concls defs th =
93.23 +fun unfold_prems_concls ctxt defs th =
93.24 if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
93.25 else
93.26 Conv.fconv_rule
93.27 (Conv.concl_conv ~1 (Conjunction.convs
93.28 - (Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th;
93.29 + (Conv.prems_conv ~1 (Raw_Simplifier.rewrite ctxt true defs)))) th;
93.30
93.31 in
93.32
93.33 -fun consume defs facts ((xx, n), th) =
93.34 +fun consume ctxt defs facts ((xx, n), th) =
93.35 let val m = Int.min (length facts, n) in
93.36 th
93.37 - |> unfold_prems n defs
93.38 - |> unfold_prems_concls defs
93.39 + |> unfold_prems ctxt n defs
93.40 + |> unfold_prems_concls ctxt defs
93.41 |> Drule.multi_resolve (take m facts)
93.42 |> Seq.map (pair (xx, (n - m, drop m facts)))
93.43 end;
94.1 --- a/src/Pure/Tools/find_theorems.ML Fri Dec 13 23:53:02 2013 +0100
94.2 +++ b/src/Pure/Tools/find_theorems.ML Sat Dec 14 17:28:05 2013 +0100
94.3 @@ -237,7 +237,9 @@
94.4 Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
94.5 fun try_thm thm =
94.6 if Thm.no_prems thm then rtac thm 1 goal'
94.7 - else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
94.8 + else
94.9 + (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
94.10 + 1 goal';
94.11 in
94.12 fn Internal (_, thm) =>
94.13 if is_some (Seq.pull (try_thm thm))
95.1 --- a/src/Pure/axclass.ML Fri Dec 13 23:53:02 2013 +0100
95.2 +++ b/src/Pure/axclass.ML Sat Dec 14 17:28:05 2013 +0100
95.3 @@ -291,11 +291,17 @@
95.4
95.5 fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
95.6
95.7 -fun unoverload thy = rewrite_rule (inst_thms thy);
95.8 -fun overload thy = rewrite_rule (map Thm.symmetric (inst_thms thy));
95.9 +fun unoverload thy =
95.10 + rewrite_rule (Proof_Context.init_global thy) (inst_thms thy);
95.11
95.12 -fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
95.13 -fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
95.14 +fun overload thy =
95.15 + rewrite_rule (Proof_Context.init_global thy) (map Thm.symmetric (inst_thms thy));
95.16 +
95.17 +fun unoverload_conv thy =
95.18 + Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (inst_thms thy);
95.19 +
95.20 +fun overload_conv thy =
95.21 + Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (map Thm.symmetric (inst_thms thy));
95.22
95.23 fun lookup_inst_param consts params (c, T) =
95.24 (case get_inst_tyco consts (c, T) of
96.1 --- a/src/Pure/goal.ML Fri Dec 13 23:53:02 2013 +0100
96.2 +++ b/src/Pure/goal.ML Sat Dec 14 17:28:05 2013 +0100
96.3 @@ -49,7 +49,7 @@
96.4 val conjunction_tac: int -> tactic
96.5 val precise_conjunction_tac: int -> int -> tactic
96.6 val recover_conjunction_tac: tactic
96.7 - val norm_hhf_tac: int -> tactic
96.8 + val norm_hhf_tac: Proof.context -> int -> tactic
96.9 val assume_rule_tac: Proof.context -> int -> tactic
96.10 end;
96.11
96.12 @@ -317,11 +317,11 @@
96.13
96.14 (* hhf normal form *)
96.15
96.16 -val norm_hhf_tac =
96.17 +fun norm_hhf_tac ctxt =
96.18 rtac Drule.asm_rl (*cheap approximation -- thanks to builtin Logic.flatten_params*)
96.19 THEN' SUBGOAL (fn (t, i) =>
96.20 if Drule.is_norm_hhf t then all_tac
96.21 - else rewrite_goal_tac Drule.norm_hhf_eqs i);
96.22 + else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
96.23
96.24
96.25 (* non-atomic goal assumptions *)
96.26 @@ -330,7 +330,7 @@
96.27 | non_atomic (Const ("all", _) $ _) = true
96.28 | non_atomic _ = false;
96.29
96.30 -fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
96.31 +fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
96.32 let
96.33 val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
96.34 val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
97.1 --- a/src/Pure/raw_simplifier.ML Fri Dec 13 23:53:02 2013 +0100
97.2 +++ b/src/Pure/raw_simplifier.ML Sat Dec 14 17:28:05 2013 +0100
97.3 @@ -57,13 +57,13 @@
97.4 val setSolver: Proof.context * solver -> Proof.context
97.5 val addSolver: Proof.context * solver -> Proof.context
97.6
97.7 - val rewrite_rule: thm list -> thm -> thm
97.8 - val rewrite_goals_rule: thm list -> thm -> thm
97.9 - val rewrite_goals_tac: thm list -> tactic
97.10 - val rewrite_goal_tac: thm list -> int -> tactic
97.11 - val prune_params_tac: tactic
97.12 - val fold_rule: thm list -> thm -> thm
97.13 - val fold_goals_tac: thm list -> tactic
97.14 + val rewrite_rule: Proof.context -> thm list -> thm -> thm
97.15 + val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm
97.16 + val rewrite_goals_tac: Proof.context -> thm list -> tactic
97.17 + val rewrite_goal_tac: Proof.context -> thm list -> int -> tactic
97.18 + val prune_params_tac: Proof.context -> tactic
97.19 + val fold_rule: Proof.context -> thm list -> thm -> thm
97.20 + val fold_goals_tac: Proof.context -> thm list -> tactic
97.21 val norm_hhf: thm -> thm
97.22 val norm_hhf_protect: thm -> thm
97.23 end;
97.24 @@ -126,7 +126,7 @@
97.25 (Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm
97.26 val generic_rewrite_goal_tac: bool * bool * bool ->
97.27 (Proof.context -> tactic) -> Proof.context -> int -> tactic
97.28 - val rewrite: bool -> thm list -> conv
97.29 + val rewrite: Proof.context -> bool -> thm list -> conv
97.30 end;
97.31
97.32 structure Raw_Simplifier: RAW_SIMPLIFIER =
97.33 @@ -1366,12 +1366,12 @@
97.34 val simple_prover =
97.35 SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
97.36
97.37 -fun rewrite _ [] ct = Thm.reflexive ct
97.38 - | rewrite full thms ct =
97.39 +fun rewrite _ _ [] = Thm.reflexive
97.40 + | rewrite ctxt full thms =
97.41 rewrite_cterm (full, false, false) simple_prover
97.42 - (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
97.43 + (empty_simpset ctxt addsimps thms);
97.44
97.45 -val rewrite_rule = Conv.fconv_rule o rewrite true;
97.46 +fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
97.47
97.48 (*simple term rewriting -- no proof*)
97.49 fun rewrite_term thy rules procs =
97.50 @@ -1380,15 +1380,15 @@
97.51 fun rewrite_thm mode prover ctxt = Conv.fconv_rule (rewrite_cterm mode prover ctxt);
97.52
97.53 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
97.54 -fun rewrite_goals_rule thms th =
97.55 +fun rewrite_goals_rule ctxt thms th =
97.56 Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
97.57 - (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
97.58 + (empty_simpset ctxt addsimps thms))) th;
97.59
97.60
97.61 (** meta-rewriting tactics **)
97.62
97.63 (*Rewrite all subgoals*)
97.64 -fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
97.65 +fun rewrite_goals_tac ctxt defs = PRIMITIVE (rewrite_goals_rule ctxt defs);
97.66
97.67 (*Rewrite one subgoal*)
97.68 fun generic_rewrite_goal_tac mode prover_tac ctxt i thm =
97.69 @@ -1396,12 +1396,12 @@
97.70 Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
97.71 else Seq.empty;
97.72
97.73 -fun rewrite_goal_tac rews i st =
97.74 +fun rewrite_goal_tac ctxt rews =
97.75 generic_rewrite_goal_tac (true, false, false) (K no_tac)
97.76 - (global_context (Thm.theory_of_thm st) empty_ss addsimps rews) i st;
97.77 + (empty_simpset ctxt addsimps rews);
97.78
97.79 (*Prunes all redundant parameters from the proof state by rewriting.*)
97.80 -val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
97.81 +fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
97.82
97.83
97.84 (* for folding definitions, handling critical pairs *)
97.85 @@ -1422,8 +1422,8 @@
97.86
97.87 val rev_defs = sort_lhs_depths o map Thm.symmetric;
97.88
97.89 -fun fold_rule defs = fold rewrite_rule (rev_defs defs);
97.90 -fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
97.91 +fun fold_rule ctxt defs = fold (rewrite_rule ctxt) (rev_defs defs);
97.92 +fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs));
97.93
97.94
97.95 (* HHF normal form: !! before ==>, outermost !! generalized *)
98.1 --- a/src/Sequents/S4.thy Fri Dec 13 23:53:02 2013 +0100
98.2 +++ b/src/Sequents/S4.thy Sat Dec 14 17:28:05 2013 +0100
98.3 @@ -43,7 +43,8 @@
98.4 )
98.5 *}
98.6
98.7 -method_setup S4_solve = {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *}
98.8 +method_setup S4_solve =
98.9 + {* Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2)) *}
98.10
98.11
98.12 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
99.1 --- a/src/Sequents/S43.thy Fri Dec 13 23:53:02 2013 +0100
99.2 +++ b/src/Sequents/S43.thy Sat Dec 14 17:28:05 2013 +0100
99.3 @@ -90,8 +90,8 @@
99.4
99.5
99.6 method_setup S43_solve = {*
99.7 - Scan.succeed (K (SIMPLE_METHOD
99.8 - (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
99.9 + Scan.succeed (fn ctxt => SIMPLE_METHOD
99.10 + (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3))
99.11 *}
99.12
99.13
100.1 --- a/src/Sequents/T.thy Fri Dec 13 23:53:02 2013 +0100
100.2 +++ b/src/Sequents/T.thy Sat Dec 14 17:28:05 2013 +0100
100.3 @@ -42,7 +42,7 @@
100.4 )
100.5 *}
100.6
100.7 -method_setup T_solve = {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *}
100.8 +method_setup T_solve = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (T_Prover.solve_tac ctxt 2)) *}
100.9
100.10
100.11 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
101.1 --- a/src/Sequents/modal.ML Fri Dec 13 23:53:02 2013 +0100
101.2 +++ b/src/Sequents/modal.ML Sat Dec 14 17:28:05 2013 +0100
101.3 @@ -19,7 +19,7 @@
101.4 val rule_tac : thm list -> int ->tactic
101.5 val step_tac : int -> tactic
101.6 val solven_tac : int -> int -> tactic
101.7 - val solve_tac : int -> tactic
101.8 + val solve_tac : Proof.context -> int -> tactic
101.9 end;
101.10
101.11 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER =
101.12 @@ -78,7 +78,7 @@
101.13 ((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND
101.14 (fres_bound_tac n THEN UPTOGOAL n (solven_tac (d-1)))));
101.15
101.16 -fun solve_tac d = rewrite_goals_tac Modal_Rule.rewrite_rls THEN solven_tac d 1;
101.17 +fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac d 1;
101.18
101.19 fun step_tac n =
101.20 COND (has_fewer_prems 1) all_tac
102.1 --- a/src/Tools/atomize_elim.ML Fri Dec 13 23:53:02 2013 +0100
102.2 +++ b/src/Tools/atomize_elim.ML Sat Dec 14 17:28:05 2013 +0100
102.3 @@ -59,8 +59,8 @@
102.4 (EX x y z. ...) | ... | (EX a b c. ...)
102.5 *)
102.6 fun atomize_elim_conv ctxt ct =
102.7 - (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
102.8 - then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
102.9 + (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
102.10 + then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt)
102.11 then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
102.12 then all_conv ct'
102.13 else raise CTERM ("atomize_elim", [ct', ct])))
103.1 --- a/src/Tools/case_product.ML Fri Dec 13 23:53:02 2013 +0100
103.2 +++ b/src/Tools/case_product.ML Sat Dec 14 17:28:05 2013 +0100
103.3 @@ -65,14 +65,14 @@
103.4 (concl, prems)
103.5 end
103.6
103.7 -fun case_product_tac prems struc thm1 thm2 =
103.8 +fun case_product_tac ctxt prems struc thm1 thm2 =
103.9 let
103.10 val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
103.11 val thm2' = thm2 OF p_cons2
103.12 in
103.13 rtac (thm1 OF p_cons1)
103.14 THEN' EVERY' (map (fn p =>
103.15 - rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
103.16 + rtac thm2' THEN' EVERY' (map (Proof_Context.fact_tac ctxt o single) p)) premss)
103.17 end
103.18
103.19 fun combine ctxt thm1 thm2 =
103.20 @@ -80,8 +80,9 @@
103.21 val ((i_thm1, i_thm2), ctxt') = inst_thms thm1 thm2 ctxt
103.22 val (concl, prems_rich) = build_concl_prems i_thm1 i_thm2 ctxt'
103.23 in
103.24 - Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
103.25 - case_product_tac prems prems_rich i_thm1 i_thm2 1)
103.26 + Goal.prove ctxt' [] (flat prems_rich) concl
103.27 + (fn {context = ctxt'', prems} =>
103.28 + case_product_tac ctxt'' prems prems_rich i_thm1 i_thm2 1)
103.29 |> singleton (Variable.export ctxt' ctxt)
103.30 end
103.31
104.1 --- a/src/Tools/coherent.ML Fri Dec 13 23:53:02 2013 +0100
104.2 +++ b/src/Tools/coherent.ML Sat Dec 14 17:28:05 2013 +0100
104.3 @@ -41,14 +41,14 @@
104.4
104.5 val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
104.6
104.7 -fun rulify_elim_conv ct =
104.8 +fun rulify_elim_conv ctxt ct =
104.9 if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct
104.10 else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct)))
104.11 (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
104.12 - Raw_Simplifier.rewrite true (map Thm.symmetric
104.13 + Raw_Simplifier.rewrite ctxt true (map Thm.symmetric
104.14 [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
104.15
104.16 -fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
104.17 +fun rulify_elim ctxt th = Simplifier.norm_hhf (Conv.fconv_rule (rulify_elim_conv ctxt) th);
104.18
104.19 (* Decompose elimination rule of the form
104.20 A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
104.21 @@ -66,9 +66,9 @@
104.22 (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
104.23 end;
104.24
104.25 -fun mk_rule th =
104.26 +fun mk_rule ctxt th =
104.27 let
104.28 - val th' = rulify_elim th;
104.29 + val th' = rulify_elim ctxt th;
104.30 val (prems, cases) = dest_elim (prop_of th')
104.31 in (th', prems, cases) end;
104.32
104.33 @@ -208,19 +208,19 @@
104.34
104.35 (** external interface **)
104.36
104.37 -fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
104.38 - rtac (rulify_elim_conv concl RS Drule.equal_elim_rule2) 1 THEN
104.39 - SUBPROOF (fn {prems = prems', concl, context, ...} =>
104.40 +fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
104.41 + rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
104.42 + SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
104.43 let val xs = map (term_of o #2) params @
104.44 - map (fn (_, s) => Free (s, the (Variable.default_type context s)))
104.45 - (rev (Variable.dest_fixes context)) (* FIXME !? *)
104.46 + map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
104.47 + (rev (Variable.dest_fixes ctxt'')) (* FIXME !? *)
104.48 in
104.49 - case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
104.50 + case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
104.51 (mk_dom xs) Net.empty 0 0 of
104.52 NONE => no_tac
104.53 | SOME prf =>
104.54 - rtac (thm_of_cl_prf (Proof_Context.theory_of context) concl [] prf) 1
104.55 - end) context 1) ctxt;
104.56 + rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1
104.57 + end) ctxt' 1) ctxt;
104.58
104.59 val setup = Method.setup @{binding coherent}
104.60 (Attrib.thms >> (fn rules => fn ctxt =>
105.1 --- a/src/Tools/eqsubst.ML Fri Dec 13 23:53:02 2013 +0100
105.2 +++ b/src/Tools/eqsubst.ML Sat Dec 14 17:28:05 2013 +0100
105.3 @@ -328,7 +328,7 @@
105.4 val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
105.5 val preelimrule =
105.6 RW_Inst.rw ctxt m rule pth
105.7 - |> (Seq.hd o prune_params_tac)
105.8 + |> (Seq.hd o prune_params_tac ctxt)
105.9 |> Thm.permute_prems 0 ~1 (* put old asm first *)
105.10 |> unfix_frees cfvs (* unfix any global params *)
105.11 |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
106.1 --- a/src/Tools/induct.ML Fri Dec 13 23:53:02 2013 +0100
106.2 +++ b/src/Tools/induct.ML Sat Dec 14 17:28:05 2013 +0100
106.3 @@ -60,16 +60,16 @@
106.4 val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
106.5 (term option list * thm list) * Proof.context
106.6 val atomize_term: theory -> term -> term
106.7 - val atomize_cterm: conv
106.8 - val atomize_tac: int -> tactic
106.9 - val inner_atomize_tac: int -> tactic
106.10 + val atomize_cterm: Proof.context -> conv
106.11 + val atomize_tac: Proof.context -> int -> tactic
106.12 + val inner_atomize_tac: Proof.context -> int -> tactic
106.13 val rulified_term: thm -> theory * term
106.14 - val rulify_tac: int -> tactic
106.15 + val rulify_tac: Proof.context -> int -> tactic
106.16 val simplified_rule: Proof.context -> thm -> thm
106.17 val simplify_tac: Proof.context -> int -> tactic
106.18 val trivial_tac: int -> tactic
106.19 val rotate_tac: int -> int -> int -> tactic
106.20 - val internalize: int -> thm -> thm
106.21 + val internalize: Proof.context -> int -> thm -> thm
106.22 val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
106.23 val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
106.24 thm list -> int -> cases_tactic
106.25 @@ -433,10 +433,10 @@
106.26
106.27 fun mark_constraints n ctxt = Conv.fconv_rule
106.28 (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n
106.29 - (Raw_Simplifier.rewrite false [equal_def']))) ctxt));
106.30 + (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt));
106.31
106.32 -val unmark_constraints = Conv.fconv_rule
106.33 - (Raw_Simplifier.rewrite true [Induct_Args.equal_def]);
106.34 +fun unmark_constraints ctxt =
106.35 + Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
106.36
106.37
106.38 (* simplify *)
106.39 @@ -504,11 +504,11 @@
106.40 in
106.41 fn i => fn st =>
106.42 ruleq
106.43 - |> Seq.maps (Rule_Cases.consume [] facts)
106.44 + |> Seq.maps (Rule_Cases.consume ctxt [] facts)
106.45 |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
106.46 let
106.47 val rule' = rule
106.48 - |> simp ? (simplified_rule' ctxt #> unmark_constraints);
106.49 + |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
106.50 in
106.51 CASES (Rule_Cases.make_common (thy,
106.52 Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
106.53 @@ -532,12 +532,12 @@
106.54 Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
106.55 #> Object_Logic.drop_judgment thy;
106.56
106.57 -val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
106.58 +fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
106.59
106.60 -val atomize_tac = rewrite_goal_tac Induct_Args.atomize;
106.61 +fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
106.62
106.63 -val inner_atomize_tac =
106.64 - rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
106.65 +fun inner_atomize_tac ctxt =
106.66 + rewrite_goal_tac ctxt (map Thm.symmetric conjunction_congs) THEN' atomize_tac ctxt;
106.67
106.68
106.69 (* rulify *)
106.70 @@ -553,11 +553,11 @@
106.71 val (As, B) = Logic.strip_horn (Thm.prop_of thm);
106.72 in (thy, Logic.list_implies (map rulify As, rulify B)) end;
106.73
106.74 -val rulify_tac =
106.75 - rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
106.76 - rewrite_goal_tac Induct_Args.rulify_fallback THEN'
106.77 +fun rulify_tac ctxt =
106.78 + rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
106.79 + rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
106.80 Goal.conjunction_tac THEN_ALL_NEW
106.81 - (rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
106.82 + (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
106.83
106.84
106.85 (* prepare rule *)
106.86 @@ -565,9 +565,9 @@
106.87 fun rule_instance ctxt inst rule =
106.88 Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
106.89
106.90 -fun internalize k th =
106.91 +fun internalize ctxt k th =
106.92 th |> Thm.permute_prems 0 k
106.93 - |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
106.94 + |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) (atomize_cterm ctxt));
106.95
106.96
106.97 (* guess rule instantiation -- cannot handle pending goal parameters *)
106.98 @@ -683,8 +683,10 @@
106.99 | NONE => all_tac)
106.100 end);
106.101
106.102 -fun miniscope_tac p = CONVERSION o
106.103 - Conv.params_conv p (K (Raw_Simplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
106.104 +fun miniscope_tac p =
106.105 + CONVERSION o
106.106 + Conv.params_conv p (fn ctxt =>
106.107 + Raw_Simplifier.rewrite ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
106.108
106.109 in
106.110
106.111 @@ -743,7 +745,7 @@
106.112 val thy = Proof_Context.theory_of ctxt;
106.113
106.114 val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
106.115 - val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs;
106.116 + val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
106.117
106.118 fun inst_rule (concls, r) =
106.119 (if null insts then `Rule_Cases.get r
106.120 @@ -774,7 +776,7 @@
106.121 in
106.122 (fn i => fn st =>
106.123 ruleq
106.124 - |> Seq.maps (Rule_Cases.consume (flat defs) facts)
106.125 + |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
106.126 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
106.127 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
106.128 (CONJUNCTS (ALLGOALS
106.129 @@ -791,9 +793,9 @@
106.130 else
106.131 arbitrary_tac defs_ctxt k xs)
106.132 end)
106.133 - THEN' inner_atomize_tac) j))
106.134 - THEN' atomize_tac) i st |> Seq.maps (fn st' =>
106.135 - guess_instance ctxt (internalize more_consumes rule) i st'
106.136 + THEN' inner_atomize_tac defs_ctxt) j))
106.137 + THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
106.138 + guess_instance ctxt (internalize ctxt more_consumes rule) i st'
106.139 |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
106.140 |> Seq.maps (fn rule' =>
106.141 CASES (rule_cases ctxt rule' cases)
106.142 @@ -802,7 +804,7 @@
106.143 THEN_ALL_NEW_CASES
106.144 ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
106.145 else K all_tac)
106.146 - THEN_ALL_NEW rulify_tac)
106.147 + THEN_ALL_NEW rulify_tac ctxt)
106.148 end;
106.149
106.150 val induct_tac = gen_induct_tac (K I);
106.151 @@ -849,7 +851,7 @@
106.152 in
106.153 SUBGOAL_CASES (fn (goal, i) => fn st =>
106.154 ruleq goal
106.155 - |> Seq.maps (Rule_Cases.consume [] facts)
106.156 + |> Seq.maps (Rule_Cases.consume ctxt [] facts)
106.157 |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
106.158 guess_instance ctxt rule i st
106.159 |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
107.1 --- a/src/Tools/induct_tacs.ML Fri Dec 13 23:53:02 2013 +0100
107.2 +++ b/src/Tools/induct_tacs.ML Sat Dec 14 17:28:05 2013 +0100
107.3 @@ -98,7 +98,7 @@
107.4 (_, rule) :: _ => rule
107.5 | [] => raise THM ("No induction rules", 0, [])));
107.6
107.7 - val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
107.8 + val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 (Object_Logic.atomize ctxt));
107.9 val _ = Method.trace ctxt [rule'];
107.10
107.11 val concls = Logic.dest_conjunctions (Thm.concl_of rule);
108.1 --- a/src/Tools/intuitionistic.ML Fri Dec 13 23:53:02 2013 +0100
108.2 +++ b/src/Tools/intuitionistic.ML Sat Dec 14 17:28:05 2013 +0100
108.3 @@ -89,7 +89,7 @@
108.4 Method.setup name
108.5 (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
108.6 (fn opt_lim => fn ctxt =>
108.7 - SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
108.8 + SIMPLE_METHOD' (Object_Logic.atomize_prems_tac ctxt THEN' prover_tac ctxt opt_lim)))
108.9 "intuitionistic proof search";
108.10
108.11 end;
109.1 --- a/src/ZF/Tools/cartprod.ML Fri Dec 13 23:53:02 2013 +0100
109.2 +++ b/src/ZF/Tools/cartprod.ML Sat Dec 14 17:28:05 2013 +0100
109.3 @@ -51,9 +51,9 @@
109.4 val mk_prod : typ * typ -> typ
109.5 val mk_tuple : term -> typ -> term list -> term
109.6 val pseudo_type : term -> typ
109.7 - val remove_split : thm -> thm
109.8 + val remove_split : Proof.context -> thm -> thm
109.9 val split_const : typ -> term
109.10 - val split_rule_var : term * typ * thm -> thm
109.11 + val split_rule_var : Proof.context -> term * typ * thm -> thm
109.12 end;
109.13
109.14
109.15 @@ -100,18 +100,18 @@
109.16 | mk_tuple pair T (t::_) = t;
109.17
109.18 (*Attempts to remove occurrences of split, and pair-valued parameters*)
109.19 -val remove_split = rewrite_rule [Pr.split_eq];
109.20 +fun remove_split ctxt = rewrite_rule ctxt [Pr.split_eq];
109.21
109.22 (*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
109.23 -fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
109.24 +fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) =
109.25 let val T' = factors T1 ---> T2
109.26 val newt = ap_split T1 T2 (Var(v,T'))
109.27 val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
109.28 in
109.29 - remove_split (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
109.30 + remove_split ctxt (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
109.31 cterm newt)]) rl)
109.32 end
109.33 - | split_rule_var (t,T,rl) = rl;
109.34 + | split_rule_var _ (t,T,rl) = rl;
109.35
109.36 end;
109.37
110.1 --- a/src/ZF/Tools/datatype_package.ML Fri Dec 13 23:53:02 2013 +0100
110.2 +++ b/src/ZF/Tools/datatype_package.ML Sat Dec 14 17:28:05 2013 +0100
110.3 @@ -288,8 +288,8 @@
110.4 Goal.prove_global thy1 [] []
110.5 (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
110.6 (*Proves a single case equation. Could use simp_tac, but it's slower!*)
110.7 - (fn _ => EVERY
110.8 - [rewrite_goals_tac [con_def],
110.9 + (fn {context = ctxt, ...} => EVERY
110.10 + [rewrite_goals_tac ctxt [con_def],
110.11 rtac case_trans 1,
110.12 REPEAT
110.13 (resolve_tac [@{thm refl}, split_trans,
110.14 @@ -353,9 +353,9 @@
110.15 val ctxt = Proof_Context.init_global thy;
110.16 in
110.17 Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
110.18 - (fn _ => EVERY
110.19 - [rewrite_goals_tac con_defs,
110.20 - fast_tac (put_claset ZF_cs ctxt addSEs free_SEs @ Su.free_SEs) 1])
110.21 + (fn {context = ctxt', ...} => EVERY
110.22 + [rewrite_goals_tac ctxt' con_defs,
110.23 + fast_tac (put_claset ZF_cs ctxt' addSEs free_SEs @ Su.free_SEs) 1])
110.24 end;
110.25
110.26 val simps = case_eqns @ recursor_eqns;
111.1 --- a/src/ZF/Tools/ind_cases.ML Fri Dec 13 23:53:02 2013 +0100
111.2 +++ b/src/ZF/Tools/ind_cases.ML Sat Dec 14 17:28:05 2013 +0100
111.3 @@ -58,7 +58,7 @@
111.4 val setup =
111.5 Method.setup @{binding "ind_cases"}
111.6 (Scan.lift (Scan.repeat1 Args.name_source) >>
111.7 - (fn props => fn ctxt => Method.erule 0 (map (smart_cases ctxt) props)))
111.8 + (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
111.9 "dynamic case analysis on sets";
111.10
111.11
112.1 --- a/src/ZF/Tools/inductive_package.ML Fri Dec 13 23:53:02 2013 +0100
112.2 +++ b/src/ZF/Tools/inductive_package.ML Sat Dec 14 17:28:05 2013 +0100
112.3 @@ -214,7 +214,7 @@
112.4
112.5 (*Type-checking is hardest aspect of proof;
112.6 disjIn selects the correct disjunct after unfolding*)
112.7 - fun intro_tacsf disjIn =
112.8 + fun intro_tacsf disjIn ctxt =
112.9 [DETERM (stac unfold 1),
112.10 REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
112.11 (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
112.12 @@ -223,7 +223,7 @@
112.13 backtracking may occur if the premises have extra variables!*)
112.14 DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
112.15 (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
112.16 - rewrite_goals_tac con_defs,
112.17 + rewrite_goals_tac ctxt con_defs,
112.18 REPEAT (rtac @{thm refl} 2),
112.19 (*Typechecking; this can fail*)
112.20 if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
112.21 @@ -246,7 +246,7 @@
112.22 (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
112.23 |> ListPair.map (fn (t, tacs) =>
112.24 Goal.prove_global thy1 [] [] t
112.25 - (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
112.26 + (fn {context = ctxt, ...} => EVERY (rewrite_goals_tac ctxt part_rec_defs :: tacs ctxt)));
112.27
112.28 (********)
112.29 val dummy = writeln " Proving the elimination rule...";
112.30 @@ -255,9 +255,9 @@
112.31 fun basic_elim_tac ctxt =
112.32 REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
112.33 ORELSE' bound_hyp_subst_tac ctxt))
112.34 - THEN prune_params_tac
112.35 + THEN prune_params_tac ctxt
112.36 (*Mutual recursion: collapse references to Part(D,h)*)
112.37 - THEN (PRIMITIVE (fold_rule part_rec_defs));
112.38 + THEN (PRIMITIVE (fold_rule ctxt part_rec_defs));
112.39
112.40 (*Elimination*)
112.41 val elim =
112.42 @@ -337,8 +337,8 @@
112.43 val quant_induct =
112.44 Goal.prove_global thy1 [] ind_prems
112.45 (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
112.46 - (fn {prems, ...} => EVERY
112.47 - [rewrite_goals_tac part_rec_defs,
112.48 + (fn {context = ctxt, prems} => EVERY
112.49 + [rewrite_goals_tac ctxt part_rec_defs,
112.50 rtac (@{thm impI} RS @{thm allI}) 1,
112.51 DETERM (etac raw_induct 1),
112.52 (*Push Part inside Collect*)
112.53 @@ -349,7 +349,7 @@
112.54 some premise involves disjunction.*)
112.55 REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
112.56 ORELSE' (bound_hyp_subst_tac ctxt1))),
112.57 - ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
112.58 + ind_tac (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
112.59
112.60 val dummy =
112.61 if ! Ind_Syntax.trace then
112.62 @@ -422,9 +422,9 @@
112.63 (writeln " Proving the mutual induction rule...";
112.64 Goal.prove_global thy1 [] []
112.65 (Logic.mk_implies (induct_concl, mutual_induct_concl))
112.66 - (fn _ => EVERY
112.67 - [rewrite_goals_tac part_rec_defs,
112.68 - REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
112.69 + (fn {context = ctxt, ...} => EVERY
112.70 + [rewrite_goals_tac ctxt part_rec_defs,
112.71 + REPEAT (rewrite_goals_tac ctxt [Pr.split_eq] THEN lemma_tac 1)]))
112.72 else (writeln " [ No mutual induction rule needed ]"; @{thm TrueI});
112.73
112.74 val dummy =
112.75 @@ -452,15 +452,15 @@
112.76 RLN (2,[@{thm rev_subsetD}]);
112.77
112.78 (*Minimizes backtracking by delivering the correct premise to each goal*)
112.79 - fun mutual_ind_tac [] 0 = all_tac
112.80 - | mutual_ind_tac(prem::prems) i =
112.81 + fun mutual_ind_tac _ [] 0 = all_tac
112.82 + | mutual_ind_tac ctxt (prem::prems) i =
112.83 DETERM
112.84 (SELECT_GOAL
112.85 (
112.86 (*Simplify the assumptions and goal by unfolding Part and
112.87 using freeness of the Sum constructors; proves all but one
112.88 conjunct by contradiction*)
112.89 - rewrite_goals_tac all_defs THEN
112.90 + rewrite_goals_tac ctxt all_defs THEN
112.91 simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1 THEN
112.92 IF_UNSOLVED (*simp_tac may have finished it off!*)
112.93 ((*simplify assumptions*)
112.94 @@ -471,20 +471,20 @@
112.95 THEN
112.96 (*unpackage and use "prem" in the corresponding place*)
112.97 REPEAT (rtac @{thm impI} 1) THEN
112.98 - rtac (rewrite_rule all_defs prem) 1 THEN
112.99 + rtac (rewrite_rule ctxt all_defs prem) 1 THEN
112.100 (*prem must not be REPEATed below: could loop!*)
112.101 DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
112.102 eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
112.103 ) i)
112.104 - THEN mutual_ind_tac prems (i-1);
112.105 + THEN mutual_ind_tac ctxt prems (i-1);
112.106
112.107 val mutual_induct_fsplit =
112.108 if need_mutual then
112.109 Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
112.110 mutual_induct_concl
112.111 - (fn {prems, ...} => EVERY
112.112 + (fn {context = ctxt, prems} => EVERY
112.113 [rtac (quant_induct RS lemma) 1,
112.114 - mutual_ind_tac (rev prems) (length prems)])
112.115 + mutual_ind_tac ctxt (rev prems) (length prems)])
112.116 else @{thm TrueI};
112.117
112.118 (** Uncurrying the predicate in the ordinary induction rule **)
112.119 @@ -502,9 +502,11 @@
112.120
112.121 val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
112.122
112.123 - val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
112.124 - |> Drule.export_without_context
112.125 - and mutual_induct = CP.remove_split mutual_induct_fsplit
112.126 + val induct =
112.127 + CP.split_rule_var (Proof_Context.init_global thy)
112.128 + (pred_var, elem_type-->FOLogic.oT, induct0)
112.129 + |> Drule.export_without_context
112.130 + and mutual_induct = CP.remove_split (Proof_Context.init_global thy) mutual_induct_fsplit
112.131
112.132 val ([induct', mutual_induct'], thy') =
112.133 thy
113.1 --- a/src/ZF/Tools/primrec_package.ML Fri Dec 13 23:53:02 2013 +0100
113.2 +++ b/src/ZF/Tools/primrec_package.ML Sat Dec 14 17:28:05 2013 +0100
113.3 @@ -176,7 +176,7 @@
113.4 val eqn_thms =
113.5 eqn_terms |> map (fn t =>
113.6 Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
113.7 - (fn _ => EVERY [rewrite_goals_tac rewrites, rtac @{thm refl} 1]));
113.8 + (fn {context = ctxt, ...} => EVERY [rewrite_goals_tac ctxt rewrites, rtac @{thm refl} 1]));
113.9
113.10 val (eqn_thms', thy2) =
113.11 thy1
114.1 --- a/src/ZF/UNITY/Constrains.thy Fri Dec 13 23:53:02 2013 +0100
114.2 +++ b/src/ZF/UNITY/Constrains.thy Sat Dec 14 17:28:05 2013 +0100
114.3 @@ -479,7 +479,7 @@
114.4 @{thm constrains_imp_Constrains}] 1),
114.5 rtac @{thm constrainsI} 1,
114.6 (* Three subgoals *)
114.7 - rewrite_goal_tac [@{thm st_set_def}] 3,
114.8 + rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
114.9 REPEAT (force_tac ctxt 2),
114.10 full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1,
114.11 ALLGOALS (clarify_tac ctxt),