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