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