eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
--- 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 \<notin> 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 = {*
--- 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
--- 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))",
"[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> <h$t,h'$t'> : 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));
--- 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 \<notin> 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 = {*
--- 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)
--- 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
--- 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
--- 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 \<notin> 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 = {*
--- 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*}
--- 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
--- 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
--- 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;
--- 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
--- 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
--- 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)
--- 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)])
--- 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 ****)
--- 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},
--- 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 "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
(\<forall>x. \<exists>y. R(x,y)) -->
~ (\<forall>x. P x = (\<forall>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 @@
(\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
(\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
\<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>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*}
--- 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
--- 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
--- 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
--- 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
--- 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]
--- 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 = \<bottom> \<Longrightarrow> R"
by simp
--- 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
--- 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;