--- a/NEWS Fri May 13 21:36:01 2011 +0200
+++ b/NEWS Fri May 13 23:59:48 2011 +0200
@@ -144,6 +144,14 @@
* Slightly more special eq_list/eq_set, with shortcut involving
pointer equality (assumes that eq relation is reflexive).
+* Classical tactics use proper Proof.context instead of historic types
+claset/clasimpset. Old-style declarations like addIs, addEs, addDs
+operate directly on Proof.context. Raw type claset retains its use as
+snapshot of the classical context, which can be recovered via
+(put_claset HOL_cs) etc. Type clasimpset has been discontinued.
+INCOMPATIBILITY, classical tactics and derived proof methods require
+proper Proof.context.
+
New in Isabelle2011 (January 2011)
--- a/doc-src/TutorialI/Protocol/Message.thy Fri May 13 21:36:01 2011 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Fri May 13 23:59:48 2011 +0200
@@ -840,31 +840,24 @@
eresolve_tac [asm_rl, @{thm synth.Inj}];
fun Fake_insert_simp_tac ss i =
- REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
fun atomic_spy_analz_tac ctxt =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- SELECT_GOAL
- (Fake_insert_simp_tac ss 1
- THEN
- IF_UNSOLVED (Blast.depth_tac
- (cs addIs [analz_insertI,
- impOfSubs analz_subset_parts]) 4 1))
- end;
+ SELECT_GOAL
+ (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
+ IF_UNSOLVED (Blast.depth_tac (ctxt addIs [analz_insertI, impOfSubs analz_subset_parts]) 4 1));
fun spy_analz_tac ctxt i =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- DETERM
- (SELECT_GOAL
- (EVERY
- [ (*push in occurrences of X...*)
- (REPEAT o CHANGED)
- (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
- (*...allowing further simplifications*)
- simp_tac ss 1,
- REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
- DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
- end;
+ DETERM
+ (SELECT_GOAL
+ (EVERY
+ [ (*push in occurrences of X...*)
+ (REPEAT o CHANGED)
+ (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+ DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
*}
text{*By default only @{text o_apply} is built-in. But in the presence of
--- a/src/CCL/Type.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/CCL/Type.thy Fri May 13 23:59:48 2011 +0200
@@ -132,7 +132,7 @@
REPEAT_SOME (eresolve_tac (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN
ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
- safe_tac (claset_of ctxt addSIs prems))
+ safe_tac (ctxt addSIs prems))
*}
method_setup ncanT = {*
@@ -397,8 +397,7 @@
ML {*
val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} =>
- (fast_tac (claset_of ctxt addIs
- (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1));
+ fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1);
*}
method_setup coinduct3 = {*
@@ -419,8 +418,8 @@
fun genIs_tac ctxt genXH gen_mono =
rtac (genXH RS @{thm iffD2}) THEN'
simp_tac (simpset_of ctxt) THEN'
- TRY o fast_tac (claset_of ctxt addIs
- [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
+ TRY o fast_tac
+ (ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
*}
method_setup genIs = {*
@@ -454,7 +453,7 @@
ML {*
fun POgen_tac ctxt (rla, rlb) i =
- SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN
+ SELECT_GOAL (safe_tac ctxt) i THEN
rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
(REPEAT (resolve_tac
(@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @
@@ -499,7 +498,7 @@
fun EQgen_tac ctxt rews i =
SELECT_GOAL
- (TRY (safe_tac (claset_of ctxt)) THEN
+ (TRY (safe_tac ctxt) THEN
resolve_tac ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN
ALLGOALS (simp_tac (simpset_of ctxt)) THEN
ALLGOALS EQgen_raw_tac) i
--- a/src/FOL/FOL.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/FOL/FOL.thy Fri May 13 23:59:48 2011 +0200
@@ -12,7 +12,6 @@
"~~/src/Provers/clasimp.ML"
"~~/src/Tools/induct.ML"
"~~/src/Tools/case_product.ML"
- ("cladata.ML")
("simpdata.ML")
begin
@@ -167,9 +166,36 @@
section {* Classical Reasoner *}
-use "cladata.ML"
+ML {*
+structure Cla = ClassicalFun
+(
+ val imp_elim = @{thm imp_elim}
+ val not_elim = @{thm notE}
+ val swap = @{thm swap}
+ val classical = @{thm classical}
+ val sizef = size_of_thm
+ val hyp_subst_tacs = [hyp_subst_tac]
+);
+
+ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
+
+structure Basic_Classical: BASIC_CLASSICAL = Cla;
+open Basic_Classical;
+*}
+
setup Cla.setup
-ML {* Context.>> (Cla.map_cs (K FOL_cs)) *}
+
+(*Propositional rules*)
+lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
+ and [elim!] = conjE disjE impCE FalseE iffCE
+ML {* val prop_cs = @{claset} *}
+
+(*Quantifier rules*)
+lemmas [intro!] = allI ex_ex1I
+ and [intro] = exI
+ and [elim!] = exE alt_ex1E
+ and [elim] = allE
+ML {* val FOL_cs = @{claset} *}
ML {*
structure Blast = Blast
@@ -316,7 +342,7 @@
val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
*}
-setup {* Simplifier.map_simpset (K FOL_ss) *}
+setup {* Simplifier.map_simpset_global (K FOL_ss) *}
setup "Simplifier.method_setup Splitter.split_modifiers"
setup Splitter.setup
--- a/src/FOL/IsaMakefile Fri May 13 21:36:01 2011 +0200
+++ b/src/FOL/IsaMakefile Fri May 13 23:59:48 2011 +0200
@@ -29,14 +29,13 @@
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
- $(SRC)/Tools/case_product.ML \
- $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
- $(SRC)/Tools/IsaPlanner/rw_tools.ML \
+ $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML \
+ $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
$(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \
- $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML cladata.ML \
+ $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \
document/root.tex fologic.ML hypsubstdata.ML intprover.ML \
simpdata.ML
@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
--- a/src/FOL/cladata.ML Fri May 13 21:36:01 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(* Title: FOL/cladata.ML
- Author: Tobias Nipkow
- Copyright 1996 University of Cambridge
-
-Setting up the classical reasoner.
-*)
-
-(*** Applying ClassicalFun to create a classical prover ***)
-structure Classical_Data =
-struct
- val imp_elim = @{thm imp_elim}
- val not_elim = @{thm notE}
- val swap = @{thm swap}
- val classical = @{thm classical}
- val sizef = size_of_thm
- val hyp_subst_tacs=[hyp_subst_tac]
-end;
-
-structure Cla = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
-
-ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
-
-
-(*Propositional rules*)
-val prop_cs = empty_cs
- addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI},
- @{thm notI}, @{thm iffI}]
- addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}];
-
-(*Quantifier rules*)
-val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
- addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
-
--- a/src/FOL/ex/Classical.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/FOL/ex/Classical.thy Fri May 13 23:59:48 2011 +0200
@@ -436,7 +436,7 @@
((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))
-->
~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by (tactic{*Blast.depth_tac @{claset} 12 1*})
+by (blast 12)
--{*Needed because the search for depths below 12 is very slow*}
--- a/src/FOL/simpdata.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/FOL/simpdata.ML Fri May 13 23:59:48 2011 +0200
@@ -142,6 +142,3 @@
);
open Clasimp;
-ML_Antiquote.value "clasimpset"
- (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
-
--- a/src/HOL/Algebra/abstract/Ideal2.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Algebra/abstract/Ideal2.thy Fri May 13 23:59:48 2011 +0200
@@ -276,7 +276,7 @@
apply (unfold prime_def)
apply (rule conjI)
apply (rule_tac [2] conjI)
- apply (tactic "clarify_tac @{claset} 3")
+ apply (tactic "clarify_tac @{context} 3")
apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)
apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)
apply (simp add: ideal_of_2_structure)
--- a/src/HOL/Algebra/abstract/Ring2.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Fri May 13 23:59:48 2011 +0200
@@ -466,7 +466,7 @@
(* fields are integral domains *)
lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
- apply (tactic "step_tac @{claset} 1")
+ apply (tactic "step_tac @{context} 1")
apply (rule_tac a = " (a*b) * inverse b" in box_equals)
apply (rule_tac [3] refl)
prefer 2
--- a/src/HOL/Auth/Message.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Auth/Message.thy Fri May 13 23:59:48 2011 +0200
@@ -830,31 +830,26 @@
eresolve_tac [asm_rl, @{thm synth.Inj}];
fun Fake_insert_simp_tac ss i =
- REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
fun atomic_spy_analz_tac ctxt =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- SELECT_GOAL
- (Fake_insert_simp_tac ss 1
- THEN
- IF_UNSOLVED (Blast.depth_tac
- (cs addIs [@{thm analz_insertI},
- impOfSubs @{thm analz_subset_parts}]) 4 1))
- end;
+ SELECT_GOAL
+ (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
+ IF_UNSOLVED
+ (Blast.depth_tac
+ (ctxt addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1));
fun spy_analz_tac ctxt i =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- DETERM
- (SELECT_GOAL
- (EVERY
- [ (*push in occurrences of X...*)
- (REPEAT o CHANGED)
- (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
- (*...allowing further simplifications*)
- simp_tac ss 1,
- REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
- DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
- end;
+ DETERM
+ (SELECT_GOAL
+ (EVERY
+ [ (*push in occurrences of X...*)
+ (REPEAT o CHANGED)
+ (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+ DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
*}
text{*By default only @{text o_apply} is built-in. But in the presence of
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri May 13 23:59:48 2011 +0200
@@ -749,7 +749,7 @@
(*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN
(*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN
(*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
- (*Base*) (force_tac (clasimpset_of ctxt)) 1
+ (*Base*) (force_tac ctxt) 1
val analz_prepare_tac =
prepare_tac THEN
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 13 23:59:48 2011 +0200
@@ -748,7 +748,7 @@
fun prepare_tac ctxt =
(*SR_U8*) forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
- (*SR_U8*) clarify_tac (claset_of ctxt) 15 THEN
+ (*SR_U8*) clarify_tac ctxt 15 THEN
(*SR_U9*) forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN
(*SR_U11*) forward_tac [@{thm Outpts_A_Card_form_10}] 21
@@ -758,7 +758,7 @@
(*SR_U9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN
(*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN
(*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
- (*Base*) (force_tac (clasimpset_of ctxt)) 1
+ (*Base*) (force_tac ctxt) 1
fun analz_prepare_tac ctxt =
prepare_tac ctxt THEN
--- a/src/HOL/Bali/AxCompl.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Bali/AxCompl.thy Fri May 13 23:59:48 2011 +0200
@@ -1391,7 +1391,7 @@
using finU uA
apply -
apply (induct_tac "n")
-apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
+apply (tactic "ALLGOALS (clarsimp_tac @{context})")
apply (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *})
apply simp
apply (erule finite_imageI)
--- a/src/HOL/Bali/AxSem.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Bali/AxSem.thy Fri May 13 23:59:48 2011 +0200
@@ -661,7 +661,7 @@
lemma ax_thin [rule_format (no_asm)]:
"G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
apply (erule ax_derivs.induct)
-apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
+apply (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
apply (rule ax_derivs.empty)
apply (erule (1) ax_derivs.insert)
apply (fast intro: ax_derivs.asm)
@@ -692,7 +692,7 @@
(*42 subgoals*)
apply (tactic "ALLGOALS strip_tac")
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
- etac disjE, fast_tac (@{claset} addSIs @{thms ax_derivs.empty})]))*})
+ etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
apply (tactic "TRYALL hyp_subst_tac")
apply (simp, rule ax_derivs.empty)
apply (drule subset_insertD)
@@ -703,7 +703,7 @@
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
(*37 subgoals*)
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})
- THEN_ALL_NEW fast_tac @{claset}) *})
+ THEN_ALL_NEW fast_tac @{context}) *})
(*1 subgoal*)
apply (clarsimp simp add: subset_mtriples_iff)
apply (rule ax_derivs.Methd)
--- a/src/HOL/HOL.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/HOL.thy Fri May 13 23:59:48 2011 +0200
@@ -1205,7 +1205,7 @@
use "Tools/simpdata.ML"
ML {* open Simpdata *}
-setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
+setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Fri May 13 23:59:48 2011 +0200
@@ -152,12 +152,12 @@
lemma slen_fscons_eq_rev:
"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
apply (simp add: fscons_def2 slen_scons_eq_rev)
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
apply (erule contrapos_np)
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
done
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri May 13 23:59:48 2011 +0200
@@ -83,9 +83,9 @@
lemma last_ind_on_first:
"l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
apply simp
- apply (tactic {* auto_tac (@{claset},
+ apply (tactic {* auto_tac (map_simpset (fn _ =>
HOL_ss addsplits [@{thm list.split}]
- addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) *})
+ addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
done
text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri May 13 23:59:48 2011 +0200
@@ -604,10 +604,10 @@
ML {*
fun abstraction_tac ctxt =
- let val (cs, ss) = clasimpset_of ctxt in
- SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
- ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
- end
+ SELECT_GOAL (auto_tac
+ (ctxt addSIs @{thms weak_strength_lemmas}
+ |> map_simpset (fn ss =>
+ ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
*}
method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Fri May 13 23:59:48 2011 +0200
@@ -400,7 +400,7 @@
==> input_enabled (A||B)"
apply (unfold input_enabled_def)
apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac (global_claset_of @{theory Fun})")
+apply (tactic "safe_tac (Proof_Context.init_global @{theory Fun})")
apply (simp add: inp_is_act)
prefer 2
apply (simp add: inp_is_act)
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Fri May 13 23:59:48 2011 +0200
@@ -298,7 +298,7 @@
let val ss = simpset_of ctxt in
EVERY1[Seq_induct_tac ctxt sch defs,
asm_full_simp_tac ss,
- SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})),
+ SELECT_GOAL (safe_tac (Proof_Context.init_global @{theory Fun})),
Seq_case_simp_tac ctxt exA,
Seq_case_simp_tac ctxt exB,
asm_full_simp_tac ss,
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri May 13 23:59:48 2011 +0200
@@ -150,7 +150,7 @@
(Ps ~~ take_consts ~~ xs)
val goal = mk_trp (foldr1 mk_conj concls)
- fun tacf {prems, context} =
+ fun tacf {prems, context = ctxt} =
let
(* Prove stronger prems, without definedness side conditions *)
fun con_thm p (con, args) =
@@ -165,23 +165,23 @@
map arg_tac args @
[REPEAT (rtac impI 1), ALLGOALS simplify]
in
- Goal.prove context [] [] subgoal (K (EVERY tacs))
+ Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
end
fun eq_thms (p, cons) = map (con_thm p) cons
val conss = map #con_specs constr_infos
val prems' = maps eq_thms (Ps ~~ conss)
val tacs1 = [
- quant_tac context 1,
+ quant_tac ctxt 1,
simp_tac HOL_ss 1,
- InductTacs.induct_tac context [[SOME "n"]] 1,
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1,
simp_tac (take_ss addsimps prems) 1,
- TRY (safe_tac HOL_cs)]
+ TRY (safe_tac (put_claset HOL_cs ctxt))]
fun con_tac _ =
asm_simp_tac take_ss 1 THEN
(resolve_tac prems' THEN_ALL_NEW etac spec) 1
fun cases_tacs (cons, exhaust) =
- res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
+ res_inst_tac ctxt [(("y", 0), "x")] exhaust 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
map con_tac cons
val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
@@ -196,15 +196,15 @@
val concls = map (op $) (Ps ~~ xs)
val goal = mk_trp (foldr1 mk_conj concls)
val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps
- fun tacf {prems, context} =
+ fun tacf {prems, context = ctxt} =
let
fun finite_tac (take_induct, fin_ind) =
rtac take_induct 1 THEN
(if is_finite then all_tac else resolve_tac prems 1) THEN
(rtac fin_ind THEN_ALL_NEW solve_tac prems) 1
- val fin_inds = Project_Rule.projections context finite_ind
+ val fin_inds = Project_Rule.projections ctxt finite_ind
in
- TRY (safe_tac HOL_cs) THEN
+ TRY (safe_tac (put_claset HOL_cs ctxt)) THEN
EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
end
in Goal.prove_global thy [] (adms @ assms) goal tacf end
@@ -318,18 +318,18 @@
val goal =
mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)))
val rules = @{thm Rep_cfun_strict1} :: take_0_thms
- fun tacf {prems, context} =
+ fun tacf {prems, context = ctxt} =
let
val prem' = rewrite_rule [bisim_def_thm] (hd prems)
- val prems' = Project_Rule.projections context prem'
+ val prems' = Project_Rule.projections ctxt prem'
val dests = map (fn th => th RS spec RS spec RS mp) prems'
fun one_tac (dest, rews) =
- dtac dest 1 THEN safe_tac HOL_cs THEN
+ dtac dest 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN
ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews))
in
rtac @{thm nat.induct} 1 THEN
simp_tac (HOL_ss addsimps rules) 1 THEN
- safe_tac HOL_cs THEN
+ safe_tac (put_claset HOL_cs ctxt) THEN
EVERY (map one_tac (dests ~~ take_rews))
end
in
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Fri May 13 23:59:48 2011 +0200
@@ -128,6 +128,6 @@
Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont
end
-fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy
+fun setup thy = Simplifier.map_simpset_global (fn ss => ss addsimprocs [cont_proc thy]) thy
end
--- a/src/HOL/Hoare/hoare_tac.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Fri May 13 23:59:48 2011 +0200
@@ -78,7 +78,7 @@
val MsetT = fastype_of big_Collect;
fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
- val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1);
+ val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1);
in (vars, th) end;
end;
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 13 23:59:48 2011 +0200
@@ -774,13 +774,13 @@
--{* 32 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 20 subgoals left *}
-apply(tactic{* TRYALL (clarify_tac @{claset}) *})
+apply(tactic{* TRYALL (clarify_tac @{context}) *})
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (etac disjE) *})
apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{clasimpset}]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
done
subsubsection {* Interference freedom Mutator-Collector *}
@@ -794,7 +794,7 @@
apply(tactic {* TRYALL (interfree_aux_tac) *})
--{* 64 subgoals left *}
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
-apply(tactic{* TRYALL (clarify_tac @{claset}) *})
+apply(tactic{* TRYALL (clarify_tac @{context}) *})
--{* 4 subgoals left *}
apply force
apply(simp add:Append_to_free2)
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 23:59:48 2011 +0200
@@ -132,7 +132,7 @@
apply(simp_all add:mul_mutator_interfree)
apply(simp_all add: mul_mutator_defs)
apply(tactic {* TRYALL (interfree_aux_tac) *})
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply (simp_all add:nth_list_update)
done
@@ -1123,7 +1123,7 @@
interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
apply(erule_tac x=j in allE, force dest:Graph3)+
done
@@ -1132,7 +1132,7 @@
interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def mul_mutator_defs nth_list_update)
done
@@ -1140,7 +1140,7 @@
interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1
Graph12 nth_list_update)
done
@@ -1149,7 +1149,7 @@
interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply(simp_all add: mul_mutator_defs nth_list_update)
apply(simp add:Mul_AppendInv_def Append_to_free0)
done
@@ -1178,7 +1178,7 @@
--{* 24 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 14 subgoals left *}
-apply(tactic {* TRYALL (clarify_tac @{claset}) *})
+apply(tactic {* TRYALL (clarify_tac @{context}) *})
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (rtac conjI) *})
apply(tactic {* TRYALL (rtac impI) *})
@@ -1189,7 +1189,7 @@
--{* 72 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
--{* 28 subgoals left *}
apply(tactic {* TRYALL (etac conjE) *})
apply(tactic {* TRYALL (etac disjE) *})
@@ -1199,17 +1199,21 @@
apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
apply(simp_all add:Graph10)
--{* 47 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *})
--{* 41 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
+ force_tac (map_simpset (fn ss => ss addsimps
+ [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
--{* 31 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
--{* 29 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
--{* 25 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
+ force_tac (map_simpset (fn ss => ss addsimps
+ [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
--{* 10 subgoals left *}
apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
done
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Fri May 13 23:59:48 2011 +0200
@@ -170,10 +170,10 @@
--{* 35 vc *}
apply simp_all
--{* 21 vc *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
--{* 11 vc *}
apply simp_all
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
--{* 10 subgoals left *}
apply(erule less_SucE)
apply simp
@@ -430,13 +430,13 @@
.{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
apply oghoare
--{* 138 vc *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
--{* 112 subgoals left *}
apply(simp_all (no_asm))
--{* 97 subgoals left *}
apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
--{* 930 subgoals left *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
--{* 99 subgoals left *}
apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym])
--{* 20 subgoals left *}
@@ -535,7 +535,7 @@
.{\<acute>x=n}."
apply oghoare
apply (simp_all cong del: strong_setsum_cong)
-apply (tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply (tactic {* ALLGOALS (clarify_tac @{context}) *})
apply (simp_all cong del: strong_setsum_cong)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
--- a/src/HOL/IMPP/Hoare.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/IMPP/Hoare.thy Fri May 13 23:59:48 2011 +0200
@@ -209,7 +209,7 @@
*)
lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
apply (erule hoare_derivs.induct)
-apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
+apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1]) *})
apply (rule hoare_derivs.empty)
apply (erule (1) hoare_derivs.insert)
apply (fast intro: hoare_derivs.asm)
@@ -218,7 +218,7 @@
apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
prefer 7
apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
-apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{claset})) *})
+apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *})
done
lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
@@ -287,10 +287,10 @@
apply (blast) (* weaken *)
apply (tactic {* ALLGOALS (EVERY'
[REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
- simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
+ simp_tac @{simpset}, clarify_tac @{context}, REPEAT o smp_tac 1]) *})
apply (simp_all (no_asm_use) add: triple_valid_def2)
apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
-apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *)
+apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *)
prefer 3 apply (force) (* Call *)
apply (erule_tac [2] evaln_elim_cases) (* If *)
apply blast+
@@ -335,17 +335,17 @@
lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>
!pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
apply (induct_tac c)
-apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
+apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *})
prefer 7 apply (fast intro: domI)
apply (erule_tac [6] MGT_alternD)
apply (unfold MGT_def)
apply (drule_tac [7] bspec, erule_tac [7] domI)
-apply (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 7 *},
+apply (rule_tac [7] escape, tactic {* clarsimp_tac @{context} 7 *},
rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
apply (erule_tac [!] thin_rl)
apply (rule hoare_derivs.Skip [THEN conseq2])
apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
-apply (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 3 *},
+apply (rule_tac [3] escape, tactic {* clarsimp_tac @{context} 3 *},
rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
erule_tac [3] conseq12)
apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
@@ -364,7 +364,7 @@
shows "finite U ==> uG = mgt_call`U ==>
!G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
apply (induct_tac n)
-apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
+apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *})
apply (subgoal_tac "G = mgt_call ` U")
prefer 2
apply (simp add: card_seteq)
--- a/src/HOL/MicroJava/J/Conform.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri May 13 23:59:48 2011 +0200
@@ -328,8 +328,9 @@
apply auto
apply(rule hconfI)
apply(drule conforms_heapD)
-apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}]
- addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
+apply(tactic {*
+ auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
+ |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *})
done
lemma conforms_upd_local:
--- a/src/HOL/MicroJava/J/WellForm.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Fri May 13 23:59:48 2011 +0200
@@ -315,7 +315,7 @@
apply( clarify)
apply( frule fields_rec, assumption)
apply( fastsimp)
-apply( tactic "safe_tac HOL_cs")
+apply( tactic "safe_tac (put_claset HOL_cs @{context})")
apply( subst fields_rec)
apply( assumption)
apply( assumption)
--- a/src/HOL/Multivariate_Analysis/normarith.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Fri May 13 23:59:48 2011 +0200
@@ -384,7 +384,7 @@
end
fun norm_arith_tac ctxt =
- clarify_tac HOL_cs THEN'
+ clarify_tac (put_claset HOL_cs ctxt) THEN'
Object_Logic.full_atomize_tac THEN'
CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
--- a/src/HOL/NanoJava/AxSem.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Fri May 13 23:59:48 2011 +0200
@@ -151,7 +151,7 @@
"(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and>
(A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))"
apply (rule hoare_ehoare.induct)
-apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
+apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
apply (blast intro: hoare_ehoare.Skip)
apply (blast intro: hoare_ehoare.Comp)
apply (blast intro: hoare_ehoare.Cond)
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri May 13 23:59:48 2011 +0200
@@ -264,7 +264,7 @@
apply (simp add: zmult_assoc)
apply (rule_tac [5] zcong_zmult)
apply (rule_tac [5] inv_is_inv)
- apply (tactic "clarify_tac @{claset} 4")
+ apply (tactic "clarify_tac @{context} 4")
apply (subgoal_tac [4] "a \<in> wset (a - 1) p")
apply (rule_tac [5] wset_inv_mem_mem)
apply (simp_all add: wset_fin)
--- a/src/HOL/Orderings.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Orderings.thy Fri May 13 23:59:48 2011 +0200
@@ -564,11 +564,12 @@
handle THM _ => NONE;
fun add_simprocs procs thy =
- Simplifier.map_simpset (fn ss => ss
+ Simplifier.map_simpset_global (fn ss => ss
addsimprocs (map (fn (name, raw_ts, proc) =>
Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
+
fun add_solver name tac =
- Simplifier.map_simpset (fn ss => ss addSolver
+ Simplifier.map_simpset_global (fn ss => ss addSolver
mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
in
--- a/src/HOL/Prolog/Test.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Prolog/Test.thy Fri May 13 23:59:48 2011 +0200
@@ -234,9 +234,9 @@
(* disjunction in atom: *)
lemma "(!P. g P :- (P => b | a)) => g(a | b)"
- apply (tactic "step_tac HOL_cs 1")
- apply (tactic "step_tac HOL_cs 1")
- apply (tactic "step_tac HOL_cs 1")
+ apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
+ apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
+ apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
prefer 2
apply fast
apply fast
--- a/src/HOL/Proofs/Lambda/Commutation.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Proofs/Lambda/Commutation.thy Fri May 13 23:59:48 2011 +0200
@@ -127,9 +127,9 @@
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
apply (unfold square_def commute_def diamond_def Church_Rosser_def)
- apply (tactic {* safe_tac HOL_cs *})
+ apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
apply (tactic {*
- blast_tac (HOL_cs addIs
+ blast_tac (put_claset HOL_cs @{context} addIs
[@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
@{thm rtranclp_converseI}, @{thm conversepI},
@{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
--- a/src/HOL/SET_Protocol/Message_SET.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Fri May 13 23:59:48 2011 +0200
@@ -853,31 +853,26 @@
eresolve_tac [asm_rl, @{thm synth.Inj}];
fun Fake_insert_simp_tac ss i =
- REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
fun atomic_spy_analz_tac ctxt =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- SELECT_GOAL
- (Fake_insert_simp_tac ss 1
- THEN
- IF_UNSOLVED (Blast.depth_tac
- (cs addIs [@{thm analz_insertI},
- impOfSubs @{thm analz_subset_parts}]) 4 1))
- end;
+ SELECT_GOAL
+ (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
+ IF_UNSOLVED
+ (Blast.depth_tac (ctxt addIs [@{thm analz_insertI},
+ impOfSubs @{thm analz_subset_parts}]) 4 1));
fun spy_analz_tac ctxt i =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- DETERM
- (SELECT_GOAL
- (EVERY
- [ (*push in occurrences of X...*)
- (REPEAT o CHANGED)
- (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
- (*...allowing further simplifications*)
- simp_tac ss 1,
- REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
- DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
- end;
+ DETERM
+ (SELECT_GOAL
+ (EVERY
+ [ (*push in occurrences of X...*)
+ (REPEAT o CHANGED)
+ (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+ DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
*}
(*>*)
--- a/src/HOL/TLA/Action.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/TLA/Action.thy Fri May 13 23:59:48 2011 +0200
@@ -277,16 +277,20 @@
The following tactic combines these steps except the final one.
*)
-fun enabled_tac (cs, ss) base_vars =
- clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss);
+fun enabled_tac ctxt base_vars =
+ clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]);
*}
+method_setup enabled = {*
+ Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
+*} ""
+
(* Example *)
lemma
assumes "basevars (x,y,z)"
shows "|- x --> Enabled ($x & (y$ = #False))"
- apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *})
+ apply (enabled assms)
apply auto
done
--- a/src/HOL/TLA/Inc/Inc.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Fri May 13 23:59:48 2011 +0200
@@ -161,7 +161,7 @@
lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = gamma1 in enabled_mono)
- apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+ apply (enabled Inc_base)
apply (force simp: gamma1_def)
apply (force simp: angle_def gamma1_def N1_def)
done
@@ -183,7 +183,7 @@
lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = gamma2 in enabled_mono)
- apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+ apply (enabled Inc_base)
apply (force simp: gamma2_def)
apply (force simp: angle_def gamma2_def N2_def)
done
@@ -202,7 +202,7 @@
lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = beta2 in enabled_mono)
- apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+ apply (enabled Inc_base)
apply (force simp: beta2_def)
apply (force simp: angle_def beta2_def N2_def)
done
@@ -244,7 +244,7 @@
"|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = alpha1 in enabled_mono)
- apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+ apply (enabled Inc_base)
apply (force simp: alpha1_def PsiInv_defs)
apply (force simp: angle_def alpha1_def N1_def)
done
@@ -285,7 +285,7 @@
lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = beta1 in enabled_mono)
- apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+ apply (enabled Inc_base)
apply (force simp: beta1_def)
apply (force simp: angle_def beta1_def N1_def)
done
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Fri May 13 23:59:48 2011 +0200
@@ -791,15 +791,20 @@
steps of the implementation, and try to solve the idling case by simplification
*)
ML {*
-fun split_idle_tac ctxt simps i =
- let val ss = simpset_of ctxt in
- TRY (rtac @{thm actionI} i) THEN
- InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
+fun split_idle_tac ctxt =
+ SELECT_GOAL
+ (TRY (rtac @{thm actionI} 1) THEN
+ InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
rewrite_goals_tac @{thms action_rews} THEN
- forward_tac [temp_use @{thm Step1_4_7}] i THEN
- asm_full_simp_tac (ss addsimps simps) i
- end
+ forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
+ asm_full_simp_tac (simpset_of ctxt) 1);
*}
+
+method_setup split_idle = {*
+ Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers)
+ >> (K (SIMPLE_METHOD' o split_idle_tac))
+*} ""
+
(* ----------------------------------------------------------------------
Combine steps 1.2 and 1.4 to prove that the implementation satisfies
the specification's next-state relation.
@@ -810,7 +815,7 @@
lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
- apply (tactic {* split_idle_tac @{context} [@{thm square_def}] 1 *})
+ apply (split_idle simp: square_def)
apply force
done
(* turn into (unsafe, looping!) introduction rule *)
@@ -882,7 +887,7 @@
lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S1 rmhist p)$ | (S2 rmhist p)$"
- apply (tactic "split_idle_tac @{context} [] 1")
+ apply split_idle
apply (auto dest!: Step1_2_1 [temp_use])
done
@@ -916,7 +921,7 @@
lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S2 rmhist p)$ | (S3 rmhist p)$"
- apply (tactic "split_idle_tac @{context} [] 1")
+ apply split_idle
apply (auto dest!: Step1_2_2 [temp_use])
done
@@ -942,7 +947,7 @@
lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
- apply (tactic "split_idle_tac @{context} [] 1")
+ apply split_idle
apply (auto dest!: Step1_2_3 [temp_use])
done
@@ -970,7 +975,7 @@
lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
& (ALL l. $MemInv mm l)
--> (S4 rmhist p)$ | (S5 rmhist p)$"
- apply (tactic "split_idle_tac @{context} [] 1")
+ apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
done
@@ -980,7 +985,7 @@
& ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
--> (S4 rmhist p & ires!p = #NotAResult)$
| ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
- apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
+ apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
done
@@ -1011,7 +1016,7 @@
lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
& ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
--> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
- apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
+ apply (split_idle simp: m_def)
apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
done
@@ -1040,7 +1045,7 @@
lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S5 rmhist p)$ | (S6 rmhist p)$"
- apply (tactic "split_idle_tac @{context} [] 1")
+ apply split_idle
apply (auto dest!: Step1_2_5 [temp_use])
done
@@ -1066,7 +1071,7 @@
lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
- apply (tactic "split_idle_tac @{context} [] 1")
+ apply split_idle
apply (auto dest!: Step1_2_6 [temp_use])
done
@@ -1281,7 +1286,7 @@
apply clarsimp
apply (drule WriteS4 [action_use])
apply assumption
- apply (tactic "split_idle_tac @{context} [] 1")
+ apply split_idle
apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
S4RPCUnch [temp_use])
apply (auto simp: square_def dest: S4Write [temp_use])
--- a/src/HOL/TLA/TLA.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/TLA/TLA.thy Fri May 13 23:59:48 2011 +0200
@@ -310,6 +310,11 @@
eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
*}
+method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} ""
+method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *} ""
+method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *} ""
+method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *} ""
+
(* rewrite rule to push universal quantification through box:
(sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
*)
@@ -317,8 +322,7 @@
lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
apply (auto simp add: dmd_def split_box_conj [try_rewrite])
- apply (erule contrapos_np, tactic "merge_box_tac 1",
- fastsimp elim!: STL4E [temp_use])+
+ apply (erule contrapos_np, merge_box, fastsimp elim!: STL4E [temp_use])+
done
lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
@@ -328,7 +332,7 @@
lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
apply (erule dup_boxE)
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (erule STL4E)
apply assumption
done
@@ -338,7 +342,7 @@
apply (unfold dmd_def)
apply auto
apply (erule notE)
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (fastsimp elim!: STL4E [temp_use])
done
@@ -349,7 +353,7 @@
shows "sigma |= []<>H"
apply (insert 1 2)
apply (erule_tac F = G in dup_boxE)
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (fastsimp elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
done
@@ -359,7 +363,7 @@
apply (unfold dmd_def)
apply clarsimp
apply (erule dup_boxE)
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (erule contrapos_np)
apply (fastsimp elim!: STL4E [temp_use])
done
@@ -368,14 +372,14 @@
lemma BoxDmd_simple: "|- []F & <>G --> <>(F & G)"
apply (unfold dmd_def)
apply clarsimp
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (fastsimp elim!: notE STL4E [temp_use])
done
lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)"
apply (unfold dmd_def)
apply clarsimp
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (fastsimp elim!: notE STL4E [temp_use])
done
@@ -579,11 +583,13 @@
ML {*
(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
-fun inv_tac css = SELECT_GOAL
- (EVERY [auto_tac css,
- TRY (merge_box_tac 1),
- rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
- TRYALL (etac @{thm Stable})]);
+fun inv_tac ctxt =
+ SELECT_GOAL
+ (EVERY
+ [auto_tac ctxt,
+ TRY (merge_box_tac 1),
+ rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
+ TRYALL (etac @{thm Stable})]);
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals
in simple cases it may be able to handle goals like |- MyProg --> []Inv.
@@ -591,15 +597,15 @@
auto-tactic, which applies too much propositional logic and simplifies
too late.
*)
-fun auto_inv_tac ss = SELECT_GOAL
- ((inv_tac (@{claset}, ss) 1) THEN
- (TRYALL (action_simp_tac
- (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
+fun auto_inv_tac ss =
+ SELECT_GOAL
+ (inv_tac (map_simpset (K ss) @{context}) 1 THEN
+ (TRYALL (action_simp_tac
+ (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
*}
method_setup invariant = {*
- Method.sections Clasimp.clasimp_modifiers
- >> (K (SIMPLE_METHOD' o inv_tac o clasimpset_of))
+ Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
*} ""
method_setup auto_invariant = {*
@@ -610,7 +616,7 @@
lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
apply (unfold dmd_def)
apply (clarsimp dest!: BoxPrime [temp_use])
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (erule contrapos_np)
apply (fastsimp elim!: Stable [temp_use])
done
@@ -840,7 +846,7 @@
apply (unfold leadsto_def)
apply clarsimp
apply (erule dup_boxE) (* [][] (Init G --> H) *)
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (clarsimp elim!: STL4E [temp_use])
apply (rule dup_dmdD)
apply (subgoal_tac "sigmaa |= <>Init G")
@@ -862,7 +868,7 @@
lemma LatticeDisjunctionIntro: "|- (F ~> H) & (G ~> H) --> (F | G ~> H)"
apply (unfold leadsto_def)
apply clarsimp
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
@@ -943,7 +949,7 @@
apply (clarsimp dest!: BoxSFI [temp_use])
apply (erule (2) ensures [temp_use])
apply (erule_tac F = F in dup_boxE)
- apply (tactic "merge_temp_box_tac @{context} 1")
+ apply merge_temp_box
apply (erule STL4Edup)
apply assumption
apply (clarsimp simp: SF_def)
@@ -962,7 +968,7 @@
apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
simp: WF_def [where A = M])
apply (erule_tac F = F in dup_boxE)
- apply (tactic "merge_temp_box_tac @{context} 1")
+ apply merge_temp_box
apply (erule STL4Edup)
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
@@ -971,7 +977,7 @@
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
- apply (tactic "merge_act_box_tac @{context} 1")
+ apply merge_act_box
apply (frule 4 [temp_use])
apply assumption+
apply (drule STL6 [temp_use])
@@ -980,7 +986,7 @@
apply (erule_tac V = "sigmaa |= []F" in thin_rl)
apply (drule BoxWFI [temp_use])
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
- apply (tactic "merge_temp_box_tac @{context} 1")
+ apply merge_temp_box
apply (erule DmdImpldup)
apply assumption
apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
@@ -1000,7 +1006,7 @@
apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
apply (erule_tac F = F in dup_boxE)
apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE)
- apply (tactic "merge_temp_box_tac @{context} 1")
+ apply merge_temp_box
apply (erule STL4Edup)
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
@@ -1009,14 +1015,14 @@
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
- apply (tactic "merge_act_box_tac @{context} 1")
+ apply merge_act_box
apply (frule 4 [temp_use])
apply assumption+
apply (erule_tac V = "sigmaa |= []F" in thin_rl)
apply (drule BoxSFI [temp_use])
apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
- apply (tactic "merge_temp_box_tac @{context} 1")
+ apply merge_temp_box
apply (erule DmdImpldup)
apply assumption
apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
@@ -1055,7 +1061,6 @@
apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps)
apply (erule wf_leadsto)
apply (rule ensures_simple [temp_use])
- apply (tactic "TRYALL atac")
apply (auto simp: square_def angle_def)
done
@@ -1149,7 +1154,7 @@
apply (rule conjI)
prefer 2
apply (insert 2)
- apply (tactic "merge_box_tac 1")
+ apply merge_box
apply (force elim!: STL4E [temp_use] 5 [temp_use])
apply (insert 1)
apply (force simp: Init_defs elim!: 4 [temp_use])
--- a/src/HOL/Tools/Function/fun.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Function/fun.ML Fri May 13 23:59:48 2011 +0200
@@ -143,7 +143,7 @@
let
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1
- THEN auto_tac (clasimpset_of ctxt)
+ THEN auto_tac ctxt
fun prove_termination lthy =
Function.prove_termination NONE
(Function_Common.get_termination_prover lthy lthy) lthy
--- a/src/HOL/Tools/Function/function_core.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Fri May 13 23:59:48 2011 +0200
@@ -702,7 +702,7 @@
Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
|> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
- |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
+ |> (SINGLE (auto_tac ctxt)) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
--- a/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 23:59:48 2011 +0200
@@ -214,9 +214,9 @@
end
fun lexicographic_order_tac quiet ctxt =
- TRY (Function_Common.apply_termination_rule ctxt 1)
- THEN lex_order_tac quiet ctxt
- (auto_tac (claset_of ctxt, simpset_of ctxt addsimps Function_Common.Termination_Simps.get ctxt))
+ TRY (Function_Common.apply_termination_rule ctxt 1) THEN
+ lex_order_tac quiet ctxt
+ (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 23:59:48 2011 +0200
@@ -338,7 +338,7 @@
fun decomp_scnp_tac orders ctxt =
let
val extra_simps = Function_Common.Termination_Simps.get ctxt
- val autom_tac = auto_tac (claset_of ctxt, simpset_of ctxt addsimps extra_simps)
+ val autom_tac = auto_tac (map_simpset (fn ss => ss addsimps extra_simps) ctxt)
in
gen_sizechange_tac orders autom_tac ctxt
end
--- a/src/HOL/Tools/Function/termination.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Function/termination.ML Fri May 13 23:59:48 2011 +0200
@@ -297,7 +297,7 @@
THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *)
ORELSE' ((rtac @{thm conjI})
THEN' (rtac @{thm refl})
- THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *)
+ THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *)
) i
in
((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
--- a/src/HOL/Tools/Meson/meson.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri May 13 23:59:48 2011 +0200
@@ -699,8 +699,7 @@
(*First, breaks the goal into independent units*)
fun safe_best_meson_tac ctxt =
- SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
- TRYALL (best_meson_tac size_of_subgoals ctxt));
+ SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt));
(** Depth-first search version **)
@@ -742,7 +741,7 @@
end));
fun meson_tac ctxt ths =
- SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
+ SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
(**** Code to support ordinary resolution, rather than Model Elimination ****)
--- a/src/HOL/Tools/Meson/meson_tactic.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_tactic.ML Fri May 13 23:59:48 2011 +0200
@@ -17,9 +17,8 @@
open Meson_Clausify
fun meson_general_tac ctxt ths =
- let val ctxt = Classical.put_claset HOL_cs ctxt in
- Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
- end
+ let val ctxt' = put_claset HOL_cs ctxt
+ in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false 0) ths) end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri May 13 23:59:48 2011 +0200
@@ -2004,9 +2004,8 @@
map (wf_constraint_for rel side concl) main |> foldr1 s_conj
fun terminates_by ctxt timeout goal tac =
- can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
- #> SINGLE (DETERM_TIMEOUT timeout
- (tac ctxt (auto_tac (clasimpset_of ctxt))))
+ can (SINGLE (Classical.safe_tac ctxt) #> the
+ #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt)))
#> the #> Goal.finish ctxt) goal
val max_cached_wfs = 50
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 13 23:59:48 2011 +0200
@@ -1050,8 +1050,7 @@
()
val goal = prop |> cterm_of thy |> Goal.init
in
- (goal |> SINGLE (DETERM_TIMEOUT auto_timeout
- (auto_tac (clasimpset_of ctxt)))
+ (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
|> the |> Goal.finish ctxt; true)
handle THM _ => false
| TimeLimit.TimeOut => false
--- a/src/HOL/Tools/Qelim/cooper.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri May 13 23:59:48 2011 +0200
@@ -706,7 +706,7 @@
val all_maxscope_ss =
HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
in
-fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
+fun thin_prems_tac ctxt P = simp_tac all_maxscope_ss THEN'
CSUBGOAL (fn (p', i) =>
let
val (qvs, p) = strip_objall (Thm.dest_arg p')
@@ -720,7 +720,7 @@
| _ => false)
in
if ntac then no_tac
- else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
+ else rtac (Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) i
end)
end;
@@ -843,7 +843,7 @@
THEN_ALL_NEW simp_tac ss
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
THEN_ALL_NEW Object_Logic.full_atomize_tac
- THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
+ THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
THEN_ALL_NEW Object_Logic.full_atomize_tac
THEN_ALL_NEW div_mod_tac ctxt
THEN_ALL_NEW splits_tac ctxt
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri May 13 23:59:48 2011 +0200
@@ -38,8 +38,7 @@
(* defining functions *)
fun pat_completeness_auto ctxt =
- Pat_Completeness.pat_completeness_tac ctxt 1
- THEN auto_tac (clasimpset_of ctxt)
+ Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
fun define_functions (mk_equations, termination_tac) prfx argnames names Ts =
if define_foundationally andalso is_some termination_tac then
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri May 13 23:59:48 2011 +0200
@@ -97,9 +97,14 @@
val rewr_if =
@{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
in
-val simp_fast_tac =
+
+fun HOL_fast_tac ctxt =
+ Classical.fast_tac (put_claset HOL_cs ctxt)
+
+fun simp_fast_tac ctxt =
Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
- THEN_ALL_NEW Classical.fast_tac HOL_cs
+ THEN_ALL_NEW HOL_fast_tac ctxt
+
end
@@ -300,7 +305,7 @@
(* distributivity of | over & *)
fun distributivity ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
(* FIXME: not very well tested *)
@@ -356,7 +361,7 @@
fun def_axiom ctxt = Thm o try_apply ctxt [] [
named ctxt "conj/disj/distinct" prove_def_axiom,
Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
- named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
+ named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
end
@@ -417,7 +422,7 @@
fun prove_nnf ctxt = try_apply ctxt [] [
named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
- named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
+ named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
in
fun nnf ctxt vars ps ct =
(case SMT_Utils.term_of ct of
@@ -552,13 +557,13 @@
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
fun pull_quant ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
(* FIXME: not very well tested *)
(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
fun push_quant ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
(* FIXME: not very well tested *)
@@ -582,7 +587,7 @@
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
(* FIXME: not very well tested *)
@@ -694,18 +699,18 @@
Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
- THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
+ THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
- NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
+ NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
- NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
+ NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))
--- a/src/HOL/Tools/TFL/post.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/TFL/post.ML Fri May 13 23:59:48 2011 +0200
@@ -40,7 +40,7 @@
terminator =
asm_simp_tac (simpset_of ctxt) 1
THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
- fast_tac (claset_of ctxt addSDs [@{thm not0_implies_Suc}] addss (simpset_of ctxt)) 1),
+ fast_simp_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
simplifier = Rules.simpl_conv (simpset_of ctxt) []};
--- a/src/HOL/Tools/groebner.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/groebner.ML Fri May 13 23:59:48 2011 +0200
@@ -1012,10 +1012,10 @@
THEN ring_tac add_ths del_ths ctxt 1
end
in
- clarify_tac @{claset} i
+ clarify_tac @{context} i
THEN Object_Logic.full_atomize_tac i
THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i
- THEN clarify_tac @{claset} i
+ THEN clarify_tac @{context} i
THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
THEN SUBPROOF poly_exists_tac ctxt i
end
--- a/src/HOL/Tools/inductive_set.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri May 13 23:59:48 2011 +0200
@@ -557,7 +557,7 @@
Codegen.add_preprocessor codegen_preproc #>
Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
"declaration of monotonicity rule for set operators" #>
- Context.theory_map (Simplifier.map_ss (fn ss => ss addsimprocs [collect_mem_simproc]));
+ Simplifier.map_simpset_global (fn ss => ss addsimprocs [collect_mem_simproc]);
(* outer syntax *)
--- a/src/HOL/Tools/int_arith.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/int_arith.ML Fri May 13 23:59:48 2011 +0200
@@ -84,8 +84,8 @@
"(m::'a::{linordered_idom,number_ring}) <= n",
"(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
-val global_setup = Simplifier.map_simpset
- (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
+val global_setup =
+ Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
fun number_of thy T n =
--- a/src/HOL/Tools/recdef.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/recdef.ML Fri May 13 23:59:48 2011 +0200
@@ -167,7 +167,7 @@
| SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
val {simps, congs, wfs} = get_hints ctxt;
val ctxt' = ctxt
- |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
+ |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
in (ctxt', rev (map snd congs), wfs) end;
fun prepare_hints_i thy () =
@@ -175,7 +175,7 @@
val ctxt = Proof_Context.init_global thy;
val {simps, congs, wfs} = get_global_hints thy;
val ctxt' = ctxt
- |> Context.proof_map (Simplifier.map_ss (fn ss => ss addsimps simps delcongs [imp_cong]));
+ |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
in (ctxt', rev (map snd congs), wfs) end;
--- a/src/HOL/Tools/record.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/record.ML Fri May 13 23:59:48 2011 +0200
@@ -44,7 +44,7 @@
val ex_sel_eq_simproc: simproc
val split_tac: int -> tactic
val split_simp_tac: thm list -> (term -> int) -> int -> tactic
- val split_wrapper: string * wrapper
+ val split_wrapper: string * (Proof.context -> wrapper)
val updateN: string
val ext_typeN: string
@@ -1508,7 +1508,7 @@
(* wrapper *)
val split_name = "record_split_tac";
-val split_wrapper = (split_name, fn tac => split_tac ORELSE' tac);
+val split_wrapper = (split_name, fn _ => fn tac => split_tac ORELSE' tac);
@@ -2508,8 +2508,7 @@
val setup =
Sign.add_trfuns ([], parse_translation, [], []) #>
Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
- Simplifier.map_simpset (fn ss =>
- ss addsimprocs [simproc, upd_simproc, eq_simproc]);
+ Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
(* outer syntax *)
--- a/src/HOL/Tools/simpdata.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML Fri May 13 23:59:48 2011 +0200
@@ -163,9 +163,6 @@
);
open Clasimp;
-val _ = ML_Antiquote.value "clasimpset"
- (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
-
val mksimps_pairs =
[(@{const_name HOL.implies}, [@{thm mp}]),
(@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
--- a/src/HOL/Transitive_Closure.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy Fri May 13 23:59:48 2011 +0200
@@ -1027,8 +1027,8 @@
);
*}
-declaration {* fn _ =>
- Simplifier.map_ss (fn ss => ss
+setup {*
+ Simplifier.map_simpset_global (fn ss => ss
addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Fri May 13 23:59:48 2011 +0200
@@ -331,10 +331,15 @@
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
ML {*
fun record_auto_tac ctxt =
- auto_tac (claset_of ctxt addIs [ext] addSWrapper Record.split_wrapper,
- simpset_of ctxt addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
- @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
- @{thm o_apply}, @{thm Let_def}])
+ let val ctxt' =
+ (ctxt addIs [ext])
+ |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
+ |> map_simpset (fn ss => ss addsimps
+ [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
+ @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
+ @{thm o_apply}, @{thm Let_def}])
+ in auto_tac ctxt' end;
+
*}
method_setup record_auto = {*
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Fri May 13 23:59:48 2011 +0200
@@ -102,35 +102,25 @@
text{*This ML code does the inductions directly.*}
ML{*
fun ns_constrains_tac ctxt i =
- let
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
- in
- SELECT_GOAL
- (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1),
- REPEAT (resolve_tac [@{thm StableI}, @{thm stableI},
- @{thm constrains_imp_Constrains}] 1),
- rtac @{thm ns_constrainsI} 1,
- full_simp_tac ss 1,
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS (clarify_tac (cs delrules [impI, @{thm impCE}])),
- REPEAT (FIRSTGOAL analz_mono_contra_tac),
- ALLGOALS (asm_simp_tac ss)]) i
- end;
+ SELECT_GOAL
+ (EVERY
+ [REPEAT (etac @{thm Always_ConstrainsI} 1),
+ REPEAT (resolve_tac [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1),
+ rtac @{thm ns_constrainsI} 1,
+ full_simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])),
+ REPEAT (FIRSTGOAL analz_mono_contra_tac),
+ ALLGOALS (asm_simp_tac (simpset_of ctxt))]) i;
(*Tactic for proving secrecy theorems*)
fun ns_induct_tac ctxt =
- let
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
- in
- (SELECT_GOAL o EVERY)
- [rtac @{thm AlwaysI} 1,
- force_tac (cs,ss) 1,
- (*"reachable" gets in here*)
- rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
- ns_constrains_tac ctxt 1]
- end;
+ (SELECT_GOAL o EVERY)
+ [rtac @{thm AlwaysI} 1,
+ force_tac ctxt 1,
+ (*"reachable" gets in here*)
+ rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
+ ns_constrains_tac ctxt 1];
*}
method_setup ns_induct = {*
--- a/src/HOL/UNITY/UNITY_Main.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Fri May 13 23:59:48 2011 +0200
@@ -19,4 +19,10 @@
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
*} "for proving progress properties"
+setup {*
+ Simplifier.map_simpset_global (fn ss => ss
+ addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
+ addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}))
+*}
+
end
--- a/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 23:59:48 2011 +0200
@@ -14,51 +14,42 @@
(*Proves "co" properties when the program is specified. Any use of invariants
(from weak constrains) must have been done already.*)
fun constrains_tac ctxt i =
- let
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
- in
- SELECT_GOAL
- (EVERY [REPEAT (Always_Int_tac 1),
- (*reduce the fancy safety properties to "constrains"*)
- REPEAT (etac @{thm Always_ConstrainsI} 1
- ORELSE
- resolve_tac [@{thm StableI}, @{thm stableI},
- @{thm constrains_imp_Constrains}] 1),
- (*for safety, the totalize operator can be ignored*)
- simp_tac (HOL_ss addsimps
- [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
- rtac @{thm constrainsI} 1,
- full_simp_tac ss 1,
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS (clarify_tac cs),
- ALLGOALS (asm_full_simp_tac ss)]) i
- end;
+ SELECT_GOAL
+ (EVERY
+ [REPEAT (Always_Int_tac 1),
+ (*reduce the fancy safety properties to "constrains"*)
+ REPEAT (etac @{thm Always_ConstrainsI} 1
+ ORELSE
+ resolve_tac [@{thm StableI}, @{thm stableI},
+ @{thm constrains_imp_Constrains}] 1),
+ (*for safety, the totalize operator can be ignored*)
+ simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
+ rtac @{thm constrainsI} 1,
+ full_simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac ctxt),
+ ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac ctxt sact =
- let
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
- in
- SELECT_GOAL
- (EVERY [REPEAT (Always_Int_tac 1),
- etac @{thm Always_LeadsTo_Basis} 1
- ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
- @{thm EnsuresI}, @{thm ensuresI}] 1),
- (*now there are two subgoals: co & transient*)
- simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
- res_inst_tac (Simplifier.the_context ss)
- [(("act", 0), sact)] @{thm totalize_transientI} 2
- ORELSE res_inst_tac (Simplifier.the_context ss)
- [(("act", 0), sact)] @{thm transientI} 2,
- (*simplify the command's domain*)
- simp_tac (ss addsimps [@{thm Domain_def}]) 3,
- constrains_tac ctxt 1,
- ALLGOALS (clarify_tac cs),
- ALLGOALS (asm_lr_simp_tac ss)])
- end;
+ SELECT_GOAL
+ (EVERY
+ [REPEAT (Always_Int_tac 1),
+ etac @{thm Always_LeadsTo_Basis} 1
+ ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
+ REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
+ @{thm EnsuresI}, @{thm ensuresI}] 1),
+ (*now there are two subgoals: co & transient*)
+ simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
+ res_inst_tac ctxt
+ [(("act", 0), sact)] @{thm totalize_transientI} 2
+ ORELSE res_inst_tac ctxt
+ [(("act", 0), sact)] @{thm transientI} 2,
+ (*simplify the command's domain*)
+ simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
+ constrains_tac ctxt 1,
+ ALLGOALS (clarify_tac ctxt),
+ ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
(*Composition equivalences, from Lift_prog*)
@@ -68,6 +59,3 @@
th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
-Simplifier.change_simpset (fn ss => ss
- addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
- addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));
--- a/src/HOL/Word/Word.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/Word/Word.thy Fri May 13 23:59:48 2011 +0200
@@ -1475,11 +1475,9 @@
fun arith_tac' n t =
Arith_Data.verbose_arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty;
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
in
- [ clarify_tac cs 1,
- full_simp_tac (uint_arith_ss_of ss) 1,
+ [ clarify_tac ctxt 1,
+ full_simp_tac (uint_arith_ss_of (simpset_of ctxt)) 1,
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits}
addcongs @{thms power_False_cong})),
rewrite_goals_tac @{thms word_size},
@@ -2034,11 +2032,9 @@
fun arith_tac' n t =
Arith_Data.verbose_arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty;
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
in
- [ clarify_tac cs 1,
- full_simp_tac (unat_arith_ss_of ss) 1,
+ [ clarify_tac ctxt 1,
+ full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1,
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits}
addcongs @{thms power_False_cong})),
rewrite_goals_tac @{thms word_size},
--- a/src/HOL/ex/MT.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/HOL/ex/MT.thy Fri May 13 23:59:48 2011 +0200
@@ -869,7 +869,7 @@
ve + {ev |-> v} hastyenv te + {ev |=> t}"
apply (unfold hasty_env_def)
apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
-apply (tactic {* safe_tac HOL_cs *})
+apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
apply (case_tac "ev=x")
apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
apply (simp add: ve_app_owr2 te_app_owr2)
@@ -906,7 +906,7 @@
v_clos(cl) hasty t"
apply (unfold hasty_env_def hasty_def)
apply (drule elab_fix_elim)
-apply (tactic {* safe_tac HOL_cs *})
+apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
(*Do a single unfolding of cl*)
apply (frule ssubst) prefer 2 apply assumption
apply (rule hasty_rel_clos_coind)
@@ -914,7 +914,7 @@
apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
-apply (tactic {* safe_tac HOL_cs *})
+apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
apply (case_tac "ev2=ev1a")
apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
apply blast
--- a/src/Provers/blast.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/Provers/blast.ML Fri May 13 23:59:48 2011 +0200
@@ -51,7 +51,6 @@
signature BLAST =
sig
- type claset
exception TRANS of string (*reports translation errors*)
datatype term =
Const of string * term list
@@ -61,9 +60,9 @@
| Bound of int
| Abs of string*term
| $ of term*term;
- val depth_tac: claset -> int -> int -> tactic
+ val depth_tac: Proof.context -> int -> int -> tactic
val depth_limit: int Config.T
- val blast_tac: claset -> int -> tactic
+ val blast_tac: Proof.context -> int -> tactic
val setup: theory -> theory
(*debugging tools*)
type branch
@@ -75,8 +74,8 @@
val fromSubgoal: theory -> Term.term -> term
val instVars: term -> (unit -> unit)
val toTerm: int -> term -> Term.term
- val readGoal: theory -> string -> term
- val tryInThy: theory -> claset -> int -> string ->
+ val readGoal: Proof.context -> string -> term
+ val tryIt: Proof.context -> int -> string ->
(int -> tactic) list * branch list list * (int * int * exn) list
val normBr: branch -> branch
end;
@@ -85,7 +84,6 @@
struct
structure Classical = Data.Classical;
-type claset = Classical.claset;
val trace = Unsynchronized.ref false
and stats = Unsynchronized.ref false; (*for runtime and search statistics*)
@@ -915,9 +913,10 @@
bound on unsafe expansions.
"start" is CPU time at start, for printing search time
*)
-fun prove (state, start, cs, brs, cont) =
+fun prove (state, start, ctxt, brs, cont) =
let val State {thy, ntrail, nclosed, ntried, ...} = state;
- val {safe0_netpair, safep_netpair, haz_netpair, ...} = Classical.rep_cs cs
+ val {safe0_netpair, safep_netpair, haz_netpair, ...} =
+ Classical.rep_cs (Classical.claset_of ctxt);
val safeList = [safe0_netpair, safep_netpair]
and hazList = [haz_netpair]
fun prv (tacs, trs, choices, []) =
@@ -1237,7 +1236,7 @@
"start" is CPU time at start, for printing SEARCH time
(also prints reconstruction time)
"lim" is depth limit.*)
-fun timing_depth_tac start cs lim i st0 =
+fun timing_depth_tac start ctxt lim i st0 =
let val thy = Thm.theory_of_thm st0
val state = initialize thy
val st = st0
@@ -1261,20 +1260,20 @@
Seq.make(fn()=> cell))
end
in
- prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
+ prove (state, start, ctxt, [initBranch (mkGoal concl :: hyps, lim)], cont)
|> Seq.map (rotate_prems (1 - i))
end
handle PROVE => Seq.empty;
(*Public version with fixed depth*)
-fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
+fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;
val (depth_limit, setup_depth_limit) =
Attrib.config_int_global @{binding blast_depth_limit} (K 20);
-fun blast_tac cs i st =
+fun blast_tac ctxt i st =
((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
- (timing_depth_tac (Timing.start ()) cs) 0) i
+ (timing_depth_tac (Timing.start ()) ctxt) 0) i
THEN flexflex_tac) st
handle TRANS s =>
((if !trace then warning ("blast: " ^ s) else ());
@@ -1288,13 +1287,15 @@
val fullTrace = Unsynchronized.ref ([]: branch list list);
(*Read a string to make an initial, singleton branch*)
-fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
+fun readGoal ctxt s =
+ Syntax.read_prop ctxt s |> fromTerm (Proof_Context.theory_of ctxt) |> rand |> mkGoal;
-fun tryInThy thy cs lim s =
+fun tryIt ctxt lim s =
let
+ val thy = Proof_Context.theory_of ctxt;
val state as State {fullTrace = ft, ...} = initialize thy;
val res = timeap prove
- (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I);
+ (state, Timing.start (), ctxt, [initBranch ([readGoal ctxt s], lim)], I);
val _ = fullTrace := !ft;
in res end;
@@ -1305,8 +1306,8 @@
setup_depth_limit #>
Method.setup @{binding blast}
(Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
- (fn NONE => Classical.cla_meth' blast_tac
- | SOME lim => Classical.cla_meth' (fn cs => depth_tac cs lim)))
+ (fn NONE => SIMPLE_METHOD' o blast_tac
+ | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
"classical tableau prover";
end;
--- a/src/Provers/clasimp.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/Provers/clasimp.ML Fri May 13 23:59:48 2011 +0200
@@ -5,48 +5,28 @@
splitter.ML, classical.ML, blast.ML).
*)
-infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2
- addSss addss addss' addIffs delIffs;
-
signature CLASIMP_DATA =
sig
structure Splitter: SPLITTER
structure Classical: CLASSICAL
structure Blast: BLAST
- sharing type Classical.claset = Blast.claset
val notE: thm
val iffD1: thm
val iffD2: thm
-end
+end;
signature CLASIMP =
sig
- type claset
- type clasimpset
- val get_css: Context.generic -> clasimpset
- val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic
- val clasimpset_of: Proof.context -> clasimpset
- val addSIs2: clasimpset * thm list -> clasimpset
- val addSEs2: clasimpset * thm list -> clasimpset
- val addSDs2: clasimpset * thm list -> clasimpset
- val addIs2: clasimpset * thm list -> clasimpset
- val addEs2: clasimpset * thm list -> clasimpset
- val addDs2: clasimpset * thm list -> clasimpset
- val addsimps2: clasimpset * thm list -> clasimpset
- val delsimps2: clasimpset * thm list -> clasimpset
- val addSss: claset * simpset -> claset
- val addss: claset * simpset -> claset
- val addss': claset * simpset -> claset
- val addIffs: clasimpset * thm list -> clasimpset
- val delIffs: clasimpset * thm list -> clasimpset
- val clarsimp_tac: clasimpset -> int -> tactic
- val mk_auto_tac: clasimpset -> int -> int -> tactic
- val auto_tac: clasimpset -> tactic
- val force_tac: clasimpset -> int -> tactic
- val fast_simp_tac: clasimpset -> int -> tactic
- val slow_simp_tac: clasimpset -> int -> tactic
- val best_simp_tac: clasimpset -> int -> tactic
- val attrib: (clasimpset * thm list -> clasimpset) -> attribute
+ val addSss: Proof.context -> Proof.context
+ val addss: Proof.context -> Proof.context
+ val addss': Proof.context -> Proof.context
+ val clarsimp_tac: Proof.context -> int -> tactic
+ val mk_auto_tac: Proof.context -> int -> int -> tactic
+ val auto_tac: Proof.context -> tactic
+ val force_tac: Proof.context -> int -> tactic
+ val fast_simp_tac: Proof.context -> int -> tactic
+ val slow_simp_tac: Proof.context -> int -> tactic
+ val best_simp_tac: Proof.context -> int -> tactic
val iff_add: attribute
val iff_add': attribute
val iff_del: attribute
@@ -63,198 +43,149 @@
structure Blast = Data.Blast;
-(* type clasimpset *)
+(* simp as classical wrapper *)
-type claset = Classical.claset;
-type clasimpset = claset * simpset;
-
-fun get_css context = (Classical.get_cs context, Simplifier.get_ss context);
+(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
+val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);
-fun map_css f context =
- let
- val (cs, ss) = get_css context;
- val (cs', ss') = f (cs, Simplifier.context (Context.proof_of context) ss);
- in
- context
- |> Classical.map_cs (K cs')
- |> Simplifier.map_ss (K (Simplifier.inherit_context ss ss'))
- end;
+fun clasimp f name tac ctxt =
+ Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
-fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);
+(*Add a simpset to the claset!*)
+(*Caution: only one simpset added can be added by each of addSss and addss*)
+val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
+val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
+(* FIXME "asm_lr_simp_tac" !? *)
+val addss' = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_lr_simp_tac;
-(* clasimpset operations *)
-
-(*this interface for updating a clasimpset is rudimentary and just for
- convenience for the most common cases*)
-
-fun pair_upd1 f ((a, b), x) = (f (a, x), b);
-fun pair_upd2 f ((a, b), x) = (a, f (b, x));
+(* iffs: addition of rules to simpsets and clasets simultaneously *)
-fun op addSIs2 arg = pair_upd1 Classical.addSIs arg;
-fun op addSEs2 arg = pair_upd1 Classical.addSEs arg;
-fun op addSDs2 arg = pair_upd1 Classical.addSDs arg;
-fun op addIs2 arg = pair_upd1 Classical.addIs arg;
-fun op addEs2 arg = pair_upd1 Classical.addEs arg;
-fun op addDs2 arg = pair_upd1 Classical.addDs arg;
-fun op addsimps2 arg = pair_upd2 Simplifier.addsimps arg;
-fun op delsimps2 arg = pair_upd2 Simplifier.delsimps arg;
-
-(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
-val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true,true,true);
-
-(*Add a simpset to a classical set!*)
-(*Caution: only one simpset added can be added by each of addSss and addss*)
-fun cs addSss ss =
- Classical.addSafter (cs, ("safe_asm_full_simp_tac", CHANGED o safe_asm_full_simp_tac ss));
-
-fun cs addss ss =
- Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_full_simp_tac ss));
-
-fun cs addss' ss =
- Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_lr_simp_tac ss));
-
-(* iffs: addition of rules to simpsets and clasets simultaneously *)
+local
(*Takes (possibly conditional) theorems of the form A<->B to
the Safe Intr rule B==>A and
the Safe Destruct rule A==>B.
Also ~A goes to the Safe Elim rule A ==> ?R
Failing other cases, A is added as a Safe Intr rule*)
-local
-fun addIff decls1 decls2 simp ((cs, ss), th) =
- let
- val n = nprems_of th;
- val (elim, intro) = if n = 0 then decls1 else decls2;
- val zero_rotate = zero_var_indexes o rotate_prems n;
- in
- (elim (intro (cs, [zero_rotate (th RS Data.iffD2)]),
- [Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
- handle THM _ => (elim (cs, [zero_rotate (th RS Data.notE)])
- handle THM _ => intro (cs, [th])),
- simp (ss, [th]))
- end;
+fun app (att: attribute) th context = #1 (att (context, th));
-fun delIff delcs delss ((cs, ss), th) =
+fun add_iff safe unsafe =
+ Thm.declaration_attribute (fn th =>
+ let
+ val n = nprems_of th;
+ val (elim, intro) = if n = 0 then safe else unsafe;
+ val zero_rotate = zero_var_indexes o rotate_prems n;
+ in
+ app intro (zero_rotate (th RS Data.iffD2)) #>
+ app elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
+ handle THM _ => (app elim (zero_rotate (th RS Data.notE)) handle THM _ => app intro th)
+ end);
+
+fun del_iff del = Thm.declaration_attribute (fn th =>
let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
- (delcs (cs, [zero_rotate (th RS Data.iffD2),
- Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
- handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
- handle THM _ => delcs (cs, [th])),
- delss (ss, [th]))
- end;
-
-fun modifier att (x, ths) =
- fst (Library.foldl_map (Library.apply [att]) (x, rev ths));
-
-val addXIs = modifier (Context_Rules.intro_query NONE);
-val addXEs = modifier (Context_Rules.elim_query NONE);
-val delXs = modifier Context_Rules.rule_del;
+ app del (zero_rotate (th RS Data.iffD2)) #>
+ app del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
+ handle THM _ => (app del (zero_rotate (th RS Data.notE)) handle THM _ => app del th)
+ end);
in
-val op addIffs =
- Library.foldl
- (addIff (Classical.addSEs, Classical.addSIs)
- (Classical.addEs, Classical.addIs)
- Simplifier.addsimps);
-val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps);
+val iff_add =
+ add_iff
+ (Classical.safe_elim NONE, Classical.safe_intro NONE)
+ (Classical.haz_elim NONE, Classical.haz_intro NONE)
+ #> Simplifier.simp_add;
-fun addIffs_generic (x, ths) =
- Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1;
+val iff_add' =
+ add_iff
+ (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE)
+ (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
-fun delIffs_generic (x, ths) =
- Library.foldl (delIff delXs #1) ((x, ()), ths) |> #1;
+val iff_del =
+ del_iff Classical.rule_del #>
+ del_iff Context_Rules.rule_del #>
+ Simplifier.simp_del;
end;
(* tactics *)
-fun clarsimp_tac (cs, ss) =
- safe_asm_full_simp_tac ss THEN_ALL_NEW
- Classical.clarify_tac (cs addSss ss);
+fun clarsimp_tac ctxt =
+ safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
+ Classical.clarify_tac (addSss ctxt);
(* auto_tac *)
-fun blast_depth_tac cs m i thm =
- Blast.depth_tac cs m i thm
+fun blast_depth_tac ctxt m i thm =
+ Blast.depth_tac ctxt m i thm
handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
(* a variant of depth_tac that avoids interference of the simplifier
with dup_step_tac when they are combined by auto_tac *)
local
-fun slow_step_tac' cs =
- Classical.appWrappers cs
- (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
+fun slow_step_tac' ctxt =
+ Classical.appWrappers ctxt
+ (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt);
in
-fun nodup_depth_tac cs m i st =
+fun nodup_depth_tac ctxt m i st =
SELECT_GOAL
- (Classical.safe_steps_tac cs 1 THEN_ELSE
- (DEPTH_SOLVE (nodup_depth_tac cs m 1),
- Classical.inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
- (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m - 1) 1)))) i st;
+ (Classical.safe_steps_tac ctxt 1 THEN_ELSE
+ (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
+ Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
+ (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
end;
(*Designed to be idempotent, except if blast_depth_tac instantiates variables
in some of the subgoals*)
-fun mk_auto_tac (cs, ss) m n =
+fun mk_auto_tac ctxt m n =
let
- val cs' = cs addss ss;
val main_tac =
- blast_depth_tac cs m (* fast but can't use wrappers *)
+ blast_depth_tac ctxt m (* fast but can't use wrappers *)
ORELSE'
- (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
+ (CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *)
in
- PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)) THEN
- TRY (Classical.safe_tac cs) THEN
+ PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN
+ TRY (Classical.safe_tac ctxt) THEN
REPEAT_DETERM (FIRSTGOAL main_tac) THEN
- TRY (Classical.safe_tac (cs addSss ss)) THEN
+ TRY (Classical.safe_tac (addSss ctxt)) THEN
prune_params_tac
end;
-fun auto_tac css = mk_auto_tac css 4 2;
+fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
(* force_tac *)
(* aimed to solve the given subgoal totally, using whatever tools possible *)
-fun force_tac (cs, ss) =
- let val cs' = cs addss ss in
+fun force_tac ctxt =
+ let val ctxt' = addss ctxt in
SELECT_GOAL
- (Classical.clarify_tac cs' 1 THEN
- IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1) THEN
- ALLGOALS (Classical.first_best_tac cs'))
+ (Classical.clarify_tac ctxt' 1 THEN
+ IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN
+ ALLGOALS (Classical.first_best_tac ctxt'))
end;
(* basic combinations *)
-fun ADDSS tac (cs, ss) = let val cs' = cs addss ss in tac cs' end;
-
-val fast_simp_tac = ADDSS Classical.fast_tac;
-val slow_simp_tac = ADDSS Classical.slow_tac;
-val best_simp_tac = ADDSS Classical.best_tac;
+val fast_simp_tac = Classical.fast_tac o addss;
+val slow_simp_tac = Classical.slow_tac o addss;
+val best_simp_tac = Classical.best_tac o addss;
-(** access clasimpset **)
+(** concrete syntax **)
(* attributes *)
-fun attrib f = Thm.declaration_attribute (fn th => map_css (fn css => f (css, [th])));
-fun attrib' f (x, th) = (f (x, [th]), th);
-
-val iff_add = attrib (op addIffs);
-val iff_add' = attrib' addIffs_generic;
-val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
-
fun iff_att x = (Scan.lift
(Args.del >> K iff_del ||
Scan.option Args.add -- Args.query >> K iff_add' ||
@@ -277,21 +208,14 @@
(* methods *)
-fun clasimp_meth tac ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt));
-
-fun clasimp_meth' tac ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt)));
-
-
fun clasimp_method' tac =
- Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
+ Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
val auto_method =
Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
Method.sections clasimp_modifiers >>
- (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
- | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
+ (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
+ | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
(* theory setup *)
--- a/src/Provers/classical.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/Provers/classical.ML Fri May 13 23:59:48 2011 +0200
@@ -25,11 +25,11 @@
signature CLASSICAL_DATA =
sig
- val imp_elim : thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
- val not_elim : thm (* ~P ==> P ==> R *)
- val swap : thm (* ~ P ==> (~ R ==> P) ==> R *)
- val classical : thm (* (~ P ==> P) ==> P *)
- val sizef : thm -> int (* size function for BEST_FIRST *)
+ val imp_elim: thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
+ val not_elim: thm (* ~P ==> P ==> R *)
+ val swap: thm (* ~ P ==> (~ R ==> P) ==> R *)
+ val classical: thm (* (~ P ==> P) ==> P *)
+ val sizef: thm -> int (* size function for BEST_FIRST *)
val hyp_subst_tacs: (int -> tactic) list
end;
@@ -37,84 +37,82 @@
sig
type claset
val empty_cs: claset
- val print_cs: Proof.context -> claset -> unit
- val rep_cs:
- claset -> {safeIs: thm list, safeEs: thm list,
- hazIs: thm list, hazEs: thm list,
- swrappers: (string * wrapper) list,
- uwrappers: (string * wrapper) list,
- safe0_netpair: netpair, safep_netpair: netpair,
- haz_netpair: netpair, dup_netpair: netpair,
- xtra_netpair: Context_Rules.netpair}
- val merge_cs : claset * claset -> claset
- val addDs : claset * thm list -> claset
- val addEs : claset * thm list -> claset
- val addIs : claset * thm list -> claset
- val addSDs : claset * thm list -> claset
- val addSEs : claset * thm list -> claset
- val addSIs : claset * thm list -> claset
- val delrules : claset * thm list -> claset
- val addSWrapper : claset * (string * wrapper) -> claset
- val delSWrapper : claset * string -> claset
- val addWrapper : claset * (string * wrapper) -> claset
- val delWrapper : claset * string -> claset
- val addSbefore : claset * (string * (int -> tactic)) -> claset
- val addSafter : claset * (string * (int -> tactic)) -> claset
- val addbefore : claset * (string * (int -> tactic)) -> claset
- val addafter : claset * (string * (int -> tactic)) -> claset
- val addD2 : claset * (string * thm) -> claset
- val addE2 : claset * (string * thm) -> claset
- val addSD2 : claset * (string * thm) -> claset
- val addSE2 : claset * (string * thm) -> claset
- val appSWrappers : claset -> wrapper
- val appWrappers : claset -> wrapper
+ val rep_cs: claset ->
+ {safeIs: thm list,
+ safeEs: thm list,
+ hazIs: thm list,
+ hazEs: thm list,
+ swrappers: (string * (Proof.context -> wrapper)) list,
+ uwrappers: (string * (Proof.context -> wrapper)) list,
+ safe0_netpair: netpair,
+ safep_netpair: netpair,
+ haz_netpair: netpair,
+ dup_netpair: netpair,
+ xtra_netpair: Context_Rules.netpair}
+ val print_claset: Proof.context -> unit
+ val addDs: Proof.context * thm list -> Proof.context
+ val addEs: Proof.context * thm list -> Proof.context
+ val addIs: Proof.context * thm list -> Proof.context
+ val addSDs: Proof.context * thm list -> Proof.context
+ val addSEs: Proof.context * thm list -> Proof.context
+ val addSIs: Proof.context * thm list -> Proof.context
+ val delrules: Proof.context * thm list -> Proof.context
+ val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
+ val delSWrapper: claset * string -> claset
+ val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
+ val delWrapper: claset * string -> claset
+ val addSbefore: claset * (string * (int -> tactic)) -> claset
+ val addSafter: claset * (string * (int -> tactic)) -> claset
+ val addbefore: claset * (string * (int -> tactic)) -> claset
+ val addafter: claset * (string * (int -> tactic)) -> claset
+ val addD2: claset * (string * thm) -> claset
+ val addE2: claset * (string * thm) -> claset
+ val addSD2: claset * (string * thm) -> claset
+ val addSE2: claset * (string * thm) -> claset
+ val appSWrappers: Proof.context -> wrapper
+ val appWrappers: Proof.context -> wrapper
- val global_claset_of : theory -> claset
- val claset_of : Proof.context -> claset
+ val global_claset_of: theory -> claset
+ val claset_of: Proof.context -> claset
+ val map_claset: (claset -> claset) -> Proof.context -> Proof.context
+ val put_claset: claset -> Proof.context -> Proof.context
- val fast_tac : claset -> int -> tactic
- val slow_tac : claset -> int -> tactic
- val weight_ASTAR : int Unsynchronized.ref
- val astar_tac : claset -> int -> tactic
- val slow_astar_tac : claset -> int -> tactic
- val best_tac : claset -> int -> tactic
- val first_best_tac : claset -> int -> tactic
- val slow_best_tac : claset -> int -> tactic
- val depth_tac : claset -> int -> int -> tactic
- val deepen_tac : claset -> int -> int -> tactic
+ val fast_tac: Proof.context -> int -> tactic
+ val slow_tac: Proof.context -> int -> tactic
+ val astar_tac: Proof.context -> int -> tactic
+ val slow_astar_tac: Proof.context -> int -> tactic
+ val best_tac: Proof.context -> int -> tactic
+ val first_best_tac: Proof.context -> int -> tactic
+ val slow_best_tac: Proof.context -> int -> tactic
+ val depth_tac: Proof.context -> int -> int -> tactic
+ val deepen_tac: Proof.context -> int -> int -> tactic
- val contr_tac : int -> tactic
- val dup_elim : thm -> thm
- val dup_intr : thm -> thm
- val dup_step_tac : claset -> int -> tactic
- val eq_mp_tac : int -> tactic
- val haz_step_tac : claset -> int -> tactic
- val joinrules : thm list * thm list -> (bool * thm) list
- val mp_tac : int -> tactic
- val safe_tac : claset -> tactic
- val safe_steps_tac : claset -> int -> tactic
- val safe_step_tac : claset -> int -> tactic
- val clarify_tac : claset -> int -> tactic
- val clarify_step_tac : claset -> int -> tactic
- val step_tac : claset -> int -> tactic
- val slow_step_tac : claset -> int -> tactic
- val swapify : thm list -> thm list
- val swap_res_tac : thm list -> int -> tactic
- val inst_step_tac : claset -> int -> tactic
- val inst0_step_tac : claset -> int -> tactic
- val instp_step_tac : claset -> int -> tactic
+ val contr_tac: int -> tactic
+ val dup_elim: thm -> thm
+ val dup_intr: thm -> thm
+ val dup_step_tac: Proof.context -> int -> tactic
+ val eq_mp_tac: int -> tactic
+ val haz_step_tac: Proof.context -> int -> tactic
+ val joinrules: thm list * thm list -> (bool * thm) list
+ val mp_tac: int -> tactic
+ val safe_tac: Proof.context -> tactic
+ val safe_steps_tac: Proof.context -> int -> tactic
+ val safe_step_tac: Proof.context -> int -> tactic
+ val clarify_tac: Proof.context -> int -> tactic
+ val clarify_step_tac: Proof.context -> int -> tactic
+ val step_tac: Proof.context -> int -> tactic
+ val slow_step_tac: Proof.context -> int -> tactic
+ val swapify: thm list -> thm list
+ val swap_res_tac: thm list -> int -> tactic
+ val inst_step_tac: Proof.context -> int -> tactic
+ val inst0_step_tac: Proof.context -> int -> tactic
+ val instp_step_tac: Proof.context -> int -> tactic
end;
signature CLASSICAL =
sig
include BASIC_CLASSICAL
val classical_rule: thm -> thm
- val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
- val del_context_safe_wrapper: string -> theory -> theory
- val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
- val del_context_unsafe_wrapper: string -> theory -> theory
- val get_claset: Proof.context -> claset
- val put_claset: claset -> Proof.context -> Proof.context
val get_cs: Context.generic -> claset
val map_cs: (claset -> claset) -> Context.generic -> Context.generic
val safe_dest: int option -> attribute
@@ -125,10 +123,10 @@
val haz_intro: int option -> attribute
val rule_del: attribute
val cla_modifiers: Method.modifier parser list
- val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
- val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
- val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
- val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
+ val cla_method:
+ (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
+ val cla_method':
+ (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
val setup: theory -> theory
end;
@@ -136,8 +134,6 @@
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
struct
-local open Data in
-
(** classical elimination rules **)
(*
@@ -155,7 +151,7 @@
fun classical_rule rule =
if is_some (Object_Logic.elim_concl rule) then
let
- val rule' = rule RS classical;
+ val rule' = rule RS Data.classical;
val concl' = Thm.concl_of rule';
fun redundant_hyp goal =
concl' aconv Logic.strip_assums_concl goal orelse
@@ -181,15 +177,15 @@
(*Prove goal that assumes both P and ~P.
No backtracking if it finds an equal assumption. Perhaps should call
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
-val contr_tac = eresolve_tac [not_elim] THEN'
- (eq_assume_tac ORELSE' assume_tac);
+val contr_tac =
+ eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac);
(*Finds P-->Q and P in the assumptions, replaces implication by Q.
Could do the same thing for P<->Q and P... *)
-fun mp_tac i = eresolve_tac [not_elim, Data.imp_elim] i THEN assume_tac i;
+fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
(*Like mp_tac but instantiates no variables*)
-fun eq_mp_tac i = ematch_tac [not_elim, Data.imp_elim] i THEN eq_assume_tac i;
+fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
(*Creates rules to eliminate ~A, from rules to introduce A*)
fun swapify intrs = intrs RLN (2, [Data.swap]);
@@ -198,16 +194,16 @@
(*Uses introduction rules in the normal way, or on negated assumptions,
trying rules in order. *)
fun swap_res_tac rls =
- let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
- in assume_tac ORELSE'
- contr_tac ORELSE'
- biresolve_tac (fold_rev addrl rls [])
- end;
+ let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in
+ assume_tac ORELSE'
+ contr_tac ORELSE'
+ biresolve_tac (fold_rev addrl rls [])
+ end;
(*Duplication of hazardous rules, for complete provers*)
-fun dup_intr th = zero_var_indexes (th RS classical);
+fun dup_intr th = zero_var_indexes (th RS Data.classical);
-fun dup_elim th =
+fun dup_elim th = (* FIXME proper context!? *)
let
val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
@@ -217,17 +213,18 @@
(**** Classical rule sets ****)
datatype claset =
- CS of {safeIs : thm list, (*safe introduction rules*)
- safeEs : thm list, (*safe elimination rules*)
- hazIs : thm list, (*unsafe introduction rules*)
- hazEs : thm list, (*unsafe elimination rules*)
- swrappers : (string * wrapper) list, (*for transforming safe_step_tac*)
- uwrappers : (string * wrapper) list, (*for transforming step_tac*)
- safe0_netpair : netpair, (*nets for trivial cases*)
- safep_netpair : netpair, (*nets for >0 subgoals*)
- haz_netpair : netpair, (*nets for unsafe rules*)
- dup_netpair : netpair, (*nets for duplication*)
- xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
+ CS of
+ {safeIs : thm list, (*safe introduction rules*)
+ safeEs : thm list, (*safe elimination rules*)
+ hazIs : thm list, (*unsafe introduction rules*)
+ hazEs : thm list, (*unsafe elimination rules*)
+ swrappers : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*)
+ uwrappers : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*)
+ safe0_netpair : netpair, (*nets for trivial cases*)
+ safep_netpair : netpair, (*nets for >0 subgoals*)
+ haz_netpair : netpair, (*nets for unsafe rules*)
+ dup_netpair : netpair, (*nets for duplication*)
+ xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
(*Desired invariants are
safe0_netpair = build safe0_brls,
@@ -246,34 +243,21 @@
val empty_netpair = (Net.empty, Net.empty);
val empty_cs =
- CS{safeIs = [],
- safeEs = [],
- hazIs = [],
- hazEs = [],
- swrappers = [],
- uwrappers = [],
- safe0_netpair = empty_netpair,
- safep_netpair = empty_netpair,
- haz_netpair = empty_netpair,
- dup_netpair = empty_netpair,
- xtra_netpair = empty_netpair};
-
-fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
- let val pretty_thms = map (Display.pretty_thm ctxt) in
- [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
- Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
- Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
- Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
- Pretty.strs ("safe wrappers:" :: map #1 swrappers),
- Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
- |> Pretty.chunks |> Pretty.writeln
- end;
+ CS
+ {safeIs = [],
+ safeEs = [],
+ hazIs = [],
+ hazEs = [],
+ swrappers = [],
+ uwrappers = [],
+ safe0_netpair = empty_netpair,
+ safep_netpair = empty_netpair,
+ haz_netpair = empty_netpair,
+ dup_netpair = empty_netpair,
+ xtra_netpair = empty_netpair};
fun rep_cs (CS args) = args;
-fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
-fun appWrappers (CS {uwrappers, ...}) = fold snd uwrappers;
-
(*** Adding (un)safe introduction or elimination rules.
@@ -313,151 +297,144 @@
val mem_thm = member Thm.eq_thm_prop
and rem_thm = remove Thm.eq_thm_prop;
-(*Warn if the rule is already present ELSEWHERE in the claset. The addition
- is still allowed.*)
-fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
- if mem_thm safeIs th then
- warning ("Rule already declared as safe introduction (intro!)\n" ^
- Display.string_of_thm_without_context th)
- else if mem_thm safeEs th then
- warning ("Rule already declared as safe elimination (elim!)\n" ^
- Display.string_of_thm_without_context th)
- else if mem_thm hazIs th then
- warning ("Rule already declared as introduction (intro)\n" ^
- Display.string_of_thm_without_context th)
- else if mem_thm hazEs th then
- warning ("Rule already declared as elimination (elim)\n" ^
- Display.string_of_thm_without_context th)
- else ();
+fun string_of_thm NONE = Display.string_of_thm_without_context
+ | string_of_thm (SOME context) =
+ Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
+
+fun make_elim context th =
+ if has_fewer_prems 1 th then
+ error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
+ else Tactic.make_elim th;
+
+fun warn context msg rules th =
+ mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true);
+
+fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
+ warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
+ warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
+ warn context "Rule already declared as introduction (intro)\n" hazIs th orelse
+ warn context "Rule already declared as elimination (elim)\n" hazEs th;
(*** Safe rules ***)
-fun addSI w th
- (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
- safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm safeIs th then
- (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
- Display.string_of_thm_without_context th); cs)
+fun addSI w context th
+ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
+ if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
else
- let val th' = flat_rule th
+ let
+ val th' = flat_rule th;
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
- List.partition Thm.no_prems [th']
- val nI = length safeIs + 1
- and nE = length safeEs
- in warn_dup th cs;
- CS{safeIs = th::safeIs,
+ List.partition Thm.no_prems [th'];
+ val nI = length safeIs + 1;
+ val nE = length safeEs;
+ val _ = warn_other context th cs;
+ in
+ CS
+ {safeIs = th::safeIs,
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
- safeEs = safeEs,
- hazIs = hazIs,
- hazEs = hazEs,
- swrappers = swrappers,
- uwrappers = uwrappers,
- haz_netpair = haz_netpair,
- dup_netpair = dup_netpair,
+ safeEs = safeEs,
+ hazIs = hazIs,
+ hazEs = hazEs,
+ swrappers = swrappers,
+ uwrappers = uwrappers,
+ haz_netpair = haz_netpair,
+ dup_netpair = dup_netpair,
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
- end;
+ end;
-fun addSE w th
- (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
- safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm safeEs th then
- (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
- Display.string_of_thm_without_context th); cs)
+fun addSE w context th
+ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
+ if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
else if has_fewer_prems 1 th then
- error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
+ error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
- let
- val th' = classical_rule (flat_rule th)
+ let
+ val th' = classical_rule (flat_rule th);
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
- List.partition (fn rl => nprems_of rl=1) [th']
- val nI = length safeIs
- and nE = length safeEs + 1
- in warn_dup th cs;
- CS{safeEs = th::safeEs,
+ List.partition (fn rl => nprems_of rl=1) [th'];
+ val nI = length safeIs;
+ val nE = length safeEs + 1;
+ val _ = warn_other context th cs;
+ in
+ CS
+ {safeEs = th::safeEs,
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
- safeIs = safeIs,
- hazIs = hazIs,
- hazEs = hazEs,
- swrappers = swrappers,
- uwrappers = uwrappers,
- haz_netpair = haz_netpair,
- dup_netpair = dup_netpair,
+ safeIs = safeIs,
+ hazIs = hazIs,
+ hazEs = hazEs,
+ swrappers = swrappers,
+ uwrappers = uwrappers,
+ haz_netpair = haz_netpair,
+ dup_netpair = dup_netpair,
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
- end;
+ end;
-fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
-fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
-
-fun make_elim th =
- if has_fewer_prems 1 th then
- error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
- else Tactic.make_elim th;
-
-fun cs addSDs ths = cs addSEs (map make_elim ths);
+fun addSD w context th = addSE w context (make_elim context th);
(*** Hazardous (unsafe) rules ***)
-fun addI w th
- (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
- safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm hazIs th then
- (warning ("Ignoring duplicate introduction (intro)\n" ^
- Display.string_of_thm_without_context th); cs)
+fun addI w context th
+ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
+ if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
else
- let val th' = flat_rule th
- val nI = length hazIs + 1
- and nE = length hazEs
- in warn_dup th cs;
- CS{hazIs = th::hazIs,
- haz_netpair = insert (nI,nE) ([th'], []) haz_netpair,
- dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair,
- safeIs = safeIs,
- safeEs = safeEs,
- hazEs = hazEs,
- swrappers = swrappers,
- uwrappers = uwrappers,
+ let
+ val th' = flat_rule th;
+ val nI = length hazIs + 1;
+ val nE = length hazEs;
+ val _ = warn_other context th cs;
+ in
+ CS
+ {hazIs = th :: hazIs,
+ haz_netpair = insert (nI, nE) ([th'], []) haz_netpair,
+ dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair,
+ safeIs = safeIs,
+ safeEs = safeEs,
+ hazEs = hazEs,
+ swrappers = swrappers,
+ uwrappers = uwrappers,
safe0_netpair = safe0_netpair,
safep_netpair = safep_netpair,
- xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
- end
- handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
- error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
+ xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair}
+ end
+ handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *)
+ error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
-fun addE w th
- (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
- safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm hazEs th then
- (warning ("Ignoring duplicate elimination (elim)\n" ^
- Display.string_of_thm_without_context th); cs)
+fun addE w context th
+ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
+ if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
else if has_fewer_prems 1 th then
- error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
+ error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
- let
- val th' = classical_rule (flat_rule th)
- val nI = length hazIs
- and nE = length hazEs + 1
- in warn_dup th cs;
- CS{hazEs = th::hazEs,
- haz_netpair = insert (nI,nE) ([], [th']) haz_netpair,
- dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair,
- safeIs = safeIs,
- safeEs = safeEs,
- hazIs = hazIs,
- swrappers = swrappers,
- uwrappers = uwrappers,
+ let
+ val th' = classical_rule (flat_rule th);
+ val nI = length hazIs;
+ val nE = length hazEs + 1;
+ val _ = warn_other context th cs;
+ in
+ CS
+ {hazEs = th :: hazEs,
+ haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
+ dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair,
+ safeIs = safeIs,
+ safeEs = safeEs,
+ hazIs = hazIs,
+ swrappers = swrappers,
+ uwrappers = uwrappers,
safe0_netpair = safe0_netpair,
safep_netpair = safep_netpair,
- xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair}
- end;
+ xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair}
+ end;
-fun cs addIs ths = fold_rev (addI NONE) ths cs;
-fun cs addEs ths = fold_rev (addE NONE) ths cs;
+fun addD w context th = addE w context (make_elim context th);
-fun cs addDs ths = cs addEs (map make_elim ths);
(*** Deletion of rules
@@ -466,102 +443,109 @@
***)
fun delSI th
- (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
- safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm safeIs th then
- let val th' = flat_rule th
- val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']
- in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
- safep_netpair = delete (safep_rls, []) safep_netpair,
- safeIs = rem_thm th safeIs,
- safeEs = safeEs,
- hazIs = hazIs,
- hazEs = hazEs,
- swrappers = swrappers,
- uwrappers = uwrappers,
- haz_netpair = haz_netpair,
- dup_netpair = dup_netpair,
- xtra_netpair = delete' ([th], []) xtra_netpair}
- end
- else cs;
-
-fun delSE th
- (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
- safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm safeEs th then
+ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
+ if mem_thm safeIs th then
let
- val th' = classical_rule (flat_rule th)
- val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
- in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
- safep_netpair = delete ([], safep_rls) safep_netpair,
- safeIs = safeIs,
- safeEs = rem_thm th safeEs,
- hazIs = hazIs,
- hazEs = hazEs,
- swrappers = swrappers,
- uwrappers = uwrappers,
- haz_netpair = haz_netpair,
- dup_netpair = dup_netpair,
- xtra_netpair = delete' ([], [th]) xtra_netpair}
+ val th' = flat_rule th;
+ val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
+ in
+ CS
+ {safe0_netpair = delete (safe0_rls, []) safe0_netpair,
+ safep_netpair = delete (safep_rls, []) safep_netpair,
+ safeIs = rem_thm th safeIs,
+ safeEs = safeEs,
+ hazIs = hazIs,
+ hazEs = hazEs,
+ swrappers = swrappers,
+ uwrappers = uwrappers,
+ haz_netpair = haz_netpair,
+ dup_netpair = dup_netpair,
+ xtra_netpair = delete' ([th], []) xtra_netpair}
end
else cs;
+fun delSE th
+ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
+ if mem_thm safeEs th then
+ let
+ val th' = classical_rule (flat_rule th);
+ val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
+ in
+ CS
+ {safe0_netpair = delete ([], safe0_rls) safe0_netpair,
+ safep_netpair = delete ([], safep_rls) safep_netpair,
+ safeIs = safeIs,
+ safeEs = rem_thm th safeEs,
+ hazIs = hazIs,
+ hazEs = hazEs,
+ swrappers = swrappers,
+ uwrappers = uwrappers,
+ haz_netpair = haz_netpair,
+ dup_netpair = dup_netpair,
+ xtra_netpair = delete' ([], [th]) xtra_netpair}
+ end
+ else cs;
-fun delI th
- (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
- safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm hazIs th then
- let val th' = flat_rule th
- in CS{haz_netpair = delete ([th'], []) haz_netpair,
+fun delI context th
+ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
+ if mem_thm hazIs th then
+ let val th' = flat_rule th in
+ CS
+ {haz_netpair = delete ([th'], []) haz_netpair,
dup_netpair = delete ([dup_intr th'], []) dup_netpair,
- safeIs = safeIs,
- safeEs = safeEs,
- hazIs = rem_thm th hazIs,
- hazEs = hazEs,
- swrappers = swrappers,
- uwrappers = uwrappers,
+ safeIs = safeIs,
+ safeEs = safeEs,
+ hazIs = rem_thm th hazIs,
+ hazEs = hazEs,
+ swrappers = swrappers,
+ uwrappers = uwrappers,
safe0_netpair = safe0_netpair,
safep_netpair = safep_netpair,
xtra_netpair = delete' ([th], []) xtra_netpair}
end
- else cs
- handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
- error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
-
+ else cs
+ handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *)
+ error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
fun delE th
- (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
- safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm hazEs th then
- let val th' = classical_rule (flat_rule th)
- in CS{haz_netpair = delete ([], [th']) haz_netpair,
+ (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
+ if mem_thm hazEs th then
+ let val th' = classical_rule (flat_rule th) in
+ CS
+ {haz_netpair = delete ([], [th']) haz_netpair,
dup_netpair = delete ([], [dup_elim th']) dup_netpair,
- safeIs = safeIs,
- safeEs = safeEs,
- hazIs = hazIs,
- hazEs = rem_thm th hazEs,
- swrappers = swrappers,
- uwrappers = uwrappers,
+ safeIs = safeIs,
+ safeEs = safeEs,
+ hazIs = hazIs,
+ hazEs = rem_thm th hazEs,
+ swrappers = swrappers,
+ uwrappers = uwrappers,
safe0_netpair = safe0_netpair,
safep_netpair = safep_netpair,
xtra_netpair = delete' ([], [th]) xtra_netpair}
- end
- else cs;
+ end
+ else cs;
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
-fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
+fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
let val th' = Tactic.make_elim th in
if mem_thm safeIs th orelse mem_thm safeEs th orelse
mem_thm hazIs th orelse mem_thm hazEs th orelse
mem_thm safeEs th' orelse mem_thm hazEs th'
- then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
- else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
+ then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
+ else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs)
end;
-fun cs delrules ths = fold delrule ths cs;
-(*** Modifying the wrapper tacticals ***)
+(** claset data **)
+
+(* wrappers *)
+
fun map_swrappers f
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
@@ -571,57 +555,15 @@
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
fun map_uwrappers f
- (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
swrappers = swrappers, uwrappers = f uwrappers,
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
-fun update_warn msg (p as (key : string, _)) xs =
- (if AList.defined (op =) xs key then warning msg else ();
- AList.update (op =) p xs);
-fun delete_warn msg (key : string) xs =
- if AList.defined (op =) xs key then AList.delete (op =) key xs
- else (warning msg; xs);
-
-(*Add/replace a safe wrapper*)
-fun cs addSWrapper new_swrapper = map_swrappers
- (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
-
-(*Add/replace an unsafe wrapper*)
-fun cs addWrapper new_uwrapper = map_uwrappers
- (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
-
-(*Remove a safe wrapper*)
-fun cs delSWrapper name = map_swrappers
- (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
-
-(*Remove an unsafe wrapper*)
-fun cs delWrapper name = map_uwrappers
- (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
-
-(* compose a safe tactic alternatively before/after safe_step_tac *)
-fun cs addSbefore (name, tac1) =
- cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
-fun cs addSafter (name, tac2) =
- cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
-
-(*compose a tactic alternatively before/after the step tactic *)
-fun cs addbefore (name, tac1) =
- cs addWrapper (name, fn tac2 => tac1 APPEND' tac2);
-fun cs addafter (name, tac2) =
- cs addWrapper (name, fn tac1 => tac1 APPEND' tac2);
-
-fun cs addD2 (name, thm) =
- cs addafter (name, datac thm 1);
-fun cs addE2 (name, thm) =
- cs addafter (name, eatac thm 1);
-fun cs addSD2 (name, thm) =
- cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
-fun cs addSE2 (name, thm) =
- cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
+(* merge_cs *)
(*Merge works by adding all new rules of the 2nd claset into the 1st claset.
Merging the term nets may look more efficient, but the rather delicate
@@ -636,132 +578,233 @@
val safeEs' = fold rem_thm safeEs safeEs2;
val hazIs' = fold rem_thm hazIs hazIs2;
val hazEs' = fold rem_thm hazEs hazEs2;
- val cs1 = cs addSIs safeIs'
- addSEs safeEs'
- addIs hazIs'
- addEs hazEs';
- val cs2 = map_swrappers
- (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
- val cs3 = map_uwrappers
- (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
- in cs3 end;
+ in
+ cs
+ |> fold_rev (addSI NONE NONE) safeIs'
+ |> fold_rev (addSE NONE NONE) safeEs'
+ |> fold_rev (addI NONE NONE) hazIs'
+ |> fold_rev (addE NONE NONE) hazEs'
+ |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
+ |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers))
+ end;
+
+
+(* data *)
+
+structure Claset = Generic_Data
+(
+ type T = claset;
+ val empty = empty_cs;
+ val extend = I;
+ val merge = merge_cs;
+);
+
+val global_claset_of = Claset.get o Context.Theory;
+val claset_of = Claset.get o Context.Proof;
+val rep_claset_of = rep_cs o claset_of;
+
+val get_cs = Claset.get;
+val map_cs = Claset.map;
+
+fun map_claset f = Context.proof_map (map_cs f);
+fun put_claset cs = map_claset (K cs);
+
+fun print_claset ctxt =
+ let
+ val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
+ val pretty_thms = map (Display.pretty_thm ctxt);
+ in
+ [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
+ Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
+ Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
+ Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
+ Pretty.strs ("safe wrappers:" :: map #1 swrappers),
+ Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
+ |> Pretty.chunks |> Pretty.writeln
+ end;
+
+
+(* old-style declarations *)
+
+fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt;
+
+val op addSIs = decl (addSI NONE);
+val op addSEs = decl (addSE NONE);
+val op addSDs = decl (addSD NONE);
+val op addIs = decl (addI NONE);
+val op addEs = decl (addE NONE);
+val op addDs = decl (addD NONE);
+val op delrules = decl delrule;
+
+
+
+(*** Modifying the wrapper tacticals ***)
+
+fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt));
+fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt));
+
+fun update_warn msg (p as (key : string, _)) xs =
+ (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
+
+fun delete_warn msg (key : string) xs =
+ if AList.defined (op =) xs key then AList.delete (op =) key xs
+ else (warning msg; xs);
+
+(*Add/replace a safe wrapper*)
+fun cs addSWrapper new_swrapper =
+ map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
+
+(*Add/replace an unsafe wrapper*)
+fun cs addWrapper new_uwrapper =
+ map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
+
+(*Remove a safe wrapper*)
+fun cs delSWrapper name =
+ map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
+
+(*Remove an unsafe wrapper*)
+fun cs delWrapper name =
+ map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
+
+(* compose a safe tactic alternatively before/after safe_step_tac *)
+fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
+fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
+
+(*compose a tactic alternatively before/after the step tactic *)
+fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
+fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
+
+fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
+fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
+fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
+fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
+
(**** Simple tactics for theorem proving ****)
(*Attack subgoals using safe inferences -- matching, not resolution*)
-fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
- appSWrappers cs (FIRST' [
- eq_assume_tac,
+fun safe_step_tac ctxt =
+ let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
+ appSWrappers ctxt
+ (FIRST'
+ [eq_assume_tac,
eq_mp_tac,
bimatch_from_nets_tac safe0_netpair,
- FIRST' hyp_subst_tacs,
- bimatch_from_nets_tac safep_netpair]);
+ FIRST' Data.hyp_subst_tacs,
+ bimatch_from_nets_tac safep_netpair])
+ end;
(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
-fun safe_steps_tac cs = REPEAT_DETERM1 o
- (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
+fun safe_steps_tac ctxt =
+ REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i));
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
-fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
+fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt));
(*** Clarify_tac: do safe steps without causing branching ***)
-fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
+fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n);
(*version of bimatch_from_nets_tac that only applies rules that
create precisely n subgoals.*)
fun n_bimatch_from_nets_tac n =
- biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
+ biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
-fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i;
+fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i;
val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
(*Two-way branching is allowed only if one of the branches immediately closes*)
fun bimatch2_tac netpair i =
- n_bimatch_from_nets_tac 2 netpair i THEN
- (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
+ n_bimatch_from_nets_tac 2 netpair i THEN
+ (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
(*Attack subgoals using safe inferences -- matching, not resolution*)
-fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
- appSWrappers cs (FIRST' [
- eq_assume_contr_tac,
+fun clarify_step_tac ctxt =
+ let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
+ appSWrappers ctxt
+ (FIRST'
+ [eq_assume_contr_tac,
bimatch_from_nets_tac safe0_netpair,
- FIRST' hyp_subst_tacs,
+ FIRST' Data.hyp_subst_tacs,
n_bimatch_from_nets_tac 1 safep_netpair,
- bimatch2_tac safep_netpair]);
+ bimatch2_tac safep_netpair])
+ end;
-fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
+fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
(*** Unsafe steps instantiate variables or lose information ***)
(*Backtracking is allowed among the various these unsafe ways of
proving a subgoal. *)
-fun inst0_step_tac (CS {safe0_netpair, ...}) =
+fun inst0_step_tac ctxt =
assume_tac APPEND'
contr_tac APPEND'
- biresolve_from_nets_tac safe0_netpair;
+ biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
(*These unsafe steps could generate more subgoals.*)
-fun instp_step_tac (CS {safep_netpair, ...}) =
- biresolve_from_nets_tac safep_netpair;
+fun instp_step_tac ctxt =
+ biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
(*These steps could instantiate variables and are therefore unsafe.*)
-fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
+fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
-fun haz_step_tac (CS{haz_netpair,...}) =
- biresolve_from_nets_tac haz_netpair;
+fun haz_step_tac ctxt =
+ biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
(*Single step for the prover. FAILS unless it makes progress. *)
-fun step_tac cs i = safe_tac cs ORELSE appWrappers cs
- (inst_step_tac cs ORELSE' haz_step_tac cs) i;
+fun step_tac ctxt i =
+ safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i;
(*Using a "safe" rule to instantiate variables is unsafe. This tactic
allows backtracking from "safe" rules to "unsafe" rules here.*)
-fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs
- (inst_step_tac cs APPEND' haz_step_tac cs) i;
+fun slow_step_tac ctxt i =
+ safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i;
+
(**** The following tactics all fail unless they solve one goal ****)
(*Dumb but fast*)
-fun fast_tac cs =
- Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+fun fast_tac ctxt =
+ Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
(*Slower but smarter than fast_tac*)
-fun best_tac cs =
+fun best_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
(*even a bit smarter than best_tac*)
-fun first_best_tac cs =
+fun first_best_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
-fun slow_tac cs =
+fun slow_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
- SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
+ SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
-fun slow_best_tac cs =
+fun slow_best_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
-val weight_ASTAR = Unsynchronized.ref 5;
-fun astar_tac cs =
+val weight_ASTAR = 5;
+
+fun astar_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL
- (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
- (step_tac cs 1));
+ (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
+ (step_tac ctxt 1));
-fun slow_astar_tac cs =
+fun slow_astar_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL
- (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
- (slow_step_tac cs 1));
+ (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
+ (slow_step_tac ctxt 1));
+
(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome
of much experimentation! Changing APPEND to ORELSE below would prove
@@ -771,141 +814,47 @@
(*Non-deterministic! Could always expand the first unsafe connective.
That's hard to implement and did not perform better in experiments, due to
greater search depth required.*)
-fun dup_step_tac (CS {dup_netpair, ...}) =
- biresolve_from_nets_tac dup_netpair;
+fun dup_step_tac ctxt =
+ biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
local
-fun slow_step_tac' cs = appWrappers cs
- (instp_step_tac cs APPEND' dup_step_tac cs);
-in fun depth_tac cs m i state = SELECT_GOAL
- (safe_steps_tac cs 1 THEN_ELSE
- (DEPTH_SOLVE (depth_tac cs m 1),
- inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
- (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
- )) i state;
+ fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt);
+in
+ fun depth_tac ctxt m i state = SELECT_GOAL
+ (safe_steps_tac ctxt 1 THEN_ELSE
+ (DEPTH_SOLVE (depth_tac ctxt m 1),
+ inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
+ (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state;
end;
(*Search, with depth bound m.
This is the "entry point", which does safe inferences first.*)
-fun safe_depth_tac cs m =
- SUBGOAL
- (fn (prem,i) =>
- let val deti =
- (*No Vars in the goal? No need to backtrack between goals.*)
- if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
- in SELECT_GOAL (TRY (safe_tac cs) THEN
- DEPTH_SOLVE (deti (depth_tac cs m 1))) i
- end);
-
-fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
-
-
-
-(** context dependent claset components **)
-
-datatype context_cs = ContextCS of
- {swrappers: (string * (Proof.context -> wrapper)) list,
- uwrappers: (string * (Proof.context -> wrapper)) list};
-
-fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
+fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) =>
let
- fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
+ val deti = (*No Vars in the goal? No need to backtrack between goals.*)
+ if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I;
in
- cs
- |> fold_rev (add_wrapper (op addSWrapper)) swrappers
- |> fold_rev (add_wrapper (op addWrapper)) uwrappers
- end;
-
-fun make_context_cs (swrappers, uwrappers) =
- ContextCS {swrappers = swrappers, uwrappers = uwrappers};
-
-val empty_context_cs = make_context_cs ([], []);
-
-fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
- if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
- else
- let
- val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
- val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
- val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
- val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
- in make_context_cs (swrappers', uwrappers') end;
-
-
-
-(** claset data **)
-
-(* global clasets *)
+ SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i
+ end);
-structure GlobalClaset = Theory_Data
-(
- type T = claset * context_cs;
- val empty = (empty_cs, empty_context_cs);
- val extend = I;
- fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
- (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
-);
-
-val get_global_claset = #1 o GlobalClaset.get;
-val map_global_claset = GlobalClaset.map o apfst;
-
-val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of;
-fun map_context_cs f = GlobalClaset.map (apsnd
- (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
-
-fun global_claset_of thy =
- let val (cs, ctxt_cs) = GlobalClaset.get thy
- in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end;
-
-
-(* context dependent components *)
-
-fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
-fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
-
-fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
-fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
-
-
-(* local clasets *)
-
-structure LocalClaset = Proof_Data
-(
- type T = claset;
- val init = get_global_claset;
-);
-
-val get_claset = LocalClaset.get;
-val put_claset = LocalClaset.put;
-
-fun claset_of ctxt =
- context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
-
-
-(* generic clasets *)
-
-val get_cs = Context.cases global_claset_of claset_of;
-fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
+fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt);
(* attributes *)
-fun attrib f = Thm.declaration_attribute (fn th =>
- Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
+fun attrib f =
+ Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context);
-fun safe_dest w = attrib (addSE w o make_elim);
val safe_elim = attrib o addSE;
val safe_intro = attrib o addSI;
-fun haz_dest w = attrib (addE w o make_elim);
+val safe_dest = attrib o addSD;
val haz_elim = attrib o addE;
val haz_intro = attrib o addI;
+val haz_dest = attrib o addD;
val rule_del = attrib delrule o Context_Rules.rule_del;
-end;
-
-
(** concrete syntax of attributes **)
@@ -934,7 +883,7 @@
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
let
val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
- val CS {xtra_netpair, ...} = claset_of ctxt;
+ val {xtra_netpair, ...} = rep_claset_of ctxt;
val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
val rules = rules1 @ rules2 @ rules3 @ rules4;
val ruleq = Drule.multi_resolves facts rules;
@@ -972,14 +921,8 @@
Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
Args.del -- Args.colon >> K (I, rule_del)];
-fun cla_meth tac ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
-
-fun cla_meth' tac ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
-
-fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
-fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
+fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
+fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
@@ -999,7 +942,7 @@
Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
- Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
+ Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
"classical prover (iterative deepening)" #>
Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
"classical prover (apply safe rules)";
@@ -1020,6 +963,6 @@
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (fn state =>
let val ctxt = Toplevel.context_of state
- in print_cs ctxt (claset_of ctxt) end)));
+ in print_claset ctxt end)));
end;
--- a/src/Pure/simplifier.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/Pure/simplifier.ML Fri May 13 23:59:48 2011 +0200
@@ -8,11 +8,11 @@
signature BASIC_SIMPLIFIER =
sig
include BASIC_RAW_SIMPLIFIER
- val change_simpset: (simpset -> simpset) -> unit
+ val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context
+ val simpset_of: Proof.context -> simpset
val global_simpset_of: theory -> simpset
val Addsimprocs: simproc list -> unit
val Delsimprocs: simproc list -> unit
- val simpset_of: Proof.context -> simpset
val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
val safe_asm_full_simp_tac: simpset -> int -> tactic
val simp_tac: simpset -> int -> tactic
@@ -30,6 +30,7 @@
signature SIMPLIFIER =
sig
include BASIC_SIMPLIFIER
+ val map_simpset_global: (simpset -> simpset) -> theory -> theory
val pretty_ss: Proof.context -> simpset -> Pretty.T
val clear_ss: simpset -> simpset
val debug_bounds: bool Unsynchronized.ref
@@ -41,10 +42,10 @@
val context: Proof.context -> simpset -> simpset
val global_context: theory -> simpset -> simpset
val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
- val simproc_global_i: theory -> string -> term list
- -> (theory -> simpset -> term -> thm option) -> simproc
- val simproc_global: theory -> string -> string list
- -> (theory -> simpset -> term -> thm option) -> simproc
+ val simproc_global_i: theory -> string -> term list ->
+ (theory -> simpset -> term -> thm option) -> simproc
+ val simproc_global: theory -> string -> string list ->
+ (theory -> simpset -> term -> thm option) -> simproc
val rewrite: simpset -> conv
val asm_rewrite: simpset -> conv
val full_rewrite: simpset -> conv
@@ -57,7 +58,6 @@
val simp_del: attribute
val cong_add: attribute
val cong_del: attribute
- val map_simpset: (simpset -> simpset) -> theory -> theory
val check_simproc: Proof.context -> xstring * Position.T -> string
val the_simproc: Proof.context -> string -> simproc
val def_simproc: {name: binding, lhss: term list,
@@ -134,25 +134,25 @@
val cong_del = attrib (op delcongs);
-(* global simpset *)
-
-fun map_simpset f = Context.theory_map (map_ss f);
-fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
-fun global_simpset_of thy =
- Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
-
-fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
-fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
-
-
(* local simpset *)
+fun map_simpset f = Context.proof_map (map_ss f);
fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
val _ = ML_Antiquote.value "simpset"
(Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
+(* global simpset *)
+
+fun map_simpset_global f = Context.theory_map (map_ss f);
+fun global_simpset_of thy =
+ Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
+
+fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args));
+fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args));
+
+
(** named simprocs **)
--- a/src/Sequents/LK.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/Sequents/LK.thy Fri May 13 23:59:48 2011 +0200
@@ -216,6 +216,7 @@
done
use "simpdata.ML"
+setup {* Simplifier.map_simpset_global (K LK_ss) *}
text {* To create substition rules *}
--- a/src/Sequents/simpdata.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/Sequents/simpdata.ML Fri May 13 23:59:48 2011 +0200
@@ -88,4 +88,3 @@
addeqcongs [@{thm left_cong}]
addcongs [@{thm imp_cong}];
-change_simpset (fn _ => LK_ss);
--- a/src/ZF/Tools/datatype_package.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML Fri May 13 23:59:48 2011 +0200
@@ -348,11 +348,14 @@
(*Typical theorems have the form ~con1=con2, con1=con2==>False,
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
fun mk_free s =
- let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*)
- Goal.prove_global thy [] [] (Syntax.read_prop_global thy s)
+ let
+ val thy = theory_of_thm elim;
+ val ctxt = Proof_Context.init_global thy;
+ in
+ Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
(fn _ => EVERY
[rewrite_goals_tac con_defs,
- fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])
+ fast_tac (put_claset ZF_cs ctxt addSEs free_SEs @ Su.free_SEs) 1])
end;
val simps = case_eqns @ recursor_eqns;
--- a/src/ZF/Tools/typechk.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/Tools/typechk.ML Fri May 13 23:59:48 2011 +0200
@@ -130,6 +130,6 @@
val setup =
Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
typecheck_setup #>
- Simplifier.map_simpset (fn ss => ss setSolver type_solver);
+ Simplifier.map_simpset_global (fn ss => ss setSolver type_solver);
end;
--- a/src/ZF/UNITY/Constrains.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/UNITY/Constrains.thy Fri May 13 23:59:48 2011 +0200
@@ -471,7 +471,7 @@
(*proves "co" properties when the program is specified*)
fun constrains_tac ctxt =
- let val css as (cs, ss) = clasimpset_of ctxt in
+ let val ss = simpset_of ctxt in
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
REPEAT (etac @{thm Always_ConstrainsI} 1
@@ -481,20 +481,20 @@
rtac @{thm constrainsI} 1,
(* Three subgoals *)
rewrite_goal_tac [@{thm st_set_def}] 3,
- REPEAT (force_tac css 2),
+ REPEAT (force_tac ctxt 2),
full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
REPEAT (FIRSTGOAL (etac @{thm disjE})),
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
REPEAT (FIRSTGOAL (etac @{thm disjE})),
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_full_simp_tac ss),
- ALLGOALS (clarify_tac cs)])
+ ALLGOALS (clarify_tac ctxt)])
end;
(*For proving invariants*)
-fun always_tac ctxt i =
- rtac @{thm AlwaysI} i THEN force_tac (clasimpset_of ctxt) i THEN constrains_tac ctxt i;
+fun always_tac ctxt i =
+ rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
*}
setup Program_Defs.setup
--- a/src/ZF/UNITY/SubstAx.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Fri May 13 23:59:48 2011 +0200
@@ -351,7 +351,7 @@
ML {*
(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac ctxt sact =
- let val css as (cs, ss) = clasimpset_of ctxt in
+ let val ss = simpset_of ctxt in
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
etac @{thm Always_LeadsTo_Basis} 1
@@ -364,14 +364,14 @@
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm domain_def}]) 3,
(* proving the domain part *)
- clarify_tac cs 3, dtac @{thm swap} 3, force_tac css 4,
- rtac @{thm ReplaceI} 3, force_tac css 3, force_tac css 4,
+ clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4,
+ rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,
asm_full_simp_tac ss 3, rtac @{thm conjI} 3, simp_tac ss 4,
REPEAT (rtac @{thm state_update_type} 3),
constrains_tac ctxt 1,
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_full_simp_tac (ss addsimps [@{thm st_set_def}])),
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_lr_simp_tac ss)])
end;
*}
--- a/src/ZF/equalities.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/equalities.thy Fri May 13 23:59:48 2011 +0200
@@ -970,17 +970,14 @@
Un_upper1 Un_upper2 Int_lower1 Int_lower2
ML {*
-val subset_cs = @{claset}
+val subset_cs =
+ claset_of (@{context}
delrules [@{thm subsetI}, @{thm subsetCE}]
addSIs @{thms subset_SIs}
addIs [@{thm Union_upper}, @{thm Inter_lower}]
- addSEs [@{thm cons_subsetE}];
-*}
-(*subset_cs is a claset for subset reasoning*)
+ addSEs [@{thm cons_subsetE}]);
-ML
-{*
-val ZF_cs = @{claset} delrules [@{thm equalityI}];
+val ZF_cs = claset_of (@{context} delrules [@{thm equalityI}]);
*}
end
--- a/src/ZF/ex/CoUnit.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/ex/CoUnit.thy Fri May 13 23:59:48 2011 +0200
@@ -76,11 +76,11 @@
"Ord(i) ==> \<forall>x y. x \<in> counit2 --> y \<in> counit2 --> x Int Vset(i) \<subseteq> y"
-- {* Lemma for proving finality. *}
apply (erule trans_induct)
- apply (tactic "safe_tac subset_cs")
+ apply (tactic "safe_tac (put_claset subset_cs @{context})")
apply (erule counit2.cases)
apply (erule counit2.cases)
apply (unfold counit2.con_defs)
- apply (tactic {* fast_tac (subset_cs
+ apply (tactic {* fast_tac (put_claset subset_cs @{context}
addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}]
addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1 *})
done
--- a/src/ZF/ex/LList.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/ex/LList.thy Fri May 13 23:59:48 2011 +0200
@@ -113,7 +113,7 @@
apply (erule llist.cases)
apply (simp_all add: QInl_def QInr_def llist.con_defs)
(*LCons case: I simply can't get rid of the deepen_tac*)
-apply (tactic "deepen_tac (@{claset} addIs [@{thm Ord_trans}]
+apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
done
@@ -216,7 +216,7 @@
apply (erule llist.cases, simp_all)
apply (simp_all add: QInl_def QInr_def llist.con_defs)
(*LCons case: I simply can't get rid of the deepen_tac*)
-apply (tactic "deepen_tac (@{claset} addIs [@{thm Ord_trans}]
+apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
done
--- a/src/ZF/pair.thy Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/pair.thy Fri May 13 23:59:48 2011 +0200
@@ -1,7 +1,6 @@
(* Title: ZF/pair.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
*)
header{*Ordered Pairs*}
@@ -10,6 +9,14 @@
uses "simpdata.ML"
begin
+setup {*
+ Simplifier.map_simpset_global (fn ss =>
+ ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
+ addcongs [@{thm if_weak_cong}])
+*}
+
+ML {* val ZF_ss = @{simpset} *}
+
simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
let
val unfold_bex_tac = unfold_tac @{thms Bex_def};
--- a/src/ZF/simpdata.ML Fri May 13 21:36:01 2011 +0200
+++ b/src/ZF/simpdata.ML Fri May 13 23:59:48 2011 +0200
@@ -43,9 +43,3 @@
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
-change_simpset (fn ss =>
- ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
- addcongs [@{thm if_weak_cong}]);
-
-val ZF_ss = @{simpset};
-