# HG changeset patch # User huffman # Date 1237653775 25200 # Node ID be354d68c4e4e98be1974fb3a3e71e86c92cdd0a # Parent 4fbe1401bac208054fb9b8c64b447ecfdd42995c# Parent 620db300c038ca4eb5d3fc433cecbfc7ab2ee586 merged diff -r 4fbe1401bac2 -r be354d68c4e4 Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Sat Mar 21 03:24:35 2009 -0700 +++ b/Admin/isatest/isatest-stats Sat Mar 21 09:42:55 2009 -0700 @@ -31,6 +31,8 @@ HOL-UNITY \ HOL-Word \ HOL-ex \ + HOLCF \ + IOA \ ZF \ ZF-Constructible \ ZF-UNITY" diff -r 4fbe1401bac2 -r be354d68c4e4 Admin/isatest/settings/at-mac-poly-5.1-para --- a/Admin/isatest/settings/at-mac-poly-5.1-para Sat Mar 21 03:24:35 2009 -0700 +++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sat Mar 21 09:42:55 2009 -0700 @@ -4,7 +4,7 @@ ML_SYSTEM="polyml-5.2.1" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 200 --immutable 800" + ML_OPTIONS="--mutable 800 --immutable 2000" ISABELLE_HOME_USER=~/isabelle-at-mac-poly-e diff -r 4fbe1401bac2 -r be354d68c4e4 NEWS --- a/NEWS Sat Mar 21 03:24:35 2009 -0700 +++ b/NEWS Sat Mar 21 09:42:55 2009 -0700 @@ -685,6 +685,12 @@ Syntax.read_term_global etc.; see also OldGoals.read_term as last resort for legacy applications. +* Disposed old declarations, tactics, tactic combinators that refer to +the simpset or claset of an implicit theory (such as Addsimps, +Simp_tac, SIMPSET). INCOMPATIBILITY, should use @{simpset} etc. in +embedded ML text, or local_simpset_of with a proper context passed as +explicit runtime argument. + * Antiquotations: block-structured compilation context indicated by \ ... \; additional antiquotation forms: diff -r 4fbe1401bac2 -r be354d68c4e4 doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/doc-src/TutorialI/Protocol/Message.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 doc-src/TutorialI/Protocol/Public.thy --- a/doc-src/TutorialI/Protocol/Public.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/doc-src/TutorialI/Protocol/Public.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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_tac 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 4fbe1401bac2 -r be354d68c4e4 src/CCL/Type.thy --- a/src/CCL/Type.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/CCL/Type.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/FOL/blastdata.ML --- a/src/FOL/blastdata.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/FOL/blastdata.ML Sat Mar 21 09:42:55 2009 -0700 @@ -1,5 +1,5 @@ -(*** Applying BlastFun to create Blast_tac ***) +(*** Applying BlastFun to create blast_tac ***) structure Blast_Data = struct type claset = Cla.claset @@ -10,13 +10,10 @@ val contr_tac = Cla.contr_tac val dup_intr = Cla.dup_intr val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac - val claset = Cla.claset - val rep_cs = Cla.rep_cs + val rep_cs = Cla.rep_cs val cla_modifiers = Cla.cla_modifiers; val cla_meth' = Cla.cla_meth' end; structure Blast = BlastFun(Blast_Data); - -val Blast_tac = Blast.Blast_tac -and blast_tac = Blast.blast_tac; +val blast_tac = Blast.blast_tac; diff -r 4fbe1401bac2 -r be354d68c4e4 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/FOL/simpdata.ML Sat Mar 21 09:42:55 2009 -0700 @@ -117,8 +117,6 @@ val split_asm_tac = Splitter.split_asm_tac; val op addsplits = Splitter.addsplits; val op delsplits = Splitter.delsplits; -val Addsplits = Splitter.Addsplits; -val Delsplits = Splitter.Delsplits; (*** Standard simpsets ***) diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Auth/Message.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/HOL.thy Sat Mar 21 09:42:55 2009 -0700 @@ -1018,12 +1018,10 @@ val contr_tac = Classical.contr_tac val dup_intr = Classical.dup_intr val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac - val claset = Classical.claset val rep_cs = Classical.rep_cs val cla_modifiers = Classical.cla_modifiers val cla_meth' = Classical.cla_meth' ); -val Blast_tac = Blast.Blast_tac; val blast_tac = Blast.blast_tac; *} diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/IMPP/Hoare.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/SET-Protocol/Cardholder_Registration.thy --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/SET-Protocol/MessageSET.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/SET-Protocol/PublicSET.thy --- a/src/HOL/SET-Protocol/PublicSET.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/SET-Protocol/PublicSET.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/SET-Protocol/Purchase.thy --- a/src/HOL/SET-Protocol/Purchase.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/SET-Protocol/Purchase.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/SizeChange/sct.ML --- a/src/HOL/SizeChange/sct.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/SizeChange/sct.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Tools/cnf_funcs.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Tools/function_package/fundef_core.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Tools/function_package/mutual.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/Tools/function_package/scnp_reconstruct.ML --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/Tools/function_package/termination.ML --- a/src/HOL/Tools/function_package/termination.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Tools/function_package/termination.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Tools/meson.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Tools/simpdata.ML Sat Mar 21 09:42:55 2009 -0700 @@ -147,8 +147,6 @@ val op addsplits = Splitter.addsplits; val op delsplits = Splitter.delsplits; -val Addsplits = Splitter.Addsplits; -val Delsplits = Splitter.Delsplits; (* integration of simplifier with classical reasoner *) diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/UNITY/UNITY_tactics.ML Sat Mar 21 09:42:55 2009 -0700 @@ -59,6 +59,6 @@ th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]), th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])]; -Addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair}); - -Addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}); +Simplifier.change_simpset (fn ss => ss + addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair}) + addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map})); diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/Word/WordArith.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOL/ex/Classical.thy --- a/src/HOL/ex/Classical.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOL/ex/Classical.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/FOCUS/Buffer.thy --- a/src/HOLCF/FOCUS/Buffer.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/FOCUS/Buffer.thy Sat Mar 21 09:42:55 2009 -0700 @@ -98,8 +98,11 @@ by (erule subst, rule refl) ML {* -fun B_prover s tac eqs = prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1, - tac 1, auto_tac (claset(), simpset() addsimps eqs)]); +fun B_prover s tac eqs = + let val thy = the_context () in + prove_goal thy s (fn prems => [cut_facts_tac prems 1, + tac 1, auto_tac (claset_of thy, simpset_of thy addsimps eqs)]) + end; fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) []; fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs; diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/Modelcheck/Cockpit.thy --- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Sat Mar 21 09:42:55 2009 -0700 @@ -102,18 +102,18 @@ (* to prove, that info is always set at the recent alarm *) lemma cockpit_implements_Info_while_Al: "cockpit =<| Info_while_Al" -apply (tactic {* is_sim_tac (thms "aut_simps") 1 *}) +apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) done (* to prove that before any alarm arrives (and after each acknowledgment), info remains at None *) lemma cockpit_implements_Info_before_Al: "cockpit =<| Info_before_Al" -apply (tactic {* is_sim_tac (thms "aut_simps") 1 *}) +apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) done (* to prove that before any alarm would be acknowledged, it must be arrived *) lemma cockpit_implements_Al_before_Ack: "cockpit_hide =<| Al_before_Ack" -apply (tactic {* is_sim_tac (thms "aut_simps") 1 *}) +apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) apply auto done diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/Modelcheck/MuIOA.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Sat Mar 21 09:42:55 2009 -0700 @@ -278,14 +278,14 @@ by (REPEAT (rtac impI 1)); by (REPEAT (dtac eq_reflection 1)); (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *) -by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs) +by (full_simp_tac ((simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @ rename_simps @ ioa_simps @ asig_simps)) 1); by (full_simp_tac (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1); by (REPEAT (if_full_simp_tac - (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1)); + (simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1)); by (call_mucke_tac 1); (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *) by (atac 1); diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Sat Mar 21 09:42:55 2009 -0700 @@ -18,18 +18,18 @@ (* is_sim_tac makes additionally to call_sim_tac some simplifications, which are suitable for implementation realtion formulas *) -fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) => +fun is_sim_tac ss thm_list = SUBGOAL (fn (goal, i) => EVERY [REPEAT (etac thin_rl i), - simp_tac (simpset() addsimps [ioa_implements_def]) i, + simp_tac (ss addsimps [ioa_implements_def]) i, rtac conjI i, rtac conjI (i+1), TRY(call_sim_tac thm_list (i+2)), TRY(atac (i+2)), REPEAT(rtac refl (i+2)), - simp_tac (simpset() addsimps (thm_list @ + simp_tac (ss addsimps (thm_list @ comp_simps @ restrict_simps @ hide_simps @ rename_simps @ ioa_simps @ asig_simps)) (i+1), - simp_tac (simpset() addsimps (thm_list @ + simp_tac (ss addsimps (thm_list @ comp_simps @ restrict_simps @ hide_simps @ rename_simps @ ioa_simps @ asig_simps)) (i)]); diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/Modelcheck/Ring3.thy --- a/src/HOLCF/IOA/Modelcheck/Ring3.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy Sat Mar 21 09:42:55 2009 -0700 @@ -114,7 +114,7 @@ (* property to prove: at most one (of 3) members of the ring will declare itself to leader *) lemma at_most_one_leader: "ring =<| one_leader" -apply (tactic {* is_sim_tac (thms "aut_simps") 1 *}) +apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) apply auto done diff -r 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/ex/TrivEx.thy --- a/src/HOLCF/IOA/ex/TrivEx.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/ex/TrivEx.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/ex/TrivEx2.thy --- a/src/HOLCF/IOA/ex/TrivEx2.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/ex/TrivEx2.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/IOA/meta_theory/Traces.thy --- a/src/HOLCF/IOA/meta_theory/Traces.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/HOLCF/Lift.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/Provers/blast.ML --- a/src/Provers/blast.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Provers/blast.ML Sat Mar 21 09:42:55 2009 -0700 @@ -48,7 +48,6 @@ val contr_tac : int -> tactic val dup_intr : thm -> thm val hyp_subst_tac : bool -> int -> tactic - val claset : unit -> claset val rep_cs : (* dependent on classical.ML *) claset -> {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, @@ -77,7 +76,6 @@ val depth_tac : claset -> int -> int -> tactic val depth_limit : int Config.T val blast_tac : claset -> int -> tactic - val Blast_tac : int -> tactic val setup : theory -> theory (*debugging tools*) val stats : bool ref @@ -89,7 +87,7 @@ val instVars : term -> (unit -> unit) val toTerm : int -> term -> Term.term val readGoal : theory -> string -> term - val tryInThy : theory -> int -> string -> + val tryInThy : theory -> claset -> int -> string -> (int->tactic) list * branch list list * (int*int*exn) list val normBr : branch -> branch end; @@ -1283,7 +1281,6 @@ ((if !trace then warning ("blast: " ^ s) else ()); Seq.empty); -fun Blast_tac i = blast_tac (Data.claset()) i; (*** For debugging: these apply the prover to a subgoal and return @@ -1294,11 +1291,11 @@ (*Read a string to make an initial, singleton branch*) fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal; -fun tryInThy thy lim s = +fun tryInThy thy cs lim s = let val state as State {fullTrace = ft, ...} = initialize thy; val res = timeap prove - (state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I); + (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I); val _ = fullTrace := !ft; in res end; diff -r 4fbe1401bac2 -r be354d68c4e4 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Provers/clasimp.ML Sat Mar 21 09:42:55 2009 -0700 @@ -26,8 +26,6 @@ type clasimpset val get_css: Context.generic -> clasimpset val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic - val change_clasimpset: (clasimpset -> clasimpset) -> unit - val clasimpset: unit -> clasimpset val local_clasimpset_of: Proof.context -> clasimpset val addSIs2: clasimpset * thm list -> clasimpset val addSEs2: clasimpset * thm list -> clasimpset @@ -42,19 +40,10 @@ val addss': claset * simpset -> claset val addIffs: clasimpset * thm list -> clasimpset val delIffs: clasimpset * thm list -> clasimpset - val AddIffs: thm list -> unit - val DelIffs: thm list -> unit - val CLASIMPSET: (clasimpset -> tactic) -> tactic - val CLASIMPSET': (clasimpset -> 'a -> tactic) -> 'a -> tactic val clarsimp_tac: clasimpset -> int -> tactic - val Clarsimp_tac: int -> tactic val mk_auto_tac: clasimpset -> int -> int -> tactic val auto_tac: clasimpset -> tactic - val Auto_tac: tactic - val auto: unit -> unit val force_tac: clasimpset -> int -> tactic - val Force_tac: int -> tactic - val force: int -> unit val fast_simp_tac: clasimpset -> int -> tactic val slow_simp_tac: clasimpset -> int -> tactic val best_simp_tac: clasimpset -> int -> tactic @@ -84,9 +73,6 @@ let val (cs', ss') = f (get_css context) in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end; -fun change_clasimpset f = Context.>> (fn context => (Context.the_theory context; map_css f context)); -fun clasimpset () = (Classical.claset (), Simplifier.simpset ()); - fun local_clasimpset_of ctxt = (Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt); @@ -168,9 +154,6 @@ Simplifier.addsimps); val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps); -fun AddIffs thms = change_clasimpset (fn css => css addIffs thms); -fun DelIffs thms = change_clasimpset (fn css => css delIffs thms); - fun addIffs_generic (x, ths) = Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1; @@ -182,19 +165,10 @@ (* tacticals *) -fun CLASIMPSET tacf state = - Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state; - -fun CLASIMPSET' tacf i state = - Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state; - - fun clarsimp_tac (cs, ss) = safe_asm_full_simp_tac ss THEN_ALL_NEW Classical.clarify_tac (cs addSss ss); -fun Clarsimp_tac i = clarsimp_tac (clasimpset ()) i; - (* auto_tac *) @@ -231,8 +205,6 @@ end; fun auto_tac css = mk_auto_tac css 4 2; -fun Auto_tac st = auto_tac (clasimpset ()) st; -fun auto () = by Auto_tac; (* force_tac *) @@ -242,8 +214,6 @@ Classical.clarify_tac cs' 1, IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1), ALLGOALS (Classical.first_best_tac cs')]) end; -fun Force_tac i = force_tac (clasimpset ()) i; -fun force i = by (Force_tac i); (* basic combinations *) diff -r 4fbe1401bac2 -r be354d68c4e4 src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Provers/classical.ML Sat Mar 21 09:42:55 2009 -0700 @@ -69,11 +69,7 @@ val appSWrappers : claset -> wrapper val appWrappers : claset -> wrapper - val change_claset: (claset -> claset) -> unit val claset_of: theory -> claset - val claset: unit -> claset - val CLASET: (claset -> tactic) -> tactic - val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic val local_claset_of : Proof.context -> claset val fast_tac : claset -> int -> tactic @@ -107,24 +103,6 @@ val inst_step_tac : claset -> int -> tactic val inst0_step_tac : claset -> int -> tactic val instp_step_tac : claset -> int -> tactic - - val AddDs : thm list -> unit - val AddEs : thm list -> unit - val AddIs : thm list -> unit - val AddSDs : thm list -> unit - val AddSEs : thm list -> unit - val AddSIs : thm list -> unit - val Delrules : thm list -> unit - val Safe_tac : tactic - val Safe_step_tac : int -> tactic - val Clarify_tac : int -> tactic - val Clarify_step_tac : int -> tactic - val Step_tac : int -> tactic - val Fast_tac : int -> tactic - val Best_tac : int -> tactic - val Slow_tac : int -> tactic - val Slow_best_tac : int -> tactic - val Deepen_tac : int -> int -> tactic end; signature CLASSICAL = @@ -870,23 +848,9 @@ fun map_context_cs f = GlobalClaset.map (apsnd (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers)))); -fun change_claset f = Context.>> (Context.map_theory (map_claset f)); - fun claset_of thy = let val (cs, ctxt_cs) = GlobalClaset.get thy in context_cs (ProofContext.init thy) cs (ctxt_cs) end; -val claset = claset_of o ML_Context.the_global_context; - -fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st; -fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st; - -fun AddDs args = change_claset (fn cs => cs addDs args); -fun AddEs args = change_claset (fn cs => cs addEs args); -fun AddIs args = change_claset (fn cs => cs addIs args); -fun AddSDs args = change_claset (fn cs => cs addSDs args); -fun AddSEs args = change_claset (fn cs => cs addSEs args); -fun AddSIs args = change_claset (fn cs => cs addSIs args); -fun Delrules args = change_claset (fn cs => cs delrules args); (* context dependent components *) @@ -930,21 +894,6 @@ val rule_del = attrib delrule o ContextRules.rule_del; -(* tactics referring to the implicit claset *) - -(*the abstraction over the proof state delays the dereferencing*) -fun Safe_tac st = safe_tac (claset()) st; -fun Safe_step_tac i st = safe_step_tac (claset()) i st; -fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; -fun Clarify_tac i st = clarify_tac (claset()) i st; -fun Step_tac i st = step_tac (claset()) i st; -fun Fast_tac i st = fast_tac (claset()) i st; -fun Best_tac i st = best_tac (claset()) i st; -fun Slow_tac i st = slow_tac (claset()) i st; -fun Slow_best_tac i st = slow_best_tac (claset()) i st; -fun Deepen_tac m = deepen_tac (claset()) m; - - end; @@ -972,15 +921,12 @@ (** proof methods **) -fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt)); -fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); - - local -fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) => +fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => let val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt; + val CS {xtra_netpair, ...} = local_claset_of ctxt; val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair; val rules = rules1 @ rules2 @ rules3 @ rules4; val ruleq = Drule.multi_resolves facts rules; @@ -990,16 +936,15 @@ end) THEN_ALL_NEW Goal.norm_hhf_tac; -fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts - | rule_tac rules _ _ facts = Method.rule_tac rules facts; +in -fun default_tac rules ctxt cs facts = - HEADGOAL (rule_tac rules ctxt cs facts) ORELSE +fun rule_tac ctxt [] facts = some_rule_tac ctxt facts + | rule_tac _ rules facts = Method.rule_tac rules facts; + +fun default_tac ctxt rules facts = + HEADGOAL (rule_tac ctxt rules facts) ORELSE Class.default_intro_tac ctxt facts; -in - val rule = METHOD_CLASET' o rule_tac; - val default = METHOD_CLASET o default_tac; end; @@ -1033,9 +978,11 @@ (** setup_methods **) val setup_methods = - Method.setup @{binding default} (Attrib.thms >> default) + Method.setup @{binding default} + (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules))) "apply some intro/elim rule (potentially classical)" #> - Method.setup @{binding rule} (Attrib.thms >> rule) + Method.setup @{binding rule} + (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) "apply some intro/elim rule (potentially classical)" #> Method.setup @{binding contradiction} (Scan.succeed (K contradiction)) "proof by contradiction" #> diff -r 4fbe1401bac2 -r be354d68c4e4 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Provers/splitter.ML Sat Mar 21 09:42:55 2009 -0700 @@ -35,8 +35,6 @@ val split_asm_tac : thm list -> int -> tactic val addsplits : simpset * thm list -> simpset val delsplits : simpset * thm list -> simpset - val Addsplits : thm list -> unit - val Delsplits : thm list -> unit val split_add: attribute val split_del: attribute val split_modifiers : Method.modifier parser list @@ -453,9 +451,6 @@ in Simplifier.delloop (ss, split_name name asm) end in Library.foldl delsplit (ss,splits) end; -fun Addsplits splits = (change_simpset (fn ss => ss addsplits splits)); -fun Delsplits splits = (change_simpset (fn ss => ss delsplits splits)); - (* attributes *) diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/Concurrent/future.ML Sat Mar 21 09:42:55 2009 -0700 @@ -236,7 +236,7 @@ fun future_job group (e: unit -> 'a) = let val result = ref (NONE: 'a Exn.result option); - val job = Multithreading.with_attributes (Thread.getAttributes ()) + val job = Multithreading.with_attributes Multithreading.restricted_interrupts (fn _ => fn ok => let val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt; diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/General/antiquote.ML Sat Mar 21 09:42:55 2009 -0700 @@ -14,7 +14,7 @@ val is_antiq: 'a antiquote -> bool val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list - val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) -> + val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) -> Symbol_Pos.T list * Position.T -> 'a antiquote list end; @@ -83,13 +83,12 @@ (* read *) -fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos - | report_antiq _ = (); - -fun read _ ([], _) = [] - | read scanner (syms, pos) = +fun read _ _ ([], _) = [] + | read report scanner (syms, pos) = (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of - SOME xs => (List.app report_antiq xs; check_nesting xs; xs) + SOME xs => + (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs; + check_nesting xs; xs) | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); end; diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/General/markup.ML Sat Mar 21 09:42:55 2009 -0700 @@ -62,6 +62,14 @@ val propN: string val prop: T val attributeN: string val attribute: string -> T val methodN: string val method: string -> T + val ML_keywordN: string val ML_keyword: T + val ML_identN: string val ML_ident: T + val ML_tvarN: string val ML_tvar: T + val ML_numeralN: string val ML_numeral: T + val ML_charN: string val ML_char: T + val ML_stringN: string val ML_string: T + val ML_commentN: string val ML_comment: T + val ML_malformedN: string val ML_malformed: T val ML_sourceN: string val ML_source: T val doc_sourceN: string val doc_source: T val antiqN: string val antiq: T @@ -213,6 +221,18 @@ val (methodN, method) = markup_string "method" nameN; +(* ML syntax *) + +val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword"; +val (ML_identN, ML_ident) = markup_elem "ML_ident"; +val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar"; +val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; +val (ML_charN, ML_char) = markup_elem "ML_char"; +val (ML_stringN, ML_string) = markup_elem "ML_string"; +val (ML_commentN, ML_comment) = markup_elem "ML_comment"; +val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed"; + + (* embedded source text *) val (ML_sourceN, ML_source) = markup_elem "ML_source"; diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/General/markup.scala Sat Mar 21 09:42:55 2009 -0700 @@ -80,6 +80,18 @@ val DOC_ANTIQ = "doc_antiq" + /* ML syntax */ + + val ML_KEYWORD = "ML_keyword" + val ML_IDENT = "ML_ident" + val ML_TVAR = "ML_tvar" + val ML_NUMERAL = "ML_numeral" + val ML_CHAR = "ML_char" + val ML_STRING = "ML_string" + val ML_COMMENT = "ML_comment" + val ML_MALFORMED = "ML_malformed" + + /* outer syntax */ val KEYWORD_DECL = "keyword_decl" diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/ML-Systems/multithreading.ML --- a/src/Pure/ML-Systems/multithreading.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/ML-Systems/multithreading.ML Sat Mar 21 09:42:55 2009 -0700 @@ -21,6 +21,7 @@ val enabled: unit -> bool val no_interrupts: Thread.threadAttribute list val regular_interrupts: Thread.threadAttribute list + val restricted_interrupts: Thread.threadAttribute list val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b val self_critical: unit -> bool @@ -46,6 +47,9 @@ val regular_interrupts = [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]; +val restricted_interrupts = + [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce]; + fun with_attributes _ f x = f [] x; diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Mar 21 09:42:55 2009 -0700 @@ -69,6 +69,9 @@ val regular_interrupts = [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]; +val restricted_interrupts = + [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce]; + val safe_interrupts = map (fn Thread.InterruptState Thread.InterruptAsynch => Thread.InterruptState Thread.InterruptAsynchOnce diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/ML/ml_context.ML Sat Mar 21 09:42:55 2009 -0700 @@ -194,7 +194,7 @@ fun eval_antiquotes (txt, pos) opt_context = let val syms = Symbol_Pos.explode (txt, pos); - val ants = Antiquote.read ML_Lex.scan_antiq (syms, pos); + val ants = Antiquote.read ML_Lex.report_token ML_Lex.scan_antiq (syms, pos); val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context; val ((ml_env, ml_body), opt_ctxt') = if not (exists Antiquote.is_antiq ants) diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/ML/ml_lex.ML Sat Mar 21 09:42:55 2009 -0700 @@ -16,6 +16,8 @@ val pos_of: token -> string val kind_of: token -> token_kind val content_of: token -> string + val markup_of: token -> Markup.T + val report_token: token -> unit val keywords: string list val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list val source: (Symbol.symbol, 'a) Source.source -> @@ -74,6 +76,26 @@ | is_improper _ = false; +(* markup *) + +val markup_of = kind_of #> + (fn Keyword => Markup.ML_keyword + | Ident => Markup.ML_ident + | LongIdent => Markup.ML_ident + | TypeVar => Markup.ML_tvar + | Word => Markup.ML_numeral + | Int => Markup.ML_numeral + | Real => Markup.ML_numeral + | Char => Markup.ML_char + | String => Markup.ML_string + | Space => Markup.none + | Comment => Markup.ML_comment + | Error _ => Markup.ML_malformed + | EOF => Markup.none); + +fun report_token tok = Position.report (markup_of tok) (position_of tok); + + (** scanners **) diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/Thy/latex.ML Sat Mar 21 09:42:55 2009 -0700 @@ -117,7 +117,7 @@ else if T.is_kind T.Verbatim tok then let val (txt, pos) = T.source_position_of tok; - val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos); + val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos); val out = implode (map output_syms_antiq ants); in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end else output_syms s diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/Thy/thy_output.ML Sat Mar 21 09:42:55 2009 -0700 @@ -156,7 +156,7 @@ end | expand (Antiquote.Open _) = "" | expand (Antiquote.Close _) = ""; - val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos); + val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos); in if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos) diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/mk --- a/src/Pure/mk Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/mk Sat Mar 21 09:42:55 2009 -0700 @@ -92,6 +92,7 @@ -e "val ml_platform = \"$ML_PLATFORM\";" \ -e "use\"$COMPAT\" handle _ => exit 1;" \ -e "structure Isar = struct fun main () = () end;" \ + -e "ml_prompts \"ML> \" \"ML# \";" \ -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 RC="$?" elif [ -n "$RAW_SESSION" ]; then @@ -112,6 +113,7 @@ -e "val ml_system = \"$ML_SYSTEM\";" \ -e "val ml_platform = \"$ML_PLATFORM\";" \ -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ + -e "ml_prompts \"ML> \" \"ML# \";" \ -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 RC="$?" fi diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/pure_setup.ML Sat Mar 21 09:42:55 2009 -0700 @@ -50,6 +50,5 @@ (* misc *) val cd = File.cd o Path.explode; -ml_prompts "ML> " "ML# "; Proofterm.proofs := 0; diff -r 4fbe1401bac2 -r be354d68c4e4 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Pure/simplifier.ML Sat Mar 21 09:42:55 2009 -0700 @@ -10,15 +10,8 @@ include BASIC_META_SIMPLIFIER val change_simpset: (simpset -> simpset) -> unit val simpset_of: theory -> simpset - val simpset: unit -> simpset - val SIMPSET: (simpset -> tactic) -> tactic - val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic - val Addsimps: thm list -> unit - val Delsimps: thm list -> unit val Addsimprocs: simproc list -> unit val Delsimprocs: simproc list -> unit - val Addcongs: thm list -> unit - val Delcongs: thm list -> unit val local_simpset_of: Proof.context -> simpset val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic val safe_asm_full_simp_tac: simpset -> int -> tactic @@ -27,11 +20,6 @@ val full_simp_tac: simpset -> int -> tactic val asm_lr_simp_tac: simpset -> int -> tactic val asm_full_simp_tac: simpset -> int -> tactic - val Simp_tac: int -> tactic - val Asm_simp_tac: int -> tactic - val Full_simp_tac: int -> tactic - val Asm_lr_simp_tac: int -> tactic - val Asm_full_simp_tac: int -> tactic val simplify: simpset -> thm -> thm val asm_simplify: simpset -> thm -> thm val full_simplify: simpset -> thm -> thm @@ -138,17 +126,9 @@ fun map_simpset f = Context.theory_map (map_ss f); fun change_simpset f = Context.>> (Context.map_theory (map_simpset f)); fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy)); -val simpset = simpset_of o ML_Context.the_global_context; -fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st; -fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st; - -fun Addsimps args = change_simpset (fn ss => ss addsimps args); -fun Delsimps args = change_simpset (fn ss => ss delsimps args); fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args); fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args); -fun Addcongs args = change_simpset (fn ss => ss addcongs args); -fun Delcongs args = change_simpset (fn ss => ss delcongs args); (* local simpset *) @@ -283,13 +263,6 @@ val asm_full_simp_tac = generic_simp_tac false (true, true, true); val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true); -(*the abstraction over the proof state delays the dereferencing*) -fun Simp_tac i st = simp_tac (simpset ()) i st; -fun Asm_simp_tac i st = asm_simp_tac (simpset ()) i st; -fun Full_simp_tac i st = full_simp_tac (simpset ()) i st; -fun Asm_lr_simp_tac i st = asm_lr_simp_tac (simpset ()) i st; -fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st; - (* conversions *) diff -r 4fbe1401bac2 -r be354d68c4e4 src/Sequents/LK.thy --- a/src/Sequents/LK.thy Sat Mar 21 03:24:35 2009 -0700 +++ b/src/Sequents/LK.thy Sat Mar 21 09:42:55 2009 -0700 @@ -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 4fbe1401bac2 -r be354d68c4e4 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/ZF/Tools/inductive_package.ML Sat Mar 21 09:42:55 2009 -0700 @@ -16,7 +16,6 @@ dom_subset : thm, (*inclusion of recursive set in dom*) intrs : thm list, (*introduction rules*) elim : thm, (*case analysis theorem*) - mk_cases : string -> thm, (*generates case theorems*) induct : thm, (*main induction rule*) mutual_induct : thm}; (*mutual induction rule*) @@ -275,9 +274,6 @@ (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac) (Thm.assume A RS elim) |> Drule.standard'; - fun mk_cases a = make_cases (*delayed evaluation of body!*) - (simpset ()) - let val thy = Thm.theory_of_thm elim in cterm_of thy (Syntax.read_prop_global thy a) end; fun induction_rules raw_induct thy = let @@ -548,7 +544,6 @@ dom_subset = dom_subset', intrs = intrs'', elim = elim', - mk_cases = mk_cases, induct = induct, mutual_induct = mutual_induct}) end; diff -r 4fbe1401bac2 -r be354d68c4e4 src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Sat Mar 21 03:24:35 2009 -0700 +++ b/src/ZF/int_arith.ML Sat Mar 21 09:42:55 2009 -0700 @@ -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;