1.1 --- a/NEWS Fri May 13 16:03:03 2011 +0200
1.2 +++ b/NEWS Fri May 13 22:55:00 2011 +0200
1.3 @@ -144,6 +144,14 @@
1.4 * Slightly more special eq_list/eq_set, with shortcut involving
1.5 pointer equality (assumes that eq relation is reflexive).
1.6
1.7 +* Classical tactics use proper Proof.context instead of historic types
1.8 +claset/clasimpset. Old-style declarations like addIs, addEs, addDs
1.9 +operate directly on Proof.context. Raw type claset retains its use as
1.10 +snapshot of the classical context, which can be recovered via
1.11 +(put_claset HOL_cs) etc. Type clasimpset has been discontinued.
1.12 +INCOMPATIBILITY, classical tactics and derived proof methods require
1.13 +proper Proof.context.
1.14 +
1.15
1.16
1.17 New in Isabelle2011 (January 2011)
2.1 --- a/doc-src/TutorialI/Protocol/Message.thy Fri May 13 16:03:03 2011 +0200
2.2 +++ b/doc-src/TutorialI/Protocol/Message.thy Fri May 13 22:55:00 2011 +0200
2.3 @@ -840,31 +840,24 @@
2.4 eresolve_tac [asm_rl, @{thm synth.Inj}];
2.5
2.6 fun Fake_insert_simp_tac ss i =
2.7 - REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
2.8 + REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
2.9
2.10 fun atomic_spy_analz_tac ctxt =
2.11 - let val ss = simpset_of ctxt and cs = claset_of ctxt in
2.12 - SELECT_GOAL
2.13 - (Fake_insert_simp_tac ss 1
2.14 - THEN
2.15 - IF_UNSOLVED (Blast.depth_tac
2.16 - (cs addIs [analz_insertI,
2.17 - impOfSubs analz_subset_parts]) 4 1))
2.18 - end;
2.19 + SELECT_GOAL
2.20 + (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
2.21 + IF_UNSOLVED (Blast.depth_tac (ctxt addIs [analz_insertI, impOfSubs analz_subset_parts]) 4 1));
2.22
2.23 fun spy_analz_tac ctxt i =
2.24 - let val ss = simpset_of ctxt and cs = claset_of ctxt in
2.25 - DETERM
2.26 - (SELECT_GOAL
2.27 - (EVERY
2.28 - [ (*push in occurrences of X...*)
2.29 - (REPEAT o CHANGED)
2.30 - (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
2.31 - (*...allowing further simplifications*)
2.32 - simp_tac ss 1,
2.33 - REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
2.34 - DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
2.35 - end;
2.36 + DETERM
2.37 + (SELECT_GOAL
2.38 + (EVERY
2.39 + [ (*push in occurrences of X...*)
2.40 + (REPEAT o CHANGED)
2.41 + (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
2.42 + (*...allowing further simplifications*)
2.43 + simp_tac (simpset_of ctxt) 1,
2.44 + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
2.45 + DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
2.46 *}
2.47
2.48 text{*By default only @{text o_apply} is built-in. But in the presence of
3.1 --- a/src/CCL/Type.thy Fri May 13 16:03:03 2011 +0200
3.2 +++ b/src/CCL/Type.thy Fri May 13 22:55:00 2011 +0200
3.3 @@ -132,7 +132,7 @@
3.4 REPEAT_SOME (eresolve_tac (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
3.5 ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN
3.6 ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
3.7 - safe_tac (claset_of ctxt addSIs prems))
3.8 + safe_tac (ctxt addSIs prems))
3.9 *}
3.10
3.11 method_setup ncanT = {*
3.12 @@ -397,8 +397,7 @@
3.13
3.14 ML {*
3.15 val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} =>
3.16 - (fast_tac (claset_of ctxt addIs
3.17 - (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1));
3.18 + fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1);
3.19 *}
3.20
3.21 method_setup coinduct3 = {*
3.22 @@ -419,8 +418,8 @@
3.23 fun genIs_tac ctxt genXH gen_mono =
3.24 rtac (genXH RS @{thm iffD2}) THEN'
3.25 simp_tac (simpset_of ctxt) THEN'
3.26 - TRY o fast_tac (claset_of ctxt addIs
3.27 - [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
3.28 + TRY o fast_tac
3.29 + (ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
3.30 *}
3.31
3.32 method_setup genIs = {*
3.33 @@ -454,7 +453,7 @@
3.34
3.35 ML {*
3.36 fun POgen_tac ctxt (rla, rlb) i =
3.37 - SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN
3.38 + SELECT_GOAL (safe_tac ctxt) i THEN
3.39 rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
3.40 (REPEAT (resolve_tac
3.41 (@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @
3.42 @@ -499,7 +498,7 @@
3.43
3.44 fun EQgen_tac ctxt rews i =
3.45 SELECT_GOAL
3.46 - (TRY (safe_tac (claset_of ctxt)) THEN
3.47 + (TRY (safe_tac ctxt) THEN
3.48 resolve_tac ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN
3.49 ALLGOALS (simp_tac (simpset_of ctxt)) THEN
3.50 ALLGOALS EQgen_raw_tac) i
4.1 --- a/src/FOL/FOL.thy Fri May 13 16:03:03 2011 +0200
4.2 +++ b/src/FOL/FOL.thy Fri May 13 22:55:00 2011 +0200
4.3 @@ -12,7 +12,6 @@
4.4 "~~/src/Provers/clasimp.ML"
4.5 "~~/src/Tools/induct.ML"
4.6 "~~/src/Tools/case_product.ML"
4.7 - ("cladata.ML")
4.8 ("simpdata.ML")
4.9 begin
4.10
4.11 @@ -167,9 +166,36 @@
4.12
4.13 section {* Classical Reasoner *}
4.14
4.15 -use "cladata.ML"
4.16 +ML {*
4.17 +structure Cla = ClassicalFun
4.18 +(
4.19 + val imp_elim = @{thm imp_elim}
4.20 + val not_elim = @{thm notE}
4.21 + val swap = @{thm swap}
4.22 + val classical = @{thm classical}
4.23 + val sizef = size_of_thm
4.24 + val hyp_subst_tacs = [hyp_subst_tac]
4.25 +);
4.26 +
4.27 +ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
4.28 +
4.29 +structure Basic_Classical: BASIC_CLASSICAL = Cla;
4.30 +open Basic_Classical;
4.31 +*}
4.32 +
4.33 setup Cla.setup
4.34 -ML {* Context.>> (Cla.map_cs (K FOL_cs)) *}
4.35 +
4.36 +(*Propositional rules*)
4.37 +lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
4.38 + and [elim!] = conjE disjE impCE FalseE iffCE
4.39 +ML {* val prop_cs = @{claset} *}
4.40 +
4.41 +(*Quantifier rules*)
4.42 +lemmas [intro!] = allI ex_ex1I
4.43 + and [intro] = exI
4.44 + and [elim!] = exE alt_ex1E
4.45 + and [elim] = allE
4.46 +ML {* val FOL_cs = @{claset} *}
4.47
4.48 ML {*
4.49 structure Blast = Blast
5.1 --- a/src/FOL/IsaMakefile Fri May 13 16:03:03 2011 +0200
5.2 +++ b/src/FOL/IsaMakefile Fri May 13 22:55:00 2011 +0200
5.3 @@ -29,14 +29,13 @@
5.4
5.5 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
5.6 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
5.7 - $(SRC)/Tools/case_product.ML \
5.8 - $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
5.9 - $(SRC)/Tools/IsaPlanner/rw_tools.ML \
5.10 + $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML \
5.11 + $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML \
5.12 $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
5.13 $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
5.14 $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
5.15 $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \
5.16 - $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML cladata.ML \
5.17 + $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \
5.18 document/root.tex fologic.ML hypsubstdata.ML intprover.ML \
5.19 simpdata.ML
5.20 @$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
6.1 --- a/src/FOL/cladata.ML Fri May 13 16:03:03 2011 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,34 +0,0 @@
6.4 -(* Title: FOL/cladata.ML
6.5 - Author: Tobias Nipkow
6.6 - Copyright 1996 University of Cambridge
6.7 -
6.8 -Setting up the classical reasoner.
6.9 -*)
6.10 -
6.11 -(*** Applying ClassicalFun to create a classical prover ***)
6.12 -structure Classical_Data =
6.13 -struct
6.14 - val imp_elim = @{thm imp_elim}
6.15 - val not_elim = @{thm notE}
6.16 - val swap = @{thm swap}
6.17 - val classical = @{thm classical}
6.18 - val sizef = size_of_thm
6.19 - val hyp_subst_tacs=[hyp_subst_tac]
6.20 -end;
6.21 -
6.22 -structure Cla = ClassicalFun(Classical_Data);
6.23 -structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
6.24 -
6.25 -ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
6.26 -
6.27 -
6.28 -(*Propositional rules*)
6.29 -val prop_cs = empty_cs
6.30 - addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI},
6.31 - @{thm notI}, @{thm iffI}]
6.32 - addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}];
6.33 -
6.34 -(*Quantifier rules*)
6.35 -val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
6.36 - addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
6.37 -
7.1 --- a/src/FOL/simpdata.ML Fri May 13 16:03:03 2011 +0200
7.2 +++ b/src/FOL/simpdata.ML Fri May 13 22:55:00 2011 +0200
7.3 @@ -142,6 +142,3 @@
7.4 );
7.5 open Clasimp;
7.6
7.7 -ML_Antiquote.value "clasimpset"
7.8 - (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
7.9 -
8.1 --- a/src/HOL/Algebra/abstract/Ideal2.thy Fri May 13 16:03:03 2011 +0200
8.2 +++ b/src/HOL/Algebra/abstract/Ideal2.thy Fri May 13 22:55:00 2011 +0200
8.3 @@ -276,7 +276,7 @@
8.4 apply (unfold prime_def)
8.5 apply (rule conjI)
8.6 apply (rule_tac [2] conjI)
8.7 - apply (tactic "clarify_tac @{claset} 3")
8.8 + apply (tactic "clarify_tac @{context} 3")
8.9 apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)
8.10 apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)
8.11 apply (simp add: ideal_of_2_structure)
9.1 --- a/src/HOL/Algebra/abstract/Ring2.thy Fri May 13 16:03:03 2011 +0200
9.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy Fri May 13 22:55:00 2011 +0200
9.3 @@ -466,7 +466,7 @@
9.4 (* fields are integral domains *)
9.5
9.6 lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
9.7 - apply (tactic "step_tac @{claset} 1")
9.8 + apply (tactic "step_tac @{context} 1")
9.9 apply (rule_tac a = " (a*b) * inverse b" in box_equals)
9.10 apply (rule_tac [3] refl)
9.11 prefer 2
10.1 --- a/src/HOL/Auth/Message.thy Fri May 13 16:03:03 2011 +0200
10.2 +++ b/src/HOL/Auth/Message.thy Fri May 13 22:55:00 2011 +0200
10.3 @@ -830,31 +830,26 @@
10.4 eresolve_tac [asm_rl, @{thm synth.Inj}];
10.5
10.6 fun Fake_insert_simp_tac ss i =
10.7 - REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
10.8 + REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
10.9
10.10 fun atomic_spy_analz_tac ctxt =
10.11 - let val ss = simpset_of ctxt and cs = claset_of ctxt in
10.12 - SELECT_GOAL
10.13 - (Fake_insert_simp_tac ss 1
10.14 - THEN
10.15 - IF_UNSOLVED (Blast.depth_tac
10.16 - (cs addIs [@{thm analz_insertI},
10.17 - impOfSubs @{thm analz_subset_parts}]) 4 1))
10.18 - end;
10.19 + SELECT_GOAL
10.20 + (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
10.21 + IF_UNSOLVED
10.22 + (Blast.depth_tac
10.23 + (ctxt addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1));
10.24
10.25 fun spy_analz_tac ctxt i =
10.26 - let val ss = simpset_of ctxt and cs = claset_of ctxt in
10.27 - DETERM
10.28 - (SELECT_GOAL
10.29 - (EVERY
10.30 - [ (*push in occurrences of X...*)
10.31 - (REPEAT o CHANGED)
10.32 - (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
10.33 - (*...allowing further simplifications*)
10.34 - simp_tac ss 1,
10.35 - REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
10.36 - DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
10.37 - end;
10.38 + DETERM
10.39 + (SELECT_GOAL
10.40 + (EVERY
10.41 + [ (*push in occurrences of X...*)
10.42 + (REPEAT o CHANGED)
10.43 + (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
10.44 + (*...allowing further simplifications*)
10.45 + simp_tac (simpset_of ctxt) 1,
10.46 + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
10.47 + DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
10.48 *}
10.49
10.50 text{*By default only @{text o_apply} is built-in. But in the presence of
11.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri May 13 16:03:03 2011 +0200
11.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri May 13 22:55:00 2011 +0200
11.3 @@ -749,7 +749,7 @@
11.4 (*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN
11.5 (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN
11.6 (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
11.7 - (*Base*) (force_tac (clasimpset_of ctxt)) 1
11.8 + (*Base*) (force_tac ctxt) 1
11.9
11.10 val analz_prepare_tac =
11.11 prepare_tac THEN
12.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 13 16:03:03 2011 +0200
12.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 13 22:55:00 2011 +0200
12.3 @@ -748,7 +748,7 @@
12.4
12.5 fun prepare_tac ctxt =
12.6 (*SR_U8*) forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
12.7 - (*SR_U8*) clarify_tac (claset_of ctxt) 15 THEN
12.8 + (*SR_U8*) clarify_tac ctxt 15 THEN
12.9 (*SR_U9*) forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN
12.10 (*SR_U11*) forward_tac [@{thm Outpts_A_Card_form_10}] 21
12.11
12.12 @@ -758,7 +758,7 @@
12.13 (*SR_U9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN
12.14 (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN
12.15 (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
12.16 - (*Base*) (force_tac (clasimpset_of ctxt)) 1
12.17 + (*Base*) (force_tac ctxt) 1
12.18
12.19 fun analz_prepare_tac ctxt =
12.20 prepare_tac ctxt THEN
13.1 --- a/src/HOL/Bali/AxCompl.thy Fri May 13 16:03:03 2011 +0200
13.2 +++ b/src/HOL/Bali/AxCompl.thy Fri May 13 22:55:00 2011 +0200
13.3 @@ -1391,7 +1391,7 @@
13.4 using finU uA
13.5 apply -
13.6 apply (induct_tac "n")
13.7 -apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
13.8 +apply (tactic "ALLGOALS (clarsimp_tac @{context})")
13.9 apply (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *})
13.10 apply simp
13.11 apply (erule finite_imageI)
14.1 --- a/src/HOL/Bali/AxSem.thy Fri May 13 16:03:03 2011 +0200
14.2 +++ b/src/HOL/Bali/AxSem.thy Fri May 13 22:55:00 2011 +0200
14.3 @@ -661,7 +661,7 @@
14.4 lemma ax_thin [rule_format (no_asm)]:
14.5 "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
14.6 apply (erule ax_derivs.induct)
14.7 -apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
14.8 +apply (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
14.9 apply (rule ax_derivs.empty)
14.10 apply (erule (1) ax_derivs.insert)
14.11 apply (fast intro: ax_derivs.asm)
14.12 @@ -692,7 +692,7 @@
14.13 (*42 subgoals*)
14.14 apply (tactic "ALLGOALS strip_tac")
14.15 apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
14.16 - etac disjE, fast_tac (@{claset} addSIs @{thms ax_derivs.empty})]))*})
14.17 + etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
14.18 apply (tactic "TRYALL hyp_subst_tac")
14.19 apply (simp, rule ax_derivs.empty)
14.20 apply (drule subset_insertD)
14.21 @@ -703,7 +703,7 @@
14.22 apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
14.23 (*37 subgoals*)
14.24 apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})
14.25 - THEN_ALL_NEW fast_tac @{claset}) *})
14.26 + THEN_ALL_NEW fast_tac @{context}) *})
14.27 (*1 subgoal*)
14.28 apply (clarsimp simp add: subset_mtriples_iff)
14.29 apply (rule ax_derivs.Methd)
15.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy Fri May 13 16:03:03 2011 +0200
15.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Fri May 13 22:55:00 2011 +0200
15.3 @@ -152,12 +152,12 @@
15.4 lemma slen_fscons_eq_rev:
15.5 "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
15.6 apply (simp add: fscons_def2 slen_scons_eq_rev)
15.7 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
15.8 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
15.9 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
15.10 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
15.11 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
15.12 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
15.13 +apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
15.14 +apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
15.15 +apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
15.16 +apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
15.17 +apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
15.18 +apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
15.19 apply (erule contrapos_np)
15.20 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
15.21 done
16.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri May 13 16:03:03 2011 +0200
16.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri May 13 22:55:00 2011 +0200
16.3 @@ -83,9 +83,9 @@
16.4 lemma last_ind_on_first:
16.5 "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
16.6 apply simp
16.7 - apply (tactic {* auto_tac (@{claset},
16.8 + apply (tactic {* auto_tac (map_simpset_local (fn _ =>
16.9 HOL_ss addsplits [@{thm list.split}]
16.10 - addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) *})
16.11 + addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
16.12 done
16.13
16.14 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}
17.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri May 13 16:03:03 2011 +0200
17.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri May 13 22:55:00 2011 +0200
17.3 @@ -604,10 +604,10 @@
17.4
17.5 ML {*
17.6 fun abstraction_tac ctxt =
17.7 - let val (cs, ss) = clasimpset_of ctxt in
17.8 - SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
17.9 - ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
17.10 - end
17.11 + SELECT_GOAL (auto_tac
17.12 + (ctxt addSIs @{thms weak_strength_lemmas}
17.13 + |> map_simpset_local (fn ss =>
17.14 + ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
17.15 *}
17.16
17.17 method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
18.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Fri May 13 16:03:03 2011 +0200
18.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Fri May 13 22:55:00 2011 +0200
18.3 @@ -400,7 +400,7 @@
18.4 ==> input_enabled (A||B)"
18.5 apply (unfold input_enabled_def)
18.6 apply (simp add: Let_def inputs_of_par trans_of_par)
18.7 -apply (tactic "safe_tac (global_claset_of @{theory Fun})")
18.8 +apply (tactic "safe_tac (Proof_Context.init_global @{theory Fun})")
18.9 apply (simp add: inp_is_act)
18.10 prefer 2
18.11 apply (simp add: inp_is_act)
19.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Fri May 13 16:03:03 2011 +0200
19.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Fri May 13 22:55:00 2011 +0200
19.3 @@ -298,7 +298,7 @@
19.4 let val ss = simpset_of ctxt in
19.5 EVERY1[Seq_induct_tac ctxt sch defs,
19.6 asm_full_simp_tac ss,
19.7 - SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})),
19.8 + SELECT_GOAL (safe_tac (Proof_Context.init_global @{theory Fun})),
19.9 Seq_case_simp_tac ctxt exA,
19.10 Seq_case_simp_tac ctxt exB,
19.11 asm_full_simp_tac ss,
20.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri May 13 16:03:03 2011 +0200
20.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri May 13 22:55:00 2011 +0200
20.3 @@ -150,7 +150,7 @@
20.4 (Ps ~~ take_consts ~~ xs)
20.5 val goal = mk_trp (foldr1 mk_conj concls)
20.6
20.7 - fun tacf {prems, context} =
20.8 + fun tacf {prems, context = ctxt} =
20.9 let
20.10 (* Prove stronger prems, without definedness side conditions *)
20.11 fun con_thm p (con, args) =
20.12 @@ -165,23 +165,23 @@
20.13 map arg_tac args @
20.14 [REPEAT (rtac impI 1), ALLGOALS simplify]
20.15 in
20.16 - Goal.prove context [] [] subgoal (K (EVERY tacs))
20.17 + Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
20.18 end
20.19 fun eq_thms (p, cons) = map (con_thm p) cons
20.20 val conss = map #con_specs constr_infos
20.21 val prems' = maps eq_thms (Ps ~~ conss)
20.22
20.23 val tacs1 = [
20.24 - quant_tac context 1,
20.25 + quant_tac ctxt 1,
20.26 simp_tac HOL_ss 1,
20.27 - InductTacs.induct_tac context [[SOME "n"]] 1,
20.28 + InductTacs.induct_tac ctxt [[SOME "n"]] 1,
20.29 simp_tac (take_ss addsimps prems) 1,
20.30 - TRY (safe_tac HOL_cs)]
20.31 + TRY (safe_tac (put_claset HOL_cs ctxt))]
20.32 fun con_tac _ =
20.33 asm_simp_tac take_ss 1 THEN
20.34 (resolve_tac prems' THEN_ALL_NEW etac spec) 1
20.35 fun cases_tacs (cons, exhaust) =
20.36 - res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
20.37 + res_inst_tac ctxt [(("y", 0), "x")] exhaust 1 ::
20.38 asm_simp_tac (take_ss addsimps prems) 1 ::
20.39 map con_tac cons
20.40 val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
20.41 @@ -196,15 +196,15 @@
20.42 val concls = map (op $) (Ps ~~ xs)
20.43 val goal = mk_trp (foldr1 mk_conj concls)
20.44 val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps
20.45 - fun tacf {prems, context} =
20.46 + fun tacf {prems, context = ctxt} =
20.47 let
20.48 fun finite_tac (take_induct, fin_ind) =
20.49 rtac take_induct 1 THEN
20.50 (if is_finite then all_tac else resolve_tac prems 1) THEN
20.51 (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1
20.52 - val fin_inds = Project_Rule.projections context finite_ind
20.53 + val fin_inds = Project_Rule.projections ctxt finite_ind
20.54 in
20.55 - TRY (safe_tac HOL_cs) THEN
20.56 + TRY (safe_tac (put_claset HOL_cs ctxt)) THEN
20.57 EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
20.58 end
20.59 in Goal.prove_global thy [] (adms @ assms) goal tacf end
20.60 @@ -318,18 +318,18 @@
20.61 val goal =
20.62 mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)))
20.63 val rules = @{thm Rep_cfun_strict1} :: take_0_thms
20.64 - fun tacf {prems, context} =
20.65 + fun tacf {prems, context = ctxt} =
20.66 let
20.67 val prem' = rewrite_rule [bisim_def_thm] (hd prems)
20.68 - val prems' = Project_Rule.projections context prem'
20.69 + val prems' = Project_Rule.projections ctxt prem'
20.70 val dests = map (fn th => th RS spec RS spec RS mp) prems'
20.71 fun one_tac (dest, rews) =
20.72 - dtac dest 1 THEN safe_tac HOL_cs THEN
20.73 + dtac dest 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN
20.74 ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews))
20.75 in
20.76 rtac @{thm nat.induct} 1 THEN
20.77 simp_tac (HOL_ss addsimps rules) 1 THEN
20.78 - safe_tac HOL_cs THEN
20.79 + safe_tac (put_claset HOL_cs ctxt) THEN
20.80 EVERY (map one_tac (dests ~~ take_rews))
20.81 end
20.82 in
21.1 --- a/src/HOL/Hoare/hoare_tac.ML Fri May 13 16:03:03 2011 +0200
21.2 +++ b/src/HOL/Hoare/hoare_tac.ML Fri May 13 22:55:00 2011 +0200
21.3 @@ -78,7 +78,7 @@
21.4 val MsetT = fastype_of big_Collect;
21.5 fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
21.6 val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
21.7 - val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1);
21.8 + val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1);
21.9 in (vars, th) end;
21.10
21.11 end;
22.1 --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 13 16:03:03 2011 +0200
22.2 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 13 22:55:00 2011 +0200
22.3 @@ -774,13 +774,13 @@
22.4 --{* 32 subgoals left *}
22.5 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
22.6 --{* 20 subgoals left *}
22.7 -apply(tactic{* TRYALL (clarify_tac @{claset}) *})
22.8 +apply(tactic{* TRYALL (clarify_tac @{context}) *})
22.9 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
22.10 apply(tactic {* TRYALL (etac disjE) *})
22.11 apply simp_all
22.12 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
22.13 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{clasimpset}]) *})
22.14 -apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
22.15 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
22.16 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
22.17 +apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
22.18 done
22.19
22.20 subsubsection {* Interference freedom Mutator-Collector *}
22.21 @@ -794,7 +794,7 @@
22.22 apply(tactic {* TRYALL (interfree_aux_tac) *})
22.23 --{* 64 subgoals left *}
22.24 apply(simp_all add:nth_list_update Invariants Append_to_free0)+
22.25 -apply(tactic{* TRYALL (clarify_tac @{claset}) *})
22.26 +apply(tactic{* TRYALL (clarify_tac @{context}) *})
22.27 --{* 4 subgoals left *}
22.28 apply force
22.29 apply(simp add:Append_to_free2)
23.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 16:03:03 2011 +0200
23.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 22:55:00 2011 +0200
23.3 @@ -132,7 +132,7 @@
23.4 apply(simp_all add:mul_mutator_interfree)
23.5 apply(simp_all add: mul_mutator_defs)
23.6 apply(tactic {* TRYALL (interfree_aux_tac) *})
23.7 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
23.8 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
23.9 apply (simp_all add:nth_list_update)
23.10 done
23.11
23.12 @@ -1123,7 +1123,7 @@
23.13 interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
23.14 apply (unfold mul_modules)
23.15 apply interfree_aux
23.16 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
23.17 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
23.18 apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
23.19 apply(erule_tac x=j in allE, force dest:Graph3)+
23.20 done
23.21 @@ -1132,7 +1132,7 @@
23.22 interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
23.23 apply (unfold mul_modules)
23.24 apply interfree_aux
23.25 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
23.26 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
23.27 apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def mul_mutator_defs nth_list_update)
23.28 done
23.29
23.30 @@ -1140,7 +1140,7 @@
23.31 interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
23.32 apply (unfold mul_modules)
23.33 apply interfree_aux
23.34 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
23.35 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
23.36 apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1
23.37 Graph12 nth_list_update)
23.38 done
23.39 @@ -1149,7 +1149,7 @@
23.40 interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
23.41 apply (unfold mul_modules)
23.42 apply interfree_aux
23.43 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
23.44 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
23.45 apply(simp_all add: mul_mutator_defs nth_list_update)
23.46 apply(simp add:Mul_AppendInv_def Append_to_free0)
23.47 done
23.48 @@ -1178,7 +1178,7 @@
23.49 --{* 24 subgoals left *}
23.50 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
23.51 --{* 14 subgoals left *}
23.52 -apply(tactic {* TRYALL (clarify_tac @{claset}) *})
23.53 +apply(tactic {* TRYALL (clarify_tac @{context}) *})
23.54 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
23.55 apply(tactic {* TRYALL (rtac conjI) *})
23.56 apply(tactic {* TRYALL (rtac impI) *})
23.57 @@ -1189,7 +1189,7 @@
23.58 --{* 72 subgoals left *}
23.59 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
23.60 --{* 35 subgoals left *}
23.61 -apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
23.62 +apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
23.63 --{* 28 subgoals left *}
23.64 apply(tactic {* TRYALL (etac conjE) *})
23.65 apply(tactic {* TRYALL (etac disjE) *})
23.66 @@ -1199,17 +1199,21 @@
23.67 apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
23.68 apply(simp_all add:Graph10)
23.69 --{* 47 subgoals left *}
23.70 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{clasimpset}]) *})
23.71 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *})
23.72 --{* 41 subgoals left *}
23.73 -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}])]) *})
23.74 +apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
23.75 + force_tac (map_simpset_local (fn ss => ss addsimps
23.76 + [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
23.77 --{* 35 subgoals left *}
23.78 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
23.79 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
23.80 --{* 31 subgoals left *}
23.81 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
23.82 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
23.83 --{* 29 subgoals left *}
23.84 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
23.85 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
23.86 --{* 25 subgoals left *}
23.87 -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}])]) *})
23.88 +apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
23.89 + force_tac (map_simpset_local (fn ss => ss addsimps
23.90 + [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
23.91 --{* 10 subgoals left *}
23.92 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)+
23.93 done
24.1 --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Fri May 13 16:03:03 2011 +0200
24.2 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Fri May 13 22:55:00 2011 +0200
24.3 @@ -170,10 +170,10 @@
24.4 --{* 35 vc *}
24.5 apply simp_all
24.6 --{* 21 vc *}
24.7 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
24.8 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
24.9 --{* 11 vc *}
24.10 apply simp_all
24.11 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
24.12 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
24.13 --{* 10 subgoals left *}
24.14 apply(erule less_SucE)
24.15 apply simp
24.16 @@ -430,13 +430,13 @@
24.17 .{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
24.18 apply oghoare
24.19 --{* 138 vc *}
24.20 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
24.21 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
24.22 --{* 112 subgoals left *}
24.23 apply(simp_all (no_asm))
24.24 --{* 97 subgoals left *}
24.25 apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
24.26 --{* 930 subgoals left *}
24.27 -apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
24.28 +apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
24.29 --{* 99 subgoals left *}
24.30 apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym])
24.31 --{* 20 subgoals left *}
24.32 @@ -535,7 +535,7 @@
24.33 .{\<acute>x=n}."
24.34 apply oghoare
24.35 apply (simp_all cong del: strong_setsum_cong)
24.36 -apply (tactic {* ALLGOALS (clarify_tac @{claset}) *})
24.37 +apply (tactic {* ALLGOALS (clarify_tac @{context}) *})
24.38 apply (simp_all cong del: strong_setsum_cong)
24.39 apply(erule (1) Example2_lemma2)
24.40 apply(erule (1) Example2_lemma2)
25.1 --- a/src/HOL/IMPP/Hoare.thy Fri May 13 16:03:03 2011 +0200
25.2 +++ b/src/HOL/IMPP/Hoare.thy Fri May 13 22:55:00 2011 +0200
25.3 @@ -209,7 +209,7 @@
25.4 *)
25.5 lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
25.6 apply (erule hoare_derivs.induct)
25.7 -apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
25.8 +apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1]) *})
25.9 apply (rule hoare_derivs.empty)
25.10 apply (erule (1) hoare_derivs.insert)
25.11 apply (fast intro: hoare_derivs.asm)
25.12 @@ -218,7 +218,7 @@
25.13 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)
25.14 prefer 7
25.15 apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
25.16 -apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{claset})) *})
25.17 +apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *})
25.18 done
25.19
25.20 lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
25.21 @@ -287,10 +287,10 @@
25.22 apply (blast) (* weaken *)
25.23 apply (tactic {* ALLGOALS (EVERY'
25.24 [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
25.25 - simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
25.26 + simp_tac @{simpset}, clarify_tac @{context}, REPEAT o smp_tac 1]) *})
25.27 apply (simp_all (no_asm_use) add: triple_valid_def2)
25.28 apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
25.29 -apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *)
25.30 +apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *)
25.31 prefer 3 apply (force) (* Call *)
25.32 apply (erule_tac [2] evaln_elim_cases) (* If *)
25.33 apply blast+
25.34 @@ -335,17 +335,17 @@
25.35 lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>
25.36 !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
25.37 apply (induct_tac c)
25.38 -apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
25.39 +apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *})
25.40 prefer 7 apply (fast intro: domI)
25.41 apply (erule_tac [6] MGT_alternD)
25.42 apply (unfold MGT_def)
25.43 apply (drule_tac [7] bspec, erule_tac [7] domI)
25.44 -apply (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 7 *},
25.45 +apply (rule_tac [7] escape, tactic {* clarsimp_tac @{context} 7 *},
25.46 rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
25.47 apply (erule_tac [!] thin_rl)
25.48 apply (rule hoare_derivs.Skip [THEN conseq2])
25.49 apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
25.50 -apply (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 3 *},
25.51 +apply (rule_tac [3] escape, tactic {* clarsimp_tac @{context} 3 *},
25.52 rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
25.53 erule_tac [3] conseq12)
25.54 apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
25.55 @@ -364,7 +364,7 @@
25.56 shows "finite U ==> uG = mgt_call`U ==>
25.57 !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
25.58 apply (induct_tac n)
25.59 -apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
25.60 +apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *})
25.61 apply (subgoal_tac "G = mgt_call ` U")
25.62 prefer 2
25.63 apply (simp add: card_seteq)
26.1 --- a/src/HOL/MicroJava/J/Conform.thy Fri May 13 16:03:03 2011 +0200
26.2 +++ b/src/HOL/MicroJava/J/Conform.thy Fri May 13 22:55:00 2011 +0200
26.3 @@ -328,8 +328,9 @@
26.4 apply auto
26.5 apply(rule hconfI)
26.6 apply(drule conforms_heapD)
26.7 -apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}]
26.8 - addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
26.9 +apply(tactic {*
26.10 + auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
26.11 + |> map_simpset_local (fn ss => ss delsimps [@{thm split_paired_All}])) *})
26.12 done
26.13
26.14 lemma conforms_upd_local:
27.1 --- a/src/HOL/MicroJava/J/WellForm.thy Fri May 13 16:03:03 2011 +0200
27.2 +++ b/src/HOL/MicroJava/J/WellForm.thy Fri May 13 22:55:00 2011 +0200
27.3 @@ -315,7 +315,7 @@
27.4 apply( clarify)
27.5 apply( frule fields_rec, assumption)
27.6 apply( fastsimp)
27.7 -apply( tactic "safe_tac HOL_cs")
27.8 +apply( tactic "safe_tac (put_claset HOL_cs @{context})")
27.9 apply( subst fields_rec)
27.10 apply( assumption)
27.11 apply( assumption)
28.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML Fri May 13 16:03:03 2011 +0200
28.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Fri May 13 22:55:00 2011 +0200
28.3 @@ -384,7 +384,7 @@
28.4 end
28.5
28.6 fun norm_arith_tac ctxt =
28.7 - clarify_tac HOL_cs THEN'
28.8 + clarify_tac (put_claset HOL_cs ctxt) THEN'
28.9 Object_Logic.full_atomize_tac THEN'
28.10 CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
28.11
29.1 --- a/src/HOL/NanoJava/AxSem.thy Fri May 13 16:03:03 2011 +0200
29.2 +++ b/src/HOL/NanoJava/AxSem.thy Fri May 13 22:55:00 2011 +0200
29.3 @@ -151,7 +151,7 @@
29.4 "(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and>
29.5 (A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))"
29.6 apply (rule hoare_ehoare.induct)
29.7 -apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
29.8 +apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
29.9 apply (blast intro: hoare_ehoare.Skip)
29.10 apply (blast intro: hoare_ehoare.Comp)
29.11 apply (blast intro: hoare_ehoare.Cond)
30.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri May 13 16:03:03 2011 +0200
30.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri May 13 22:55:00 2011 +0200
30.3 @@ -264,7 +264,7 @@
30.4 apply (simp add: zmult_assoc)
30.5 apply (rule_tac [5] zcong_zmult)
30.6 apply (rule_tac [5] inv_is_inv)
30.7 - apply (tactic "clarify_tac @{claset} 4")
30.8 + apply (tactic "clarify_tac @{context} 4")
30.9 apply (subgoal_tac [4] "a \<in> wset (a - 1) p")
30.10 apply (rule_tac [5] wset_inv_mem_mem)
30.11 apply (simp_all add: wset_fin)
31.1 --- a/src/HOL/Prolog/Test.thy Fri May 13 16:03:03 2011 +0200
31.2 +++ b/src/HOL/Prolog/Test.thy Fri May 13 22:55:00 2011 +0200
31.3 @@ -234,9 +234,9 @@
31.4
31.5 (* disjunction in atom: *)
31.6 lemma "(!P. g P :- (P => b | a)) => g(a | b)"
31.7 - apply (tactic "step_tac HOL_cs 1")
31.8 - apply (tactic "step_tac HOL_cs 1")
31.9 - apply (tactic "step_tac HOL_cs 1")
31.10 + apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
31.11 + apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
31.12 + apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
31.13 prefer 2
31.14 apply fast
31.15 apply fast
32.1 --- a/src/HOL/Proofs/Lambda/Commutation.thy Fri May 13 16:03:03 2011 +0200
32.2 +++ b/src/HOL/Proofs/Lambda/Commutation.thy Fri May 13 22:55:00 2011 +0200
32.3 @@ -127,9 +127,9 @@
32.4
32.5 lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
32.6 apply (unfold square_def commute_def diamond_def Church_Rosser_def)
32.7 - apply (tactic {* safe_tac HOL_cs *})
32.8 + apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
32.9 apply (tactic {*
32.10 - blast_tac (HOL_cs addIs
32.11 + blast_tac (put_claset HOL_cs @{context} addIs
32.12 [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
32.13 @{thm rtranclp_converseI}, @{thm conversepI},
32.14 @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
33.1 --- a/src/HOL/SET_Protocol/Message_SET.thy Fri May 13 16:03:03 2011 +0200
33.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy Fri May 13 22:55:00 2011 +0200
33.3 @@ -853,31 +853,26 @@
33.4 eresolve_tac [asm_rl, @{thm synth.Inj}];
33.5
33.6 fun Fake_insert_simp_tac ss i =
33.7 - REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
33.8 + REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
33.9
33.10 fun atomic_spy_analz_tac ctxt =
33.11 - let val ss = simpset_of ctxt and cs = claset_of ctxt in
33.12 - SELECT_GOAL
33.13 - (Fake_insert_simp_tac ss 1
33.14 - THEN
33.15 - IF_UNSOLVED (Blast.depth_tac
33.16 - (cs addIs [@{thm analz_insertI},
33.17 - impOfSubs @{thm analz_subset_parts}]) 4 1))
33.18 - end;
33.19 + SELECT_GOAL
33.20 + (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
33.21 + IF_UNSOLVED
33.22 + (Blast.depth_tac (ctxt addIs [@{thm analz_insertI},
33.23 + impOfSubs @{thm analz_subset_parts}]) 4 1));
33.24
33.25 fun spy_analz_tac ctxt i =
33.26 - let val ss = simpset_of ctxt and cs = claset_of ctxt in
33.27 - DETERM
33.28 - (SELECT_GOAL
33.29 - (EVERY
33.30 - [ (*push in occurrences of X...*)
33.31 - (REPEAT o CHANGED)
33.32 - (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
33.33 - (*...allowing further simplifications*)
33.34 - simp_tac ss 1,
33.35 - REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
33.36 - DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
33.37 - end;
33.38 + DETERM
33.39 + (SELECT_GOAL
33.40 + (EVERY
33.41 + [ (*push in occurrences of X...*)
33.42 + (REPEAT o CHANGED)
33.43 + (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
33.44 + (*...allowing further simplifications*)
33.45 + simp_tac (simpset_of ctxt) 1,
33.46 + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
33.47 + DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
33.48 *}
33.49 (*>*)
33.50
34.1 --- a/src/HOL/TLA/Action.thy Fri May 13 16:03:03 2011 +0200
34.2 +++ b/src/HOL/TLA/Action.thy Fri May 13 22:55:00 2011 +0200
34.3 @@ -278,7 +278,7 @@
34.4 *)
34.5
34.6 fun enabled_tac ctxt base_vars =
34.7 - clarsimp_tac (claset_of ctxt addSIs [base_vars RS @{thm base_enabled}], simpset_of ctxt);
34.8 + clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]);
34.9 *}
34.10
34.11 method_setup enabled = {*
35.1 --- a/src/HOL/TLA/TLA.thy Fri May 13 16:03:03 2011 +0200
35.2 +++ b/src/HOL/TLA/TLA.thy Fri May 13 22:55:00 2011 +0200
35.3 @@ -583,11 +583,13 @@
35.4
35.5 ML {*
35.6 (* inv_tac reduces goals of the form ... ==> sigma |= []P *)
35.7 -fun inv_tac css = SELECT_GOAL
35.8 - (EVERY [auto_tac css,
35.9 - TRY (merge_box_tac 1),
35.10 - rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
35.11 - TRYALL (etac @{thm Stable})]);
35.12 +fun inv_tac ctxt =
35.13 + SELECT_GOAL
35.14 + (EVERY
35.15 + [auto_tac ctxt,
35.16 + TRY (merge_box_tac 1),
35.17 + rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
35.18 + TRYALL (etac @{thm Stable})]);
35.19
35.20 (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
35.21 in simple cases it may be able to handle goals like |- MyProg --> []Inv.
35.22 @@ -595,15 +597,15 @@
35.23 auto-tactic, which applies too much propositional logic and simplifies
35.24 too late.
35.25 *)
35.26 -fun auto_inv_tac ss = SELECT_GOAL
35.27 - ((inv_tac (@{claset}, ss) 1) THEN
35.28 - (TRYALL (action_simp_tac
35.29 - (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
35.30 +fun auto_inv_tac ss =
35.31 + SELECT_GOAL
35.32 + (inv_tac (map_simpset_local (K ss) @{context}) 1 THEN
35.33 + (TRYALL (action_simp_tac
35.34 + (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
35.35 *}
35.36
35.37 method_setup invariant = {*
35.38 - Method.sections Clasimp.clasimp_modifiers
35.39 - >> (K (SIMPLE_METHOD' o inv_tac o clasimpset_of))
35.40 + Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
35.41 *} ""
35.42
35.43 method_setup auto_invariant = {*
36.1 --- a/src/HOL/Tools/Function/fun.ML Fri May 13 16:03:03 2011 +0200
36.2 +++ b/src/HOL/Tools/Function/fun.ML Fri May 13 22:55:00 2011 +0200
36.3 @@ -143,7 +143,7 @@
36.4 let
36.5 fun pat_completeness_auto ctxt =
36.6 Pat_Completeness.pat_completeness_tac ctxt 1
36.7 - THEN auto_tac (clasimpset_of ctxt)
36.8 + THEN auto_tac ctxt
36.9 fun prove_termination lthy =
36.10 Function.prove_termination NONE
36.11 (Function_Common.get_termination_prover lthy lthy) lthy
37.1 --- a/src/HOL/Tools/Function/function_core.ML Fri May 13 16:03:03 2011 +0200
37.2 +++ b/src/HOL/Tools/Function/function_core.ML Fri May 13 22:55:00 2011 +0200
37.3 @@ -702,7 +702,7 @@
37.4 Goal.init goal
37.5 |> (SINGLE (resolve_tac [accI] 1)) |> the
37.6 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
37.7 - |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
37.8 + |> (SINGLE (auto_tac ctxt)) |> the
37.9 |> Goal.conclude
37.10 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
37.11 end
38.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 16:03:03 2011 +0200
38.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 22:55:00 2011 +0200
38.3 @@ -214,9 +214,10 @@
38.4 end
38.5
38.6 fun lexicographic_order_tac quiet ctxt =
38.7 - TRY (Function_Common.apply_termination_rule ctxt 1)
38.8 - THEN lex_order_tac quiet ctxt
38.9 - (auto_tac (claset_of ctxt, simpset_of ctxt addsimps Function_Common.Termination_Simps.get ctxt))
38.10 + TRY (Function_Common.apply_termination_rule ctxt 1) THEN
38.11 + lex_order_tac quiet ctxt
38.12 + (auto_tac
38.13 + (map_simpset_local (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
38.14
38.15 val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
38.16
39.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 16:03:03 2011 +0200
39.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 22:55:00 2011 +0200
39.3 @@ -338,7 +338,7 @@
39.4 fun decomp_scnp_tac orders ctxt =
39.5 let
39.6 val extra_simps = Function_Common.Termination_Simps.get ctxt
39.7 - val autom_tac = auto_tac (claset_of ctxt, simpset_of ctxt addsimps extra_simps)
39.8 + val autom_tac = auto_tac (map_simpset_local (fn ss => ss addsimps extra_simps) ctxt)
39.9 in
39.10 gen_sizechange_tac orders autom_tac ctxt
39.11 end
40.1 --- a/src/HOL/Tools/Function/termination.ML Fri May 13 16:03:03 2011 +0200
40.2 +++ b/src/HOL/Tools/Function/termination.ML Fri May 13 22:55:00 2011 +0200
40.3 @@ -297,7 +297,7 @@
40.4 THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *)
40.5 ORELSE' ((rtac @{thm conjI})
40.6 THEN' (rtac @{thm refl})
40.7 - THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *)
40.8 + THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *)
40.9 ) i
40.10 in
40.11 ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
41.1 --- a/src/HOL/Tools/Meson/meson.ML Fri May 13 16:03:03 2011 +0200
41.2 +++ b/src/HOL/Tools/Meson/meson.ML Fri May 13 22:55:00 2011 +0200
41.3 @@ -699,8 +699,7 @@
41.4
41.5 (*First, breaks the goal into independent units*)
41.6 fun safe_best_meson_tac ctxt =
41.7 - SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
41.8 - TRYALL (best_meson_tac size_of_subgoals ctxt));
41.9 + SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt));
41.10
41.11 (** Depth-first search version **)
41.12
41.13 @@ -742,7 +741,7 @@
41.14 end));
41.15
41.16 fun meson_tac ctxt ths =
41.17 - SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
41.18 + SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
41.19
41.20
41.21 (**** Code to support ordinary resolution, rather than Model Elimination ****)
42.1 --- a/src/HOL/Tools/Meson/meson_tactic.ML Fri May 13 16:03:03 2011 +0200
42.2 +++ b/src/HOL/Tools/Meson/meson_tactic.ML Fri May 13 22:55:00 2011 +0200
42.3 @@ -17,9 +17,8 @@
42.4 open Meson_Clausify
42.5
42.6 fun meson_general_tac ctxt ths =
42.7 - let val ctxt = Classical.put_claset HOL_cs ctxt in
42.8 - Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
42.9 - end
42.10 + let val ctxt' = put_claset HOL_cs ctxt
42.11 + in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false 0) ths) end
42.12
42.13 val setup =
42.14 Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
43.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri May 13 16:03:03 2011 +0200
43.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri May 13 22:55:00 2011 +0200
43.3 @@ -2004,9 +2004,8 @@
43.4 map (wf_constraint_for rel side concl) main |> foldr1 s_conj
43.5
43.6 fun terminates_by ctxt timeout goal tac =
43.7 - can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
43.8 - #> SINGLE (DETERM_TIMEOUT timeout
43.9 - (tac ctxt (auto_tac (clasimpset_of ctxt))))
43.10 + can (SINGLE (Classical.safe_tac ctxt) #> the
43.11 + #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt)))
43.12 #> the #> Goal.finish ctxt) goal
43.13
43.14 val max_cached_wfs = 50
44.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 13 16:03:03 2011 +0200
44.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 13 22:55:00 2011 +0200
44.3 @@ -1050,8 +1050,7 @@
44.4 ()
44.5 val goal = prop |> cterm_of thy |> Goal.init
44.6 in
44.7 - (goal |> SINGLE (DETERM_TIMEOUT auto_timeout
44.8 - (auto_tac (clasimpset_of ctxt)))
44.9 + (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
44.10 |> the |> Goal.finish ctxt; true)
44.11 handle THM _ => false
44.12 | TimeLimit.TimeOut => false
45.1 --- a/src/HOL/Tools/Qelim/cooper.ML Fri May 13 16:03:03 2011 +0200
45.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri May 13 22:55:00 2011 +0200
45.3 @@ -706,7 +706,7 @@
45.4 val all_maxscope_ss =
45.5 HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
45.6 in
45.7 -fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
45.8 +fun thin_prems_tac ctxt P = simp_tac all_maxscope_ss THEN'
45.9 CSUBGOAL (fn (p', i) =>
45.10 let
45.11 val (qvs, p) = strip_objall (Thm.dest_arg p')
45.12 @@ -720,7 +720,7 @@
45.13 | _ => false)
45.14 in
45.15 if ntac then no_tac
45.16 - else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
45.17 + else rtac (Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) i
45.18 end)
45.19 end;
45.20
45.21 @@ -843,7 +843,7 @@
45.22 THEN_ALL_NEW simp_tac ss
45.23 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
45.24 THEN_ALL_NEW Object_Logic.full_atomize_tac
45.25 - THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
45.26 + THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
45.27 THEN_ALL_NEW Object_Logic.full_atomize_tac
45.28 THEN_ALL_NEW div_mod_tac ctxt
45.29 THEN_ALL_NEW splits_tac ctxt
46.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri May 13 16:03:03 2011 +0200
46.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri May 13 22:55:00 2011 +0200
46.3 @@ -38,8 +38,7 @@
46.4 (* defining functions *)
46.5
46.6 fun pat_completeness_auto ctxt =
46.7 - Pat_Completeness.pat_completeness_tac ctxt 1
46.8 - THEN auto_tac (clasimpset_of ctxt)
46.9 + Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
46.10
46.11 fun define_functions (mk_equations, termination_tac) prfx argnames names Ts =
46.12 if define_foundationally andalso is_some termination_tac then
47.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri May 13 16:03:03 2011 +0200
47.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri May 13 22:55:00 2011 +0200
47.3 @@ -97,9 +97,14 @@
47.4 val rewr_if =
47.5 @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
47.6 in
47.7 -val simp_fast_tac =
47.8 +
47.9 +fun HOL_fast_tac ctxt =
47.10 + Classical.fast_tac (put_claset HOL_cs ctxt)
47.11 +
47.12 +fun simp_fast_tac ctxt =
47.13 Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
47.14 - THEN_ALL_NEW Classical.fast_tac HOL_cs
47.15 + THEN_ALL_NEW HOL_fast_tac ctxt
47.16 +
47.17 end
47.18
47.19
47.20 @@ -300,7 +305,7 @@
47.21
47.22 (* distributivity of | over & *)
47.23 fun distributivity ctxt = Thm o try_apply ctxt [] [
47.24 - named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
47.25 + named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
47.26 (* FIXME: not very well tested *)
47.27
47.28
47.29 @@ -356,7 +361,7 @@
47.30 fun def_axiom ctxt = Thm o try_apply ctxt [] [
47.31 named ctxt "conj/disj/distinct" prove_def_axiom,
47.32 Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
47.33 - named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
47.34 + named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
47.35 end
47.36
47.37
47.38 @@ -417,7 +422,7 @@
47.39 fun prove_nnf ctxt = try_apply ctxt [] [
47.40 named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
47.41 Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
47.42 - named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
47.43 + named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
47.44 in
47.45 fun nnf ctxt vars ps ct =
47.46 (case SMT_Utils.term_of ct of
47.47 @@ -552,13 +557,13 @@
47.48
47.49 (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
47.50 fun pull_quant ctxt = Thm o try_apply ctxt [] [
47.51 - named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
47.52 + named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
47.53 (* FIXME: not very well tested *)
47.54
47.55
47.56 (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
47.57 fun push_quant ctxt = Thm o try_apply ctxt [] [
47.58 - named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
47.59 + named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
47.60 (* FIXME: not very well tested *)
47.61
47.62
47.63 @@ -582,7 +587,7 @@
47.64
47.65 (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
47.66 fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
47.67 - named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
47.68 + named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
47.69 (* FIXME: not very well tested *)
47.70
47.71
47.72 @@ -694,18 +699,18 @@
47.73 Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
47.74 Z3_Proof_Tools.by_tac (
47.75 NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
47.76 - THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
47.77 + THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
47.78 Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
47.79 Z3_Proof_Tools.by_tac (
47.80 NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
47.81 THEN_ALL_NEW (
47.82 - NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
47.83 + NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
47.84 ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
47.85 Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
47.86 Z3_Proof_Tools.by_tac (
47.87 NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
47.88 THEN_ALL_NEW (
47.89 - NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
47.90 + NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
47.91 ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
47.92 named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))
47.93
48.1 --- a/src/HOL/Tools/TFL/post.ML Fri May 13 16:03:03 2011 +0200
48.2 +++ b/src/HOL/Tools/TFL/post.ML Fri May 13 22:55:00 2011 +0200
48.3 @@ -40,7 +40,7 @@
48.4 terminator =
48.5 asm_simp_tac (simpset_of ctxt) 1
48.6 THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
48.7 - fast_tac (claset_of ctxt addSDs [@{thm not0_implies_Suc}] addss (simpset_of ctxt)) 1),
48.8 + fast_simp_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
48.9 simplifier = Rules.simpl_conv (simpset_of ctxt) []};
48.10
48.11
49.1 --- a/src/HOL/Tools/groebner.ML Fri May 13 16:03:03 2011 +0200
49.2 +++ b/src/HOL/Tools/groebner.ML Fri May 13 22:55:00 2011 +0200
49.3 @@ -1012,10 +1012,10 @@
49.4 THEN ring_tac add_ths del_ths ctxt 1
49.5 end
49.6 in
49.7 - clarify_tac @{claset} i
49.8 + clarify_tac @{context} i
49.9 THEN Object_Logic.full_atomize_tac i
49.10 THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i
49.11 - THEN clarify_tac @{claset} i
49.12 + THEN clarify_tac @{context} i
49.13 THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
49.14 THEN SUBPROOF poly_exists_tac ctxt i
49.15 end
50.1 --- a/src/HOL/Tools/record.ML Fri May 13 16:03:03 2011 +0200
50.2 +++ b/src/HOL/Tools/record.ML Fri May 13 22:55:00 2011 +0200
50.3 @@ -44,7 +44,7 @@
50.4 val ex_sel_eq_simproc: simproc
50.5 val split_tac: int -> tactic
50.6 val split_simp_tac: thm list -> (term -> int) -> int -> tactic
50.7 - val split_wrapper: string * wrapper
50.8 + val split_wrapper: string * (Proof.context -> wrapper)
50.9
50.10 val updateN: string
50.11 val ext_typeN: string
50.12 @@ -1508,7 +1508,7 @@
50.13 (* wrapper *)
50.14
50.15 val split_name = "record_split_tac";
50.16 -val split_wrapper = (split_name, fn tac => split_tac ORELSE' tac);
50.17 +val split_wrapper = (split_name, fn _ => fn tac => split_tac ORELSE' tac);
50.18
50.19
50.20
51.1 --- a/src/HOL/Tools/simpdata.ML Fri May 13 16:03:03 2011 +0200
51.2 +++ b/src/HOL/Tools/simpdata.ML Fri May 13 22:55:00 2011 +0200
51.3 @@ -163,9 +163,6 @@
51.4 );
51.5 open Clasimp;
51.6
51.7 -val _ = ML_Antiquote.value "clasimpset"
51.8 - (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
51.9 -
51.10 val mksimps_pairs =
51.11 [(@{const_name HOL.implies}, [@{thm mp}]),
51.12 (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
52.1 --- a/src/HOL/UNITY/Comp/Alloc.thy Fri May 13 16:03:03 2011 +0200
52.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy Fri May 13 22:55:00 2011 +0200
52.3 @@ -331,10 +331,15 @@
52.4 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
52.5 ML {*
52.6 fun record_auto_tac ctxt =
52.7 - auto_tac (claset_of ctxt addIs [ext] addSWrapper Record.split_wrapper,
52.8 - simpset_of ctxt addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
52.9 - @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
52.10 - @{thm o_apply}, @{thm Let_def}])
52.11 + let val ctxt' =
52.12 + (ctxt addIs [ext])
52.13 + |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
52.14 + |> map_simpset_local (fn ss => ss
52.15 + addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
52.16 + @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
52.17 + @{thm o_apply}, @{thm Let_def}])
52.18 + in auto_tac ctxt' end;
52.19 +
52.20 *}
52.21
52.22 method_setup record_auto = {*
53.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri May 13 16:03:03 2011 +0200
53.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Fri May 13 22:55:00 2011 +0200
53.3 @@ -102,35 +102,25 @@
53.4 text{*This ML code does the inductions directly.*}
53.5 ML{*
53.6 fun ns_constrains_tac ctxt i =
53.7 - let
53.8 - val cs = claset_of ctxt;
53.9 - val ss = simpset_of ctxt;
53.10 - in
53.11 - SELECT_GOAL
53.12 - (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1),
53.13 - REPEAT (resolve_tac [@{thm StableI}, @{thm stableI},
53.14 - @{thm constrains_imp_Constrains}] 1),
53.15 - rtac @{thm ns_constrainsI} 1,
53.16 - full_simp_tac ss 1,
53.17 - REPEAT (FIRSTGOAL (etac disjE)),
53.18 - ALLGOALS (clarify_tac (cs delrules [impI, @{thm impCE}])),
53.19 - REPEAT (FIRSTGOAL analz_mono_contra_tac),
53.20 - ALLGOALS (asm_simp_tac ss)]) i
53.21 - end;
53.22 + SELECT_GOAL
53.23 + (EVERY
53.24 + [REPEAT (etac @{thm Always_ConstrainsI} 1),
53.25 + REPEAT (resolve_tac [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1),
53.26 + rtac @{thm ns_constrainsI} 1,
53.27 + full_simp_tac (simpset_of ctxt) 1,
53.28 + REPEAT (FIRSTGOAL (etac disjE)),
53.29 + ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])),
53.30 + REPEAT (FIRSTGOAL analz_mono_contra_tac),
53.31 + ALLGOALS (asm_simp_tac (simpset_of ctxt))]) i;
53.32
53.33 (*Tactic for proving secrecy theorems*)
53.34 fun ns_induct_tac ctxt =
53.35 - let
53.36 - val cs = claset_of ctxt;
53.37 - val ss = simpset_of ctxt;
53.38 - in
53.39 - (SELECT_GOAL o EVERY)
53.40 - [rtac @{thm AlwaysI} 1,
53.41 - force_tac (cs,ss) 1,
53.42 - (*"reachable" gets in here*)
53.43 - rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
53.44 - ns_constrains_tac ctxt 1]
53.45 - end;
53.46 + (SELECT_GOAL o EVERY)
53.47 + [rtac @{thm AlwaysI} 1,
53.48 + force_tac ctxt 1,
53.49 + (*"reachable" gets in here*)
53.50 + rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
53.51 + ns_constrains_tac ctxt 1];
53.52 *}
53.53
53.54 method_setup ns_induct = {*
54.1 --- a/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 16:03:03 2011 +0200
54.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 22:55:00 2011 +0200
54.3 @@ -14,51 +14,42 @@
54.4 (*Proves "co" properties when the program is specified. Any use of invariants
54.5 (from weak constrains) must have been done already.*)
54.6 fun constrains_tac ctxt i =
54.7 - let
54.8 - val cs = claset_of ctxt;
54.9 - val ss = simpset_of ctxt;
54.10 - in
54.11 - SELECT_GOAL
54.12 - (EVERY [REPEAT (Always_Int_tac 1),
54.13 - (*reduce the fancy safety properties to "constrains"*)
54.14 - REPEAT (etac @{thm Always_ConstrainsI} 1
54.15 - ORELSE
54.16 - resolve_tac [@{thm StableI}, @{thm stableI},
54.17 - @{thm constrains_imp_Constrains}] 1),
54.18 - (*for safety, the totalize operator can be ignored*)
54.19 - simp_tac (HOL_ss addsimps
54.20 - [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
54.21 - rtac @{thm constrainsI} 1,
54.22 - full_simp_tac ss 1,
54.23 - REPEAT (FIRSTGOAL (etac disjE)),
54.24 - ALLGOALS (clarify_tac cs),
54.25 - ALLGOALS (asm_full_simp_tac ss)]) i
54.26 - end;
54.27 + SELECT_GOAL
54.28 + (EVERY
54.29 + [REPEAT (Always_Int_tac 1),
54.30 + (*reduce the fancy safety properties to "constrains"*)
54.31 + REPEAT (etac @{thm Always_ConstrainsI} 1
54.32 + ORELSE
54.33 + resolve_tac [@{thm StableI}, @{thm stableI},
54.34 + @{thm constrains_imp_Constrains}] 1),
54.35 + (*for safety, the totalize operator can be ignored*)
54.36 + simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
54.37 + rtac @{thm constrainsI} 1,
54.38 + full_simp_tac (simpset_of ctxt) 1,
54.39 + REPEAT (FIRSTGOAL (etac disjE)),
54.40 + ALLGOALS (clarify_tac ctxt),
54.41 + ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
54.42
54.43 (*proves "ensures/leadsTo" properties when the program is specified*)
54.44 fun ensures_tac ctxt sact =
54.45 - let
54.46 - val cs = claset_of ctxt;
54.47 - val ss = simpset_of ctxt;
54.48 - in
54.49 - SELECT_GOAL
54.50 - (EVERY [REPEAT (Always_Int_tac 1),
54.51 - etac @{thm Always_LeadsTo_Basis} 1
54.52 - ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
54.53 - REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
54.54 - @{thm EnsuresI}, @{thm ensuresI}] 1),
54.55 - (*now there are two subgoals: co & transient*)
54.56 - simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
54.57 - res_inst_tac (Simplifier.the_context ss)
54.58 - [(("act", 0), sact)] @{thm totalize_transientI} 2
54.59 - ORELSE res_inst_tac (Simplifier.the_context ss)
54.60 - [(("act", 0), sact)] @{thm transientI} 2,
54.61 - (*simplify the command's domain*)
54.62 - simp_tac (ss addsimps [@{thm Domain_def}]) 3,
54.63 - constrains_tac ctxt 1,
54.64 - ALLGOALS (clarify_tac cs),
54.65 - ALLGOALS (asm_lr_simp_tac ss)])
54.66 - end;
54.67 + SELECT_GOAL
54.68 + (EVERY
54.69 + [REPEAT (Always_Int_tac 1),
54.70 + etac @{thm Always_LeadsTo_Basis} 1
54.71 + ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
54.72 + REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
54.73 + @{thm EnsuresI}, @{thm ensuresI}] 1),
54.74 + (*now there are two subgoals: co & transient*)
54.75 + simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
54.76 + res_inst_tac ctxt
54.77 + [(("act", 0), sact)] @{thm totalize_transientI} 2
54.78 + ORELSE res_inst_tac ctxt
54.79 + [(("act", 0), sact)] @{thm transientI} 2,
54.80 + (*simplify the command's domain*)
54.81 + simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
54.82 + constrains_tac ctxt 1,
54.83 + ALLGOALS (clarify_tac ctxt),
54.84 + ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
54.85
54.86
54.87 (*Composition equivalences, from Lift_prog*)
55.1 --- a/src/HOL/Word/Word.thy Fri May 13 16:03:03 2011 +0200
55.2 +++ b/src/HOL/Word/Word.thy Fri May 13 22:55:00 2011 +0200
55.3 @@ -1475,11 +1475,9 @@
55.4 fun arith_tac' n t =
55.5 Arith_Data.verbose_arith_tac ctxt n t
55.6 handle Cooper.COOPER _ => Seq.empty;
55.7 - val cs = claset_of ctxt;
55.8 - val ss = simpset_of ctxt;
55.9 in
55.10 - [ clarify_tac cs 1,
55.11 - full_simp_tac (uint_arith_ss_of ss) 1,
55.12 + [ clarify_tac ctxt 1,
55.13 + full_simp_tac (uint_arith_ss_of (simpset_of ctxt)) 1,
55.14 ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits}
55.15 addcongs @{thms power_False_cong})),
55.16 rewrite_goals_tac @{thms word_size},
55.17 @@ -2034,11 +2032,9 @@
55.18 fun arith_tac' n t =
55.19 Arith_Data.verbose_arith_tac ctxt n t
55.20 handle Cooper.COOPER _ => Seq.empty;
55.21 - val cs = claset_of ctxt;
55.22 - val ss = simpset_of ctxt;
55.23 in
55.24 - [ clarify_tac cs 1,
55.25 - full_simp_tac (unat_arith_ss_of ss) 1,
55.26 + [ clarify_tac ctxt 1,
55.27 + full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1,
55.28 ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits}
55.29 addcongs @{thms power_False_cong})),
55.30 rewrite_goals_tac @{thms word_size},
56.1 --- a/src/HOL/ex/MT.thy Fri May 13 16:03:03 2011 +0200
56.2 +++ b/src/HOL/ex/MT.thy Fri May 13 22:55:00 2011 +0200
56.3 @@ -869,7 +869,7 @@
56.4 ve + {ev |-> v} hastyenv te + {ev |=> t}"
56.5 apply (unfold hasty_env_def)
56.6 apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
56.7 -apply (tactic {* safe_tac HOL_cs *})
56.8 +apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
56.9 apply (case_tac "ev=x")
56.10 apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
56.11 apply (simp add: ve_app_owr2 te_app_owr2)
56.12 @@ -906,7 +906,7 @@
56.13 v_clos(cl) hasty t"
56.14 apply (unfold hasty_env_def hasty_def)
56.15 apply (drule elab_fix_elim)
56.16 -apply (tactic {* safe_tac HOL_cs *})
56.17 +apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
56.18 (*Do a single unfolding of cl*)
56.19 apply (frule ssubst) prefer 2 apply assumption
56.20 apply (rule hasty_rel_clos_coind)
56.21 @@ -914,7 +914,7 @@
56.22 apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
56.23
56.24 apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
56.25 -apply (tactic {* safe_tac HOL_cs *})
56.26 +apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
56.27 apply (case_tac "ev2=ev1a")
56.28 apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
56.29 apply blast
57.1 --- a/src/Provers/blast.ML Fri May 13 16:03:03 2011 +0200
57.2 +++ b/src/Provers/blast.ML Fri May 13 22:55:00 2011 +0200
57.3 @@ -51,7 +51,6 @@
57.4
57.5 signature BLAST =
57.6 sig
57.7 - type claset
57.8 exception TRANS of string (*reports translation errors*)
57.9 datatype term =
57.10 Const of string * term list
57.11 @@ -61,9 +60,9 @@
57.12 | Bound of int
57.13 | Abs of string*term
57.14 | $ of term*term;
57.15 - val depth_tac: claset -> int -> int -> tactic
57.16 + val depth_tac: Proof.context -> int -> int -> tactic
57.17 val depth_limit: int Config.T
57.18 - val blast_tac: claset -> int -> tactic
57.19 + val blast_tac: Proof.context -> int -> tactic
57.20 val setup: theory -> theory
57.21 (*debugging tools*)
57.22 type branch
57.23 @@ -75,8 +74,8 @@
57.24 val fromSubgoal: theory -> Term.term -> term
57.25 val instVars: term -> (unit -> unit)
57.26 val toTerm: int -> term -> Term.term
57.27 - val readGoal: theory -> string -> term
57.28 - val tryInThy: theory -> claset -> int -> string ->
57.29 + val readGoal: Proof.context -> string -> term
57.30 + val tryIt: Proof.context -> int -> string ->
57.31 (int -> tactic) list * branch list list * (int * int * exn) list
57.32 val normBr: branch -> branch
57.33 end;
57.34 @@ -85,7 +84,6 @@
57.35 struct
57.36
57.37 structure Classical = Data.Classical;
57.38 -type claset = Classical.claset;
57.39
57.40 val trace = Unsynchronized.ref false
57.41 and stats = Unsynchronized.ref false; (*for runtime and search statistics*)
57.42 @@ -915,9 +913,10 @@
57.43 bound on unsafe expansions.
57.44 "start" is CPU time at start, for printing search time
57.45 *)
57.46 -fun prove (state, start, cs, brs, cont) =
57.47 +fun prove (state, start, ctxt, brs, cont) =
57.48 let val State {thy, ntrail, nclosed, ntried, ...} = state;
57.49 - val {safe0_netpair, safep_netpair, haz_netpair, ...} = Classical.rep_cs cs
57.50 + val {safe0_netpair, safep_netpair, haz_netpair, ...} =
57.51 + Classical.rep_cs (Classical.claset_of ctxt);
57.52 val safeList = [safe0_netpair, safep_netpair]
57.53 and hazList = [haz_netpair]
57.54 fun prv (tacs, trs, choices, []) =
57.55 @@ -1237,7 +1236,7 @@
57.56 "start" is CPU time at start, for printing SEARCH time
57.57 (also prints reconstruction time)
57.58 "lim" is depth limit.*)
57.59 -fun timing_depth_tac start cs lim i st0 =
57.60 +fun timing_depth_tac start ctxt lim i st0 =
57.61 let val thy = Thm.theory_of_thm st0
57.62 val state = initialize thy
57.63 val st = st0
57.64 @@ -1261,20 +1260,20 @@
57.65 Seq.make(fn()=> cell))
57.66 end
57.67 in
57.68 - prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
57.69 + prove (state, start, ctxt, [initBranch (mkGoal concl :: hyps, lim)], cont)
57.70 |> Seq.map (rotate_prems (1 - i))
57.71 end
57.72 handle PROVE => Seq.empty;
57.73
57.74 (*Public version with fixed depth*)
57.75 -fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
57.76 +fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;
57.77
57.78 val (depth_limit, setup_depth_limit) =
57.79 Attrib.config_int_global @{binding blast_depth_limit} (K 20);
57.80
57.81 -fun blast_tac cs i st =
57.82 +fun blast_tac ctxt i st =
57.83 ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
57.84 - (timing_depth_tac (Timing.start ()) cs) 0) i
57.85 + (timing_depth_tac (Timing.start ()) ctxt) 0) i
57.86 THEN flexflex_tac) st
57.87 handle TRANS s =>
57.88 ((if !trace then warning ("blast: " ^ s) else ());
57.89 @@ -1288,13 +1287,15 @@
57.90 val fullTrace = Unsynchronized.ref ([]: branch list list);
57.91
57.92 (*Read a string to make an initial, singleton branch*)
57.93 -fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
57.94 +fun readGoal ctxt s =
57.95 + Syntax.read_prop ctxt s |> fromTerm (Proof_Context.theory_of ctxt) |> rand |> mkGoal;
57.96
57.97 -fun tryInThy thy cs lim s =
57.98 +fun tryIt ctxt lim s =
57.99 let
57.100 + val thy = Proof_Context.theory_of ctxt;
57.101 val state as State {fullTrace = ft, ...} = initialize thy;
57.102 val res = timeap prove
57.103 - (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I);
57.104 + (state, Timing.start (), ctxt, [initBranch ([readGoal ctxt s], lim)], I);
57.105 val _ = fullTrace := !ft;
57.106 in res end;
57.107
57.108 @@ -1305,8 +1306,8 @@
57.109 setup_depth_limit #>
57.110 Method.setup @{binding blast}
57.111 (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
57.112 - (fn NONE => Classical.cla_meth' blast_tac
57.113 - | SOME lim => Classical.cla_meth' (fn cs => depth_tac cs lim)))
57.114 + (fn NONE => SIMPLE_METHOD' o blast_tac
57.115 + | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
57.116 "classical tableau prover";
57.117
57.118 end;
58.1 --- a/src/Provers/clasimp.ML Fri May 13 16:03:03 2011 +0200
58.2 +++ b/src/Provers/clasimp.ML Fri May 13 22:55:00 2011 +0200
58.3 @@ -5,14 +5,11 @@
58.4 splitter.ML, classical.ML, blast.ML).
58.5 *)
58.6
58.7 -infix 4 addSss addss addss';
58.8 -
58.9 signature CLASIMP_DATA =
58.10 sig
58.11 structure Splitter: SPLITTER
58.12 structure Classical: CLASSICAL
58.13 structure Blast: BLAST
58.14 - sharing type Classical.claset = Blast.claset
58.15 val notE: thm
58.16 val iffD1: thm
58.17 val iffD2: thm
58.18 @@ -20,19 +17,16 @@
58.19
58.20 signature CLASIMP =
58.21 sig
58.22 - type claset
58.23 - type clasimpset
58.24 - val clasimpset_of: Proof.context -> clasimpset
58.25 - val addSss: claset * simpset -> claset
58.26 - val addss: claset * simpset -> claset
58.27 - val addss': claset * simpset -> claset
58.28 - val clarsimp_tac: clasimpset -> int -> tactic
58.29 - val mk_auto_tac: clasimpset -> int -> int -> tactic
58.30 - val auto_tac: clasimpset -> tactic
58.31 - val force_tac: clasimpset -> int -> tactic
58.32 - val fast_simp_tac: clasimpset -> int -> tactic
58.33 - val slow_simp_tac: clasimpset -> int -> tactic
58.34 - val best_simp_tac: clasimpset -> int -> tactic
58.35 + val addSss: Proof.context -> Proof.context
58.36 + val addss: Proof.context -> Proof.context
58.37 + val addss': Proof.context -> Proof.context
58.38 + val clarsimp_tac: Proof.context -> int -> tactic
58.39 + val mk_auto_tac: Proof.context -> int -> int -> tactic
58.40 + val auto_tac: Proof.context -> tactic
58.41 + val force_tac: Proof.context -> int -> tactic
58.42 + val fast_simp_tac: Proof.context -> int -> tactic
58.43 + val slow_simp_tac: Proof.context -> int -> tactic
58.44 + val best_simp_tac: Proof.context -> int -> tactic
58.45 val iff_add: attribute
58.46 val iff_add': attribute
58.47 val iff_del: attribute
58.48 @@ -49,29 +43,20 @@
58.49 structure Blast = Data.Blast;
58.50
58.51
58.52 -(* type clasimpset *)
58.53 -
58.54 -type claset = Classical.claset;
58.55 -type clasimpset = claset * simpset;
58.56 -
58.57 -fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);
58.58 -
58.59 -
58.60 (* simp as classical wrapper *)
58.61
58.62 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
58.63 val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);
58.64
58.65 -(*Add a simpset to a classical set!*)
58.66 +fun clasimp f name tac ctxt =
58.67 + Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
58.68 +
58.69 +(*Add a simpset to the claset!*)
58.70 (*Caution: only one simpset added can be added by each of addSss and addss*)
58.71 -fun cs addSss ss =
58.72 - Classical.addSafter (cs, ("safe_asm_full_simp_tac", CHANGED o safe_asm_full_simp_tac ss));
58.73 -
58.74 -fun cs addss ss =
58.75 - Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_full_simp_tac ss));
58.76 -
58.77 -fun cs addss' ss =
58.78 - Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_lr_simp_tac ss));
58.79 +val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
58.80 +val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
58.81 +(* FIXME "asm_lr_simp_tac" !? *)
58.82 +val addss' = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_lr_simp_tac;
58.83
58.84
58.85 (* iffs: addition of rules to simpsets and clasets simultaneously *)
58.86 @@ -128,75 +113,72 @@
58.87
58.88 (* tactics *)
58.89
58.90 -fun clarsimp_tac (cs, ss) =
58.91 - safe_asm_full_simp_tac ss THEN_ALL_NEW
58.92 - Classical.clarify_tac (cs addSss ss);
58.93 +fun clarsimp_tac ctxt =
58.94 + safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
58.95 + Classical.clarify_tac (addSss ctxt);
58.96
58.97
58.98 (* auto_tac *)
58.99
58.100 -fun blast_depth_tac cs m i thm =
58.101 - Blast.depth_tac cs m i thm
58.102 +fun blast_depth_tac ctxt m i thm =
58.103 + Blast.depth_tac ctxt m i thm
58.104 handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
58.105
58.106 (* a variant of depth_tac that avoids interference of the simplifier
58.107 with dup_step_tac when they are combined by auto_tac *)
58.108 local
58.109
58.110 -fun slow_step_tac' cs =
58.111 - Classical.appWrappers cs
58.112 - (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
58.113 +fun slow_step_tac' ctxt =
58.114 + Classical.appWrappers ctxt
58.115 + (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt);
58.116
58.117 in
58.118
58.119 -fun nodup_depth_tac cs m i st =
58.120 +fun nodup_depth_tac ctxt m i st =
58.121 SELECT_GOAL
58.122 - (Classical.safe_steps_tac cs 1 THEN_ELSE
58.123 - (DEPTH_SOLVE (nodup_depth_tac cs m 1),
58.124 - Classical.inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
58.125 - (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m - 1) 1)))) i st;
58.126 + (Classical.safe_steps_tac ctxt 1 THEN_ELSE
58.127 + (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
58.128 + Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
58.129 + (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
58.130
58.131 end;
58.132
58.133 (*Designed to be idempotent, except if blast_depth_tac instantiates variables
58.134 in some of the subgoals*)
58.135 -fun mk_auto_tac (cs, ss) m n =
58.136 +fun mk_auto_tac ctxt m n =
58.137 let
58.138 - val cs' = cs addss ss;
58.139 val main_tac =
58.140 - blast_depth_tac cs m (* fast but can't use wrappers *)
58.141 + blast_depth_tac ctxt m (* fast but can't use wrappers *)
58.142 ORELSE'
58.143 - (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
58.144 + (CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *)
58.145 in
58.146 - PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)) THEN
58.147 - TRY (Classical.safe_tac cs) THEN
58.148 + PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN
58.149 + TRY (Classical.safe_tac ctxt) THEN
58.150 REPEAT_DETERM (FIRSTGOAL main_tac) THEN
58.151 - TRY (Classical.safe_tac (cs addSss ss)) THEN
58.152 + TRY (Classical.safe_tac (addSss ctxt)) THEN
58.153 prune_params_tac
58.154 end;
58.155
58.156 -fun auto_tac css = mk_auto_tac css 4 2;
58.157 +fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
58.158
58.159
58.160 (* force_tac *)
58.161
58.162 (* aimed to solve the given subgoal totally, using whatever tools possible *)
58.163 -fun force_tac (cs, ss) =
58.164 - let val cs' = cs addss ss in
58.165 +fun force_tac ctxt =
58.166 + let val ctxt' = addss ctxt in
58.167 SELECT_GOAL
58.168 - (Classical.clarify_tac cs' 1 THEN
58.169 - IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1) THEN
58.170 - ALLGOALS (Classical.first_best_tac cs'))
58.171 + (Classical.clarify_tac ctxt' 1 THEN
58.172 + IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN
58.173 + ALLGOALS (Classical.first_best_tac ctxt'))
58.174 end;
58.175
58.176
58.177 (* basic combinations *)
58.178
58.179 -fun ADDSS tac (cs, ss) = let val cs' = cs addss ss in tac cs' end;
58.180 -
58.181 -val fast_simp_tac = ADDSS Classical.fast_tac;
58.182 -val slow_simp_tac = ADDSS Classical.slow_tac;
58.183 -val best_simp_tac = ADDSS Classical.best_tac;
58.184 +val fast_simp_tac = Classical.fast_tac o addss;
58.185 +val slow_simp_tac = Classical.slow_tac o addss;
58.186 +val best_simp_tac = Classical.best_tac o addss;
58.187
58.188
58.189
58.190 @@ -226,21 +208,14 @@
58.191
58.192 (* methods *)
58.193
58.194 -fun clasimp_meth tac ctxt = METHOD (fn facts =>
58.195 - ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt));
58.196 -
58.197 -fun clasimp_meth' tac ctxt = METHOD (fn facts =>
58.198 - HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt)));
58.199 -
58.200 -
58.201 fun clasimp_method' tac =
58.202 - Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
58.203 + Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
58.204
58.205 val auto_method =
58.206 Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
58.207 Method.sections clasimp_modifiers >>
58.208 - (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
58.209 - | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
58.210 + (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
58.211 + | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
58.212
58.213
58.214 (* theory setup *)
59.1 --- a/src/Provers/classical.ML Fri May 13 16:03:03 2011 +0200
59.2 +++ b/src/Provers/classical.ML Fri May 13 22:55:00 2011 +0200
59.3 @@ -37,30 +37,29 @@
59.4 sig
59.5 type claset
59.6 val empty_cs: claset
59.7 - val print_cs: Proof.context -> claset -> unit
59.8 val rep_cs: claset ->
59.9 {safeIs: thm list,
59.10 safeEs: thm list,
59.11 hazIs: thm list,
59.12 hazEs: thm list,
59.13 - swrappers: (string * wrapper) list,
59.14 - uwrappers: (string * wrapper) list,
59.15 + swrappers: (string * (Proof.context -> wrapper)) list,
59.16 + uwrappers: (string * (Proof.context -> wrapper)) list,
59.17 safe0_netpair: netpair,
59.18 safep_netpair: netpair,
59.19 haz_netpair: netpair,
59.20 dup_netpair: netpair,
59.21 xtra_netpair: Context_Rules.netpair}
59.22 - val merge_cs: claset * claset -> claset
59.23 - val addDs: claset * thm list -> claset
59.24 - val addEs: claset * thm list -> claset
59.25 - val addIs: claset * thm list -> claset
59.26 - val addSDs: claset * thm list -> claset
59.27 - val addSEs: claset * thm list -> claset
59.28 - val addSIs: claset * thm list -> claset
59.29 - val delrules: claset * thm list -> claset
59.30 - val addSWrapper: claset * (string * wrapper) -> claset
59.31 + val print_claset: Proof.context -> unit
59.32 + val addDs: Proof.context * thm list -> Proof.context
59.33 + val addEs: Proof.context * thm list -> Proof.context
59.34 + val addIs: Proof.context * thm list -> Proof.context
59.35 + val addSDs: Proof.context * thm list -> Proof.context
59.36 + val addSEs: Proof.context * thm list -> Proof.context
59.37 + val addSIs: Proof.context * thm list -> Proof.context
59.38 + val delrules: Proof.context * thm list -> Proof.context
59.39 + val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
59.40 val delSWrapper: claset * string -> claset
59.41 - val addWrapper: claset * (string * wrapper) -> claset
59.42 + val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
59.43 val delWrapper: claset * string -> claset
59.44 val addSbefore: claset * (string * (int -> tactic)) -> claset
59.45 val addSafter: claset * (string * (int -> tactic)) -> claset
59.46 @@ -70,54 +69,50 @@
59.47 val addE2: claset * (string * thm) -> claset
59.48 val addSD2: claset * (string * thm) -> claset
59.49 val addSE2: claset * (string * thm) -> claset
59.50 - val appSWrappers: claset -> wrapper
59.51 - val appWrappers: claset -> wrapper
59.52 + val appSWrappers: Proof.context -> wrapper
59.53 + val appWrappers: Proof.context -> wrapper
59.54
59.55 val global_claset_of: theory -> claset
59.56 val claset_of: Proof.context -> claset
59.57 + val map_claset: (claset -> claset) -> Proof.context -> Proof.context
59.58 + val put_claset: claset -> Proof.context -> Proof.context
59.59
59.60 - val fast_tac: claset -> int -> tactic
59.61 - val slow_tac: claset -> int -> tactic
59.62 - val astar_tac: claset -> int -> tactic
59.63 - val slow_astar_tac: claset -> int -> tactic
59.64 - val best_tac: claset -> int -> tactic
59.65 - val first_best_tac: claset -> int -> tactic
59.66 - val slow_best_tac: claset -> int -> tactic
59.67 - val depth_tac: claset -> int -> int -> tactic
59.68 - val deepen_tac: claset -> int -> int -> tactic
59.69 + val fast_tac: Proof.context -> int -> tactic
59.70 + val slow_tac: Proof.context -> int -> tactic
59.71 + val astar_tac: Proof.context -> int -> tactic
59.72 + val slow_astar_tac: Proof.context -> int -> tactic
59.73 + val best_tac: Proof.context -> int -> tactic
59.74 + val first_best_tac: Proof.context -> int -> tactic
59.75 + val slow_best_tac: Proof.context -> int -> tactic
59.76 + val depth_tac: Proof.context -> int -> int -> tactic
59.77 + val deepen_tac: Proof.context -> int -> int -> tactic
59.78
59.79 val contr_tac: int -> tactic
59.80 val dup_elim: thm -> thm
59.81 val dup_intr: thm -> thm
59.82 - val dup_step_tac: claset -> int -> tactic
59.83 + val dup_step_tac: Proof.context -> int -> tactic
59.84 val eq_mp_tac: int -> tactic
59.85 - val haz_step_tac: claset -> int -> tactic
59.86 + val haz_step_tac: Proof.context -> int -> tactic
59.87 val joinrules: thm list * thm list -> (bool * thm) list
59.88 val mp_tac: int -> tactic
59.89 - val safe_tac: claset -> tactic
59.90 - val safe_steps_tac: claset -> int -> tactic
59.91 - val safe_step_tac: claset -> int -> tactic
59.92 - val clarify_tac: claset -> int -> tactic
59.93 - val clarify_step_tac: claset -> int -> tactic
59.94 - val step_tac: claset -> int -> tactic
59.95 - val slow_step_tac: claset -> int -> tactic
59.96 + val safe_tac: Proof.context -> tactic
59.97 + val safe_steps_tac: Proof.context -> int -> tactic
59.98 + val safe_step_tac: Proof.context -> int -> tactic
59.99 + val clarify_tac: Proof.context -> int -> tactic
59.100 + val clarify_step_tac: Proof.context -> int -> tactic
59.101 + val step_tac: Proof.context -> int -> tactic
59.102 + val slow_step_tac: Proof.context -> int -> tactic
59.103 val swapify: thm list -> thm list
59.104 val swap_res_tac: thm list -> int -> tactic
59.105 - val inst_step_tac: claset -> int -> tactic
59.106 - val inst0_step_tac: claset -> int -> tactic
59.107 - val instp_step_tac: claset -> int -> tactic
59.108 + val inst_step_tac: Proof.context -> int -> tactic
59.109 + val inst0_step_tac: Proof.context -> int -> tactic
59.110 + val instp_step_tac: Proof.context -> int -> tactic
59.111 end;
59.112
59.113 signature CLASSICAL =
59.114 sig
59.115 include BASIC_CLASSICAL
59.116 val classical_rule: thm -> thm
59.117 - val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
59.118 - val del_context_safe_wrapper: string -> theory -> theory
59.119 - val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
59.120 - val del_context_unsafe_wrapper: string -> theory -> theory
59.121 - val get_claset: Proof.context -> claset
59.122 - val put_claset: claset -> Proof.context -> Proof.context
59.123 val get_cs: Context.generic -> claset
59.124 val map_cs: (claset -> claset) -> Context.generic -> Context.generic
59.125 val safe_dest: int option -> attribute
59.126 @@ -128,10 +123,10 @@
59.127 val haz_intro: int option -> attribute
59.128 val rule_del: attribute
59.129 val cla_modifiers: Method.modifier parser list
59.130 - val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
59.131 - val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
59.132 - val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
59.133 - val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
59.134 + val cla_method:
59.135 + (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
59.136 + val cla_method':
59.137 + (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
59.138 val setup: theory -> theory
59.139 end;
59.140
59.141 @@ -208,7 +203,7 @@
59.142 (*Duplication of hazardous rules, for complete provers*)
59.143 fun dup_intr th = zero_var_indexes (th RS Data.classical);
59.144
59.145 -fun dup_elim th =
59.146 +fun dup_elim th = (* FIXME proper context!? *)
59.147 let
59.148 val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
59.149 val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
59.150 @@ -218,17 +213,18 @@
59.151 (**** Classical rule sets ****)
59.152
59.153 datatype claset =
59.154 - CS of {safeIs : thm list, (*safe introduction rules*)
59.155 - safeEs : thm list, (*safe elimination rules*)
59.156 - hazIs : thm list, (*unsafe introduction rules*)
59.157 - hazEs : thm list, (*unsafe elimination rules*)
59.158 - swrappers : (string * wrapper) list, (*for transforming safe_step_tac*)
59.159 - uwrappers : (string * wrapper) list, (*for transforming step_tac*)
59.160 - safe0_netpair : netpair, (*nets for trivial cases*)
59.161 - safep_netpair : netpair, (*nets for >0 subgoals*)
59.162 - haz_netpair : netpair, (*nets for unsafe rules*)
59.163 - dup_netpair : netpair, (*nets for duplication*)
59.164 - xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
59.165 + CS of
59.166 + {safeIs : thm list, (*safe introduction rules*)
59.167 + safeEs : thm list, (*safe elimination rules*)
59.168 + hazIs : thm list, (*unsafe introduction rules*)
59.169 + hazEs : thm list, (*unsafe elimination rules*)
59.170 + swrappers : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*)
59.171 + uwrappers : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*)
59.172 + safe0_netpair : netpair, (*nets for trivial cases*)
59.173 + safep_netpair : netpair, (*nets for >0 subgoals*)
59.174 + haz_netpair : netpair, (*nets for unsafe rules*)
59.175 + dup_netpair : netpair, (*nets for duplication*)
59.176 + xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
59.177
59.178 (*Desired invariants are
59.179 safe0_netpair = build safe0_brls,
59.180 @@ -247,34 +243,21 @@
59.181 val empty_netpair = (Net.empty, Net.empty);
59.182
59.183 val empty_cs =
59.184 - CS{safeIs = [],
59.185 - safeEs = [],
59.186 - hazIs = [],
59.187 - hazEs = [],
59.188 - swrappers = [],
59.189 - uwrappers = [],
59.190 - safe0_netpair = empty_netpair,
59.191 - safep_netpair = empty_netpair,
59.192 - haz_netpair = empty_netpair,
59.193 - dup_netpair = empty_netpair,
59.194 - xtra_netpair = empty_netpair};
59.195 -
59.196 -fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
59.197 - let val pretty_thms = map (Display.pretty_thm ctxt) in
59.198 - [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
59.199 - Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
59.200 - Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
59.201 - Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
59.202 - Pretty.strs ("safe wrappers:" :: map #1 swrappers),
59.203 - Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
59.204 - |> Pretty.chunks |> Pretty.writeln
59.205 - end;
59.206 + CS
59.207 + {safeIs = [],
59.208 + safeEs = [],
59.209 + hazIs = [],
59.210 + hazEs = [],
59.211 + swrappers = [],
59.212 + uwrappers = [],
59.213 + safe0_netpair = empty_netpair,
59.214 + safep_netpair = empty_netpair,
59.215 + haz_netpair = empty_netpair,
59.216 + dup_netpair = empty_netpair,
59.217 + xtra_netpair = empty_netpair};
59.218
59.219 fun rep_cs (CS args) = args;
59.220
59.221 -fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
59.222 -fun appWrappers (CS {uwrappers, ...}) = fold snd uwrappers;
59.223 -
59.224
59.225 (*** Adding (un)safe introduction or elimination rules.
59.226
59.227 @@ -314,22 +297,31 @@
59.228 val mem_thm = member Thm.eq_thm_prop
59.229 and rem_thm = remove Thm.eq_thm_prop;
59.230
59.231 -fun warn msg rules th =
59.232 - mem_thm rules th andalso (warning (msg ^ Display.string_of_thm_without_context th); true);
59.233 +fun string_of_thm NONE = Display.string_of_thm_without_context
59.234 + | string_of_thm (SOME context) =
59.235 + Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
59.236
59.237 -fun warn_other th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
59.238 - warn "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
59.239 - warn "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
59.240 - warn "Rule already declared as introduction (intro)\n" hazIs th orelse
59.241 - warn "Rule already declared as elimination (elim)\n" hazEs th;
59.242 +fun make_elim context th =
59.243 + if has_fewer_prems 1 th then
59.244 + error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
59.245 + else Tactic.make_elim th;
59.246 +
59.247 +fun warn context msg rules th =
59.248 + mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true);
59.249 +
59.250 +fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
59.251 + warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
59.252 + warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
59.253 + warn context "Rule already declared as introduction (intro)\n" hazIs th orelse
59.254 + warn context "Rule already declared as elimination (elim)\n" hazEs th;
59.255
59.256
59.257 (*** Safe rules ***)
59.258
59.259 -fun addSI w th
59.260 +fun addSI w context th
59.261 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.262 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
59.263 - if warn "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
59.264 + if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
59.265 else
59.266 let
59.267 val th' = flat_rule th;
59.268 @@ -337,7 +329,7 @@
59.269 List.partition Thm.no_prems [th'];
59.270 val nI = length safeIs + 1;
59.271 val nE = length safeEs;
59.272 - val _ = warn_other th cs;
59.273 + val _ = warn_other context th cs;
59.274 in
59.275 CS
59.276 {safeIs = th::safeIs,
59.277 @@ -353,12 +345,12 @@
59.278 xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
59.279 end;
59.280
59.281 -fun addSE w th
59.282 +fun addSE w context th
59.283 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.284 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
59.285 - if warn "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
59.286 + if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
59.287 else if has_fewer_prems 1 th then
59.288 - error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
59.289 + error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
59.290 else
59.291 let
59.292 val th' = classical_rule (flat_rule th);
59.293 @@ -366,7 +358,7 @@
59.294 List.partition (fn rl => nprems_of rl=1) [th'];
59.295 val nI = length safeIs;
59.296 val nE = length safeEs + 1;
59.297 - val _ = warn_other th cs;
59.298 + val _ = warn_other context th cs;
59.299 in
59.300 CS
59.301 {safeEs = th::safeEs,
59.302 @@ -382,19 +374,21 @@
59.303 xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
59.304 end;
59.305
59.306 +fun addSD w context th = addSE w context (make_elim context th);
59.307 +
59.308
59.309 (*** Hazardous (unsafe) rules ***)
59.310
59.311 -fun addI w th
59.312 +fun addI w context th
59.313 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.314 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
59.315 - if warn "Ignoring duplicate introduction (intro)\n" hazIs th then cs
59.316 + if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
59.317 else
59.318 let
59.319 val th' = flat_rule th;
59.320 val nI = length hazIs + 1;
59.321 val nE = length hazEs;
59.322 - val _ = warn_other th cs;
59.323 + val _ = warn_other context th cs;
59.324 in
59.325 CS
59.326 {hazIs = th :: hazIs,
59.327 @@ -410,20 +404,20 @@
59.328 xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair}
59.329 end
59.330 handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *)
59.331 - error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
59.332 + error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
59.333
59.334 -fun addE w th
59.335 +fun addE w context th
59.336 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.337 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
59.338 - if warn "Ignoring duplicate elimination (elim)\n" hazEs th then cs
59.339 + if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
59.340 else if has_fewer_prems 1 th then
59.341 - error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
59.342 + error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
59.343 else
59.344 let
59.345 val th' = classical_rule (flat_rule th);
59.346 val nI = length hazIs;
59.347 val nE = length hazEs + 1;
59.348 - val _ = warn_other th cs;
59.349 + val _ = warn_other context th cs;
59.350 in
59.351 CS
59.352 {hazEs = th :: hazEs,
59.353 @@ -439,6 +433,8 @@
59.354 xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair}
59.355 end;
59.356
59.357 +fun addD w context th = addE w context (make_elim context th);
59.358 +
59.359
59.360
59.361 (*** Deletion of rules
59.362 @@ -492,7 +488,7 @@
59.363 end
59.364 else cs;
59.365
59.366 -fun delI th
59.367 +fun delI context th
59.368 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.369 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
59.370 if mem_thm hazIs th then
59.371 @@ -512,7 +508,7 @@
59.372 end
59.373 else cs
59.374 handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *)
59.375 - error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
59.376 + error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
59.377
59.378 fun delE th
59.379 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.380 @@ -535,32 +531,21 @@
59.381 else cs;
59.382
59.383 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
59.384 -fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
59.385 - let val th' = Tactic.make_elim th (* FIXME classical make_elim!? *) in
59.386 +fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
59.387 + let val th' = Tactic.make_elim th in
59.388 if mem_thm safeIs th orelse mem_thm safeEs th orelse
59.389 mem_thm hazIs th orelse mem_thm hazEs th orelse
59.390 mem_thm safeEs th' orelse mem_thm hazEs th'
59.391 - then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
59.392 - else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
59.393 + then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
59.394 + else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs)
59.395 end;
59.396
59.397 -fun cs delrules ths = fold delrule ths cs;
59.398
59.399
59.400 -fun make_elim th =
59.401 - if has_fewer_prems 1 th then
59.402 - error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
59.403 - else Tactic.make_elim th;
59.404 +(** claset data **)
59.405
59.406 -fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
59.407 -fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
59.408 -fun cs addSDs ths = cs addSEs (map make_elim ths);
59.409 -fun cs addIs ths = fold_rev (addI NONE) ths cs;
59.410 -fun cs addEs ths = fold_rev (addE NONE) ths cs;
59.411 -fun cs addDs ths = cs addEs (map make_elim ths);
59.412 +(* wrappers *)
59.413
59.414 -
59.415 -(*** Modifying the wrapper tacticals ***)
59.416 fun map_swrappers f
59.417 (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.418 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
59.419 @@ -570,48 +555,15 @@
59.420 haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
59.421
59.422 fun map_uwrappers f
59.423 - (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.424 + (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
59.425 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
59.426 CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
59.427 swrappers = swrappers, uwrappers = f uwrappers,
59.428 safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
59.429 haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
59.430
59.431 -fun update_warn msg (p as (key : string, _)) xs =
59.432 - (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
59.433
59.434 -fun delete_warn msg (key : string) xs =
59.435 - if AList.defined (op =) xs key then AList.delete (op =) key xs
59.436 - else (warning msg; xs);
59.437 -
59.438 -(*Add/replace a safe wrapper*)
59.439 -fun cs addSWrapper new_swrapper = map_swrappers
59.440 - (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
59.441 -
59.442 -(*Add/replace an unsafe wrapper*)
59.443 -fun cs addWrapper new_uwrapper = map_uwrappers
59.444 - (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
59.445 -
59.446 -(*Remove a safe wrapper*)
59.447 -fun cs delSWrapper name = map_swrappers
59.448 - (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
59.449 -
59.450 -(*Remove an unsafe wrapper*)
59.451 -fun cs delWrapper name = map_uwrappers
59.452 - (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
59.453 -
59.454 -(* compose a safe tactic alternatively before/after safe_step_tac *)
59.455 -fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
59.456 -fun cs addSafter (name, tac2) = cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
59.457 -
59.458 -(*compose a tactic alternatively before/after the step tactic *)
59.459 -fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2);
59.460 -fun cs addafter (name, tac2) = cs addWrapper (name, fn tac1 => tac1 APPEND' tac2);
59.461 -
59.462 -fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
59.463 -fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
59.464 -fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
59.465 -fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
59.466 +(* merge_cs *)
59.467
59.468 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
59.469 Merging the term nets may look more efficient, but the rather delicate
59.470 @@ -626,29 +578,129 @@
59.471 val safeEs' = fold rem_thm safeEs safeEs2;
59.472 val hazIs' = fold rem_thm hazIs hazIs2;
59.473 val hazEs' = fold rem_thm hazEs hazEs2;
59.474 - val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs';
59.475 - val cs2 = map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
59.476 - val cs3 = map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
59.477 - in cs3 end;
59.478 + in
59.479 + cs
59.480 + |> fold_rev (addSI NONE NONE) safeIs'
59.481 + |> fold_rev (addSE NONE NONE) safeEs'
59.482 + |> fold_rev (addI NONE NONE) hazIs'
59.483 + |> fold_rev (addE NONE NONE) hazEs'
59.484 + |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
59.485 + |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers))
59.486 + end;
59.487 +
59.488 +
59.489 +(* data *)
59.490 +
59.491 +structure Claset = Generic_Data
59.492 +(
59.493 + type T = claset;
59.494 + val empty = empty_cs;
59.495 + val extend = I;
59.496 + val merge = merge_cs;
59.497 +);
59.498 +
59.499 +val global_claset_of = Claset.get o Context.Theory;
59.500 +val claset_of = Claset.get o Context.Proof;
59.501 +val rep_claset_of = rep_cs o claset_of;
59.502 +
59.503 +val get_cs = Claset.get;
59.504 +val map_cs = Claset.map;
59.505 +
59.506 +fun map_claset f = Context.proof_map (map_cs f);
59.507 +fun put_claset cs = map_claset (K cs);
59.508 +
59.509 +fun print_claset ctxt =
59.510 + let
59.511 + val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
59.512 + val pretty_thms = map (Display.pretty_thm ctxt);
59.513 + in
59.514 + [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
59.515 + Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
59.516 + Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
59.517 + Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
59.518 + Pretty.strs ("safe wrappers:" :: map #1 swrappers),
59.519 + Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
59.520 + |> Pretty.chunks |> Pretty.writeln
59.521 + end;
59.522 +
59.523 +
59.524 +(* old-style declarations *)
59.525 +
59.526 +fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt;
59.527 +
59.528 +val op addSIs = decl (addSI NONE);
59.529 +val op addSEs = decl (addSE NONE);
59.530 +val op addSDs = decl (addSD NONE);
59.531 +val op addIs = decl (addI NONE);
59.532 +val op addEs = decl (addE NONE);
59.533 +val op addDs = decl (addD NONE);
59.534 +val op delrules = decl delrule;
59.535 +
59.536 +
59.537 +
59.538 +(*** Modifying the wrapper tacticals ***)
59.539 +
59.540 +fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt));
59.541 +fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt));
59.542 +
59.543 +fun update_warn msg (p as (key : string, _)) xs =
59.544 + (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
59.545 +
59.546 +fun delete_warn msg (key : string) xs =
59.547 + if AList.defined (op =) xs key then AList.delete (op =) key xs
59.548 + else (warning msg; xs);
59.549 +
59.550 +(*Add/replace a safe wrapper*)
59.551 +fun cs addSWrapper new_swrapper =
59.552 + map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
59.553 +
59.554 +(*Add/replace an unsafe wrapper*)
59.555 +fun cs addWrapper new_uwrapper =
59.556 + map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
59.557 +
59.558 +(*Remove a safe wrapper*)
59.559 +fun cs delSWrapper name =
59.560 + map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
59.561 +
59.562 +(*Remove an unsafe wrapper*)
59.563 +fun cs delWrapper name =
59.564 + map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
59.565 +
59.566 +(* compose a safe tactic alternatively before/after safe_step_tac *)
59.567 +fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
59.568 +fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
59.569 +
59.570 +(*compose a tactic alternatively before/after the step tactic *)
59.571 +fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
59.572 +fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
59.573 +
59.574 +fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
59.575 +fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
59.576 +fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
59.577 +fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
59.578 +
59.579
59.580
59.581 (**** Simple tactics for theorem proving ****)
59.582
59.583 (*Attack subgoals using safe inferences -- matching, not resolution*)
59.584 -fun safe_step_tac (cs as CS {safe0_netpair, safep_netpair, ...}) =
59.585 - appSWrappers cs (FIRST' [
59.586 - eq_assume_tac,
59.587 +fun safe_step_tac ctxt =
59.588 + let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
59.589 + appSWrappers ctxt
59.590 + (FIRST'
59.591 + [eq_assume_tac,
59.592 eq_mp_tac,
59.593 bimatch_from_nets_tac safe0_netpair,
59.594 FIRST' Data.hyp_subst_tacs,
59.595 - bimatch_from_nets_tac safep_netpair]);
59.596 + bimatch_from_nets_tac safep_netpair])
59.597 + end;
59.598
59.599 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
59.600 -fun safe_steps_tac cs =
59.601 - REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
59.602 +fun safe_steps_tac ctxt =
59.603 + REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i));
59.604
59.605 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
59.606 -fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
59.607 +fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt));
59.608
59.609
59.610 (*** Clarify_tac: do safe steps without causing branching ***)
59.611 @@ -669,86 +721,89 @@
59.612 (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
59.613
59.614 (*Attack subgoals using safe inferences -- matching, not resolution*)
59.615 -fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
59.616 - appSWrappers cs (FIRST' [
59.617 - eq_assume_contr_tac,
59.618 +fun clarify_step_tac ctxt =
59.619 + let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
59.620 + appSWrappers ctxt
59.621 + (FIRST'
59.622 + [eq_assume_contr_tac,
59.623 bimatch_from_nets_tac safe0_netpair,
59.624 FIRST' Data.hyp_subst_tacs,
59.625 n_bimatch_from_nets_tac 1 safep_netpair,
59.626 - bimatch2_tac safep_netpair]);
59.627 + bimatch2_tac safep_netpair])
59.628 + end;
59.629
59.630 -fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
59.631 +fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
59.632
59.633
59.634 (*** Unsafe steps instantiate variables or lose information ***)
59.635
59.636 (*Backtracking is allowed among the various these unsafe ways of
59.637 proving a subgoal. *)
59.638 -fun inst0_step_tac (CS {safe0_netpair, ...}) =
59.639 +fun inst0_step_tac ctxt =
59.640 assume_tac APPEND'
59.641 contr_tac APPEND'
59.642 - biresolve_from_nets_tac safe0_netpair;
59.643 + biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
59.644
59.645 (*These unsafe steps could generate more subgoals.*)
59.646 -fun instp_step_tac (CS {safep_netpair, ...}) =
59.647 - biresolve_from_nets_tac safep_netpair;
59.648 +fun instp_step_tac ctxt =
59.649 + biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
59.650
59.651 (*These steps could instantiate variables and are therefore unsafe.*)
59.652 -fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
59.653 +fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
59.654
59.655 -fun haz_step_tac (CS{haz_netpair,...}) =
59.656 - biresolve_from_nets_tac haz_netpair;
59.657 +fun haz_step_tac ctxt =
59.658 + biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
59.659
59.660 (*Single step for the prover. FAILS unless it makes progress. *)
59.661 -fun step_tac cs i =
59.662 - safe_tac cs ORELSE appWrappers cs (inst_step_tac cs ORELSE' haz_step_tac cs) i;
59.663 +fun step_tac ctxt i =
59.664 + safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i;
59.665
59.666 (*Using a "safe" rule to instantiate variables is unsafe. This tactic
59.667 allows backtracking from "safe" rules to "unsafe" rules here.*)
59.668 -fun slow_step_tac cs i =
59.669 - safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i;
59.670 +fun slow_step_tac ctxt i =
59.671 + safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i;
59.672
59.673
59.674 (**** The following tactics all fail unless they solve one goal ****)
59.675
59.676 (*Dumb but fast*)
59.677 -fun fast_tac cs =
59.678 - Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
59.679 +fun fast_tac ctxt =
59.680 + Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
59.681
59.682 (*Slower but smarter than fast_tac*)
59.683 -fun best_tac cs =
59.684 +fun best_tac ctxt =
59.685 Object_Logic.atomize_prems_tac THEN'
59.686 - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac cs 1));
59.687 + SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
59.688
59.689 (*even a bit smarter than best_tac*)
59.690 -fun first_best_tac cs =
59.691 +fun first_best_tac ctxt =
59.692 Object_Logic.atomize_prems_tac THEN'
59.693 - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac cs)));
59.694 + SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
59.695
59.696 -fun slow_tac cs =
59.697 +fun slow_tac ctxt =
59.698 Object_Logic.atomize_prems_tac THEN'
59.699 - SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
59.700 + SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
59.701
59.702 -fun slow_best_tac cs =
59.703 +fun slow_best_tac ctxt =
59.704 Object_Logic.atomize_prems_tac THEN'
59.705 - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac cs 1));
59.706 + SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
59.707
59.708
59.709 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
59.710
59.711 val weight_ASTAR = 5;
59.712
59.713 -fun astar_tac cs =
59.714 +fun astar_tac ctxt =
59.715 Object_Logic.atomize_prems_tac THEN'
59.716 SELECT_GOAL
59.717 (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
59.718 - (step_tac cs 1));
59.719 + (step_tac ctxt 1));
59.720
59.721 -fun slow_astar_tac cs =
59.722 +fun slow_astar_tac ctxt =
59.723 Object_Logic.atomize_prems_tac THEN'
59.724 SELECT_GOAL
59.725 (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
59.726 - (slow_step_tac cs 1));
59.727 + (slow_step_tac ctxt 1));
59.728
59.729
59.730 (**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome
59.731 @@ -759,132 +814,44 @@
59.732 (*Non-deterministic! Could always expand the first unsafe connective.
59.733 That's hard to implement and did not perform better in experiments, due to
59.734 greater search depth required.*)
59.735 -fun dup_step_tac (CS {dup_netpair, ...}) =
59.736 - biresolve_from_nets_tac dup_netpair;
59.737 +fun dup_step_tac ctxt =
59.738 + biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
59.739
59.740 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
59.741 local
59.742 - fun slow_step_tac' cs = appWrappers cs (instp_step_tac cs APPEND' dup_step_tac cs);
59.743 + fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt);
59.744 in
59.745 - fun depth_tac cs m i state = SELECT_GOAL
59.746 - (safe_steps_tac cs 1 THEN_ELSE
59.747 - (DEPTH_SOLVE (depth_tac cs m 1),
59.748 - inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
59.749 - (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m - 1) 1)))) i state;
59.750 + fun depth_tac ctxt m i state = SELECT_GOAL
59.751 + (safe_steps_tac ctxt 1 THEN_ELSE
59.752 + (DEPTH_SOLVE (depth_tac ctxt m 1),
59.753 + inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
59.754 + (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state;
59.755 end;
59.756
59.757 (*Search, with depth bound m.
59.758 This is the "entry point", which does safe inferences first.*)
59.759 -fun safe_depth_tac cs m = SUBGOAL (fn (prem,i) =>
59.760 - let val deti =
59.761 - (*No Vars in the goal? No need to backtrack between goals.*)
59.762 - if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
59.763 +fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) =>
59.764 + let
59.765 + val deti = (*No Vars in the goal? No need to backtrack between goals.*)
59.766 + if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I;
59.767 in
59.768 - SELECT_GOAL (TRY (safe_tac cs) THEN DEPTH_SOLVE (deti (depth_tac cs m 1))) i
59.769 + SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i
59.770 end);
59.771
59.772 -fun deepen_tac cs = DEEPEN (2, 10) (safe_depth_tac cs);
59.773 -
59.774 -
59.775 -
59.776 -(** context dependent claset components **)
59.777 -
59.778 -datatype context_cs = ContextCS of
59.779 - {swrappers: (string * (Proof.context -> wrapper)) list,
59.780 - uwrappers: (string * (Proof.context -> wrapper)) list};
59.781 -
59.782 -fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
59.783 - let
59.784 - fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
59.785 - in
59.786 - cs
59.787 - |> fold_rev (add_wrapper (op addSWrapper)) swrappers
59.788 - |> fold_rev (add_wrapper (op addWrapper)) uwrappers
59.789 - end;
59.790 -
59.791 -fun make_context_cs (swrappers, uwrappers) =
59.792 - ContextCS {swrappers = swrappers, uwrappers = uwrappers};
59.793 -
59.794 -val empty_context_cs = make_context_cs ([], []);
59.795 -
59.796 -fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
59.797 - if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
59.798 - else
59.799 - let
59.800 - val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
59.801 - val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
59.802 - val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
59.803 - val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
59.804 - in make_context_cs (swrappers', uwrappers') end;
59.805 -
59.806 -
59.807 -
59.808 -(** claset data **)
59.809 -
59.810 -(* global clasets *)
59.811 -
59.812 -structure GlobalClaset = Theory_Data
59.813 -(
59.814 - type T = claset * context_cs;
59.815 - val empty = (empty_cs, empty_context_cs);
59.816 - val extend = I;
59.817 - fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
59.818 - (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
59.819 -);
59.820 -
59.821 -val get_global_claset = #1 o GlobalClaset.get;
59.822 -val map_global_claset = GlobalClaset.map o apfst;
59.823 -
59.824 -val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of;
59.825 -fun map_context_cs f = GlobalClaset.map (apsnd
59.826 - (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
59.827 -
59.828 -fun global_claset_of thy =
59.829 - let val (cs, ctxt_cs) = GlobalClaset.get thy
59.830 - in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end;
59.831 -
59.832 -
59.833 -(* context dependent components *)
59.834 -
59.835 -fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
59.836 -fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
59.837 -
59.838 -fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
59.839 -fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
59.840 -
59.841 -
59.842 -(* local clasets *)
59.843 -
59.844 -structure LocalClaset = Proof_Data
59.845 -(
59.846 - type T = claset;
59.847 - val init = get_global_claset;
59.848 -);
59.849 -
59.850 -val get_claset = LocalClaset.get;
59.851 -val put_claset = LocalClaset.put;
59.852 -
59.853 -fun claset_of ctxt =
59.854 - context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
59.855 -
59.856 -
59.857 -(* generic clasets *)
59.858 -
59.859 -val get_cs = Context.cases global_claset_of claset_of;
59.860 -fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
59.861 +fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt);
59.862
59.863
59.864 (* attributes *)
59.865
59.866 -fun attrib f = Thm.declaration_attribute (fn th =>
59.867 - Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
59.868 +fun attrib f =
59.869 + Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context);
59.870
59.871 -fun safe_dest w = attrib (addSE w o make_elim);
59.872 val safe_elim = attrib o addSE;
59.873 val safe_intro = attrib o addSI;
59.874 -fun haz_dest w = attrib (addE w o make_elim);
59.875 +val safe_dest = attrib o addSD;
59.876 val haz_elim = attrib o addE;
59.877 val haz_intro = attrib o addI;
59.878 +val haz_dest = attrib o addD;
59.879 val rule_del = attrib delrule o Context_Rules.rule_del;
59.880
59.881
59.882 @@ -916,7 +883,7 @@
59.883 fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
59.884 let
59.885 val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
59.886 - val CS {xtra_netpair, ...} = claset_of ctxt;
59.887 + val {xtra_netpair, ...} = rep_claset_of ctxt;
59.888 val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
59.889 val rules = rules1 @ rules2 @ rules3 @ rules4;
59.890 val ruleq = Drule.multi_resolves facts rules;
59.891 @@ -954,14 +921,8 @@
59.892 Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
59.893 Args.del -- Args.colon >> K (I, rule_del)];
59.894
59.895 -fun cla_meth tac ctxt = METHOD (fn facts =>
59.896 - ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
59.897 -
59.898 -fun cla_meth' tac ctxt = METHOD (fn facts =>
59.899 - HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
59.900 -
59.901 -fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
59.902 -fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
59.903 +fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
59.904 +fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
59.905
59.906
59.907
59.908 @@ -981,7 +942,7 @@
59.909 Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
59.910 Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
59.911 Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
59.912 - Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
59.913 + Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
59.914 "classical prover (iterative deepening)" #>
59.915 Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
59.916 "classical prover (apply safe rules)";
59.917 @@ -1002,6 +963,6 @@
59.918 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
59.919 Toplevel.keep (fn state =>
59.920 let val ctxt = Toplevel.context_of state
59.921 - in print_cs ctxt (claset_of ctxt) end)));
59.922 + in print_claset ctxt end)));
59.923
59.924 end;
60.1 --- a/src/Pure/simplifier.ML Fri May 13 16:03:03 2011 +0200
60.2 +++ b/src/Pure/simplifier.ML Fri May 13 22:55:00 2011 +0200
60.3 @@ -8,6 +8,7 @@
60.4 signature BASIC_SIMPLIFIER =
60.5 sig
60.6 include BASIC_RAW_SIMPLIFIER
60.7 + val map_simpset_local: (simpset -> simpset) -> Proof.context -> Proof.context
60.8 val change_simpset: (simpset -> simpset) -> unit
60.9 val global_simpset_of: theory -> simpset
60.10 val Addsimprocs: simproc list -> unit
60.11 @@ -136,7 +137,7 @@
60.12
60.13 (* global simpset *)
60.14
60.15 -fun map_simpset f = Context.theory_map (map_ss f);
60.16 +fun map_simpset f = Context.theory_map (map_ss f); (* FIXME global *)
60.17 fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
60.18 fun global_simpset_of thy =
60.19 Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
60.20 @@ -147,6 +148,7 @@
60.21
60.22 (* local simpset *)
60.23
60.24 +fun map_simpset_local f = Context.proof_map (map_ss f);
60.25 fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
60.26
60.27 val _ = ML_Antiquote.value "simpset"
61.1 --- a/src/ZF/Tools/datatype_package.ML Fri May 13 16:03:03 2011 +0200
61.2 +++ b/src/ZF/Tools/datatype_package.ML Fri May 13 22:55:00 2011 +0200
61.3 @@ -348,11 +348,14 @@
61.4 (*Typical theorems have the form ~con1=con2, con1=con2==>False,
61.5 con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
61.6 fun mk_free s =
61.7 - let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*)
61.8 - Goal.prove_global thy [] [] (Syntax.read_prop_global thy s)
61.9 + let
61.10 + val thy = theory_of_thm elim;
61.11 + val ctxt = Proof_Context.init_global thy;
61.12 + in
61.13 + Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
61.14 (fn _ => EVERY
61.15 [rewrite_goals_tac con_defs,
61.16 - fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])
61.17 + fast_tac (put_claset ZF_cs ctxt addSEs free_SEs @ Su.free_SEs) 1])
61.18 end;
61.19
61.20 val simps = case_eqns @ recursor_eqns;
62.1 --- a/src/ZF/UNITY/Constrains.thy Fri May 13 16:03:03 2011 +0200
62.2 +++ b/src/ZF/UNITY/Constrains.thy Fri May 13 22:55:00 2011 +0200
62.3 @@ -471,7 +471,7 @@
62.4 (*proves "co" properties when the program is specified*)
62.5
62.6 fun constrains_tac ctxt =
62.7 - let val css as (cs, ss) = clasimpset_of ctxt in
62.8 + let val ss = simpset_of ctxt in
62.9 SELECT_GOAL
62.10 (EVERY [REPEAT (Always_Int_tac 1),
62.11 REPEAT (etac @{thm Always_ConstrainsI} 1
62.12 @@ -481,20 +481,20 @@
62.13 rtac @{thm constrainsI} 1,
62.14 (* Three subgoals *)
62.15 rewrite_goal_tac [@{thm st_set_def}] 3,
62.16 - REPEAT (force_tac css 2),
62.17 + REPEAT (force_tac ctxt 2),
62.18 full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
62.19 - ALLGOALS (clarify_tac cs),
62.20 + ALLGOALS (clarify_tac ctxt),
62.21 REPEAT (FIRSTGOAL (etac @{thm disjE})),
62.22 - ALLGOALS (clarify_tac cs),
62.23 + ALLGOALS (clarify_tac ctxt),
62.24 REPEAT (FIRSTGOAL (etac @{thm disjE})),
62.25 - ALLGOALS (clarify_tac cs),
62.26 + ALLGOALS (clarify_tac ctxt),
62.27 ALLGOALS (asm_full_simp_tac ss),
62.28 - ALLGOALS (clarify_tac cs)])
62.29 + ALLGOALS (clarify_tac ctxt)])
62.30 end;
62.31
62.32 (*For proving invariants*)
62.33 -fun always_tac ctxt i =
62.34 - rtac @{thm AlwaysI} i THEN force_tac (clasimpset_of ctxt) i THEN constrains_tac ctxt i;
62.35 +fun always_tac ctxt i =
62.36 + rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
62.37 *}
62.38
62.39 setup Program_Defs.setup
63.1 --- a/src/ZF/UNITY/SubstAx.thy Fri May 13 16:03:03 2011 +0200
63.2 +++ b/src/ZF/UNITY/SubstAx.thy Fri May 13 22:55:00 2011 +0200
63.3 @@ -351,7 +351,7 @@
63.4 ML {*
63.5 (*proves "ensures/leadsTo" properties when the program is specified*)
63.6 fun ensures_tac ctxt sact =
63.7 - let val css as (cs, ss) = clasimpset_of ctxt in
63.8 + let val ss = simpset_of ctxt in
63.9 SELECT_GOAL
63.10 (EVERY [REPEAT (Always_Int_tac 1),
63.11 etac @{thm Always_LeadsTo_Basis} 1
63.12 @@ -364,14 +364,14 @@
63.13 (*simplify the command's domain*)
63.14 simp_tac (ss addsimps [@{thm domain_def}]) 3,
63.15 (* proving the domain part *)
63.16 - clarify_tac cs 3, dtac @{thm swap} 3, force_tac css 4,
63.17 - rtac @{thm ReplaceI} 3, force_tac css 3, force_tac css 4,
63.18 + clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4,
63.19 + rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,
63.20 asm_full_simp_tac ss 3, rtac @{thm conjI} 3, simp_tac ss 4,
63.21 REPEAT (rtac @{thm state_update_type} 3),
63.22 constrains_tac ctxt 1,
63.23 - ALLGOALS (clarify_tac cs),
63.24 + ALLGOALS (clarify_tac ctxt),
63.25 ALLGOALS (asm_full_simp_tac (ss addsimps [@{thm st_set_def}])),
63.26 - ALLGOALS (clarify_tac cs),
63.27 + ALLGOALS (clarify_tac ctxt),
63.28 ALLGOALS (asm_lr_simp_tac ss)])
63.29 end;
63.30 *}
64.1 --- a/src/ZF/equalities.thy Fri May 13 16:03:03 2011 +0200
64.2 +++ b/src/ZF/equalities.thy Fri May 13 22:55:00 2011 +0200
64.3 @@ -970,17 +970,14 @@
64.4 Un_upper1 Un_upper2 Int_lower1 Int_lower2
64.5
64.6 ML {*
64.7 -val subset_cs = @{claset}
64.8 +val subset_cs =
64.9 + claset_of (@{context}
64.10 delrules [@{thm subsetI}, @{thm subsetCE}]
64.11 addSIs @{thms subset_SIs}
64.12 addIs [@{thm Union_upper}, @{thm Inter_lower}]
64.13 - addSEs [@{thm cons_subsetE}];
64.14 -*}
64.15 -(*subset_cs is a claset for subset reasoning*)
64.16 + addSEs [@{thm cons_subsetE}]);
64.17
64.18 -ML
64.19 -{*
64.20 -val ZF_cs = @{claset} delrules [@{thm equalityI}];
64.21 +val ZF_cs = claset_of (@{context} delrules [@{thm equalityI}]);
64.22 *}
64.23
64.24 end
65.1 --- a/src/ZF/ex/CoUnit.thy Fri May 13 16:03:03 2011 +0200
65.2 +++ b/src/ZF/ex/CoUnit.thy Fri May 13 22:55:00 2011 +0200
65.3 @@ -76,11 +76,11 @@
65.4 "Ord(i) ==> \<forall>x y. x \<in> counit2 --> y \<in> counit2 --> x Int Vset(i) \<subseteq> y"
65.5 -- {* Lemma for proving finality. *}
65.6 apply (erule trans_induct)
65.7 - apply (tactic "safe_tac subset_cs")
65.8 + apply (tactic "safe_tac (put_claset subset_cs @{context})")
65.9 apply (erule counit2.cases)
65.10 apply (erule counit2.cases)
65.11 apply (unfold counit2.con_defs)
65.12 - apply (tactic {* fast_tac (subset_cs
65.13 + apply (tactic {* fast_tac (put_claset subset_cs @{context}
65.14 addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}]
65.15 addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1 *})
65.16 done
66.1 --- a/src/ZF/ex/LList.thy Fri May 13 16:03:03 2011 +0200
66.2 +++ b/src/ZF/ex/LList.thy Fri May 13 22:55:00 2011 +0200
66.3 @@ -113,7 +113,7 @@
66.4 apply (erule llist.cases)
66.5 apply (simp_all add: QInl_def QInr_def llist.con_defs)
66.6 (*LCons case: I simply can't get rid of the deepen_tac*)
66.7 -apply (tactic "deepen_tac (@{claset} addIs [@{thm Ord_trans}]
66.8 +apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
66.9 addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
66.10 done
66.11
66.12 @@ -216,7 +216,7 @@
66.13 apply (erule llist.cases, simp_all)
66.14 apply (simp_all add: QInl_def QInr_def llist.con_defs)
66.15 (*LCons case: I simply can't get rid of the deepen_tac*)
66.16 -apply (tactic "deepen_tac (@{claset} addIs [@{thm Ord_trans}]
66.17 +apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
66.18 addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
66.19 done
66.20