proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
--- a/NEWS Fri May 13 16:03:03 2011 +0200
+++ b/NEWS Fri May 13 22:55:00 2011 +0200
@@ -144,6 +144,14 @@
* Slightly more special eq_list/eq_set, with shortcut involving
pointer equality (assumes that eq relation is reflexive).
+* Classical tactics use proper Proof.context instead of historic types
+claset/clasimpset. Old-style declarations like addIs, addEs, addDs
+operate directly on Proof.context. Raw type claset retains its use as
+snapshot of the classical context, which can be recovered via
+(put_claset HOL_cs) etc. Type clasimpset has been discontinued.
+INCOMPATIBILITY, classical tactics and derived proof methods require
+proper Proof.context.
+
New in Isabelle2011 (January 2011)
--- a/doc-src/TutorialI/Protocol/Message.thy Fri May 13 16:03:03 2011 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Fri May 13 22:55:00 2011 +0200
@@ -840,31 +840,24 @@
eresolve_tac [asm_rl, @{thm synth.Inj}];
fun Fake_insert_simp_tac ss i =
- REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
fun atomic_spy_analz_tac ctxt =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- SELECT_GOAL
- (Fake_insert_simp_tac ss 1
- THEN
- IF_UNSOLVED (Blast.depth_tac
- (cs addIs [analz_insertI,
- impOfSubs analz_subset_parts]) 4 1))
- end;
+ SELECT_GOAL
+ (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
+ IF_UNSOLVED (Blast.depth_tac (ctxt addIs [analz_insertI, impOfSubs analz_subset_parts]) 4 1));
fun spy_analz_tac ctxt i =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- DETERM
- (SELECT_GOAL
- (EVERY
- [ (*push in occurrences of X...*)
- (REPEAT o CHANGED)
- (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
- (*...allowing further simplifications*)
- simp_tac ss 1,
- REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
- DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
- end;
+ DETERM
+ (SELECT_GOAL
+ (EVERY
+ [ (*push in occurrences of X...*)
+ (REPEAT o CHANGED)
+ (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+ DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
*}
text{*By default only @{text o_apply} is built-in. But in the presence of
--- a/src/CCL/Type.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/CCL/Type.thy Fri May 13 22:55:00 2011 +0200
@@ -132,7 +132,7 @@
REPEAT_SOME (eresolve_tac (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN
ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
- safe_tac (claset_of ctxt addSIs prems))
+ safe_tac (ctxt addSIs prems))
*}
method_setup ncanT = {*
@@ -397,8 +397,7 @@
ML {*
val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} =>
- (fast_tac (claset_of ctxt addIs
- (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1));
+ fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1);
*}
method_setup coinduct3 = {*
@@ -419,8 +418,8 @@
fun genIs_tac ctxt genXH gen_mono =
rtac (genXH RS @{thm iffD2}) THEN'
simp_tac (simpset_of ctxt) THEN'
- TRY o fast_tac (claset_of ctxt addIs
- [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
+ TRY o fast_tac
+ (ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
*}
method_setup genIs = {*
@@ -454,7 +453,7 @@
ML {*
fun POgen_tac ctxt (rla, rlb) i =
- SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN
+ SELECT_GOAL (safe_tac ctxt) i THEN
rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
(REPEAT (resolve_tac
(@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @
@@ -499,7 +498,7 @@
fun EQgen_tac ctxt rews i =
SELECT_GOAL
- (TRY (safe_tac (claset_of ctxt)) THEN
+ (TRY (safe_tac ctxt) THEN
resolve_tac ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN
ALLGOALS (simp_tac (simpset_of ctxt)) THEN
ALLGOALS EQgen_raw_tac) i
--- a/src/FOL/FOL.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/FOL/FOL.thy Fri May 13 22:55:00 2011 +0200
@@ -12,7 +12,6 @@
"~~/src/Provers/clasimp.ML"
"~~/src/Tools/induct.ML"
"~~/src/Tools/case_product.ML"
- ("cladata.ML")
("simpdata.ML")
begin
@@ -167,9 +166,36 @@
section {* Classical Reasoner *}
-use "cladata.ML"
+ML {*
+structure Cla = ClassicalFun
+(
+ val imp_elim = @{thm imp_elim}
+ val not_elim = @{thm notE}
+ val swap = @{thm swap}
+ val classical = @{thm classical}
+ val sizef = size_of_thm
+ val hyp_subst_tacs = [hyp_subst_tac]
+);
+
+ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
+
+structure Basic_Classical: BASIC_CLASSICAL = Cla;
+open Basic_Classical;
+*}
+
setup Cla.setup
-ML {* Context.>> (Cla.map_cs (K FOL_cs)) *}
+
+(*Propositional rules*)
+lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
+ and [elim!] = conjE disjE impCE FalseE iffCE
+ML {* val prop_cs = @{claset} *}
+
+(*Quantifier rules*)
+lemmas [intro!] = allI ex_ex1I
+ and [intro] = exI
+ and [elim!] = exE alt_ex1E
+ and [elim] = allE
+ML {* val FOL_cs = @{claset} *}
ML {*
structure Blast = Blast
--- a/src/FOL/IsaMakefile Fri May 13 16:03:03 2011 +0200
+++ b/src/FOL/IsaMakefile Fri May 13 22:55:00 2011 +0200
@@ -29,14 +29,13 @@
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
- $(SRC)/Tools/case_product.ML \
- $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
- $(SRC)/Tools/IsaPlanner/rw_tools.ML \
+ $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML \
+ $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
$(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \
- $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML cladata.ML \
+ $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \
document/root.tex fologic.ML hypsubstdata.ML intprover.ML \
simpdata.ML
@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
--- a/src/FOL/cladata.ML Fri May 13 16:03:03 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(* Title: FOL/cladata.ML
- Author: Tobias Nipkow
- Copyright 1996 University of Cambridge
-
-Setting up the classical reasoner.
-*)
-
-(*** Applying ClassicalFun to create a classical prover ***)
-structure Classical_Data =
-struct
- val imp_elim = @{thm imp_elim}
- val not_elim = @{thm notE}
- val swap = @{thm swap}
- val classical = @{thm classical}
- val sizef = size_of_thm
- val hyp_subst_tacs=[hyp_subst_tac]
-end;
-
-structure Cla = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
-
-ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
-
-
-(*Propositional rules*)
-val prop_cs = empty_cs
- addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI},
- @{thm notI}, @{thm iffI}]
- addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}];
-
-(*Quantifier rules*)
-val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
- addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
-
--- a/src/FOL/simpdata.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/FOL/simpdata.ML Fri May 13 22:55:00 2011 +0200
@@ -142,6 +142,3 @@
);
open Clasimp;
-ML_Antiquote.value "clasimpset"
- (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
-
--- a/src/HOL/Algebra/abstract/Ideal2.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Algebra/abstract/Ideal2.thy Fri May 13 22:55:00 2011 +0200
@@ -276,7 +276,7 @@
apply (unfold prime_def)
apply (rule conjI)
apply (rule_tac [2] conjI)
- apply (tactic "clarify_tac @{claset} 3")
+ apply (tactic "clarify_tac @{context} 3")
apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)
apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)
apply (simp add: ideal_of_2_structure)
--- a/src/HOL/Algebra/abstract/Ring2.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Fri May 13 22:55:00 2011 +0200
@@ -466,7 +466,7 @@
(* fields are integral domains *)
lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
- apply (tactic "step_tac @{claset} 1")
+ apply (tactic "step_tac @{context} 1")
apply (rule_tac a = " (a*b) * inverse b" in box_equals)
apply (rule_tac [3] refl)
prefer 2
--- a/src/HOL/Auth/Message.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Auth/Message.thy Fri May 13 22:55:00 2011 +0200
@@ -830,31 +830,26 @@
eresolve_tac [asm_rl, @{thm synth.Inj}];
fun Fake_insert_simp_tac ss i =
- REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
fun atomic_spy_analz_tac ctxt =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- SELECT_GOAL
- (Fake_insert_simp_tac ss 1
- THEN
- IF_UNSOLVED (Blast.depth_tac
- (cs addIs [@{thm analz_insertI},
- impOfSubs @{thm analz_subset_parts}]) 4 1))
- end;
+ SELECT_GOAL
+ (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
+ IF_UNSOLVED
+ (Blast.depth_tac
+ (ctxt addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1));
fun spy_analz_tac ctxt i =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- DETERM
- (SELECT_GOAL
- (EVERY
- [ (*push in occurrences of X...*)
- (REPEAT o CHANGED)
- (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
- (*...allowing further simplifications*)
- simp_tac ss 1,
- REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
- DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
- end;
+ DETERM
+ (SELECT_GOAL
+ (EVERY
+ [ (*push in occurrences of X...*)
+ (REPEAT o CHANGED)
+ (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+ DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
*}
text{*By default only @{text o_apply} is built-in. But in the presence of
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri May 13 22:55:00 2011 +0200
@@ -749,7 +749,7 @@
(*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN
(*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN
(*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
- (*Base*) (force_tac (clasimpset_of ctxt)) 1
+ (*Base*) (force_tac ctxt) 1
val analz_prepare_tac =
prepare_tac THEN
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri May 13 22:55:00 2011 +0200
@@ -748,7 +748,7 @@
fun prepare_tac ctxt =
(*SR_U8*) forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
- (*SR_U8*) clarify_tac (claset_of ctxt) 15 THEN
+ (*SR_U8*) clarify_tac ctxt 15 THEN
(*SR_U9*) forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN
(*SR_U11*) forward_tac [@{thm Outpts_A_Card_form_10}] 21
@@ -758,7 +758,7 @@
(*SR_U9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN
(*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN
(*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
- (*Base*) (force_tac (clasimpset_of ctxt)) 1
+ (*Base*) (force_tac ctxt) 1
fun analz_prepare_tac ctxt =
prepare_tac ctxt THEN
--- a/src/HOL/Bali/AxCompl.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Bali/AxCompl.thy Fri May 13 22:55:00 2011 +0200
@@ -1391,7 +1391,7 @@
using finU uA
apply -
apply (induct_tac "n")
-apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
+apply (tactic "ALLGOALS (clarsimp_tac @{context})")
apply (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *})
apply simp
apply (erule finite_imageI)
--- a/src/HOL/Bali/AxSem.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Bali/AxSem.thy Fri May 13 22:55:00 2011 +0200
@@ -661,7 +661,7 @@
lemma ax_thin [rule_format (no_asm)]:
"G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
apply (erule ax_derivs.induct)
-apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
+apply (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
apply (rule ax_derivs.empty)
apply (erule (1) ax_derivs.insert)
apply (fast intro: ax_derivs.asm)
@@ -692,7 +692,7 @@
(*42 subgoals*)
apply (tactic "ALLGOALS strip_tac")
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
- etac disjE, fast_tac (@{claset} addSIs @{thms ax_derivs.empty})]))*})
+ etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
apply (tactic "TRYALL hyp_subst_tac")
apply (simp, rule ax_derivs.empty)
apply (drule subset_insertD)
@@ -703,7 +703,7 @@
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
(*37 subgoals*)
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})
- THEN_ALL_NEW fast_tac @{claset}) *})
+ THEN_ALL_NEW fast_tac @{context}) *})
(*1 subgoal*)
apply (clarsimp simp add: subset_mtriples_iff)
apply (rule ax_derivs.Methd)
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Fri May 13 22:55:00 2011 +0200
@@ -152,12 +152,12 @@
lemma slen_fscons_eq_rev:
"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
apply (simp add: fscons_def2 slen_scons_eq_rev)
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
apply (erule contrapos_np)
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
done
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Fri May 13 22:55:00 2011 +0200
@@ -83,9 +83,9 @@
lemma last_ind_on_first:
"l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
apply simp
- apply (tactic {* auto_tac (@{claset},
+ apply (tactic {* auto_tac (map_simpset_local (fn _ =>
HOL_ss addsplits [@{thm list.split}]
- addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) *})
+ addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
done
text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Fri May 13 22:55:00 2011 +0200
@@ -604,10 +604,10 @@
ML {*
fun abstraction_tac ctxt =
- let val (cs, ss) = clasimpset_of ctxt in
- SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
- ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
- end
+ SELECT_GOAL (auto_tac
+ (ctxt addSIs @{thms weak_strength_lemmas}
+ |> map_simpset_local (fn ss =>
+ ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
*}
method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Fri May 13 22:55:00 2011 +0200
@@ -400,7 +400,7 @@
==> input_enabled (A||B)"
apply (unfold input_enabled_def)
apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac (global_claset_of @{theory Fun})")
+apply (tactic "safe_tac (Proof_Context.init_global @{theory Fun})")
apply (simp add: inp_is_act)
prefer 2
apply (simp add: inp_is_act)
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Fri May 13 22:55:00 2011 +0200
@@ -298,7 +298,7 @@
let val ss = simpset_of ctxt in
EVERY1[Seq_induct_tac ctxt sch defs,
asm_full_simp_tac ss,
- SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})),
+ SELECT_GOAL (safe_tac (Proof_Context.init_global @{theory Fun})),
Seq_case_simp_tac ctxt exA,
Seq_case_simp_tac ctxt exB,
asm_full_simp_tac ss,
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri May 13 22:55:00 2011 +0200
@@ -150,7 +150,7 @@
(Ps ~~ take_consts ~~ xs)
val goal = mk_trp (foldr1 mk_conj concls)
- fun tacf {prems, context} =
+ fun tacf {prems, context = ctxt} =
let
(* Prove stronger prems, without definedness side conditions *)
fun con_thm p (con, args) =
@@ -165,23 +165,23 @@
map arg_tac args @
[REPEAT (rtac impI 1), ALLGOALS simplify]
in
- Goal.prove context [] [] subgoal (K (EVERY tacs))
+ Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
end
fun eq_thms (p, cons) = map (con_thm p) cons
val conss = map #con_specs constr_infos
val prems' = maps eq_thms (Ps ~~ conss)
val tacs1 = [
- quant_tac context 1,
+ quant_tac ctxt 1,
simp_tac HOL_ss 1,
- InductTacs.induct_tac context [[SOME "n"]] 1,
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1,
simp_tac (take_ss addsimps prems) 1,
- TRY (safe_tac HOL_cs)]
+ TRY (safe_tac (put_claset HOL_cs ctxt))]
fun con_tac _ =
asm_simp_tac take_ss 1 THEN
(resolve_tac prems' THEN_ALL_NEW etac spec) 1
fun cases_tacs (cons, exhaust) =
- res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
+ res_inst_tac ctxt [(("y", 0), "x")] exhaust 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
map con_tac cons
val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
@@ -196,15 +196,15 @@
val concls = map (op $) (Ps ~~ xs)
val goal = mk_trp (foldr1 mk_conj concls)
val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps
- fun tacf {prems, context} =
+ fun tacf {prems, context = ctxt} =
let
fun finite_tac (take_induct, fin_ind) =
rtac take_induct 1 THEN
(if is_finite then all_tac else resolve_tac prems 1) THEN
(rtac fin_ind THEN_ALL_NEW solve_tac prems) 1
- val fin_inds = Project_Rule.projections context finite_ind
+ val fin_inds = Project_Rule.projections ctxt finite_ind
in
- TRY (safe_tac HOL_cs) THEN
+ TRY (safe_tac (put_claset HOL_cs ctxt)) THEN
EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
end
in Goal.prove_global thy [] (adms @ assms) goal tacf end
@@ -318,18 +318,18 @@
val goal =
mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)))
val rules = @{thm Rep_cfun_strict1} :: take_0_thms
- fun tacf {prems, context} =
+ fun tacf {prems, context = ctxt} =
let
val prem' = rewrite_rule [bisim_def_thm] (hd prems)
- val prems' = Project_Rule.projections context prem'
+ val prems' = Project_Rule.projections ctxt prem'
val dests = map (fn th => th RS spec RS spec RS mp) prems'
fun one_tac (dest, rews) =
- dtac dest 1 THEN safe_tac HOL_cs THEN
+ dtac dest 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN
ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews))
in
rtac @{thm nat.induct} 1 THEN
simp_tac (HOL_ss addsimps rules) 1 THEN
- safe_tac HOL_cs THEN
+ safe_tac (put_claset HOL_cs ctxt) THEN
EVERY (map one_tac (dests ~~ take_rews))
end
in
--- a/src/HOL/Hoare/hoare_tac.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Fri May 13 22:55:00 2011 +0200
@@ -78,7 +78,7 @@
val MsetT = fastype_of big_Collect;
fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
- val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1);
+ val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1);
in (vars, th) end;
end;
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 13 22:55:00 2011 +0200
@@ -774,13 +774,13 @@
--{* 32 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 20 subgoals left *}
-apply(tactic{* TRYALL (clarify_tac @{claset}) *})
+apply(tactic{* TRYALL (clarify_tac @{context}) *})
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (etac disjE) *})
apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{clasimpset}]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
done
subsubsection {* Interference freedom Mutator-Collector *}
@@ -794,7 +794,7 @@
apply(tactic {* TRYALL (interfree_aux_tac) *})
--{* 64 subgoals left *}
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
-apply(tactic{* TRYALL (clarify_tac @{claset}) *})
+apply(tactic{* TRYALL (clarify_tac @{context}) *})
--{* 4 subgoals left *}
apply force
apply(simp add:Append_to_free2)
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 13 22:55:00 2011 +0200
@@ -132,7 +132,7 @@
apply(simp_all add:mul_mutator_interfree)
apply(simp_all add: mul_mutator_defs)
apply(tactic {* TRYALL (interfree_aux_tac) *})
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply (simp_all add:nth_list_update)
done
@@ -1123,7 +1123,7 @@
interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
apply(erule_tac x=j in allE, force dest:Graph3)+
done
@@ -1132,7 +1132,7 @@
interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def mul_mutator_defs nth_list_update)
done
@@ -1140,7 +1140,7 @@
interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1
Graph12 nth_list_update)
done
@@ -1149,7 +1149,7 @@
interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply(simp_all add: mul_mutator_defs nth_list_update)
apply(simp add:Mul_AppendInv_def Append_to_free0)
done
@@ -1178,7 +1178,7 @@
--{* 24 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 14 subgoals left *}
-apply(tactic {* TRYALL (clarify_tac @{claset}) *})
+apply(tactic {* TRYALL (clarify_tac @{context}) *})
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (rtac conjI) *})
apply(tactic {* TRYALL (rtac impI) *})
@@ -1189,7 +1189,7 @@
--{* 72 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
--{* 28 subgoals left *}
apply(tactic {* TRYALL (etac conjE) *})
apply(tactic {* TRYALL (etac disjE) *})
@@ -1199,17 +1199,21 @@
apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
apply(simp_all add:Graph10)
--{* 47 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *})
--{* 41 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
+ force_tac (map_simpset_local (fn ss => ss addsimps
+ [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
--{* 31 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
--{* 29 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
--{* 25 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
+ force_tac (map_simpset_local (fn ss => ss addsimps
+ [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}]) @{context})]) *})
--{* 10 subgoals left *}
apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
done
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Fri May 13 22:55:00 2011 +0200
@@ -170,10 +170,10 @@
--{* 35 vc *}
apply simp_all
--{* 21 vc *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
--{* 11 vc *}
apply simp_all
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
--{* 10 subgoals left *}
apply(erule less_SucE)
apply simp
@@ -430,13 +430,13 @@
.{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
apply oghoare
--{* 138 vc *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
--{* 112 subgoals left *}
apply(simp_all (no_asm))
--{* 97 subgoals left *}
apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
--{* 930 subgoals left *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
--{* 99 subgoals left *}
apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym])
--{* 20 subgoals left *}
@@ -535,7 +535,7 @@
.{\<acute>x=n}."
apply oghoare
apply (simp_all cong del: strong_setsum_cong)
-apply (tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply (tactic {* ALLGOALS (clarify_tac @{context}) *})
apply (simp_all cong del: strong_setsum_cong)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
--- a/src/HOL/IMPP/Hoare.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/IMPP/Hoare.thy Fri May 13 22:55:00 2011 +0200
@@ -209,7 +209,7 @@
*)
lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
apply (erule hoare_derivs.induct)
-apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
+apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1]) *})
apply (rule hoare_derivs.empty)
apply (erule (1) hoare_derivs.insert)
apply (fast intro: hoare_derivs.asm)
@@ -218,7 +218,7 @@
apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
prefer 7
apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
-apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{claset})) *})
+apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *})
done
lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
@@ -287,10 +287,10 @@
apply (blast) (* weaken *)
apply (tactic {* ALLGOALS (EVERY'
[REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
- simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
+ simp_tac @{simpset}, clarify_tac @{context}, REPEAT o smp_tac 1]) *})
apply (simp_all (no_asm_use) add: triple_valid_def2)
apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
-apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *)
+apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *)
prefer 3 apply (force) (* Call *)
apply (erule_tac [2] evaln_elim_cases) (* If *)
apply blast+
@@ -335,17 +335,17 @@
lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>
!pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
apply (induct_tac c)
-apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
+apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *})
prefer 7 apply (fast intro: domI)
apply (erule_tac [6] MGT_alternD)
apply (unfold MGT_def)
apply (drule_tac [7] bspec, erule_tac [7] domI)
-apply (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 7 *},
+apply (rule_tac [7] escape, tactic {* clarsimp_tac @{context} 7 *},
rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
apply (erule_tac [!] thin_rl)
apply (rule hoare_derivs.Skip [THEN conseq2])
apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
-apply (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 3 *},
+apply (rule_tac [3] escape, tactic {* clarsimp_tac @{context} 3 *},
rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
erule_tac [3] conseq12)
apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
@@ -364,7 +364,7 @@
shows "finite U ==> uG = mgt_call`U ==>
!G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
apply (induct_tac n)
-apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
+apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *})
apply (subgoal_tac "G = mgt_call ` U")
prefer 2
apply (simp add: card_seteq)
--- a/src/HOL/MicroJava/J/Conform.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri May 13 22:55:00 2011 +0200
@@ -328,8 +328,9 @@
apply auto
apply(rule hconfI)
apply(drule conforms_heapD)
-apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}]
- addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
+apply(tactic {*
+ auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}]
+ |> map_simpset_local (fn ss => ss delsimps [@{thm split_paired_All}])) *})
done
lemma conforms_upd_local:
--- a/src/HOL/MicroJava/J/WellForm.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Fri May 13 22:55:00 2011 +0200
@@ -315,7 +315,7 @@
apply( clarify)
apply( frule fields_rec, assumption)
apply( fastsimp)
-apply( tactic "safe_tac HOL_cs")
+apply( tactic "safe_tac (put_claset HOL_cs @{context})")
apply( subst fields_rec)
apply( assumption)
apply( assumption)
--- a/src/HOL/Multivariate_Analysis/normarith.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Fri May 13 22:55:00 2011 +0200
@@ -384,7 +384,7 @@
end
fun norm_arith_tac ctxt =
- clarify_tac HOL_cs THEN'
+ clarify_tac (put_claset HOL_cs ctxt) THEN'
Object_Logic.full_atomize_tac THEN'
CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
--- a/src/HOL/NanoJava/AxSem.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Fri May 13 22:55:00 2011 +0200
@@ -151,7 +151,7 @@
"(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and>
(A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))"
apply (rule hoare_ehoare.induct)
-apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
+apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
apply (blast intro: hoare_ehoare.Skip)
apply (blast intro: hoare_ehoare.Comp)
apply (blast intro: hoare_ehoare.Cond)
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri May 13 22:55:00 2011 +0200
@@ -264,7 +264,7 @@
apply (simp add: zmult_assoc)
apply (rule_tac [5] zcong_zmult)
apply (rule_tac [5] inv_is_inv)
- apply (tactic "clarify_tac @{claset} 4")
+ apply (tactic "clarify_tac @{context} 4")
apply (subgoal_tac [4] "a \<in> wset (a - 1) p")
apply (rule_tac [5] wset_inv_mem_mem)
apply (simp_all add: wset_fin)
--- a/src/HOL/Prolog/Test.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Prolog/Test.thy Fri May 13 22:55:00 2011 +0200
@@ -234,9 +234,9 @@
(* disjunction in atom: *)
lemma "(!P. g P :- (P => b | a)) => g(a | b)"
- apply (tactic "step_tac HOL_cs 1")
- apply (tactic "step_tac HOL_cs 1")
- apply (tactic "step_tac HOL_cs 1")
+ apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
+ apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
+ apply (tactic "step_tac (put_claset HOL_cs @{context}) 1")
prefer 2
apply fast
apply fast
--- a/src/HOL/Proofs/Lambda/Commutation.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Proofs/Lambda/Commutation.thy Fri May 13 22:55:00 2011 +0200
@@ -127,9 +127,9 @@
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
apply (unfold square_def commute_def diamond_def Church_Rosser_def)
- apply (tactic {* safe_tac HOL_cs *})
+ apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
apply (tactic {*
- blast_tac (HOL_cs addIs
+ blast_tac (put_claset HOL_cs @{context} addIs
[@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
@{thm rtranclp_converseI}, @{thm conversepI},
@{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
--- a/src/HOL/SET_Protocol/Message_SET.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Fri May 13 22:55:00 2011 +0200
@@ -853,31 +853,26 @@
eresolve_tac [asm_rl, @{thm synth.Inj}];
fun Fake_insert_simp_tac ss i =
- REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
fun atomic_spy_analz_tac ctxt =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- SELECT_GOAL
- (Fake_insert_simp_tac ss 1
- THEN
- IF_UNSOLVED (Blast.depth_tac
- (cs addIs [@{thm analz_insertI},
- impOfSubs @{thm analz_subset_parts}]) 4 1))
- end;
+ SELECT_GOAL
+ (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
+ IF_UNSOLVED
+ (Blast.depth_tac (ctxt addIs [@{thm analz_insertI},
+ impOfSubs @{thm analz_subset_parts}]) 4 1));
fun spy_analz_tac ctxt i =
- let val ss = simpset_of ctxt and cs = claset_of ctxt in
- DETERM
- (SELECT_GOAL
- (EVERY
- [ (*push in occurrences of X...*)
- (REPEAT o CHANGED)
- (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
- (*...allowing further simplifications*)
- simp_tac ss 1,
- REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
- DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
- end;
+ DETERM
+ (SELECT_GOAL
+ (EVERY
+ [ (*push in occurrences of X...*)
+ (REPEAT o CHANGED)
+ (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+ DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
*}
(*>*)
--- a/src/HOL/TLA/Action.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/TLA/Action.thy Fri May 13 22:55:00 2011 +0200
@@ -278,7 +278,7 @@
*)
fun enabled_tac ctxt base_vars =
- clarsimp_tac (claset_of ctxt addSIs [base_vars RS @{thm base_enabled}], simpset_of ctxt);
+ clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]);
*}
method_setup enabled = {*
--- a/src/HOL/TLA/TLA.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/TLA/TLA.thy Fri May 13 22:55:00 2011 +0200
@@ -583,11 +583,13 @@
ML {*
(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
-fun inv_tac css = SELECT_GOAL
- (EVERY [auto_tac css,
- TRY (merge_box_tac 1),
- rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
- TRYALL (etac @{thm Stable})]);
+fun inv_tac ctxt =
+ SELECT_GOAL
+ (EVERY
+ [auto_tac ctxt,
+ TRY (merge_box_tac 1),
+ rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
+ TRYALL (etac @{thm Stable})]);
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals
in simple cases it may be able to handle goals like |- MyProg --> []Inv.
@@ -595,15 +597,15 @@
auto-tactic, which applies too much propositional logic and simplifies
too late.
*)
-fun auto_inv_tac ss = SELECT_GOAL
- ((inv_tac (@{claset}, ss) 1) THEN
- (TRYALL (action_simp_tac
- (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
+fun auto_inv_tac ss =
+ SELECT_GOAL
+ (inv_tac (map_simpset_local (K ss) @{context}) 1 THEN
+ (TRYALL (action_simp_tac
+ (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
*}
method_setup invariant = {*
- Method.sections Clasimp.clasimp_modifiers
- >> (K (SIMPLE_METHOD' o inv_tac o clasimpset_of))
+ Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
*} ""
method_setup auto_invariant = {*
--- a/src/HOL/Tools/Function/fun.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Function/fun.ML Fri May 13 22:55:00 2011 +0200
@@ -143,7 +143,7 @@
let
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1
- THEN auto_tac (clasimpset_of ctxt)
+ THEN auto_tac ctxt
fun prove_termination lthy =
Function.prove_termination NONE
(Function_Common.get_termination_prover lthy lthy) lthy
--- a/src/HOL/Tools/Function/function_core.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Fri May 13 22:55:00 2011 +0200
@@ -702,7 +702,7 @@
Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
|> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
- |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
+ |> (SINGLE (auto_tac ctxt)) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
--- a/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri May 13 22:55:00 2011 +0200
@@ -214,9 +214,10 @@
end
fun lexicographic_order_tac quiet ctxt =
- TRY (Function_Common.apply_termination_rule ctxt 1)
- THEN lex_order_tac quiet ctxt
- (auto_tac (claset_of ctxt, simpset_of ctxt addsimps Function_Common.Termination_Simps.get ctxt))
+ TRY (Function_Common.apply_termination_rule ctxt 1) THEN
+ lex_order_tac quiet ctxt
+ (auto_tac
+ (map_simpset_local (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 22:55:00 2011 +0200
@@ -338,7 +338,7 @@
fun decomp_scnp_tac orders ctxt =
let
val extra_simps = Function_Common.Termination_Simps.get ctxt
- val autom_tac = auto_tac (claset_of ctxt, simpset_of ctxt addsimps extra_simps)
+ val autom_tac = auto_tac (map_simpset_local (fn ss => ss addsimps extra_simps) ctxt)
in
gen_sizechange_tac orders autom_tac ctxt
end
--- a/src/HOL/Tools/Function/termination.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Function/termination.ML Fri May 13 22:55:00 2011 +0200
@@ -297,7 +297,7 @@
THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *)
ORELSE' ((rtac @{thm conjI})
THEN' (rtac @{thm refl})
- THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *)
+ THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *)
) i
in
((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
--- a/src/HOL/Tools/Meson/meson.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri May 13 22:55:00 2011 +0200
@@ -699,8 +699,7 @@
(*First, breaks the goal into independent units*)
fun safe_best_meson_tac ctxt =
- SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
- TRYALL (best_meson_tac size_of_subgoals ctxt));
+ SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt));
(** Depth-first search version **)
@@ -742,7 +741,7 @@
end));
fun meson_tac ctxt ths =
- SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
+ SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
(**** Code to support ordinary resolution, rather than Model Elimination ****)
--- a/src/HOL/Tools/Meson/meson_tactic.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_tactic.ML Fri May 13 22:55:00 2011 +0200
@@ -17,9 +17,8 @@
open Meson_Clausify
fun meson_general_tac ctxt ths =
- let val ctxt = Classical.put_claset HOL_cs ctxt in
- Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
- end
+ let val ctxt' = put_claset HOL_cs ctxt
+ in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false 0) ths) end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri May 13 22:55:00 2011 +0200
@@ -2004,9 +2004,8 @@
map (wf_constraint_for rel side concl) main |> foldr1 s_conj
fun terminates_by ctxt timeout goal tac =
- can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
- #> SINGLE (DETERM_TIMEOUT timeout
- (tac ctxt (auto_tac (clasimpset_of ctxt))))
+ can (SINGLE (Classical.safe_tac ctxt) #> the
+ #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt)))
#> the #> Goal.finish ctxt) goal
val max_cached_wfs = 50
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 13 22:55:00 2011 +0200
@@ -1050,8 +1050,7 @@
()
val goal = prop |> cterm_of thy |> Goal.init
in
- (goal |> SINGLE (DETERM_TIMEOUT auto_timeout
- (auto_tac (clasimpset_of ctxt)))
+ (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
|> the |> Goal.finish ctxt; true)
handle THM _ => false
| TimeLimit.TimeOut => false
--- a/src/HOL/Tools/Qelim/cooper.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri May 13 22:55:00 2011 +0200
@@ -706,7 +706,7 @@
val all_maxscope_ss =
HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
in
-fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
+fun thin_prems_tac ctxt P = simp_tac all_maxscope_ss THEN'
CSUBGOAL (fn (p', i) =>
let
val (qvs, p) = strip_objall (Thm.dest_arg p')
@@ -720,7 +720,7 @@
| _ => false)
in
if ntac then no_tac
- else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
+ else rtac (Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) i
end)
end;
@@ -843,7 +843,7 @@
THEN_ALL_NEW simp_tac ss
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
THEN_ALL_NEW Object_Logic.full_atomize_tac
- THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
+ THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
THEN_ALL_NEW Object_Logic.full_atomize_tac
THEN_ALL_NEW div_mod_tac ctxt
THEN_ALL_NEW splits_tac ctxt
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri May 13 22:55:00 2011 +0200
@@ -38,8 +38,7 @@
(* defining functions *)
fun pat_completeness_auto ctxt =
- Pat_Completeness.pat_completeness_tac ctxt 1
- THEN auto_tac (clasimpset_of ctxt)
+ Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
fun define_functions (mk_equations, termination_tac) prfx argnames names Ts =
if define_foundationally andalso is_some termination_tac then
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri May 13 22:55:00 2011 +0200
@@ -97,9 +97,14 @@
val rewr_if =
@{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
in
-val simp_fast_tac =
+
+fun HOL_fast_tac ctxt =
+ Classical.fast_tac (put_claset HOL_cs ctxt)
+
+fun simp_fast_tac ctxt =
Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
- THEN_ALL_NEW Classical.fast_tac HOL_cs
+ THEN_ALL_NEW HOL_fast_tac ctxt
+
end
@@ -300,7 +305,7 @@
(* distributivity of | over & *)
fun distributivity ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
(* FIXME: not very well tested *)
@@ -356,7 +361,7 @@
fun def_axiom ctxt = Thm o try_apply ctxt [] [
named ctxt "conj/disj/distinct" prove_def_axiom,
Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
- named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
+ named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
end
@@ -417,7 +422,7 @@
fun prove_nnf ctxt = try_apply ctxt [] [
named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
- named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
+ named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
in
fun nnf ctxt vars ps ct =
(case SMT_Utils.term_of ct of
@@ -552,13 +557,13 @@
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
fun pull_quant ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
(* FIXME: not very well tested *)
(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
fun push_quant ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
(* FIXME: not very well tested *)
@@ -582,7 +587,7 @@
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
(* FIXME: not very well tested *)
@@ -694,18 +699,18 @@
Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
- THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
+ THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
- NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
+ NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
Z3_Proof_Tools.by_tac (
NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
THEN_ALL_NEW (
- NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
+ NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))
--- a/src/HOL/Tools/TFL/post.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/TFL/post.ML Fri May 13 22:55:00 2011 +0200
@@ -40,7 +40,7 @@
terminator =
asm_simp_tac (simpset_of ctxt) 1
THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
- fast_tac (claset_of ctxt addSDs [@{thm not0_implies_Suc}] addss (simpset_of ctxt)) 1),
+ fast_simp_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
simplifier = Rules.simpl_conv (simpset_of ctxt) []};
--- a/src/HOL/Tools/groebner.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/groebner.ML Fri May 13 22:55:00 2011 +0200
@@ -1012,10 +1012,10 @@
THEN ring_tac add_ths del_ths ctxt 1
end
in
- clarify_tac @{claset} i
+ clarify_tac @{context} i
THEN Object_Logic.full_atomize_tac i
THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i
- THEN clarify_tac @{claset} i
+ THEN clarify_tac @{context} i
THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
THEN SUBPROOF poly_exists_tac ctxt i
end
--- a/src/HOL/Tools/record.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/record.ML Fri May 13 22:55:00 2011 +0200
@@ -44,7 +44,7 @@
val ex_sel_eq_simproc: simproc
val split_tac: int -> tactic
val split_simp_tac: thm list -> (term -> int) -> int -> tactic
- val split_wrapper: string * wrapper
+ val split_wrapper: string * (Proof.context -> wrapper)
val updateN: string
val ext_typeN: string
@@ -1508,7 +1508,7 @@
(* wrapper *)
val split_name = "record_split_tac";
-val split_wrapper = (split_name, fn tac => split_tac ORELSE' tac);
+val split_wrapper = (split_name, fn _ => fn tac => split_tac ORELSE' tac);
--- a/src/HOL/Tools/simpdata.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML Fri May 13 22:55:00 2011 +0200
@@ -163,9 +163,6 @@
);
open Clasimp;
-val _ = ML_Antiquote.value "clasimpset"
- (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
-
val mksimps_pairs =
[(@{const_name HOL.implies}, [@{thm mp}]),
(@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Fri May 13 22:55:00 2011 +0200
@@ -331,10 +331,15 @@
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
ML {*
fun record_auto_tac ctxt =
- auto_tac (claset_of ctxt addIs [ext] addSWrapper Record.split_wrapper,
- simpset_of ctxt addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
- @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
- @{thm o_apply}, @{thm Let_def}])
+ let val ctxt' =
+ (ctxt addIs [ext])
+ |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
+ |> map_simpset_local (fn ss => ss
+ addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
+ @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
+ @{thm o_apply}, @{thm Let_def}])
+ in auto_tac ctxt' end;
+
*}
method_setup record_auto = {*
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Fri May 13 22:55:00 2011 +0200
@@ -102,35 +102,25 @@
text{*This ML code does the inductions directly.*}
ML{*
fun ns_constrains_tac ctxt i =
- let
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
- in
- SELECT_GOAL
- (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1),
- REPEAT (resolve_tac [@{thm StableI}, @{thm stableI},
- @{thm constrains_imp_Constrains}] 1),
- rtac @{thm ns_constrainsI} 1,
- full_simp_tac ss 1,
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS (clarify_tac (cs delrules [impI, @{thm impCE}])),
- REPEAT (FIRSTGOAL analz_mono_contra_tac),
- ALLGOALS (asm_simp_tac ss)]) i
- end;
+ SELECT_GOAL
+ (EVERY
+ [REPEAT (etac @{thm Always_ConstrainsI} 1),
+ REPEAT (resolve_tac [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1),
+ rtac @{thm ns_constrainsI} 1,
+ full_simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])),
+ REPEAT (FIRSTGOAL analz_mono_contra_tac),
+ ALLGOALS (asm_simp_tac (simpset_of ctxt))]) i;
(*Tactic for proving secrecy theorems*)
fun ns_induct_tac ctxt =
- let
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
- in
- (SELECT_GOAL o EVERY)
- [rtac @{thm AlwaysI} 1,
- force_tac (cs,ss) 1,
- (*"reachable" gets in here*)
- rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
- ns_constrains_tac ctxt 1]
- end;
+ (SELECT_GOAL o EVERY)
+ [rtac @{thm AlwaysI} 1,
+ force_tac ctxt 1,
+ (*"reachable" gets in here*)
+ rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
+ ns_constrains_tac ctxt 1];
*}
method_setup ns_induct = {*
--- a/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 22:55:00 2011 +0200
@@ -14,51 +14,42 @@
(*Proves "co" properties when the program is specified. Any use of invariants
(from weak constrains) must have been done already.*)
fun constrains_tac ctxt i =
- let
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
- in
- SELECT_GOAL
- (EVERY [REPEAT (Always_Int_tac 1),
- (*reduce the fancy safety properties to "constrains"*)
- REPEAT (etac @{thm Always_ConstrainsI} 1
- ORELSE
- resolve_tac [@{thm StableI}, @{thm stableI},
- @{thm constrains_imp_Constrains}] 1),
- (*for safety, the totalize operator can be ignored*)
- simp_tac (HOL_ss addsimps
- [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
- rtac @{thm constrainsI} 1,
- full_simp_tac ss 1,
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS (clarify_tac cs),
- ALLGOALS (asm_full_simp_tac ss)]) i
- end;
+ SELECT_GOAL
+ (EVERY
+ [REPEAT (Always_Int_tac 1),
+ (*reduce the fancy safety properties to "constrains"*)
+ REPEAT (etac @{thm Always_ConstrainsI} 1
+ ORELSE
+ resolve_tac [@{thm StableI}, @{thm stableI},
+ @{thm constrains_imp_Constrains}] 1),
+ (*for safety, the totalize operator can be ignored*)
+ simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
+ rtac @{thm constrainsI} 1,
+ full_simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac ctxt),
+ ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac ctxt sact =
- let
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
- in
- SELECT_GOAL
- (EVERY [REPEAT (Always_Int_tac 1),
- etac @{thm Always_LeadsTo_Basis} 1
- ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
- @{thm EnsuresI}, @{thm ensuresI}] 1),
- (*now there are two subgoals: co & transient*)
- simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
- res_inst_tac (Simplifier.the_context ss)
- [(("act", 0), sact)] @{thm totalize_transientI} 2
- ORELSE res_inst_tac (Simplifier.the_context ss)
- [(("act", 0), sact)] @{thm transientI} 2,
- (*simplify the command's domain*)
- simp_tac (ss addsimps [@{thm Domain_def}]) 3,
- constrains_tac ctxt 1,
- ALLGOALS (clarify_tac cs),
- ALLGOALS (asm_lr_simp_tac ss)])
- end;
+ SELECT_GOAL
+ (EVERY
+ [REPEAT (Always_Int_tac 1),
+ etac @{thm Always_LeadsTo_Basis} 1
+ ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
+ REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
+ @{thm EnsuresI}, @{thm ensuresI}] 1),
+ (*now there are two subgoals: co & transient*)
+ simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
+ res_inst_tac ctxt
+ [(("act", 0), sact)] @{thm totalize_transientI} 2
+ ORELSE res_inst_tac ctxt
+ [(("act", 0), sact)] @{thm transientI} 2,
+ (*simplify the command's domain*)
+ simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
+ constrains_tac ctxt 1,
+ ALLGOALS (clarify_tac ctxt),
+ ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
(*Composition equivalences, from Lift_prog*)
--- a/src/HOL/Word/Word.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Word/Word.thy Fri May 13 22:55:00 2011 +0200
@@ -1475,11 +1475,9 @@
fun arith_tac' n t =
Arith_Data.verbose_arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty;
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
in
- [ clarify_tac cs 1,
- full_simp_tac (uint_arith_ss_of ss) 1,
+ [ clarify_tac ctxt 1,
+ full_simp_tac (uint_arith_ss_of (simpset_of ctxt)) 1,
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits}
addcongs @{thms power_False_cong})),
rewrite_goals_tac @{thms word_size},
@@ -2034,11 +2032,9 @@
fun arith_tac' n t =
Arith_Data.verbose_arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty;
- val cs = claset_of ctxt;
- val ss = simpset_of ctxt;
in
- [ clarify_tac cs 1,
- full_simp_tac (unat_arith_ss_of ss) 1,
+ [ clarify_tac ctxt 1,
+ full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1,
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits}
addcongs @{thms power_False_cong})),
rewrite_goals_tac @{thms word_size},
--- a/src/HOL/ex/MT.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/ex/MT.thy Fri May 13 22:55:00 2011 +0200
@@ -869,7 +869,7 @@
ve + {ev |-> v} hastyenv te + {ev |=> t}"
apply (unfold hasty_env_def)
apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
-apply (tactic {* safe_tac HOL_cs *})
+apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
apply (case_tac "ev=x")
apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
apply (simp add: ve_app_owr2 te_app_owr2)
@@ -906,7 +906,7 @@
v_clos(cl) hasty t"
apply (unfold hasty_env_def hasty_def)
apply (drule elab_fix_elim)
-apply (tactic {* safe_tac HOL_cs *})
+apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
(*Do a single unfolding of cl*)
apply (frule ssubst) prefer 2 apply assumption
apply (rule hasty_rel_clos_coind)
@@ -914,7 +914,7 @@
apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
-apply (tactic {* safe_tac HOL_cs *})
+apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
apply (case_tac "ev2=ev1a")
apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
apply blast
--- a/src/Provers/blast.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/Provers/blast.ML Fri May 13 22:55:00 2011 +0200
@@ -51,7 +51,6 @@
signature BLAST =
sig
- type claset
exception TRANS of string (*reports translation errors*)
datatype term =
Const of string * term list
@@ -61,9 +60,9 @@
| Bound of int
| Abs of string*term
| $ of term*term;
- val depth_tac: claset -> int -> int -> tactic
+ val depth_tac: Proof.context -> int -> int -> tactic
val depth_limit: int Config.T
- val blast_tac: claset -> int -> tactic
+ val blast_tac: Proof.context -> int -> tactic
val setup: theory -> theory
(*debugging tools*)
type branch
@@ -75,8 +74,8 @@
val fromSubgoal: theory -> Term.term -> term
val instVars: term -> (unit -> unit)
val toTerm: int -> term -> Term.term
- val readGoal: theory -> string -> term
- val tryInThy: theory -> claset -> int -> string ->
+ val readGoal: Proof.context -> string -> term
+ val tryIt: Proof.context -> int -> string ->
(int -> tactic) list * branch list list * (int * int * exn) list
val normBr: branch -> branch
end;
@@ -85,7 +84,6 @@
struct
structure Classical = Data.Classical;
-type claset = Classical.claset;
val trace = Unsynchronized.ref false
and stats = Unsynchronized.ref false; (*for runtime and search statistics*)
@@ -915,9 +913,10 @@
bound on unsafe expansions.
"start" is CPU time at start, for printing search time
*)
-fun prove (state, start, cs, brs, cont) =
+fun prove (state, start, ctxt, brs, cont) =
let val State {thy, ntrail, nclosed, ntried, ...} = state;
- val {safe0_netpair, safep_netpair, haz_netpair, ...} = Classical.rep_cs cs
+ val {safe0_netpair, safep_netpair, haz_netpair, ...} =
+ Classical.rep_cs (Classical.claset_of ctxt);
val safeList = [safe0_netpair, safep_netpair]
and hazList = [haz_netpair]
fun prv (tacs, trs, choices, []) =
@@ -1237,7 +1236,7 @@
"start" is CPU time at start, for printing SEARCH time
(also prints reconstruction time)
"lim" is depth limit.*)
-fun timing_depth_tac start cs lim i st0 =
+fun timing_depth_tac start ctxt lim i st0 =
let val thy = Thm.theory_of_thm st0
val state = initialize thy
val st = st0
@@ -1261,20 +1260,20 @@
Seq.make(fn()=> cell))
end
in
- prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
+ prove (state, start, ctxt, [initBranch (mkGoal concl :: hyps, lim)], cont)
|> Seq.map (rotate_prems (1 - i))
end
handle PROVE => Seq.empty;
(*Public version with fixed depth*)
-fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
+fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;
val (depth_limit, setup_depth_limit) =
Attrib.config_int_global @{binding blast_depth_limit} (K 20);
-fun blast_tac cs i st =
+fun blast_tac ctxt i st =
((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
- (timing_depth_tac (Timing.start ()) cs) 0) i
+ (timing_depth_tac (Timing.start ()) ctxt) 0) i
THEN flexflex_tac) st
handle TRANS s =>
((if !trace then warning ("blast: " ^ s) else ());
@@ -1288,13 +1287,15 @@
val fullTrace = Unsynchronized.ref ([]: branch list list);
(*Read a string to make an initial, singleton branch*)
-fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
+fun readGoal ctxt s =
+ Syntax.read_prop ctxt s |> fromTerm (Proof_Context.theory_of ctxt) |> rand |> mkGoal;
-fun tryInThy thy cs lim s =
+fun tryIt ctxt lim s =
let
+ val thy = Proof_Context.theory_of ctxt;
val state as State {fullTrace = ft, ...} = initialize thy;
val res = timeap prove
- (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I);
+ (state, Timing.start (), ctxt, [initBranch ([readGoal ctxt s], lim)], I);
val _ = fullTrace := !ft;
in res end;
@@ -1305,8 +1306,8 @@
setup_depth_limit #>
Method.setup @{binding blast}
(Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
- (fn NONE => Classical.cla_meth' blast_tac
- | SOME lim => Classical.cla_meth' (fn cs => depth_tac cs lim)))
+ (fn NONE => SIMPLE_METHOD' o blast_tac
+ | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
"classical tableau prover";
end;
--- a/src/Provers/clasimp.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/Provers/clasimp.ML Fri May 13 22:55:00 2011 +0200
@@ -5,14 +5,11 @@
splitter.ML, classical.ML, blast.ML).
*)
-infix 4 addSss addss addss';
-
signature CLASIMP_DATA =
sig
structure Splitter: SPLITTER
structure Classical: CLASSICAL
structure Blast: BLAST
- sharing type Classical.claset = Blast.claset
val notE: thm
val iffD1: thm
val iffD2: thm
@@ -20,19 +17,16 @@
signature CLASIMP =
sig
- type claset
- type clasimpset
- val clasimpset_of: Proof.context -> clasimpset
- val addSss: claset * simpset -> claset
- val addss: claset * simpset -> claset
- val addss': claset * simpset -> claset
- val clarsimp_tac: clasimpset -> int -> tactic
- val mk_auto_tac: clasimpset -> int -> int -> tactic
- val auto_tac: clasimpset -> tactic
- val force_tac: clasimpset -> int -> tactic
- val fast_simp_tac: clasimpset -> int -> tactic
- val slow_simp_tac: clasimpset -> int -> tactic
- val best_simp_tac: clasimpset -> int -> tactic
+ val addSss: Proof.context -> Proof.context
+ val addss: Proof.context -> Proof.context
+ val addss': Proof.context -> Proof.context
+ val clarsimp_tac: Proof.context -> int -> tactic
+ val mk_auto_tac: Proof.context -> int -> int -> tactic
+ val auto_tac: Proof.context -> tactic
+ val force_tac: Proof.context -> int -> tactic
+ val fast_simp_tac: Proof.context -> int -> tactic
+ val slow_simp_tac: Proof.context -> int -> tactic
+ val best_simp_tac: Proof.context -> int -> tactic
val iff_add: attribute
val iff_add': attribute
val iff_del: attribute
@@ -49,29 +43,20 @@
structure Blast = Data.Blast;
-(* type clasimpset *)
-
-type claset = Classical.claset;
-type clasimpset = claset * simpset;
-
-fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);
-
-
(* simp as classical wrapper *)
(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);
-(*Add a simpset to a classical set!*)
-(*Caution: only one simpset added can be added by each of addSss and addss*)
-fun cs addSss ss =
- Classical.addSafter (cs, ("safe_asm_full_simp_tac", CHANGED o safe_asm_full_simp_tac ss));
+fun clasimp f name tac ctxt =
+ Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
-fun cs addss ss =
- Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_full_simp_tac ss));
-
-fun cs addss' ss =
- Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_lr_simp_tac ss));
+(*Add a simpset to the claset!*)
+(*Caution: only one simpset added can be added by each of addSss and addss*)
+val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
+val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
+(* FIXME "asm_lr_simp_tac" !? *)
+val addss' = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_lr_simp_tac;
(* iffs: addition of rules to simpsets and clasets simultaneously *)
@@ -128,75 +113,72 @@
(* tactics *)
-fun clarsimp_tac (cs, ss) =
- safe_asm_full_simp_tac ss THEN_ALL_NEW
- Classical.clarify_tac (cs addSss ss);
+fun clarsimp_tac ctxt =
+ safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
+ Classical.clarify_tac (addSss ctxt);
(* auto_tac *)
-fun blast_depth_tac cs m i thm =
- Blast.depth_tac cs m i thm
+fun blast_depth_tac ctxt m i thm =
+ Blast.depth_tac ctxt m i thm
handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
(* a variant of depth_tac that avoids interference of the simplifier
with dup_step_tac when they are combined by auto_tac *)
local
-fun slow_step_tac' cs =
- Classical.appWrappers cs
- (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
+fun slow_step_tac' ctxt =
+ Classical.appWrappers ctxt
+ (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt);
in
-fun nodup_depth_tac cs m i st =
+fun nodup_depth_tac ctxt m i st =
SELECT_GOAL
- (Classical.safe_steps_tac cs 1 THEN_ELSE
- (DEPTH_SOLVE (nodup_depth_tac cs m 1),
- Classical.inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
- (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m - 1) 1)))) i st;
+ (Classical.safe_steps_tac ctxt 1 THEN_ELSE
+ (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
+ Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
+ (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
end;
(*Designed to be idempotent, except if blast_depth_tac instantiates variables
in some of the subgoals*)
-fun mk_auto_tac (cs, ss) m n =
+fun mk_auto_tac ctxt m n =
let
- val cs' = cs addss ss;
val main_tac =
- blast_depth_tac cs m (* fast but can't use wrappers *)
+ blast_depth_tac ctxt m (* fast but can't use wrappers *)
ORELSE'
- (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
+ (CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *)
in
- PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)) THEN
- TRY (Classical.safe_tac cs) THEN
+ PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN
+ TRY (Classical.safe_tac ctxt) THEN
REPEAT_DETERM (FIRSTGOAL main_tac) THEN
- TRY (Classical.safe_tac (cs addSss ss)) THEN
+ TRY (Classical.safe_tac (addSss ctxt)) THEN
prune_params_tac
end;
-fun auto_tac css = mk_auto_tac css 4 2;
+fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
(* force_tac *)
(* aimed to solve the given subgoal totally, using whatever tools possible *)
-fun force_tac (cs, ss) =
- let val cs' = cs addss ss in
+fun force_tac ctxt =
+ let val ctxt' = addss ctxt in
SELECT_GOAL
- (Classical.clarify_tac cs' 1 THEN
- IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1) THEN
- ALLGOALS (Classical.first_best_tac cs'))
+ (Classical.clarify_tac ctxt' 1 THEN
+ IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN
+ ALLGOALS (Classical.first_best_tac ctxt'))
end;
(* basic combinations *)
-fun ADDSS tac (cs, ss) = let val cs' = cs addss ss in tac cs' end;
-
-val fast_simp_tac = ADDSS Classical.fast_tac;
-val slow_simp_tac = ADDSS Classical.slow_tac;
-val best_simp_tac = ADDSS Classical.best_tac;
+val fast_simp_tac = Classical.fast_tac o addss;
+val slow_simp_tac = Classical.slow_tac o addss;
+val best_simp_tac = Classical.best_tac o addss;
@@ -226,21 +208,14 @@
(* methods *)
-fun clasimp_meth tac ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt));
-
-fun clasimp_meth' tac ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt)));
-
-
fun clasimp_method' tac =
- Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
+ Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
val auto_method =
Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
Method.sections clasimp_modifiers >>
- (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
- | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
+ (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
+ | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
(* theory setup *)
--- a/src/Provers/classical.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/Provers/classical.ML Fri May 13 22:55:00 2011 +0200
@@ -37,30 +37,29 @@
sig
type claset
val empty_cs: claset
- val print_cs: Proof.context -> claset -> unit
val rep_cs: claset ->
{safeIs: thm list,
safeEs: thm list,
hazIs: thm list,
hazEs: thm list,
- swrappers: (string * wrapper) list,
- uwrappers: (string * wrapper) list,
+ swrappers: (string * (Proof.context -> wrapper)) list,
+ uwrappers: (string * (Proof.context -> wrapper)) list,
safe0_netpair: netpair,
safep_netpair: netpair,
haz_netpair: netpair,
dup_netpair: netpair,
xtra_netpair: Context_Rules.netpair}
- val merge_cs: claset * claset -> claset
- val addDs: claset * thm list -> claset
- val addEs: claset * thm list -> claset
- val addIs: claset * thm list -> claset
- val addSDs: claset * thm list -> claset
- val addSEs: claset * thm list -> claset
- val addSIs: claset * thm list -> claset
- val delrules: claset * thm list -> claset
- val addSWrapper: claset * (string * wrapper) -> claset
+ val print_claset: Proof.context -> unit
+ val addDs: Proof.context * thm list -> Proof.context
+ val addEs: Proof.context * thm list -> Proof.context
+ val addIs: Proof.context * thm list -> Proof.context
+ val addSDs: Proof.context * thm list -> Proof.context
+ val addSEs: Proof.context * thm list -> Proof.context
+ val addSIs: Proof.context * thm list -> Proof.context
+ val delrules: Proof.context * thm list -> Proof.context
+ val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
val delSWrapper: claset * string -> claset
- val addWrapper: claset * (string * wrapper) -> claset
+ val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
val delWrapper: claset * string -> claset
val addSbefore: claset * (string * (int -> tactic)) -> claset
val addSafter: claset * (string * (int -> tactic)) -> claset
@@ -70,54 +69,50 @@
val addE2: claset * (string * thm) -> claset
val addSD2: claset * (string * thm) -> claset
val addSE2: claset * (string * thm) -> claset
- val appSWrappers: claset -> wrapper
- val appWrappers: claset -> wrapper
+ val appSWrappers: Proof.context -> wrapper
+ val appWrappers: Proof.context -> wrapper
val global_claset_of: theory -> claset
val claset_of: Proof.context -> claset
+ val map_claset: (claset -> claset) -> Proof.context -> Proof.context
+ val put_claset: claset -> Proof.context -> Proof.context
- val fast_tac: claset -> int -> tactic
- val slow_tac: claset -> int -> tactic
- val astar_tac: claset -> int -> tactic
- val slow_astar_tac: claset -> int -> tactic
- val best_tac: claset -> int -> tactic
- val first_best_tac: claset -> int -> tactic
- val slow_best_tac: claset -> int -> tactic
- val depth_tac: claset -> int -> int -> tactic
- val deepen_tac: claset -> int -> int -> tactic
+ val fast_tac: Proof.context -> int -> tactic
+ val slow_tac: Proof.context -> int -> tactic
+ val astar_tac: Proof.context -> int -> tactic
+ val slow_astar_tac: Proof.context -> int -> tactic
+ val best_tac: Proof.context -> int -> tactic
+ val first_best_tac: Proof.context -> int -> tactic
+ val slow_best_tac: Proof.context -> int -> tactic
+ val depth_tac: Proof.context -> int -> int -> tactic
+ val deepen_tac: Proof.context -> int -> int -> tactic
val contr_tac: int -> tactic
val dup_elim: thm -> thm
val dup_intr: thm -> thm
- val dup_step_tac: claset -> int -> tactic
+ val dup_step_tac: Proof.context -> int -> tactic
val eq_mp_tac: int -> tactic
- val haz_step_tac: claset -> int -> tactic
+ val haz_step_tac: Proof.context -> int -> tactic
val joinrules: thm list * thm list -> (bool * thm) list
val mp_tac: int -> tactic
- val safe_tac: claset -> tactic
- val safe_steps_tac: claset -> int -> tactic
- val safe_step_tac: claset -> int -> tactic
- val clarify_tac: claset -> int -> tactic
- val clarify_step_tac: claset -> int -> tactic
- val step_tac: claset -> int -> tactic
- val slow_step_tac: claset -> int -> tactic
+ val safe_tac: Proof.context -> tactic
+ val safe_steps_tac: Proof.context -> int -> tactic
+ val safe_step_tac: Proof.context -> int -> tactic
+ val clarify_tac: Proof.context -> int -> tactic
+ val clarify_step_tac: Proof.context -> int -> tactic
+ val step_tac: Proof.context -> int -> tactic
+ val slow_step_tac: Proof.context -> int -> tactic
val swapify: thm list -> thm list
val swap_res_tac: thm list -> int -> tactic
- val inst_step_tac: claset -> int -> tactic
- val inst0_step_tac: claset -> int -> tactic
- val instp_step_tac: claset -> int -> tactic
+ val inst_step_tac: Proof.context -> int -> tactic
+ val inst0_step_tac: Proof.context -> int -> tactic
+ val instp_step_tac: Proof.context -> int -> tactic
end;
signature CLASSICAL =
sig
include BASIC_CLASSICAL
val classical_rule: thm -> thm
- val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
- val del_context_safe_wrapper: string -> theory -> theory
- val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
- val del_context_unsafe_wrapper: string -> theory -> theory
- val get_claset: Proof.context -> claset
- val put_claset: claset -> Proof.context -> Proof.context
val get_cs: Context.generic -> claset
val map_cs: (claset -> claset) -> Context.generic -> Context.generic
val safe_dest: int option -> attribute
@@ -128,10 +123,10 @@
val haz_intro: int option -> attribute
val rule_del: attribute
val cla_modifiers: Method.modifier parser list
- val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
- val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
- val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
- val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
+ val cla_method:
+ (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
+ val cla_method':
+ (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
val setup: theory -> theory
end;
@@ -208,7 +203,7 @@
(*Duplication of hazardous rules, for complete provers*)
fun dup_intr th = zero_var_indexes (th RS Data.classical);
-fun dup_elim th =
+fun dup_elim th = (* FIXME proper context!? *)
let
val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
@@ -218,17 +213,18 @@
(**** Classical rule sets ****)
datatype claset =
- CS of {safeIs : thm list, (*safe introduction rules*)
- safeEs : thm list, (*safe elimination rules*)
- hazIs : thm list, (*unsafe introduction rules*)
- hazEs : thm list, (*unsafe elimination rules*)
- swrappers : (string * wrapper) list, (*for transforming safe_step_tac*)
- uwrappers : (string * wrapper) list, (*for transforming step_tac*)
- safe0_netpair : netpair, (*nets for trivial cases*)
- safep_netpair : netpair, (*nets for >0 subgoals*)
- haz_netpair : netpair, (*nets for unsafe rules*)
- dup_netpair : netpair, (*nets for duplication*)
- xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
+ CS of
+ {safeIs : thm list, (*safe introduction rules*)
+ safeEs : thm list, (*safe elimination rules*)
+ hazIs : thm list, (*unsafe introduction rules*)
+ hazEs : thm list, (*unsafe elimination rules*)
+ swrappers : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*)
+ uwrappers : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*)
+ safe0_netpair : netpair, (*nets for trivial cases*)
+ safep_netpair : netpair, (*nets for >0 subgoals*)
+ haz_netpair : netpair, (*nets for unsafe rules*)
+ dup_netpair : netpair, (*nets for duplication*)
+ xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
(*Desired invariants are
safe0_netpair = build safe0_brls,
@@ -247,34 +243,21 @@
val empty_netpair = (Net.empty, Net.empty);
val empty_cs =
- CS{safeIs = [],
- safeEs = [],
- hazIs = [],
- hazEs = [],
- swrappers = [],
- uwrappers = [],
- safe0_netpair = empty_netpair,
- safep_netpair = empty_netpair,
- haz_netpair = empty_netpair,
- dup_netpair = empty_netpair,
- xtra_netpair = empty_netpair};
-
-fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
- let val pretty_thms = map (Display.pretty_thm ctxt) in
- [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
- Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
- Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
- Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
- Pretty.strs ("safe wrappers:" :: map #1 swrappers),
- Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
- |> Pretty.chunks |> Pretty.writeln
- end;
+ CS
+ {safeIs = [],
+ safeEs = [],
+ hazIs = [],
+ hazEs = [],
+ swrappers = [],
+ uwrappers = [],
+ safe0_netpair = empty_netpair,
+ safep_netpair = empty_netpair,
+ haz_netpair = empty_netpair,
+ dup_netpair = empty_netpair,
+ xtra_netpair = empty_netpair};
fun rep_cs (CS args) = args;
-fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
-fun appWrappers (CS {uwrappers, ...}) = fold snd uwrappers;
-
(*** Adding (un)safe introduction or elimination rules.
@@ -314,22 +297,31 @@
val mem_thm = member Thm.eq_thm_prop
and rem_thm = remove Thm.eq_thm_prop;
-fun warn msg rules th =
- mem_thm rules th andalso (warning (msg ^ Display.string_of_thm_without_context th); true);
+fun string_of_thm NONE = Display.string_of_thm_without_context
+ | string_of_thm (SOME context) =
+ Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
+
+fun make_elim context th =
+ if has_fewer_prems 1 th then
+ error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
+ else Tactic.make_elim th;
-fun warn_other th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
- warn "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
- warn "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
- warn "Rule already declared as introduction (intro)\n" hazIs th orelse
- warn "Rule already declared as elimination (elim)\n" hazEs th;
+fun warn context msg rules th =
+ mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true);
+
+fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
+ warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
+ warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
+ warn context "Rule already declared as introduction (intro)\n" hazIs th orelse
+ warn context "Rule already declared as elimination (elim)\n" hazEs th;
(*** Safe rules ***)
-fun addSI w th
+fun addSI w context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if warn "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
+ if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
else
let
val th' = flat_rule th;
@@ -337,7 +329,7 @@
List.partition Thm.no_prems [th'];
val nI = length safeIs + 1;
val nE = length safeEs;
- val _ = warn_other th cs;
+ val _ = warn_other context th cs;
in
CS
{safeIs = th::safeIs,
@@ -353,12 +345,12 @@
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
end;
-fun addSE w th
+fun addSE w context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if warn "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
+ if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
else if has_fewer_prems 1 th then
- error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
+ error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
let
val th' = classical_rule (flat_rule th);
@@ -366,7 +358,7 @@
List.partition (fn rl => nprems_of rl=1) [th'];
val nI = length safeIs;
val nE = length safeEs + 1;
- val _ = warn_other th cs;
+ val _ = warn_other context th cs;
in
CS
{safeEs = th::safeEs,
@@ -382,19 +374,21 @@
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
end;
+fun addSD w context th = addSE w context (make_elim context th);
+
(*** Hazardous (unsafe) rules ***)
-fun addI w th
+fun addI w context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if warn "Ignoring duplicate introduction (intro)\n" hazIs th then cs
+ if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
else
let
val th' = flat_rule th;
val nI = length hazIs + 1;
val nE = length hazEs;
- val _ = warn_other th cs;
+ val _ = warn_other context th cs;
in
CS
{hazIs = th :: hazIs,
@@ -410,20 +404,20 @@
xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair}
end
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *)
- error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
+ error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
-fun addE w th
+fun addE w context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if warn "Ignoring duplicate elimination (elim)\n" hazEs th then cs
+ if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
else if has_fewer_prems 1 th then
- error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
+ error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
let
val th' = classical_rule (flat_rule th);
val nI = length hazIs;
val nE = length hazEs + 1;
- val _ = warn_other th cs;
+ val _ = warn_other context th cs;
in
CS
{hazEs = th :: hazEs,
@@ -439,6 +433,8 @@
xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair}
end;
+fun addD w context th = addE w context (make_elim context th);
+
(*** Deletion of rules
@@ -492,7 +488,7 @@
end
else cs;
-fun delI th
+fun delI context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm hazIs th then
@@ -512,7 +508,7 @@
end
else cs
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *)
- error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
+ error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
fun delE th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
@@ -535,32 +531,21 @@
else cs;
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
-fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
- let val th' = Tactic.make_elim th (* FIXME classical make_elim!? *) in
+fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
+ let val th' = Tactic.make_elim th in
if mem_thm safeIs th orelse mem_thm safeEs th orelse
mem_thm hazIs th orelse mem_thm hazEs th orelse
mem_thm safeEs th' orelse mem_thm hazEs th'
- then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
- else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
+ then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
+ else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs)
end;
-fun cs delrules ths = fold delrule ths cs;
-
-fun make_elim th =
- if has_fewer_prems 1 th then
- error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
- else Tactic.make_elim th;
+
+(** claset data **)
-fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
-fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
-fun cs addSDs ths = cs addSEs (map make_elim ths);
-fun cs addIs ths = fold_rev (addI NONE) ths cs;
-fun cs addEs ths = fold_rev (addE NONE) ths cs;
-fun cs addDs ths = cs addEs (map make_elim ths);
+(* wrappers *)
-
-(*** Modifying the wrapper tacticals ***)
fun map_swrappers f
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
@@ -570,48 +555,15 @@
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
fun map_uwrappers f
- (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+ (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
swrappers = swrappers, uwrappers = f uwrappers,
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
-fun update_warn msg (p as (key : string, _)) xs =
- (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
-fun delete_warn msg (key : string) xs =
- if AList.defined (op =) xs key then AList.delete (op =) key xs
- else (warning msg; xs);
-
-(*Add/replace a safe wrapper*)
-fun cs addSWrapper new_swrapper = map_swrappers
- (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
-
-(*Add/replace an unsafe wrapper*)
-fun cs addWrapper new_uwrapper = map_uwrappers
- (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
-
-(*Remove a safe wrapper*)
-fun cs delSWrapper name = map_swrappers
- (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
-
-(*Remove an unsafe wrapper*)
-fun cs delWrapper name = map_uwrappers
- (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
-
-(* compose a safe tactic alternatively before/after safe_step_tac *)
-fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
-fun cs addSafter (name, tac2) = cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
-
-(*compose a tactic alternatively before/after the step tactic *)
-fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2);
-fun cs addafter (name, tac2) = cs addWrapper (name, fn tac1 => tac1 APPEND' tac2);
-
-fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
-fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
-fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
-fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
+(* merge_cs *)
(*Merge works by adding all new rules of the 2nd claset into the 1st claset.
Merging the term nets may look more efficient, but the rather delicate
@@ -626,29 +578,129 @@
val safeEs' = fold rem_thm safeEs safeEs2;
val hazIs' = fold rem_thm hazIs hazIs2;
val hazEs' = fold rem_thm hazEs hazEs2;
- val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs';
- val cs2 = map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
- val cs3 = map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
- in cs3 end;
+ in
+ cs
+ |> fold_rev (addSI NONE NONE) safeIs'
+ |> fold_rev (addSE NONE NONE) safeEs'
+ |> fold_rev (addI NONE NONE) hazIs'
+ |> fold_rev (addE NONE NONE) hazEs'
+ |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
+ |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers))
+ end;
+
+
+(* data *)
+
+structure Claset = Generic_Data
+(
+ type T = claset;
+ val empty = empty_cs;
+ val extend = I;
+ val merge = merge_cs;
+);
+
+val global_claset_of = Claset.get o Context.Theory;
+val claset_of = Claset.get o Context.Proof;
+val rep_claset_of = rep_cs o claset_of;
+
+val get_cs = Claset.get;
+val map_cs = Claset.map;
+
+fun map_claset f = Context.proof_map (map_cs f);
+fun put_claset cs = map_claset (K cs);
+
+fun print_claset ctxt =
+ let
+ val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
+ val pretty_thms = map (Display.pretty_thm ctxt);
+ in
+ [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
+ Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
+ Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
+ Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
+ Pretty.strs ("safe wrappers:" :: map #1 swrappers),
+ Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
+ |> Pretty.chunks |> Pretty.writeln
+ end;
+
+
+(* old-style declarations *)
+
+fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt;
+
+val op addSIs = decl (addSI NONE);
+val op addSEs = decl (addSE NONE);
+val op addSDs = decl (addSD NONE);
+val op addIs = decl (addI NONE);
+val op addEs = decl (addE NONE);
+val op addDs = decl (addD NONE);
+val op delrules = decl delrule;
+
+
+
+(*** Modifying the wrapper tacticals ***)
+
+fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt));
+fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt));
+
+fun update_warn msg (p as (key : string, _)) xs =
+ (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
+
+fun delete_warn msg (key : string) xs =
+ if AList.defined (op =) xs key then AList.delete (op =) key xs
+ else (warning msg; xs);
+
+(*Add/replace a safe wrapper*)
+fun cs addSWrapper new_swrapper =
+ map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
+
+(*Add/replace an unsafe wrapper*)
+fun cs addWrapper new_uwrapper =
+ map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
+
+(*Remove a safe wrapper*)
+fun cs delSWrapper name =
+ map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
+
+(*Remove an unsafe wrapper*)
+fun cs delWrapper name =
+ map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
+
+(* compose a safe tactic alternatively before/after safe_step_tac *)
+fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
+fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
+
+(*compose a tactic alternatively before/after the step tactic *)
+fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
+fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
+
+fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
+fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
+fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
+fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
+
(**** Simple tactics for theorem proving ****)
(*Attack subgoals using safe inferences -- matching, not resolution*)
-fun safe_step_tac (cs as CS {safe0_netpair, safep_netpair, ...}) =
- appSWrappers cs (FIRST' [
- eq_assume_tac,
+fun safe_step_tac ctxt =
+ let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
+ appSWrappers ctxt
+ (FIRST'
+ [eq_assume_tac,
eq_mp_tac,
bimatch_from_nets_tac safe0_netpair,
FIRST' Data.hyp_subst_tacs,
- bimatch_from_nets_tac safep_netpair]);
+ bimatch_from_nets_tac safep_netpair])
+ end;
(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
-fun safe_steps_tac cs =
- REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
+fun safe_steps_tac ctxt =
+ REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i));
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
-fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
+fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt));
(*** Clarify_tac: do safe steps without causing branching ***)
@@ -669,86 +721,89 @@
(eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
(*Attack subgoals using safe inferences -- matching, not resolution*)
-fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
- appSWrappers cs (FIRST' [
- eq_assume_contr_tac,
+fun clarify_step_tac ctxt =
+ let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
+ appSWrappers ctxt
+ (FIRST'
+ [eq_assume_contr_tac,
bimatch_from_nets_tac safe0_netpair,
FIRST' Data.hyp_subst_tacs,
n_bimatch_from_nets_tac 1 safep_netpair,
- bimatch2_tac safep_netpair]);
+ bimatch2_tac safep_netpair])
+ end;
-fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
+fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
(*** Unsafe steps instantiate variables or lose information ***)
(*Backtracking is allowed among the various these unsafe ways of
proving a subgoal. *)
-fun inst0_step_tac (CS {safe0_netpair, ...}) =
+fun inst0_step_tac ctxt =
assume_tac APPEND'
contr_tac APPEND'
- biresolve_from_nets_tac safe0_netpair;
+ biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
(*These unsafe steps could generate more subgoals.*)
-fun instp_step_tac (CS {safep_netpair, ...}) =
- biresolve_from_nets_tac safep_netpair;
+fun instp_step_tac ctxt =
+ biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
(*These steps could instantiate variables and are therefore unsafe.*)
-fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
+fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
-fun haz_step_tac (CS{haz_netpair,...}) =
- biresolve_from_nets_tac haz_netpair;
+fun haz_step_tac ctxt =
+ biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
(*Single step for the prover. FAILS unless it makes progress. *)
-fun step_tac cs i =
- safe_tac cs ORELSE appWrappers cs (inst_step_tac cs ORELSE' haz_step_tac cs) i;
+fun step_tac ctxt i =
+ safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i;
(*Using a "safe" rule to instantiate variables is unsafe. This tactic
allows backtracking from "safe" rules to "unsafe" rules here.*)
-fun slow_step_tac cs i =
- safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i;
+fun slow_step_tac ctxt i =
+ safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i;
(**** The following tactics all fail unless they solve one goal ****)
(*Dumb but fast*)
-fun fast_tac cs =
- Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+fun fast_tac ctxt =
+ Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
(*Slower but smarter than fast_tac*)
-fun best_tac cs =
+fun best_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac cs 1));
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
(*even a bit smarter than best_tac*)
-fun first_best_tac cs =
+fun first_best_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac cs)));
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
-fun slow_tac cs =
+fun slow_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
- SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
+ SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
-fun slow_best_tac cs =
+fun slow_best_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac cs 1));
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
val weight_ASTAR = 5;
-fun astar_tac cs =
+fun astar_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
- (step_tac cs 1));
+ (step_tac ctxt 1));
-fun slow_astar_tac cs =
+fun slow_astar_tac ctxt =
Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
- (slow_step_tac cs 1));
+ (slow_step_tac ctxt 1));
(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome
@@ -759,132 +814,44 @@
(*Non-deterministic! Could always expand the first unsafe connective.
That's hard to implement and did not perform better in experiments, due to
greater search depth required.*)
-fun dup_step_tac (CS {dup_netpair, ...}) =
- biresolve_from_nets_tac dup_netpair;
+fun dup_step_tac ctxt =
+ biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
local
- fun slow_step_tac' cs = appWrappers cs (instp_step_tac cs APPEND' dup_step_tac cs);
+ fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt);
in
- fun depth_tac cs m i state = SELECT_GOAL
- (safe_steps_tac cs 1 THEN_ELSE
- (DEPTH_SOLVE (depth_tac cs m 1),
- inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
- (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m - 1) 1)))) i state;
+ fun depth_tac ctxt m i state = SELECT_GOAL
+ (safe_steps_tac ctxt 1 THEN_ELSE
+ (DEPTH_SOLVE (depth_tac ctxt m 1),
+ inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
+ (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state;
end;
(*Search, with depth bound m.
This is the "entry point", which does safe inferences first.*)
-fun safe_depth_tac cs m = SUBGOAL (fn (prem,i) =>
- let val deti =
- (*No Vars in the goal? No need to backtrack between goals.*)
- if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
+fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) =>
+ let
+ val deti = (*No Vars in the goal? No need to backtrack between goals.*)
+ if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I;
in
- SELECT_GOAL (TRY (safe_tac cs) THEN DEPTH_SOLVE (deti (depth_tac cs m 1))) i
+ SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i
end);
-fun deepen_tac cs = DEEPEN (2, 10) (safe_depth_tac cs);
-
-
-
-(** context dependent claset components **)
-
-datatype context_cs = ContextCS of
- {swrappers: (string * (Proof.context -> wrapper)) list,
- uwrappers: (string * (Proof.context -> wrapper)) list};
-
-fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
- let
- fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
- in
- cs
- |> fold_rev (add_wrapper (op addSWrapper)) swrappers
- |> fold_rev (add_wrapper (op addWrapper)) uwrappers
- end;
-
-fun make_context_cs (swrappers, uwrappers) =
- ContextCS {swrappers = swrappers, uwrappers = uwrappers};
-
-val empty_context_cs = make_context_cs ([], []);
-
-fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
- if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
- else
- let
- val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
- val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
- val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
- val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
- in make_context_cs (swrappers', uwrappers') end;
-
-
-
-(** claset data **)
-
-(* global clasets *)
-
-structure GlobalClaset = Theory_Data
-(
- type T = claset * context_cs;
- val empty = (empty_cs, empty_context_cs);
- val extend = I;
- fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
- (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
-);
-
-val get_global_claset = #1 o GlobalClaset.get;
-val map_global_claset = GlobalClaset.map o apfst;
-
-val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of;
-fun map_context_cs f = GlobalClaset.map (apsnd
- (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
-
-fun global_claset_of thy =
- let val (cs, ctxt_cs) = GlobalClaset.get thy
- in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end;
-
-
-(* context dependent components *)
-
-fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
-fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
-
-fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
-fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
-
-
-(* local clasets *)
-
-structure LocalClaset = Proof_Data
-(
- type T = claset;
- val init = get_global_claset;
-);
-
-val get_claset = LocalClaset.get;
-val put_claset = LocalClaset.put;
-
-fun claset_of ctxt =
- context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
-
-
-(* generic clasets *)
-
-val get_cs = Context.cases global_claset_of claset_of;
-fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
+fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt);
(* attributes *)
-fun attrib f = Thm.declaration_attribute (fn th =>
- Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
+fun attrib f =
+ Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context);
-fun safe_dest w = attrib (addSE w o make_elim);
val safe_elim = attrib o addSE;
val safe_intro = attrib o addSI;
-fun haz_dest w = attrib (addE w o make_elim);
+val safe_dest = attrib o addSD;
val haz_elim = attrib o addE;
val haz_intro = attrib o addI;
+val haz_dest = attrib o addD;
val rule_del = attrib delrule o Context_Rules.rule_del;
@@ -916,7 +883,7 @@
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
let
val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
- val CS {xtra_netpair, ...} = claset_of ctxt;
+ val {xtra_netpair, ...} = rep_claset_of ctxt;
val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
val rules = rules1 @ rules2 @ rules3 @ rules4;
val ruleq = Drule.multi_resolves facts rules;
@@ -954,14 +921,8 @@
Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
Args.del -- Args.colon >> K (I, rule_del)];
-fun cla_meth tac ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
-
-fun cla_meth' tac ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
-
-fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
-fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
+fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
+fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
@@ -981,7 +942,7 @@
Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
- Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
+ Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
"classical prover (iterative deepening)" #>
Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
"classical prover (apply safe rules)";
@@ -1002,6 +963,6 @@
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (fn state =>
let val ctxt = Toplevel.context_of state
- in print_cs ctxt (claset_of ctxt) end)));
+ in print_claset ctxt end)));
end;
--- a/src/Pure/simplifier.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/Pure/simplifier.ML Fri May 13 22:55:00 2011 +0200
@@ -8,6 +8,7 @@
signature BASIC_SIMPLIFIER =
sig
include BASIC_RAW_SIMPLIFIER
+ val map_simpset_local: (simpset -> simpset) -> Proof.context -> Proof.context
val change_simpset: (simpset -> simpset) -> unit
val global_simpset_of: theory -> simpset
val Addsimprocs: simproc list -> unit
@@ -136,7 +137,7 @@
(* global simpset *)
-fun map_simpset f = Context.theory_map (map_ss f);
+fun map_simpset f = Context.theory_map (map_ss f); (* FIXME global *)
fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
fun global_simpset_of thy =
Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
@@ -147,6 +148,7 @@
(* local simpset *)
+fun map_simpset_local f = Context.proof_map (map_ss f);
fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
val _ = ML_Antiquote.value "simpset"
--- a/src/ZF/Tools/datatype_package.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML Fri May 13 22:55:00 2011 +0200
@@ -348,11 +348,14 @@
(*Typical theorems have the form ~con1=con2, con1=con2==>False,
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
fun mk_free s =
- let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*)
- Goal.prove_global thy [] [] (Syntax.read_prop_global thy s)
+ let
+ val thy = theory_of_thm elim;
+ val ctxt = Proof_Context.init_global thy;
+ in
+ Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
(fn _ => EVERY
[rewrite_goals_tac con_defs,
- fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])
+ fast_tac (put_claset ZF_cs ctxt addSEs free_SEs @ Su.free_SEs) 1])
end;
val simps = case_eqns @ recursor_eqns;
--- a/src/ZF/UNITY/Constrains.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/ZF/UNITY/Constrains.thy Fri May 13 22:55:00 2011 +0200
@@ -471,7 +471,7 @@
(*proves "co" properties when the program is specified*)
fun constrains_tac ctxt =
- let val css as (cs, ss) = clasimpset_of ctxt in
+ let val ss = simpset_of ctxt in
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
REPEAT (etac @{thm Always_ConstrainsI} 1
@@ -481,20 +481,20 @@
rtac @{thm constrainsI} 1,
(* Three subgoals *)
rewrite_goal_tac [@{thm st_set_def}] 3,
- REPEAT (force_tac css 2),
+ REPEAT (force_tac ctxt 2),
full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
REPEAT (FIRSTGOAL (etac @{thm disjE})),
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
REPEAT (FIRSTGOAL (etac @{thm disjE})),
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_full_simp_tac ss),
- ALLGOALS (clarify_tac cs)])
+ ALLGOALS (clarify_tac ctxt)])
end;
(*For proving invariants*)
-fun always_tac ctxt i =
- rtac @{thm AlwaysI} i THEN force_tac (clasimpset_of ctxt) i THEN constrains_tac ctxt i;
+fun always_tac ctxt i =
+ rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
*}
setup Program_Defs.setup
--- a/src/ZF/UNITY/SubstAx.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Fri May 13 22:55:00 2011 +0200
@@ -351,7 +351,7 @@
ML {*
(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac ctxt sact =
- let val css as (cs, ss) = clasimpset_of ctxt in
+ let val ss = simpset_of ctxt in
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
etac @{thm Always_LeadsTo_Basis} 1
@@ -364,14 +364,14 @@
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm domain_def}]) 3,
(* proving the domain part *)
- clarify_tac cs 3, dtac @{thm swap} 3, force_tac css 4,
- rtac @{thm ReplaceI} 3, force_tac css 3, force_tac css 4,
+ clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4,
+ rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,
asm_full_simp_tac ss 3, rtac @{thm conjI} 3, simp_tac ss 4,
REPEAT (rtac @{thm state_update_type} 3),
constrains_tac ctxt 1,
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_full_simp_tac (ss addsimps [@{thm st_set_def}])),
- ALLGOALS (clarify_tac cs),
+ ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_lr_simp_tac ss)])
end;
*}
--- a/src/ZF/equalities.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/ZF/equalities.thy Fri May 13 22:55:00 2011 +0200
@@ -970,17 +970,14 @@
Un_upper1 Un_upper2 Int_lower1 Int_lower2
ML {*
-val subset_cs = @{claset}
+val subset_cs =
+ claset_of (@{context}
delrules [@{thm subsetI}, @{thm subsetCE}]
addSIs @{thms subset_SIs}
addIs [@{thm Union_upper}, @{thm Inter_lower}]
- addSEs [@{thm cons_subsetE}];
-*}
-(*subset_cs is a claset for subset reasoning*)
+ addSEs [@{thm cons_subsetE}]);
-ML
-{*
-val ZF_cs = @{claset} delrules [@{thm equalityI}];
+val ZF_cs = claset_of (@{context} delrules [@{thm equalityI}]);
*}
end
--- a/src/ZF/ex/CoUnit.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/ZF/ex/CoUnit.thy Fri May 13 22:55:00 2011 +0200
@@ -76,11 +76,11 @@
"Ord(i) ==> \<forall>x y. x \<in> counit2 --> y \<in> counit2 --> x Int Vset(i) \<subseteq> y"
-- {* Lemma for proving finality. *}
apply (erule trans_induct)
- apply (tactic "safe_tac subset_cs")
+ apply (tactic "safe_tac (put_claset subset_cs @{context})")
apply (erule counit2.cases)
apply (erule counit2.cases)
apply (unfold counit2.con_defs)
- apply (tactic {* fast_tac (subset_cs
+ apply (tactic {* fast_tac (put_claset subset_cs @{context}
addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}]
addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1 *})
done
--- a/src/ZF/ex/LList.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/ZF/ex/LList.thy Fri May 13 22:55:00 2011 +0200
@@ -113,7 +113,7 @@
apply (erule llist.cases)
apply (simp_all add: QInl_def QInr_def llist.con_defs)
(*LCons case: I simply can't get rid of the deepen_tac*)
-apply (tactic "deepen_tac (@{claset} addIs [@{thm Ord_trans}]
+apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
done
@@ -216,7 +216,7 @@
apply (erule llist.cases, simp_all)
apply (simp_all add: QInl_def QInr_def llist.con_defs)
(*LCons case: I simply can't get rid of the deepen_tac*)
-apply (tactic "deepen_tac (@{claset} addIs [@{thm Ord_trans}]
+apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
done