--- a/src/HOL/Arith.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Arith.ML Sat Mar 07 16:29:29 1998 +0100
@@ -433,12 +433,11 @@
qed "less_imp_diff_positive";
goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
-by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
- addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]) 1);
qed "if_Suc_diff_n";
goal Arith.thy "Suc(m)-n <= Suc(m-n)";
-by (simp_tac (simpset() addsimps [if_Suc_diff_n] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
qed "diff_Suc_le_Suc_diff";
goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
--- a/src/HOL/Auth/Event.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Event.ML Sat Mar 07 16:29:29 1998 +0100
@@ -46,22 +46,20 @@
qed "spies_subset_spies_Says";
goal thy "spies evs <= spies (Notes A X # evs)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Fast_tac 1);
qed "spies_subset_spies_Notes";
(*Spy sees all traffic*)
goal thy "Says A B X : set evs --> X : spies evs";
by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsplits [expand_event_case, expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
qed_spec_mp "Says_imp_spies";
(*Spy sees Notes of bad agents*)
goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsplits [expand_event_case, expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
qed_spec_mp "Notes_imp_spies";
(*Use with addSEs to derive contradictions from old Says events containing
@@ -80,7 +78,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [parts_insert_spies]
- addsplits [expand_event_case, expand_if])));
+ addsplits [expand_event_case])));
by (ALLGOALS Blast_tac);
qed "parts_spies_subset_used";
@@ -91,7 +89,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [parts_insert_spies]
- addsplits [expand_event_case, expand_if])));
+ addsplits [expand_event_case])));
by (ALLGOALS Blast_tac);
bind_thm ("initState_into_used", impOfSubs (result()));
--- a/src/HOL/Auth/Message.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Message.ML Sat Mar 07 16:29:29 1998 +0100
@@ -896,7 +896,7 @@
(REPEAT o CHANGED)
(res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
- simp_tac (simpset() addsplits [expand_if]) 1,
+ Simp_tac 1,
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
DEPTH_SOLVE
(Fake_insert_simp_tac 1
--- a/src/HOL/Auth/NS_Public.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/NS_Public.ML Sat Mar 07 16:29:29 1998 +0100
@@ -116,9 +116,9 @@
(*Tactic for proving secrecy theorems*)
-fun analz_induct_tac i =
+fun analz_induct_tac i =
etac ns_public.induct i THEN
- ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
+ ALLGOALS Asm_simp_tac;
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
--- a/src/HOL/Auth/NS_Public_Bad.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML Sat Mar 07 16:29:29 1998 +0100
@@ -122,7 +122,7 @@
(*Tactic for proving secrecy theorems*)
fun analz_induct_tac i =
etac ns_public.induct i THEN
- ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
+ ALLGOALS Asm_simp_tac;
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
--- a/src/HOL/Auth/Public.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Public.ML Sat Mar 07 16:29:29 1998 +0100
@@ -76,7 +76,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [imageI, spies_Cons]
- addsplits [expand_event_case, expand_if])));
+ addsplits [expand_event_case])));
qed_spec_mp "spies_pubK";
(*Spy sees private keys of bad agents!*)
@@ -84,7 +84,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [imageI, spies_Cons]
- addsplits [expand_event_case, expand_if])));
+ addsplits [expand_event_case])));
qed "Spy_spies_bad";
AddIffs [spies_pubK, spies_pubK RS analz.Inj];
@@ -132,7 +132,7 @@
by (res_inst_tac [("x","0")] exI 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [used_Cons]
- addsplits [expand_event_case, expand_if])));
+ addsplits [expand_event_case])));
by Safe_tac;
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
@@ -177,6 +177,5 @@
addsimps [image_insert RS sym, image_Un RS sym,
rangeI,
insert_Key_singleton,
- insert_Key_image, Un_assoc RS sym]
- addsplits [expand_if];
+ insert_Key_image, Un_assoc RS sym];
--- a/src/HOL/Auth/Shared.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Shared.ML Sat Mar 07 16:29:29 1998 +0100
@@ -51,7 +51,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [imageI, spies_Cons]
- addsplits [expand_event_case, expand_if])));
+ addsplits [expand_event_case])));
qed "Spy_spies_bad";
AddSIs [Spy_spies_bad];
@@ -125,7 +125,7 @@
by (res_inst_tac [("x","0")] exI 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [used_Cons]
- addsplits [expand_event_case, expand_if])));
+ addsplits [expand_event_case])));
by Safe_tac;
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
@@ -246,8 +246,7 @@
analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
insert_Key_singleton, subset_Compl_range,
Key_not_used, insert_Key_image, Un_assoc RS sym]
- @disj_comms)
- addsplits [expand_if];
+ @disj_comms);
(*Lemma for the trivial direction of the if-and-only-if*)
goal thy
--- a/src/HOL/Auth/TLS.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/TLS.ML Sat Mar 07 16:29:29 1998 +0100
@@ -145,7 +145,7 @@
REPEAT (FIRSTGOAL analz_mono_contra_tac)
THEN
fast_tac (claset() addss (simpset())) i THEN
- ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
+ ALLGOALS Asm_simp_tac;
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
@@ -193,14 +193,12 @@
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*)
ALLGOALS (asm_simp_tac
(simpset() addcongs [if_weak_cong]
- addsimps (expand_ifs@pushes)
- addsplits [expand_if])) THEN
+ addsimps (expand_ifs@pushes))) THEN
(*Remove instances of pubK B: the Spy already knows all public keys.
Combining the two simplifier calls makes them run extremely slowly.*)
ALLGOALS (asm_simp_tac
(simpset() addcongs [if_weak_cong]
- addsimps [insert_absorb]
- addsplits [expand_if]));
+ addsimps [insert_absorb]));
(*** Properties of items found in Notes ***)
--- a/src/HOL/Auth/Yahalom2.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Sat Mar 07 16:29:29 1998 +0100
@@ -216,8 +216,7 @@
by (ALLGOALS
(asm_simp_tac
(simpset() addsimps expand_ifs
- addsimps [analz_insert_eq, analz_insert_freshK]
- addsplits [expand_if])));
+ addsimps [analz_insert_eq, analz_insert_freshK])));
(*Oops*)
by (blast_tac (claset() addDs [unique_session_keys]) 3);
(*YM3*)
--- a/src/HOL/Divides.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Divides.ML Sat Mar 07 16:29:29 1998 +0100
@@ -229,7 +229,7 @@
goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
by (subgoal_tac "k mod 2 < 2" 1);
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
by Safe_tac;
qed "mod2_cases";
--- a/src/HOL/Finite.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Finite.ML Sat Mar 07 16:29:29 1998 +0100
@@ -257,7 +257,7 @@
by (SELECT_GOAL Safe_tac 1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (Blast_tac 1);
by (dtac sym 1);
by (rotate_tac ~1 1);
@@ -271,7 +271,7 @@
by (SELECT_GOAL Safe_tac 1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (Blast_tac 1);
by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
by (SELECT_GOAL Safe_tac 1);
@@ -285,7 +285,7 @@
by (SELECT_GOAL Safe_tac 1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Blast_tac 1);
val lemma = result();
@@ -341,9 +341,7 @@
goal Finite.thy "!!A B. [| finite A; finite B |]\
\ ==> A Int B = {} --> card(A Un B) = card A + card B";
by (etac finite_induct 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [Int_insert_left]
- addsplits [expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));
qed_spec_mp "card_Un_disjoint";
goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
--- a/src/HOL/IMP/Hoare.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/IMP/Hoare.ML Sat Mar 07 16:29:29 1998 +0100
@@ -61,13 +61,13 @@
(*Not suitable for rewriting: LOOPS!*)
goal Hoare.thy "wp (WHILE b DO c) Q s = \
\ (if b s then wp (c;WHILE b DO c) Q s else Q s)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
qed "wp_While_if";
goal thy
"wp (WHILE b DO c) Q s = \
\ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (rtac iffI 1);
by (rtac weak_coinduct 1);
by (etac CollectI 1);
--- a/src/HOL/Induct/Com.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/Com.ML Sat Mar 07 16:29:29 1998 +0100
@@ -54,7 +54,7 @@
goalw thy [assign_def] "s[s x/x] = s";
by (rtac ext 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
qed "assign_triv";
Addsimps [assign_same, assign_different, assign_triv];
--- a/src/HOL/Induct/LFilter.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/LFilter.ML Sat Mar 07 16:29:29 1998 +0100
@@ -98,7 +98,7 @@
Addsimps [find_LCons_seek];
goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
qed "find_LCons";
@@ -148,8 +148,7 @@
goal thy "lfilter p (LCons x l) = \
\ (if p x then LCons x (lfilter p l) else lfilter p l)";
-by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]
- addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]) 1);
qed "lfilter_LCons";
AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
@@ -193,7 +192,7 @@
goal thy "lfilter p (lfilter p l) = lfilter p l";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
by Safe_tac;
(*Cases: p x is true or false*)
by (rtac (lfilter_cases RS disjE) 1);
@@ -250,7 +249,7 @@
\ ==> l'' = LCons y l' --> \
\ (lfilter q l, LCons y (lfilter q l')) : findRel p";
by (etac findRel.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
qed_spec_mp "findRel_conj_lfilter";
@@ -291,7 +290,7 @@
goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
by (blast_tac (claset() addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
qed "lfilter_conj";
@@ -329,7 +328,7 @@
goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
by Safe_tac;
by (case_tac "lmap f l : Domain (findRel p)" 1);
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
--- a/src/HOL/Induct/Mutil.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/Mutil.ML Sat Mar 07 16:29:29 1998 +0100
@@ -92,7 +92,7 @@
goalw thy [evnodd_def]
"evnodd (insert (i,j) C) b = \
\ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "evnodd_insert";
@@ -107,8 +107,7 @@
by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
by (REPEAT_FIRST assume_tac);
(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
-by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]
- addsplits [expand_if]) 1
+by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1
THEN Blast_tac 1));
qed "domino_singleton";
--- a/src/HOL/Induct/Perm.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/Perm.ML Sat Mar 07 16:29:29 1998 +0100
@@ -41,7 +41,7 @@
goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
by (etac perm.induct 1);
by (Fast_tac 4);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
val perm_mem_lemma = result();
bind_thm ("perm_mem", perm_mem_lemma RS mp);
--- a/src/HOL/Induct/PropLog.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/PropLog.ML Sat Mar 07 16:29:29 1998 +0100
@@ -141,9 +141,7 @@
we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
by (PropLog.pl.induct_tac "p" 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
by (Fast_tac 1);
qed "hyps_Diff";
@@ -151,9 +149,7 @@
we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
by (PropLog.pl.induct_tac "p" 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
by (Fast_tac 1);
qed "hyps_insert";
@@ -174,7 +170,7 @@
goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
by (PropLog.pl.induct_tac "p" 1);
-by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Simp_tac);
by (Blast_tac 1);
qed "hyps_subset";
--- a/src/HOL/Induct/SList.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Induct/SList.ML Sat Mar 07 16:29:29 1998 +0100
@@ -317,12 +317,12 @@
goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "mem_append2";
goal SList.thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "mem_filter2";
--- a/src/HOL/Integ/Bin.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Integ/Bin.ML Sat Mar 07 16:29:29 1998 +0100
@@ -100,8 +100,6 @@
(**** The carry/borrow functions, bin_succ and bin_pred ****)
-val if_ss = simpset() addsplits [expand_if];
-
(**** integ_of_bin ****)
@@ -109,26 +107,26 @@
qed_goal "integ_of_bin_norm_Bcons" Bin.thy
"integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
(fn _ =>[(bin.induct_tac "w" 1),
- (ALLGOALS(simp_tac if_ss)) ]);
+ (ALLGOALS Simp_tac) ]);
qed_goal "integ_of_bin_succ" Bin.thy
"integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
(fn _ =>[(rtac bin.induct 1),
(ALLGOALS(asm_simp_tac
- (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
+ (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
qed_goal "integ_of_bin_pred" Bin.thy
"integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
(fn _ =>[(rtac bin.induct 1),
(ALLGOALS(asm_simp_tac
- (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
+ (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
qed_goal "integ_of_bin_minus" Bin.thy
"integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
(fn _ =>[(rtac bin.induct 1),
(Simp_tac 1),
(Simp_tac 1),
- (asm_simp_tac (if_ss
+ (asm_simp_tac (simpset()
delsimps [pred_Plus,pred_Minus,pred_Bcons]
addsimps [integ_of_bin_succ,integ_of_bin_pred,
zadd_assoc]) 1)]);
@@ -143,16 +141,16 @@
goal Bin.thy
"! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
by (bin.induct_tac "v" 1);
-by (simp_tac (if_ss addsimps bin_add_simps) 1);
-by (simp_tac (if_ss addsimps bin_add_simps) 1);
+by (simp_tac (simpset() addsimps bin_add_simps) 1);
+by (simp_tac (simpset() addsimps bin_add_simps) 1);
by (rtac allI 1);
by (bin.induct_tac "w" 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps)) 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
by (cut_inst_tac [("P","bool")] True_or_False 1);
by (etac disjE 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
val integ_of_bin_add_lemma = result();
goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
@@ -165,12 +163,12 @@
goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
by (bin.induct_tac "v" 1);
-by (simp_tac (if_ss addsimps bin_mult_simps) 1);
-by (simp_tac (if_ss addsimps bin_mult_simps) 1);
+by (simp_tac (simpset() addsimps bin_mult_simps) 1);
+by (simp_tac (simpset() addsimps bin_mult_simps) 1);
by (cut_inst_tac [("P","bool")] True_or_False 1);
by (etac disjE 1);
-by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
-by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @
+by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
+by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @
zadd_ac)) 1);
qed "integ_of_bin_mult";
--- a/src/HOL/Lambda/Eta.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lambda/Eta.ML Sat Mar 07 16:29:29 1998 +0100
@@ -50,7 +50,7 @@
by (Blast_tac 2);
by (asm_full_simp_tac (addsplit (simpset())) 2);
by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
- addsplits [expand_if,expand_nat_case]) 1);
+ addsplits [expand_nat_case]) 1);
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
qed "free_subst";
@@ -168,7 +168,7 @@
goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
by (dB.induct_tac "s" 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (SELECT_GOAL(safe_tac HOL_cs)1);
by (etac nat_neqE 1);
by (res_inst_tac [("x","Var nat")] exI 1);
@@ -179,7 +179,7 @@
by (assume_tac 2);
by (etac thin_rl 1);
by (res_inst_tac [("dB","t")] dB_case_distinction 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
by (Simp_tac 1);
by (Simp_tac 1);
@@ -195,7 +195,7 @@
by (etac exE 1);
by (etac rev_mp 1);
by (res_inst_tac [("dB","t")] dB_case_distinction 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (Simp_tac 1);
by (Blast_tac 1);
by (Simp_tac 1);
@@ -209,7 +209,7 @@
by (etac exE 1);
by (etac rev_mp 1);
by (res_inst_tac [("dB","t")] dB_case_distinction 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Blast_tac 1);
--- a/src/HOL/Lambda/Lambda.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lambda/Lambda.ML Sat Mar 07 16:29:29 1998 +0100
@@ -46,6 +46,7 @@
(*** subst and lift ***)
fun addsplit ss = ss addsimps [subst_Var]
+ delsplits [expand_if]
setloop (split_inside_tac [expand_if]);
goal Lambda.thy "(Var k)[u/k] = u";
@@ -66,8 +67,7 @@
goal Lambda.thy
"!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]
- addSolver cut_trans_tac)));
+by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
qed_spec_mp "lift_lift";
@@ -76,7 +76,7 @@
\ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
- addsplits [expand_if,expand_nat_case]
+ addsplits [expand_nat_case]
addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
@@ -88,7 +88,6 @@
\ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
- addsplits [expand_if]
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
@@ -96,7 +95,7 @@
goal Lambda.thy "!k s. (lift t k)[s/k] = t";
by (dB.induct_tac "t" 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_full_simp_tac);
qed "subst_lift";
Addsimps [subst_lift];
@@ -106,7 +105,9 @@
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac
(simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
- addsplits [expand_if,expand_nat_case]
+ delsplits [expand_if]
+ addsplits [expand_nat_case]
+ addloop ("if",split_inside_tac[expand_if])
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
--- a/src/HOL/Lex/AutoChopper.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lex/AutoChopper.ML Sat Mar 07 16:29:29 1998 +0100
@@ -18,7 +18,7 @@
goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
by (list.induct_tac "xs" 1);
by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
val accept_not_Nil = result() repeat_RS spec;
Addsimps [accept_not_Nil];
@@ -27,7 +27,7 @@
\ zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
by (list.induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (strip_tac 1);
by (rtac conjI 1);
by (Fast_tac 1);
@@ -53,17 +53,17 @@
\ acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
\ ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
+by (Asm_simp_tac 1);
by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
by (rename_tac "vss lrst" 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
by (res_inst_tac[("xs","vss")] list_eq_cases 1);
by (hyp_subst_tac 1);
by (Simp_tac 1);
by (fast_tac (claset() addSDs [no_acc]) 1);
by (hyp_subst_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
val step2_a = (result() repeat_RS spec) RS mp;
@@ -73,11 +73,11 @@
\ (if acc_prefix A st xs \
\ then ys ~= [] \
\ else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
by (rename_tac "vss lrst" 1);
by (Asm_simp_tac 1);
@@ -96,11 +96,11 @@
\ (if acc_prefix A st xs \
\ then ? g. ys=r@g & fin A (nexts A st g) \
\ else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (strip_tac 1);
by (rtac conjI 1);
by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
@@ -135,11 +135,11 @@
\ (if acc_prefix A st xs \
\ then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
\ else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
by (rename_tac "vss lrst" 1);
by (Asm_simp_tac 1);
@@ -164,7 +164,7 @@
by (Simp_tac 1);
by (rtac trans 1);
by (etac step2_a 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
val step2_d = (result() repeat_RS spec) RS mp;
Delsimps [split_paired_All];
@@ -174,11 +174,11 @@
\ (if acc_prefix A st xs \
\ then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
\ else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (strip_tac 1);
by (case_tac "acc_prefix A (next A st a) list" 1);
by (rtac conjI 1);
@@ -225,18 +225,18 @@
by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
by (rtac mp 1);
by (etac step2_b 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (rtac conjI 1);
by (rtac mp 1);
by (etac step2_c 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (rtac conjI 1);
- by (asm_simp_tac (simpset() addsimps [step2_a] addsplits [expand_if]) 1);
+ by (asm_simp_tac (simpset() addsimps [step2_a]) 1);
by (rtac conjI 1);
by (rtac mp 1);
by (etac step2_d 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (rtac mp 1);
by (etac step2_e 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
qed"auto_chopper_is_auto_chopper";
--- a/src/HOL/Lex/Regset_of_auto.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Lex/Regset_of_auto.ML Sat Mar 07 16:29:29 1998 +0100
@@ -23,15 +23,14 @@
goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
by (exhaust_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "butlast_empty";
AddIffs [butlast_empty];
goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
by (induct_tac "xss" 1);
by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
- addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps) 1);
by (rtac conjI 1);
by (Clarify_tac 1);
by (rtac conjI 1);
@@ -91,7 +90,7 @@
by (res_inst_tac[("x","a#pref")]exI 1);
by (res_inst_tac[("x","mids")]exI 1);
by (res_inst_tac[("x","suf")]exI 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
qed_spec_mp "decompose";
goal thy "!i. length(trace A i xs) = length xs";
@@ -137,7 +136,7 @@
\ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))";
by (induct_tac "xs" 1);
by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [insert_commute]) 1);
qed "set_trace_conv";
goal thy
@@ -157,8 +156,7 @@
"!i j xs. xs : regset_of A i j k = \
\ ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
by (induct_tac "k" 1);
- by (simp_tac (simpset() addcongs [conj_cong]
- addsplits [expand_if,split_list_case]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong] addsplits [split_list_case]) 1);
by (strip_tac 1);
by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
by (rtac iffI 1);
@@ -168,12 +166,10 @@
by (Asm_full_simp_tac 1);
by (subgoal_tac
"(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1);
- by (asm_simp_tac (simpset() addsplits [expand_if]
- addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
+ by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
by (etac star.induct 1);
by (Simp_tac 1);
- by (asm_full_simp_tac (simpset() addsplits [expand_if]
- addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
by (case_tac "k : set(butlast(trace A i xs))" 1);
by (rtac disjI1 2);
by (blast_tac (claset() addIs [lemma]) 2);
--- a/src/HOL/List.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/List.ML Sat Mar 07 16:29:29 1998 +0100
@@ -311,13 +311,13 @@
goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "mem_append";
Addsimps[mem_append];
goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "mem_filter";
Addsimps[mem_filter];
@@ -333,7 +333,7 @@
goal thy "(x mem xs) = (x: set xs)";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
qed "set_mem_eq";
@@ -368,7 +368,7 @@
goal thy "(x : set(filter P xs)) = (x : set xs & P x)";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by(Blast_tac 1);
qed "in_set_filter";
Addsimps [in_set_filter];
@@ -392,7 +392,7 @@
goal thy "list_all P xs = (!x. x mem xs --> P(x))";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
qed "list_all_mem_conv";
@@ -403,7 +403,7 @@
goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
by (induct_tac "xs" 1);
- by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "filter_append";
Addsimps [filter_append];
@@ -421,7 +421,7 @@
goal thy "length (filter P xs) <= length xs";
by (induct_tac "xs" 1);
- by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "length_filter";
@@ -512,7 +512,7 @@
(* case 0 *)
by (Asm_full_simp_tac 1);
(* case Suc x *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_full_simp_tac 1);
qed_spec_mp "nth_mem";
Addsimps [nth_mem];
@@ -565,42 +565,40 @@
goal thy "last(xs@[x]) = x";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "last_snoc";
Addsimps [last_snoc];
goal thy "butlast(xs@[x]) = xs";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "butlast_snoc";
Addsimps [butlast_snoc];
goal thy "length(butlast xs) = length xs - 1";
-by(res_inst_tac [("xs","xs")] snoc_induct 1);
-by(ALLGOALS Asm_simp_tac);
+by (res_inst_tac [("xs","xs")] snoc_induct 1);
+by (ALLGOALS Asm_simp_tac);
qed "length_butlast";
Addsimps [length_butlast];
goal thy
"!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
by (induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed_spec_mp "butlast_append";
goal thy "x:set(butlast xs) --> x:set xs";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed_spec_mp "in_set_butlastD";
goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
-by (asm_simp_tac (simpset() addsimps [butlast_append]
- addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
by (blast_tac (claset() addDs [in_set_butlastD]) 1);
qed "in_set_butlast_appendI1";
goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
-by (asm_simp_tac (simpset() addsimps [butlast_append]
- addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
by (Clarify_tac 1);
by (Full_simp_tac 1);
qed "in_set_butlast_appendI2";
@@ -751,15 +749,13 @@
goal thy "takeWhile P xs @ dropWhile P xs = xs";
by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
qed "takeWhile_dropWhile_id";
Addsimps [takeWhile_dropWhile_id];
goal thy "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
by (Blast_tac 1);
bind_thm("takeWhile_append1", conjI RS (result() RS mp));
Addsimps [takeWhile_append1];
@@ -767,16 +763,14 @@
goal thy
"(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
bind_thm("takeWhile_append2", ballI RS (result() RS mp));
Addsimps [takeWhile_append2];
goal thy
"x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
by (Blast_tac 1);
bind_thm("dropWhile_append1", conjI RS (result() RS mp));
Addsimps [dropWhile_append1];
@@ -784,15 +778,13 @@
goal thy
"(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
bind_thm("dropWhile_append2", ballI RS (result() RS mp));
Addsimps [dropWhile_append2];
goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
qed_spec_mp"set_take_whileD";
qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]);
@@ -805,21 +797,18 @@
goal thy "set(remdups xs) = set xs";
by (induct_tac "xs" 1);
by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [insert_absorb]
- addsplits [expand_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1);
qed "set_remdups";
Addsimps [set_remdups];
goal thy "nodups(remdups xs)";
by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
qed "nodups_remdups";
goal thy "nodups xs --> nodups (filter P xs)";
by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_full_simp_tac);
qed_spec_mp "nodups_filter";
(** replicate **)
--- a/src/HOL/Map.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Map.ML Sat Mar 07 16:29:29 1998 +0100
@@ -21,7 +21,7 @@
qed_goal "update_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
(K [Asm_simp_tac 1]);
qed_goal "update_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
- (K [rtac ext 1, asm_simp_tac (simpset() addsplits [expand_if]) 1]);
+ (K [rtac ext 1, Asm_simp_tac 1]);
(*Addsimps [update_same, update_other, update_triv];*)
section "++";
@@ -56,14 +56,14 @@
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (rtac ext 1);
-by (asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
+by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
qed "map_of_append";
Addsimps [map_of_append];
goal thy "map_of xs k = Some y --> (k,y):set xs";
by (list.induct_tac "xs" 1);
by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
by (split_all_tac 1);
by (Simp_tac 1);
qed_spec_mp "map_of_SomeD";
@@ -76,7 +76,7 @@
Addsimps [dom_empty];
goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "dom_update";
Addsimps [dom_update];
--- a/src/HOL/MiniML/Generalize.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/Generalize.ML Sat Mar 07 16:29:29 1998 +0100
@@ -45,8 +45,8 @@
by (typ.induct_tac "t1" 1);
by (Simp_tac 1);
by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
by (Fast_tac 1);
by (Asm_simp_tac 1);
by (Fast_tac 1);
@@ -97,7 +97,7 @@
by (rename_tac "R" 1);
by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
by (typ.induct_tac "t" 1);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "gen_bound_typ_instance";
@@ -107,7 +107,7 @@
by (rename_tac "S" 1);
by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
by (typ.induct_tac "t" 1);
- by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Asm_simp_tac 1);
by (Fast_tac 1);
by (Asm_simp_tac 1);
qed "free_tv_subset_gen_le";
@@ -121,8 +121,8 @@
by (typ.induct_tac "t" 1);
by (Simp_tac 1);
by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
by (subgoal_tac "n <= n + nat" 1);
by (forw_inst_tac [("t","A")] new_tv_le 1);
by (assume_tac 1);
--- a/src/HOL/MiniML/Instance.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/Instance.ML Sat Mar 07 16:29:29 1998 +0100
@@ -66,8 +66,8 @@
by (rename_tac "S1 S2" 1);
by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
by Safe_tac;
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
by (strip_tac 1);
by (dres_inst_tac [("x","x")] bspec 1);
by (assume_tac 1);
@@ -82,8 +82,8 @@
goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
\ (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
by (type_scheme.induct_tac "sch" 1);
-by (simp_tac (simpset() addsimps [leD] addsplits [expand_if]) 1);
-by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [leD]) 1);
+by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
by (Asm_simp_tac 1);
qed_spec_mp "subst_to_scheme_inverse";
@@ -96,9 +96,9 @@
\ (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
\ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
by (type_scheme.induct_tac "sch" 1);
-by (simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1);
+by (simp_tac (simpset() addsimps [leD]) 1);
by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1);
+by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
val aux2 = result () RS mp;
--- a/src/HOL/MiniML/MiniML.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/MiniML.ML Sat Mar 07 16:29:29 1998 +0100
@@ -82,7 +82,7 @@
goalw thy [free_tv_subst,dom_def]
"!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
\ free_tv A Un free_tv t";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Fast_tac 1);
qed "dom_S'";
@@ -110,7 +110,7 @@
\ (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
\ {x. ? y. x = n + y}";
by (typ.induct_tac "t1" 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Fast_tac 1);
by (Simp_tac 1);
by (Fast_tac 1);
--- a/src/HOL/MiniML/Type.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/Type.ML Sat Mar 07 16:29:29 1998 +0100
@@ -352,7 +352,7 @@
goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
by (type_scheme.induct_tac "sch" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by (strip_tac 1);
by (Fast_tac 1);
qed "free_tv_ML_scheme";
@@ -423,14 +423,14 @@
goal thy
"new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
by (typ.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "subst_te_new_tv";
Addsimps [subst_te_new_tv];
goal thy
"new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
by (type_scheme.induct_tac "sch" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed_spec_mp "subst_te_new_type_scheme";
Addsimps [subst_te_new_type_scheme];
@@ -547,13 +547,13 @@
Addsimps [new_tv_not_free_tv];
goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by Safe_tac;
by (trans_tac 1);
qed "less_maxL";
goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1);
val less_maxR = result();
@@ -586,11 +586,11 @@
Addsimps [fresh_variable_type_schemes];
goalw thy [max_def] "!!n::nat. n <= (max n n')";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
val le_maxL = result();
goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
val le_maxR = result();
--- a/src/HOL/MiniML/W.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/MiniML/W.ML Sat Mar 07 16:29:29 1998 +0100
@@ -18,7 +18,7 @@
"!A n S t m. W e A n = Some (S,t,m) --> n<=m";
by (expr.induct_tac "e" 1);
(* case Var(n) *)
-by (simp_tac (simpset() addsplits [split_option_bind,expand_if]) 1);
+by (simp_tac (simpset() addsplits [split_option_bind]) 1);
(* case Abs e *)
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
@@ -58,7 +58,7 @@
by (assume_tac 2);
by (rtac add_le_mono 1);
by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if] addsimps [max_def]) 1);
+by (simp_tac (simpset() addsimps [max_def]) 1);
by (strip_tac 1);
by (rtac new_tv_le 1);
by (mp_tac 2);
@@ -66,7 +66,7 @@
by (assume_tac 2);
by (rtac add_le_mono 1);
by (Simp_tac 1);
-by (simp_tac (simpset() addsplits [expand_if] addsimps [max_def]) 1);
+by (simp_tac (simpset() addsimps [max_def]) 1);
by (strip_tac 1);
by (dtac not_leE 1);
by (rtac less_or_eq_imp_le 1);
@@ -81,7 +81,7 @@
\ new_tv m S & new_tv m t";
by (expr.induct_tac "e" 1);
(* case Var n *)
-by (simp_tac (simpset() addsplits [split_option_bind,expand_if]) 1);
+by (simp_tac (simpset() addsplits [split_option_bind]) 1);
by (strip_tac 1);
by (dtac new_tv_nth_nat_A 1);
by (assume_tac 1);
@@ -178,7 +178,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (simp_tac (simpset() addsimps
- [free_tv_subst] addsplits [split_option_bind,expand_if]) 1);
+ [free_tv_subst] addsplits [split_option_bind]) 1);
by (strip_tac 1);
by (case_tac "v : free_tv (A!nat)" 1);
by (Asm_full_simp_tac 1);
@@ -272,7 +272,7 @@
"!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
by (expr.induct_tac "e" 1);
(* case Var n *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_full_simp_tac 1);
by (strip_tac 1);
by (rtac has_type.VarI 1);
by (Simp_tac 1);
@@ -396,7 +396,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (strip_tac 1);
-by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (eresolve_tac has_type_casesE 1);
by (asm_full_simp_tac (simpset() addsimps [is_bound_typ_instance]) 1);
by (etac exE 1);
@@ -457,7 +457,7 @@
by (case_tac "na:free_tv Sa" 2);
(* n1 ~: free_tv S1 *)
by (forward_tac [not_free_impl_id] 3);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 3);
+by (Asm_simp_tac 3);
(* na : free_tv Sa *)
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
by (dtac eq_subst_scheme_list_eq_free 2);
@@ -465,7 +465,7 @@
by (Asm_simp_tac 2);
by (case_tac "na:dom Sa" 2);
(* na ~: dom Sa *)
-by (asm_full_simp_tac (simpset() addsimps [dom_def] addsplits [expand_if]) 3);
+by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
(* na : dom Sa *)
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2);
@@ -476,8 +476,7 @@
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss
(simpset() addsimps [cod_def,free_tv_subst])) 3);
-by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst]
- addsplits [expand_if])) 2);
+by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
by (Simp_tac 2);
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2 );
@@ -488,10 +487,10 @@
by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
by (case_tac "na: free_tv t - free_tv Sa" 2);
(* case na ~: free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 3);
+by (Asm_full_simp_tac 3);
by (Fast_tac 3);
(* case na : free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
+by (Asm_full_simp_tac 2);
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
by (dtac eq_subst_scheme_list_eq_free 2);
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
@@ -527,9 +526,9 @@
new_tv_not_free_tv]) 2);
by (case_tac "na: free_tv t - free_tv Sa" 1);
(* case na ~: free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
+by (Asm_full_simp_tac 2);
(* case na : free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_full_simp_tac 1);
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
eq_subst_scheme_list_eq_free] addss ((simpset() addsimps
--- a/src/HOL/Nat.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Nat.ML Sat Mar 07 16:29:29 1998 +0100
@@ -15,7 +15,6 @@
qed "min_0R";
goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
-by (split_tac [expand_if] 1);
by (Simp_tac 1);
qed "min_Suc_Suc";
--- a/src/HOL/NatDef.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/NatDef.ML Sat Mar 07 16:29:29 1998 +0100
@@ -599,12 +599,12 @@
(** max
goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
qed "le_max_iff_disj";
goalw thy [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
qed "max_le_iff_conj";
@@ -612,12 +612,12 @@
(** min **)
goalw thy [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
qed "le_min_iff_conj";
goalw thy [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)";
-by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits) 1);
by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
qed "min_le_iff_disj";
**)
--- a/src/HOL/Ord.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Ord.ML Sat Mar 07 16:29:29 1998 +0100
@@ -43,14 +43,12 @@
(** min **)
goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
-by (split_tac [expand_if] 1);
by (Asm_simp_tac 1);
qed "min_leastL";
val prems = goalw thy [min_def]
"(!!x::'a::order. least <= x) ==> min x least = least";
by (cut_facts_tac prems 1);
-by (split_tac [expand_if] 1);
by (Asm_simp_tac 1);
by (blast_tac (claset() addIs [order_antisym]) 1);
qed "min_leastR";
@@ -65,25 +63,25 @@
qed "linorder_less_linear";
goalw thy [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
-by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by (Simp_tac 1);
by(cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "le_max_iff_disj";
goalw thy [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
-by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by (Simp_tac 1);
by(cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "max_le_iff_conj";
goalw thy [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
-by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by (Simp_tac 1);
by(cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "le_min_iff_conj";
goalw thy [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
-by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by (Simp_tac 1);
by(cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "min_le_iff_disj";
--- a/src/HOL/Set.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Set.ML Sat Mar 07 16:29:29 1998 +0100
@@ -664,7 +664,7 @@
(*Not for Addsimps -- it can cause goals to blow up!*)
goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
qed "mem_if";
val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
--- a/src/HOL/Subst/Subst.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Subst/Subst.ML Sat Mar 07 16:29:29 1998 +0100
@@ -41,7 +41,7 @@
qed "agreement";
goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
-by (simp_tac (simpset() addsimps [agreement] addsplits [expand_if]) 1);
+by (simp_tac (simpset() addsimps [agreement]) 1);
qed_spec_mp"repl_invariance";
val asms = goal Subst.thy
@@ -111,7 +111,7 @@
by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
by (alist_ind_tac "r" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "subst_comp";
Addsimps [subst_comp];
@@ -130,7 +130,7 @@
by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
by (rtac allI 1);
by (induct_tac "t" 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_full_simp_tac);
qed "Cons_trivial";
@@ -143,7 +143,7 @@
goal Subst.thy "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
by (alist_ind_tac "s" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
qed "sdom_iff";
@@ -203,7 +203,7 @@
goal Subst.thy "(M <| [(x, Var x)]) = M";
by (induct_tac "M" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "id_subst_lemma";
Addsimps [id_subst_lemma];
--- a/src/HOL/Subst/Unifier.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Subst/Unifier.ML Sat Mar 07 16:29:29 1998 +0100
@@ -82,8 +82,7 @@
goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff,
- empty_iff_all_not]
- addsplits [expand_if]) 1);
+ empty_iff_all_not]) 1);
by (Blast_tac 1);
qed_spec_mp "Var_Idem";
--- a/src/HOL/Subst/Unify.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Subst/Unify.ML Sat Mar 07 16:29:29 1998 +0100
@@ -153,8 +153,7 @@
(* Apply induction *)
by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
by (ALLGOALS
- (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0)
- addsplits [expand_if])));
+ (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0))));
(*Const-Const case*)
by (simp_tac
(simpset() addsimps [unifyRel_def, lex_prod_def, measure_def,
@@ -207,7 +206,7 @@
goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
(*Const-Const case*)
by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1);
(*Const-Var case*)
@@ -245,8 +244,7 @@
by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
by (ALLGOALS
(asm_simp_tac
- (simpset() addsimps [Var_Idem]
- addsplits [expand_if,split_option_case])));
+ (simpset() addsimps [Var_Idem] addsplits [split_option_case])));
(*Comb-Comb case*)
by Safe_tac;
by (REPEAT (dtac spec 1 THEN mp_tac 1));
--- a/src/HOL/W0/I.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/W0/I.ML Sat Mar 07 16:29:29 1998 +0100
@@ -144,7 +144,7 @@
goal I.thy "!a m s. \
\ new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
by (expr.induct_tac "e" 1);
- by (simp_tac (simpset() addsimps [app_subst_list] addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addsimps [app_subst_list]) 1);
by (Simp_tac 1);
by (strip_tac 1);
by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
--- a/src/HOL/W0/Type.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/W0/Type.ML Sat Mar 07 16:29:29 1998 +0100
@@ -157,7 +157,7 @@
goal thy
"new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
by (typ.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "subst_te_new_tv";
Addsimps [subst_te_new_tv];
@@ -259,7 +259,7 @@
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
-by (fast_tac (set_cs addss(simpset() addsplits [expand_if])) 1);
+by (fast_tac (set_cs addss simpset()) 1);
qed_spec_mp "ftv_mem_sub_ftv_list";
Addsimps [ftv_mem_sub_ftv_list];
--- a/src/HOL/W0/W.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/W0/W.ML Sat Mar 07 16:29:29 1998 +0100
@@ -14,7 +14,7 @@
"!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
by (expr.induct_tac "e" 1);
(* case Var n *)
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
(* case Abs e *)
by (asm_full_simp_tac (simpset() addsimps [app_subst_list]
addsplits [expand_bind]) 1);
@@ -45,7 +45,7 @@
"!a n s t m. W e a n = Ok (s,t,m) --> n<=m";
by (expr.induct_tac "e" 1);
(* case Var(n) *)
-by (fast_tac (HOL_cs addss(simpset() addsplits [expand_if])) 1);
+by (fast_tac (HOL_cs addss simpset()) 1);
(* case Abs e *)
by (simp_tac (simpset() addsplits [expand_bind]) 1);
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
@@ -91,8 +91,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset()
- addsimps [id_subst_def,new_tv_list,new_tv_subst]
- addsplits [expand_if])) 1);
+ addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1);
(* case Abs e *)
by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list]
addsplits [expand_bind]) 1);
@@ -159,7 +158,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list]
- addss (simpset() addsplits [expand_if])) 1);
+ addss simpset()) 1);
(* case Abs e *)
by (asm_full_simp_tac (simpset() addsimps
@@ -225,8 +224,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (strip_tac 1);
-by (simp_tac (simpset() addcongs [conj_cong]
- addsplits [expand_if]) 1);
+by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (eresolve_tac has_type_casesE 1);
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv,app_subst_list]) 1);
by (res_inst_tac [("x","s'")] exI 1);
@@ -284,7 +282,7 @@
by (case_tac "na:free_tv sa" 2);
(* na ~: free_tv sa *)
by (forward_tac [not_free_impl_id] 3);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 3);
+by (Asm_simp_tac 3);
(* na : free_tv sa *)
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
by (dtac eq_subst_tel_eq_free 2);
@@ -293,8 +291,7 @@
by (case_tac "na:dom sa" 2);
(* na ~: dom sa *)
(** LEVEL 50 **)
-by (asm_full_simp_tac (simpset() addsimps [dom_def]
- addsplits [expand_if]) 3);
+by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
(* na : dom sa *)
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2);
@@ -305,8 +302,7 @@
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss
(simpset() addsimps [cod_def,free_tv_subst])) 3);
-by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst]
- addsplits [expand_if])) 2);
+by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
(** LEVEL 60 **)
by (Simp_tac 2);
@@ -320,9 +316,9 @@
by (case_tac "na: free_tv t - free_tv sa" 2);
(** LEVEL 69 **)
(* case na ~: free_tv t - free_tv sa *)
-by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 3);
+by (Asm_full_simp_tac 3);
(* case na : free_tv t - free_tv sa *)
-by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
+by (Asm_full_simp_tac 2);
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
by (dtac eq_subst_tel_eq_free 2);
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
@@ -358,9 +354,9 @@
new_tv_not_free_tv]) 2);
by (case_tac "na: free_tv t - free_tv sa" 1);
(* case na ~: free_tv t - free_tv sa *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
+by (Asm_full_simp_tac 2);
(* case na : free_tv t - free_tv sa *)
-by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_full_simp_tac 1);
by (dtac (free_tv_app_subst_tel RS subsetD) 1);
by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
eq_subst_tel_eq_free]
--- a/src/HOL/WF.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/WF.ML Sat Mar 07 16:29:29 1998 +0100
@@ -153,7 +153,7 @@
H_cong to expose the equality*)
goalw WF.thy [cut_def]
"(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
-by (simp_tac (HOL_ss addsimps [expand_fun_eq] addsplits [expand_if]) 1);
+by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
qed "cuts_eq";
goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
@@ -193,8 +193,7 @@
and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
by (cut_facts_tac prems 1);
by (rtac ext 1);
-by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
- addsplits [expand_if]) 1);
+by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1);
qed "is_recfun_cut";
(*** Main Existence Lemma -- Basic Properties of the_recfun ***)
--- a/src/HOL/equalities.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/equalities.ML Sat Mar 07 16:29:29 1998 +0100
@@ -115,7 +115,7 @@
goalw thy [image_def]
"(%x. if P x then f x else g x) `` S \
\ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
-by (split_tac [expand_if] 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "if_image_distrib";
Addsimps[if_image_distrib];
@@ -275,13 +275,13 @@
goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
\ else B Int C)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "Int_insert_left";
goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
\ else A Int B)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "Int_insert_right";
@@ -612,7 +612,7 @@
qed "Diff_insert2";
goal thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "insert_Diff_if";
--- a/src/HOL/ex/Fib.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Fib.ML Sat Mar 07 16:29:29 1998 +0100
@@ -58,8 +58,7 @@
by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
by (ALLGOALS (*using fib.rules here results in a longer proof!*)
(asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2,
- mod_less, mod_Suc]
- addsplits [expand_if])));
+ mod_less, mod_Suc])));
by (ALLGOALS
(asm_full_simp_tac
(simpset() addsimps (fib.rules @ add_ac @ mult_ac @
--- a/src/HOL/ex/InSort.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/InSort.ML Sat Mar 07 16:29:29 1998 +0100
@@ -8,8 +8,7 @@
goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
by (list.induct_tac "xs" 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (ALLGOALS Asm_simp_tac);
qed "mset_ins";
Addsimps [mset_ins];
@@ -19,8 +18,7 @@
qed "insort_permutes";
goal thy "set(ins f x xs) = insert x (set xs)";
-by (asm_simp_tac (simpset() addsimps [set_via_mset]
- addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsimps [set_via_mset]) 1);
by (Fast_tac 1);
qed "set_ins";
Addsimps [set_ins];
@@ -28,7 +26,7 @@
val prems = goalw InSort.thy [total_def,transf_def]
"[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs";
by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by (cut_facts_tac prems 1);
by (Fast_tac 1);
qed "sorted_ins";
--- a/src/HOL/ex/Primes.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Primes.ML Sat Mar 07 16:29:29 1998 +0100
@@ -36,7 +36,7 @@
goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
by (rtac (gcd_eq RS trans) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
by (Blast_tac 1);
qed "gcd_less_0";
Addsimps [gcd_0, gcd_less_0];
--- a/src/HOL/ex/Qsort.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Qsort.ML Sat Mar 07 16:29:29 1998 +0100
@@ -26,7 +26,7 @@
goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "qsort_permutes";
goal Qsort.thy "set(qsort le xs) = set xs";
@@ -37,7 +37,7 @@
goal List.thy
"(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed"Ball_set_filter";
Addsimps [Ball_set_filter];
--- a/src/HOL/ex/Recdef.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Recdef.ML Sat Mar 07 16:29:29 1998 +0100
@@ -13,7 +13,7 @@
goal thy "(x mem qsort (ord,l)) = (x mem l)";
by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
qed "qsort_mem_stable";
--- a/src/HOL/ex/Sorting.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Sorting.ML Sat Mar 07 16:29:29 1998 +0100
@@ -8,20 +8,20 @@
goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "mset_append";
goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
\ mset xs x";
by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
qed "mset_compl_add";
Addsimps [mset_append, mset_compl_add];
goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS Asm_simp_tac);
by (Fast_tac 1);
qed "set_via_mset";
--- a/src/HOL/ex/set.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/set.ML Sat Mar 07 16:29:29 1998 +0100
@@ -81,7 +81,7 @@
goalw Lfp.thy [image_def]
"range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "range_if_then_else";