# HG changeset patch # User wenzelm # Date 1237559058 -3600 # Node ID c3d1590debd8df6937e5b62a5b2ddbd52cfe3d7b # Parent 40a1865ab1221eba6190356fb47b4f3ada9606d5 eliminated global SIMPSET, CLASET etc. -- refer to explicit context; diff -r 40a1865ab122 -r c3d1590debd8 doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Message.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Auth/Message - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge @@ -830,9 +829,9 @@ (*Prove base case (subgoal i) and simplify others. A typical base case concerns Crypt K X \ Key`shrK`bad and cannot be proved by rewriting alone.*) -fun prove_simple_subgoals_tac i = - force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN - ALLGOALS Asm_simp_tac +fun prove_simple_subgoals_tac (cs, ss) i = + force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN + ALLGOALS (asm_simp_tac ss) (*Analysis of Fake cases. Also works for messages that forward unknown parts, but this application is no longer necessary if analz_insert_eq is used. @@ -857,8 +856,7 @@ (cs addIs [analz_insertI, impOfSubs analz_subset_parts]) 4 1)) -(*The explicit claset and simpset arguments help it work with Isar*) -fun gen_spy_analz_tac (cs,ss) i = +fun spy_analz_tac (cs,ss) i = DETERM (SELECT_GOAL (EVERY @@ -870,8 +868,6 @@ simp_tac ss 1, REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) - -fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i *} text{*By default only @{text o_apply} is built-in. But in the presence of @@ -919,7 +915,7 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* diff -r 40a1865ab122 -r c3d1590debd8 doc-src/TutorialI/Protocol/Public.thy --- a/doc-src/TutorialI/Protocol/Public.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Public.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Auth/Public - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge @@ -153,15 +152,15 @@ (*Tactic for possibility theorems*) ML {* -fun possibility_tac st = st |> +fun possibility ctxt = REPEAT (*omit used_Says so that Nonces start from different traces!*) - (ALLGOALS (simp_tac (@{simpset} delsimps [used_Says])) + (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says])) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, @{thm Nonce_supply}])); *} -method_setup possibility = {* Scan.succeed (K (SIMPLE_METHOD possibility_tac)) *} +method_setup possibility = {* Scan.succeed (SIMPLE_METHOD o possibility_tac) *} "for proving possibility theorems" end diff -r 40a1865ab122 -r c3d1590debd8 src/CCL/Type.thy --- a/src/CCL/Type.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/CCL/Type.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: CCL/Type.thy - ID: $Id$ Author: Martin Coen Copyright 1993 University of Cambridge *) @@ -409,7 +408,7 @@ fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s (fn prems => [rtac (genXH RS iffD2) 1, - SIMPSET' simp_tac 1, + simp_tac (simpset_of thy) 1, TRY (fast_tac (@{claset} addIs ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] @ prems)) 1)]) @@ -442,8 +441,8 @@ "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))", "[| : lfp(%x. POgen(x) Un R Un PO); : lfp(%x. POgen(x) Un R Un PO) |] ==> : POgen(lfp(%x. POgen(x) Un R Un PO))"]; -fun POgen_tac (rla,rlb) i = - SELECT_GOAL (CLASET safe_tac) i THEN +fun POgen_tac ctxt (rla,rlb) i = + SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN (REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @ (POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i)); diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Auth/Message.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Auth/Message - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge @@ -848,9 +847,9 @@ (*Prove base case (subgoal i) and simplify others. A typical base case concerns Crypt K X \ Key`shrK`bad and cannot be proved by rewriting alone.*) -fun prove_simple_subgoals_tac i = - CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN - ALLGOALS (SIMPSET' asm_simp_tac) +fun prove_simple_subgoals_tac (cs, ss) i = + force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN + ALLGOALS (asm_simp_tac ss) (*Analysis of Fake cases. Also works for messages that forward unknown parts, but this application is no longer necessary if analz_insert_eq is used. @@ -875,8 +874,7 @@ (cs addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1)) -(*The explicit claset and simpset arguments help it work with Isar*) -fun gen_spy_analz_tac (cs,ss) i = +fun spy_analz_tac (cs,ss) i = DETERM (SELECT_GOAL (EVERY @@ -888,8 +886,6 @@ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) -val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac; - end *} @@ -941,7 +937,7 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o local_clasimpset_of) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/IMPP/Hoare.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/IMPP/Hoare.thy - ID: $Id$ Author: David von Oheimb Copyright 1999 TUM *) @@ -219,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 CLASET' fast_tac) *}) +apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *}) done lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}" @@ -291,7 +290,7 @@ simp_tac @{simpset}, clarify_tac @{claset}, 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 (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *) +apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *) prefer 3 apply (force) (* Call *) apply (erule_tac [2] evaln_elim_cases) (* If *) apply blast+ @@ -336,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 (CLASIMPSET' clarsimp_tac) *}) +apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) 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 {* CLASIMPSET' clarsimp_tac 7 *}, +apply (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 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 {* CLASIMPSET' clarsimp_tac 3 *}, +apply (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 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) @@ -365,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 (CLASIMPSET' clarsimp_tac) *}) +apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) apply (subgoal_tac "G = mgt_call ` U") prefer 2 apply (simp add: card_seteq finite_imageI) diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Fri Mar 20 15:24:18 2009 +0100 @@ -109,7 +109,7 @@ ( OldGoals.push_proof(); OldGoals.goalw_cterm [] (cterm_of sign trm); -by (SIMPSET' simp_tac 1); +by (simp_tac (simpset_of sign) 1); let val if_tmp_result = result() in diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/SET-Protocol/Cardholder_Registration.thy --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Auth/SET/Cardholder_Registration - ID: $Id$ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson, Piero Tramontano *) @@ -263,7 +262,7 @@ THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret], THEN Says_to_Gets, THEN set_cr.SET_CR6 [of concl: i C KC2]]) -apply (tactic "PublicSET.basic_possibility_tac") +apply basic_possibility apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq) done diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/SET-Protocol/MessageSET.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Auth/SET/MessageSET - ID: $Id$ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson *) @@ -846,9 +845,9 @@ (*Prove base case (subgoal i) and simplify others. A typical base case concerns Crypt K X \ Key`shrK`bad and cannot be proved by rewriting alone.*) -fun prove_simple_subgoals_tac i = - CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN - ALLGOALS (SIMPSET' asm_simp_tac) +fun prove_simple_subgoals_tac (cs, ss) i = + force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN + ALLGOALS (asm_simp_tac ss) (*Analysis of Fake cases. Also works for messages that forward unknown parts, but this application is no longer necessary if analz_insert_eq is used. @@ -873,8 +872,7 @@ (cs addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1)) -(*The explicit claset and simpset arguments help it work with Isar*) -fun gen_spy_analz_tac (cs,ss) i = +fun spy_analz_tac (cs,ss) i = DETERM (SELECT_GOAL (EVERY @@ -887,8 +885,6 @@ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) -val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac; - end *} (*>*) @@ -941,7 +937,7 @@ method_setup spy_analz = {* Scan.succeed (fn ctxt => - SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (MessageSET.spy_analz_tac (local_clasimpset_of ctxt))) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/SET-Protocol/PublicSET.thy --- a/src/HOL/SET-Protocol/PublicSET.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/SET-Protocol/PublicSET.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Auth/SET/PublicSET - ID: $Id$ - Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson + Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson *) header{*The Public-Key Theory, Modified for SET*} @@ -348,22 +347,19 @@ structure PublicSET = struct -(*Tactic for possibility theorems (Isar interface)*) -fun gen_possibility_tac ss state = state |> +(*Tactic for possibility theorems*) +fun possibility_tac ctxt = REPEAT (*omit used_Says so that Nonces start from different traces!*) - (ALLGOALS (simp_tac (ss delsimps [@{thm used_Says}, @{thm used_Notes}])) + (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}])) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, @{thm Nonce_supply}])) -(*Tactic for possibility theorems (ML script version)*) -fun possibility_tac state = gen_possibility_tac (simpset_of (Thm.theory_of_thm state)) state - (*For harder protocols (such as SET_CR!), where we have to set up some nonces and keys initially*) -fun basic_possibility_tac st = st |> +fun basic_possibility_tac ctxt = REPEAT - (ALLGOALS (asm_simp_tac (simpset_of (Thm.theory_of_thm st) setSolver safe_solver)) + (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) THEN REPEAT_FIRST (resolve_tac [refl, conjI])) @@ -371,10 +367,12 @@ *} method_setup possibility = {* - Scan.succeed (fn ctxt => - SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *} + Scan.succeed (SIMPLE_METHOD o PublicSET.possibility_tac) *} "for proving possibility theorems" +method_setup basic_possibility = {* + Scan.succeed (SIMPLE_METHOD o PublicSET.basic_possibility_tac) *} + "for proving possibility theorems" subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/SET-Protocol/Purchase.thy --- a/src/HOL/SET-Protocol/Purchase.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/SET-Protocol/Purchase.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Auth/SET/Purchase - ID: $Id$ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson *) @@ -335,7 +334,7 @@ THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID], THEN Says_to_Gets, THEN set_pur.PRes]) -apply (tactic "PublicSET.basic_possibility_tac") +apply basic_possibility apply (simp_all add: used_Cons symKeys_neq_imp_neq) done @@ -371,7 +370,7 @@ THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID], THEN Says_to_Gets, THEN set_pur.PRes]) -apply (tactic "PublicSET.basic_possibility_tac") +apply basic_possibility apply (auto simp add: used_Cons symKeys_neq_imp_neq) done diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/SizeChange/sct.ML --- a/src/HOL/SizeChange/sct.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/SizeChange/sct.ML Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/SizeChange/sct.ML - ID: $Id$ Author: Alexander Krauss, TU Muenchen Tactics for size change termination. @@ -183,8 +182,10 @@ fun rand (_ $ t) = t -fun setup_probe_goal thy domT Dtab Mtab (i, j) = +fun setup_probe_goal ctxt domT Dtab Mtab (i, j) = let + val css = local_clasimpset_of ctxt + val thy = ProofContext.theory_of ctxt val RD1 = get_elem (Dtab i) val RD2 = get_elem (Dtab j) val Ms1 = get_elem (Mtab i) @@ -200,12 +201,12 @@ val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar) |> cterm_of thy |> Goal.init - |> CLASIMPSET auto_tac |> Seq.hd + |> auto_tac css |> Seq.hd val no_step = saved_state |> forall_intr (cterm_of thy relvar) |> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const)))) - |> CLASIMPSET auto_tac |> Seq.hd + |> auto_tac css |> Seq.hd in if Thm.no_prems no_step @@ -218,7 +219,7 @@ val with_m1 = saved_state |> forall_intr (cterm_of thy mvar1) |> forall_elim (cterm_of thy M1) - |> CLASIMPSET auto_tac |> Seq.hd + |> auto_tac css |> Seq.hd fun set_m2 j = let @@ -226,15 +227,15 @@ val with_m2 = with_m1 |> forall_intr (cterm_of thy mvar2) |> forall_elim (cterm_of thy M2) - |> CLASIMPSET auto_tac |> Seq.hd + |> auto_tac css |> Seq.hd val decr = forall_intr (cterm_of thy relvar) #> forall_elim (cterm_of thy @{const HOL.less(nat)}) - #> CLASIMPSET auto_tac #> Seq.hd + #> auto_tac css #> Seq.hd val decreq = forall_intr (cterm_of thy relvar) #> forall_elim (cterm_of thy @{const HOL.less_eq(nat)}) - #> CLASIMPSET auto_tac #> Seq.hd + #> auto_tac css #> Seq.hd val thm1 = decr with_m2 in @@ -266,17 +267,17 @@ fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n)) -val in_graph_tac = +fun in_graph_tac ctxt = simp_tac (HOL_basic_ss addsimps has_edge_simps) 1 - THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *) + THEN (simp_tac (local_simpset_of ctxt) 1) (* FIXME reduce simpset *) -fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1 - | approx_tac (Graph (G, thm)) = +fun approx_tac _ (NoStep thm) = rtac disjI1 1 THEN rtac thm 1 + | approx_tac ctxt (Graph (G, thm)) = rtac disjI2 1 THEN rtac exI 1 THEN rtac conjI 1 THEN rtac thm 2 - THEN in_graph_tac + THEN (in_graph_tac ctxt) fun all_less_tac [] = rtac all_less_zero 1 | all_less_tac (t :: ts) = rtac all_less_Suc 1 @@ -292,7 +293,7 @@ fun mk_call_graph ctxt (st : thm) = let - val thy = theory_of_thm st + val thy = ProofContext.theory_of ctxt val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st)) val RDs = HOLogic.dest_list RDlist @@ -316,7 +317,7 @@ val pairs = matrix indices indices val parts = map_matrix (fn (n,m) => (timeap_msg (string_of_int n ^ "," ^ string_of_int m) - (setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs + (setup_probe_goal ctxt domT Dtab Mtab) (n,m))) pairs val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^ @@ -333,8 +334,8 @@ val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns) val tac = - (SIMPSET (unfold_tac [sound_int_def, len_simp])) - THEN all_less_tac (map (all_less_tac o map approx_tac) parts) + unfold_tac [sound_int_def, len_simp] (local_simpset_of ctxt) + THEN all_less_tac (map (all_less_tac o map (approx_tac ctxt)) parts) in tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st) end diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Tools/cnf_funcs.ML Fri Mar 20 15:24:18 2009 +0100 @@ -51,51 +51,46 @@ structure cnf : CNF = struct -fun thm_by_auto (G : string) : thm = - prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, CLASIMPSET auto_tac]); +val clause2raw_notE = @{lemma "[| P; ~P |] ==> False" by auto}; +val clause2raw_not_disj = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto}; +val clause2raw_not_not = @{lemma "P ==> ~~P" by auto}; -(* Thm.thm *) -val clause2raw_notE = thm_by_auto "[| P; ~P |] ==> False"; -val clause2raw_not_disj = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)"; -val clause2raw_not_not = thm_by_auto "P ==> ~~P"; +val iff_refl = @{lemma "(P::bool) = P" by auto}; +val iff_trans = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto}; +val conj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto}; +val disj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto}; -val iff_refl = thm_by_auto "(P::bool) = P"; -val iff_trans = thm_by_auto "[| (P::bool) = Q; Q = R |] ==> P = R"; -val conj_cong = thm_by_auto "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')"; -val disj_cong = thm_by_auto "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')"; - -val make_nnf_imp = thm_by_auto "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')"; -val make_nnf_iff = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))"; -val make_nnf_not_false = thm_by_auto "(~False) = True"; -val make_nnf_not_true = thm_by_auto "(~True) = False"; -val make_nnf_not_conj = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')"; -val make_nnf_not_disj = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')"; -val make_nnf_not_imp = thm_by_auto "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')"; -val make_nnf_not_iff = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))"; -val make_nnf_not_not = thm_by_auto "P = P' ==> (~~P) = P'"; +val make_nnf_imp = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto}; +val make_nnf_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto}; +val make_nnf_not_false = @{lemma "(~False) = True" by auto}; +val make_nnf_not_true = @{lemma "(~True) = False" by auto}; +val make_nnf_not_conj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto}; +val make_nnf_not_disj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto}; +val make_nnf_not_imp = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto}; +val make_nnf_not_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto}; +val make_nnf_not_not = @{lemma "P = P' ==> (~~P) = P'" by auto}; -val simp_TF_conj_True_l = thm_by_auto "[| P = True; Q = Q' |] ==> (P & Q) = Q'"; -val simp_TF_conj_True_r = thm_by_auto "[| P = P'; Q = True |] ==> (P & Q) = P'"; -val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False"; -val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False"; -val simp_TF_disj_True_l = thm_by_auto "P = True ==> (P | Q) = True"; -val simp_TF_disj_True_r = thm_by_auto "Q = True ==> (P | Q) = True"; -val simp_TF_disj_False_l = thm_by_auto "[| P = False; Q = Q' |] ==> (P | Q) = Q'"; -val simp_TF_disj_False_r = thm_by_auto "[| P = P'; Q = False |] ==> (P | Q) = P'"; +val simp_TF_conj_True_l = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto}; +val simp_TF_conj_True_r = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto}; +val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto}; +val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto}; +val simp_TF_disj_True_l = @{lemma "P = True ==> (P | Q) = True" by auto}; +val simp_TF_disj_True_r = @{lemma "Q = True ==> (P | Q) = True" by auto}; +val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto}; +val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto}; -val make_cnf_disj_conj_l = thm_by_auto "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)"; -val make_cnf_disj_conj_r = thm_by_auto "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)"; +val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto}; +val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto}; -val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x) | Q) = (EX x. P x | Q)"; -val make_cnfx_disj_ex_r = thm_by_auto "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)"; -val make_cnfx_newlit = thm_by_auto "(P | Q) = (EX x. (P | x) & (Q | ~x))"; -val make_cnfx_ex_cong = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)"; +val make_cnfx_disj_ex_l = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto}; +val make_cnfx_disj_ex_r = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto}; +val make_cnfx_newlit = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto}; +val make_cnfx_ex_cong = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto}; -val weakening_thm = thm_by_auto "[| P; Q |] ==> Q"; +val weakening_thm = @{lemma "[| P; Q |] ==> Q" by auto}; -val cnftac_eq_imp = thm_by_auto "[| P = Q; P |] ==> Q"; +val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto}; -(* Term.term -> bool *) fun is_atom (Const ("False", _)) = false | is_atom (Const ("True", _)) = false | is_atom (Const ("op &", _) $ _ $ _) = false @@ -105,11 +100,9 @@ | is_atom (Const ("Not", _) $ _) = false | is_atom _ = true; -(* Term.term -> bool *) fun is_literal (Const ("Not", _) $ x) = is_atom x | is_literal x = is_atom x; -(* Term.term -> bool *) fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y | is_clause x = is_literal x; diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_core.ML Fri Mar 20 15:24:18 2009 +0100 @@ -691,8 +691,9 @@ (* FIXME: This should probably use fixed goals, to be more reliable and faster *) -fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause = +fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = let + val thy = ProofContext.theory_of ctxt val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, qglr = (oqs, _, _, _), ...} = clause val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) @@ -702,7 +703,7 @@ Goal.init goal |> (SINGLE (resolve_tac [accI] 1)) |> the |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the - |> (SINGLE (CLASIMPSET auto_tac)) |> the + |> (SINGLE (auto_tac (local_clasimpset_of ctxt))) |> the |> Goal.conclude |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end @@ -831,7 +832,7 @@ ((rtac (G_induct OF [a])) THEN_ALL_NEW (rtac accI) THEN_ALL_NEW (etac R_cases) - THEN_ALL_NEW (SIMPSET' asm_full_simp_tac)) 1) + THEN_ALL_NEW (asm_full_simp_tac (local_simpset_of octxt))) 1) val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value) @@ -849,9 +850,9 @@ (fn _ => rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 - THEN (SIMPSET' simp_default_tac 1) + THEN (simp_default_tac (local_simpset_of ctxt) 1) THEN (etac not_acc_down 1) - THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1) + THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (local_simpset_of ctxt))) 1) |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end in @@ -935,7 +936,7 @@ val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses val dom_intros = if domintros - then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses) + then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses) else NONE val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Tools/function_package/mutual.ML Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/function_package/mutual.ML - ID: $Id$ Author: Alexander Krauss, TU Muenchen A package for general recursive function definitions. @@ -207,7 +206,7 @@ (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs) THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 - THEN SIMPSET' (fn ss => simp_tac (ss addsimps SumTree.proj_in_rules)) 1) + THEN (simp_tac (local_simpset_of ctxt addsimps SumTree.proj_in_rules)) 1) |> restore_cond |> export end diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Tools/function_package/scnp_reconstruct.ML --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Fri Mar 20 15:24:18 2009 +0100 @@ -291,7 +291,7 @@ THEN (rtac @{thm rp_inv_image_rp} 1) THEN (rtac (order_rpair ms_rp label) 1) THEN PRIMITIVE (instantiate' [] [SOME level_mapping]) - THEN unfold_tac @{thms rp_inv_image_def} (simpset_of thy) + THEN unfold_tac @{thms rp_inv_image_def} (local_simpset_of ctxt) THEN LocalDefs.unfold_tac ctxt (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv}) THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}])) @@ -395,7 +395,7 @@ fun gen_sizechange_tac orders autom_tac ctxt err_cont = TRY (FundefCommon.apply_termination_rule ctxt 1) - THEN TRY Termination.wf_union_tac + THEN TRY (Termination.wf_union_tac ctxt) THEN (rtac @{thm wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1) diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Tools/function_package/termination.ML --- a/src/HOL/Tools/function_package/termination.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Tools/function_package/termination.ML Fri Mar 20 15:24:18 2009 +0100 @@ -40,7 +40,7 @@ val REPEAT : ttac -> ttac - val wf_union_tac : tactic + val wf_union_tac : Proof.context -> tactic end @@ -276,9 +276,9 @@ in -fun wf_union_tac st = +fun wf_union_tac ctxt st = let - val thy = theory_of_thm st + val thy = ProofContext.theory_of ctxt val cert = cterm_of (theory_of_thm st) val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st @@ -303,7 +303,7 @@ THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *) ORELSE' ((rtac @{thm conjI}) THEN' (rtac @{thm refl}) - THEN' (CLASET' blast_tac))) (* Solve rest of context... not very elegant *) + THEN' (blast_tac (local_claset_of ctxt)))) (* Solve rest of context... not very elegant *) ) i in ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)]) diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Tools/meson.ML Fri Mar 20 15:24:18 2009 +0100 @@ -25,7 +25,7 @@ val skolemize_prems_tac: thm list -> int -> tactic val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic val best_meson_tac: (thm -> int) -> int -> tactic - val safe_best_meson_tac: int -> tactic + val safe_best_meson_tac: claset -> int -> tactic val depth_meson_tac: int -> tactic val prolog_step_tac': thm list -> int -> tactic val iter_deepen_prolog_tac: thm list -> tactic @@ -33,7 +33,7 @@ val make_meta_clause: thm -> thm val make_meta_clauses: thm list -> thm list val meson_claset_tac: thm list -> claset -> int -> tactic - val meson_tac: int -> tactic + val meson_tac: claset -> int -> tactic val negate_head: thm -> thm val select_literal: int -> thm -> thm val skolemize_tac: int -> tactic @@ -589,8 +589,8 @@ (prolog_step_tac (make_horns cls) 1)); (*First, breaks the goal into independent units*) -val safe_best_meson_tac = - SELECT_GOAL (TRY (CLASET safe_tac) THEN +fun safe_best_meson_tac cs = + SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (best_meson_tac size_of_subgoals)); (** Depth-first search version **) @@ -634,7 +634,7 @@ fun meson_claset_tac ths cs = SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths)); -val meson_tac = CLASET' (meson_claset_tac []); +val meson_tac = meson_claset_tac []; (**** Code to support ordinary resolution, rather than Model Elimination ****) diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Fri Mar 20 15:24:18 2009 +0100 @@ -511,10 +511,13 @@ addcongs @{thms power_False_cong} fun uint_arith_tacs ctxt = - let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty + let + fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty; + val cs = local_claset_of ctxt; + val ss = local_simpset_of ctxt; in - [ CLASET' clarify_tac 1, - SIMPSET' (full_simp_tac o uint_arith_ss_of) 1, + [ clarify_tac cs 1, + full_simp_tac (uint_arith_ss_of ss) 1, ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} addcongs @{thms power_False_cong})), rewrite_goals_tac @{thms word_size}, @@ -1069,10 +1072,13 @@ addcongs @{thms power_False_cong} fun unat_arith_tacs ctxt = - let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty + let + fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty; + val cs = local_claset_of ctxt; + val ss = local_simpset_of ctxt; in - [ CLASET' clarify_tac 1, - SIMPSET' (full_simp_tac o unat_arith_ss_of) 1, + [ clarify_tac cs 1, + full_simp_tac (unat_arith_ss_of ss) 1, ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} addcongs @{thms power_False_cong})), rewrite_goals_tac @{thms word_size}, diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/ex/Classical.thy --- a/src/HOL/ex/Classical.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOL/ex/Classical.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Classical - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge *) @@ -430,7 +429,7 @@ lemma "(\x y z. R(x,y) & R(y,z) --> R(x,z)) & (\x. \y. R(x,y)) --> ~ (\x. P x = (\y. R(x,y) --> ~ P y))" -by (tactic{*Meson.safe_best_meson_tac 1*}) +by (tactic{*Meson.safe_best_meson_tac @{claset} 1*}) --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*} @@ -724,7 +723,7 @@ (\x y. bird x & snail y \ ~eats x y) & (\x. (caterpillar x \ snail x) \ (\y. plant y & eats x y)) \ (\x y. animal x & animal y & (\z. grain z & eats y z & eats x y))" -by (tactic{*Meson.safe_best_meson_tac 1*}) +by (tactic{*Meson.safe_best_meson_tac @{claset} 1*}) --{*Nearly twice as fast as @{text meson}, which performs iterative deepening rather than best-first search*} diff -r 40a1865ab122 -r c3d1590debd8 src/HOLCF/IOA/ex/TrivEx.thy --- a/src/HOLCF/IOA/ex/TrivEx.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOLCF/IOA/ex/TrivEx.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/TrivEx.thy - ID: $Id$ Author: Olaf Müller *) @@ -66,7 +65,7 @@ apply (rule AbsRuleT1) apply (rule h_abs_is_abstraction) apply (rule MC_result) -apply (tactic "abstraction_tac 1") +apply abstraction apply (simp add: h_abs_def) done diff -r 40a1865ab122 -r c3d1590debd8 src/HOLCF/IOA/ex/TrivEx2.thy --- a/src/HOLCF/IOA/ex/TrivEx2.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOLCF/IOA/ex/TrivEx2.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/TrivEx.thy - ID: $Id$ Author: Olaf Müller *) @@ -85,7 +84,7 @@ txt {* is_abstraction *} apply (rule h_abs_is_abstraction) txt {* temp_weakening *} -apply (tactic "abstraction_tac 1") +apply abstraction apply (erule Enabled_implication) done @@ -96,7 +95,7 @@ apply (rule AbsRuleT2) apply (rule h_abs_is_liveabstraction) apply (rule MC_result) -apply (tactic "abstraction_tac 1") +apply abstraction apply (simp add: h_abs_def) done diff -r 40a1865ab122 -r c3d1590debd8 src/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Abstraction.thy - ID: $Id$ Author: Olaf Müller *) @@ -605,12 +604,15 @@ strength_Diamond strength_Leadsto weak_WF weak_SF ML {* -fun abstraction_tac i = - SELECT_GOAL (CLASIMPSET (fn (cs, ss) => - auto_tac (cs addSIs @{thms weak_strength_lemmas}, - ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))) i +fun abstraction_tac ctxt = + let val (cs, ss) = local_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 *} +method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} "" + use "ioa_package.ML" end diff -r 40a1865ab122 -r c3d1590debd8 src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Sequence.thy - ID: $Id$ Author: Olaf Müller Sequences over flat domains with lifted elements. @@ -340,7 +339,7 @@ lemma Seq_induct: "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x" apply (erule (2) seq.ind) -apply (tactic {* def_tac 1 *}) +apply defined apply (simp add: Consq_def) done @@ -348,14 +347,14 @@ "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] ==> seq_finite x --> P x" apply (erule (1) seq_finite_ind) -apply (tactic {* def_tac 1 *}) +apply defined apply (simp add: Consq_def) done lemma Seq_Finite_ind: "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x" apply (erule (1) Finite.induct) -apply (tactic {* def_tac 1 *}) +apply defined apply (simp add: Consq_def) done diff -r 40a1865ab122 -r c3d1590debd8 src/HOLCF/IOA/meta_theory/Traces.thy --- a/src/HOLCF/IOA/meta_theory/Traces.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy Fri Mar 20 15:24:18 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOLCF/IOA/meta_theory/Traces.thy - ID: $Id$ Author: Olaf Müller *) @@ -327,7 +326,7 @@ apply (simp (no_asm_simp)) apply (drule Finite_Last1 [THEN mp]) apply assumption -apply (tactic "def_tac 1") +apply defined done declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp] diff -r 40a1865ab122 -r c3d1590debd8 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/HOLCF/Lift.thy Fri Mar 20 15:24:18 2009 +0100 @@ -56,15 +56,13 @@ by (cases x) simp_all text {* - For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text + For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text x} by @{text "Def a"} in conclusion. *} -ML {* - local val lift_definedE = thm "lift_definedE" - in val def_tac = SIMPSET' (fn ss => - etac lift_definedE THEN' asm_simp_tac ss) - end; -*} +method_setup defined = {* + Scan.succeed (fn ctxt => SIMPLE_METHOD' + (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt))) +*} "" lemma DefE: "Def x = \ \ R" by simp diff -r 40a1865ab122 -r c3d1590debd8 src/Sequents/LK.thy --- a/src/Sequents/LK.thy Fri Mar 20 11:26:59 2009 +0100 +++ b/src/Sequents/LK.thy Fri Mar 20 15:24:18 2009 +0100 @@ -226,9 +226,9 @@ lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))" apply (rule_tac P = Q in cut) - apply (tactic {* simp_tac (simpset () addsimps @{thms if_P}) 2 *}) + apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *}) apply (rule_tac P = "~Q" in cut) - apply (tactic {* simp_tac (simpset() addsimps @{thms if_not_P}) 2 *}) + apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *}) apply (tactic {* fast_tac LK_pack 1 *}) done diff -r 40a1865ab122 -r c3d1590debd8 src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Fri Mar 20 11:26:59 2009 +0100 +++ b/src/ZF/int_arith.ML Fri Mar 20 15:24:18 2009 +0100 @@ -145,7 +145,7 @@ val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset))) + THEN ALLGOALS (asm_simp_tac (local_simpset_of (Simplifier.the_context ss))) val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) end;