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