--- a/src/HOL/Arith.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Arith.ML Fri Oct 17 15:25:12 1997 +0200
@@ -35,7 +35,7 @@
AddIffs [pred_le];
goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
-by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
+by(simp_tac (!simpset addsplits [expand_nat_case]) 1);
qed_spec_mp "pred_le_mono";
goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
@@ -434,7 +434,7 @@
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]
- setloop (split_tac [expand_if])) 1);
+ addsplits [expand_if]) 1);
qed "if_Suc_diff_n";
goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
--- a/src/HOL/Auth/Event.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Event.ML Fri Oct 17 15:25:12 1997 +0200
@@ -46,7 +46,7 @@
qed "spies_subset_spies_Says";
goal thy "spies evs <= spies (Notes A X # evs)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Fast_tac 1);
qed "spies_subset_spies_Notes";
@@ -54,14 +54,14 @@
goal thy "Says A B X : set evs --> X : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
- (!simpset setloop split_tac [expand_event_case, expand_if])));
+ (!simpset addsplits [expand_event_case, expand_if])));
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 setloop split_tac [expand_event_case, expand_if])));
+ (!simpset addsplits [expand_event_case, expand_if])));
qed_spec_mp "Notes_imp_spies";
(*Use with addSEs to derive contradictions from old Says events containing
@@ -80,7 +80,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [parts_insert_spies]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
by (ALLGOALS Blast_tac);
qed "parts_spies_subset_used";
@@ -91,7 +91,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [parts_insert_spies]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
by (ALLGOALS Blast_tac);
bind_thm ("initState_into_used", impOfSubs (result()));
--- a/src/HOL/Auth/Message.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Message.ML Fri Oct 17 15:25:12 1997 +0200
@@ -899,7 +899,7 @@
(REPEAT o CHANGED)
(res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
- simp_tac (!simpset setloop split_tac [expand_if]) 1,
+ simp_tac (!simpset addsplits [expand_if]) 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 Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML Fri Oct 17 15:25:12 1997 +0200
@@ -124,7 +124,7 @@
fun analz_induct_tac i =
etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
- (!simpset setloop split_tac [expand_if]));
+ (!simpset addsplits [expand_if]));
(*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 Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Oct 17 15:25:12 1997 +0200
@@ -126,8 +126,7 @@
(*Tactic for proving secrecy theorems*)
fun analz_induct_tac i =
etac ns_public.induct i THEN
- ALLGOALS (asm_simp_tac
- (!simpset setloop split_tac [expand_if]));
+ ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]));
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
--- a/src/HOL/Auth/NS_Shared.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Fri Oct 17 15:25:12 1997 +0200
@@ -267,7 +267,7 @@
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
(*Oops*)
by (blast_tac (!claset addDs [unique_session_keys]) 5);
(*NS3, replay sub-case*)
--- a/src/HOL/Auth/OtwayRees.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Fri Oct 17 15:25:12 1997 +0200
@@ -339,7 +339,7 @@
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
(*Oops*)
by (blast_tac (!claset addSDs [unique_session_keys]) 4);
(*OR4*)
--- a/src/HOL/Auth/OtwayRees_AN.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Oct 17 15:25:12 1997 +0200
@@ -268,7 +268,7 @@
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
(*Oops*)
by (blast_tac (!claset addSDs [unique_session_keys]) 4);
(*OR4*)
--- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Oct 17 15:25:12 1997 +0200
@@ -231,7 +231,7 @@
by (ALLGOALS
(asm_simp_tac (!simpset addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
(*Oops*)
by (blast_tac (!claset addSDs [unique_session_keys]) 4);
(*OR4*)
--- a/src/HOL/Auth/Public.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Public.ML Fri Oct 17 15:25:12 1997 +0200
@@ -58,7 +58,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [imageI, spies_Cons]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
qed_spec_mp "spies_pubK";
(*Spy sees private keys of bad agents!*)
@@ -66,7 +66,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [imageI, spies_Cons]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
qed "Spy_spies_bad";
AddIffs [spies_pubK, spies_pubK RS analz.Inj];
@@ -114,7 +114,7 @@
by (res_inst_tac [("x","0")] exI 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [used_Cons]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
by Safe_tac;
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
@@ -160,5 +160,5 @@
rangeI,
insert_Key_singleton,
insert_Key_image, Un_assoc RS sym]
- setloop split_tac [expand_if];
+ addsplits [expand_if];
--- a/src/HOL/Auth/Recur.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Fri Oct 17 15:25:12 1997 +0200
@@ -455,7 +455,7 @@
(asm_simp_tac
(!simpset addsimps [analz_insert_eq, parts_insert_spies,
analz_insert_freshK]
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
(*RA4*)
by (spy_analz_tac 5);
(*RA2*)
--- a/src/HOL/Auth/Shared.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Fri Oct 17 15:25:12 1997 +0200
@@ -36,7 +36,7 @@
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [imageI, spies_Cons]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
qed "Spy_spies_bad";
AddSIs [Spy_spies_bad];
@@ -111,7 +111,7 @@
by (res_inst_tac [("x","0")] exI 1);
by (ALLGOALS (asm_simp_tac
(!simpset addsimps [used_Cons]
- setloop split_tac [expand_event_case, expand_if])));
+ addsplits [expand_event_case, expand_if])));
by Safe_tac;
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
@@ -238,7 +238,7 @@
insert_Key_singleton, subset_Compl_range,
Key_not_used, insert_Key_image, Un_assoc RS sym]
@disj_comms)
- setloop split_tac [expand_if];
+ addsplits [expand_if];
(*Lemma for the trivial direction of the if-and-only-if*)
goal thy
--- a/src/HOL/Auth/TLS.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Fri Oct 17 15:25:12 1997 +0200
@@ -146,7 +146,7 @@
REPEAT (FIRSTGOAL analz_mono_contra_tac)
THEN
fast_tac (!claset addss (!simpset)) i THEN
- ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]));
+ ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]));
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
@@ -198,13 +198,13 @@
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*)
ALLGOALS (asm_simp_tac
(!simpset addcongs [if_weak_cong]
- setloop split_tac [expand_if])) THEN
+ addsplits [expand_if])) 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]
- setloop split_tac [expand_if]));
+ addsplits [expand_if]));
(*** Properties of items found in Notes ***)
--- a/src/HOL/Auth/Yahalom.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML Fri Oct 17 15:25:12 1997 +0200
@@ -227,7 +227,7 @@
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [analz_insert_eq, analz_insert_freshK]
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
(*Oops*)
by (blast_tac (!claset addDs [unique_session_keys]) 3);
(*YM3*)
@@ -499,7 +499,7 @@
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [analz_insert_eq, analz_insert_freshK]
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
(*Prove YM3 by showing that no NB can also be an NA*)
by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
--- a/src/HOL/Auth/Yahalom2.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Fri Oct 17 15:25:12 1997 +0200
@@ -227,7 +227,7 @@
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [analz_insert_eq, analz_insert_freshK]
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
(*Oops*)
by (blast_tac (!claset addDs [unique_session_keys]) 3);
(*YM3*)
--- a/src/HOL/Divides.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Divides.ML Fri Oct 17 15:25:12 1997 +0200
@@ -222,7 +222,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 setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
qed "mod2_cases";
--- a/src/HOL/Finite.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Finite.ML Fri Oct 17 15:25:12 1997 +0200
@@ -176,7 +176,7 @@
by (Asm_simp_tac 1);
by (rtac iffI 1);
by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
- by (simp_tac (!simpset setloop (split_tac[expand_split])) 1);
+ by (simp_tac (!simpset addsplits [expand_split]) 1);
by (etac finite_imageI 1);
by (simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
by (Auto_tac());
@@ -244,7 +244,7 @@
by (SELECT_GOAL(safe_tac (!claset))1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
- by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
by (dtac sym 1);
by (rotate_tac ~1 1);
@@ -258,7 +258,7 @@
by (SELECT_GOAL(safe_tac (!claset))1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
- by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 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 (!claset))1);
@@ -272,7 +272,7 @@
by (SELECT_GOAL(safe_tac (!claset))1);
by (res_inst_tac [("x","k")] exI 1);
by (Asm_simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
val lemma = result();
@@ -330,7 +330,7 @@
by (etac finite_induct 1);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [Int_insert_left]
- setloop split_tac [expand_if])));
+ addsplits [expand_if])));
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 Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/IMP/Hoare.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 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 setloop(split_tac[expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (rtac iffI 1);
by (rtac weak_coinduct 1);
by (etac CollectI 1);
--- a/src/HOL/IOA/IOA.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/IOA/IOA.ML Fri Oct 17 15:25:12 1997 +0200
@@ -32,7 +32,7 @@
by (rtac ext 1);
by (exhaust_tac "s(i)" 1);
by (Asm_simp_tac 1);
- by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
qed "filter_oseq_idemp";
goalw IOA.thy [mk_trace_def,filter_oseq_def]
@@ -42,7 +42,7 @@
\ (mk_trace A s n = Some(a)) = \
\ (s(n)=Some(a) & a : externals(asig_of(A)))";
by (exhaust_tac "s(n)" 1);
- by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+ by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
by (Fast_tac 1);
qed "mk_trace_thm";
@@ -135,7 +135,7 @@
\ else snd(snd(snd(t)))=snd(snd(snd(s)))))";
by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
ioa_projections)
- setloop (split_tac [expand_if])) 1);
+ addsplits [expand_if]) 1);
qed "trans_of_par4";
goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
--- a/src/HOL/IOA/Solve.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/IOA/Solve.ML Fri Oct 17 15:25:12 1997 +0200
@@ -78,7 +78,7 @@
by (asm_full_simp_tac
(!simpset addsimps [executions_def,is_execution_fragment_def,
par_def,starts_of_def,trans_of_def,filter_oseq_def]
- setloop (split_tac[expand_if,expand_option_case])) 1);
+ addsplits [expand_if,expand_option_case]) 1);
qed"comp1_reachable";
@@ -98,7 +98,7 @@
by (asm_full_simp_tac
(!simpset addsimps [executions_def,is_execution_fragment_def,
par_def,starts_of_def,trans_of_def,filter_oseq_def]
- setloop (split_tac[expand_if,expand_option_case])) 1);
+ addsplits [expand_if,expand_option_case]) 1);
qed"comp2_reachable";
@@ -141,7 +141,7 @@
by (Asm_full_simp_tac 2);
by (Fast_tac 2);
by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong]
- setloop (split_tac [expand_if])) 1);
+ addsplits [expand_if]) 1);
by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
asm_full_simp_tac(!simpset addsimps[comp1_reachable,
comp2_reachable])1));
@@ -160,7 +160,7 @@
by (asm_full_simp_tac
(!simpset addsimps [executions_def,is_execution_fragment_def,
par_def,starts_of_def,trans_of_def,rename_def]
- setloop (split_tac[expand_option_case])) 1);
+ addsplits [expand_option_case]) 1);
by (best_tac (!claset addSDs [spec] addDs [sym] addss (!simpset)) 1);
qed"reachable_rename_ioa";
--- a/src/HOL/Induct/Com.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/Com.ML Fri Oct 17 15:25:12 1997 +0200
@@ -53,7 +53,7 @@
goalw thy [assign_def] "s[s x/x] = s";
by (rtac ext 1);
-by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
qed "assign_triv";
Addsimps [assign_same, assign_different, assign_triv];
--- a/src/HOL/Induct/LFilter.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/LFilter.ML Fri Oct 17 15:25:12 1997 +0200
@@ -96,7 +96,7 @@
goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
- setloop split_tac[expand_if]) 1);
+ addsplits [expand_if]) 1);
qed "find_LCons";
@@ -141,7 +141,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]
- setloop split_tac[expand_if]) 1);
+ addsplits [expand_if]) 1);
qed "lfilter_LCons";
AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
@@ -186,7 +186,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 setloop split_tac[expand_if])));
+by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
by Safe_tac;
(*Cases: p x is true or false*)
by (Blast_tac 1);
@@ -244,7 +244,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 setloop split_tac[expand_if])));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
qed_spec_mp "findRel_conj_lfilter";
@@ -288,7 +288,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 setloop split_tac[expand_if])));
+by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
qed "lfilter_conj";
@@ -326,7 +326,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 setloop split_tac[expand_if])));
+by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
by Safe_tac;
by (Blast_tac 1);
by (case_tac "lmap f l : Domain (findRel p)" 1);
--- a/src/HOL/Induct/LList.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/LList.ML Fri Oct 17 15:25:12 1997 +0200
@@ -10,7 +10,7 @@
(** Simplification **)
-simpset := !simpset setloop split_tac [expand_split, expand_sum_case];
+simpset := !simpset addsplits [expand_split, expand_sum_case];
(*For adding _eqI rules to a simpset; we must remove Pair_eq because
it may turn an instance of reflexivity into a conjunction!*)
@@ -68,11 +68,11 @@
(*UNUSED; obsolete?
goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
-by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
+by (simp_tac (!simpset addsplits [expand_split]) 1);
qed "split_UN1";
goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
-by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
+by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
qed "sum_case2_UN1";
*)
@@ -310,7 +310,7 @@
by (rename_tac "y" 1);
by (stac prem1 1);
by (stac prem2 1);
-by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
+by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
by (strip_tac 1);
by (res_inst_tac [("n", "n")] natE 1);
by (rename_tac "m" 2);
--- a/src/HOL/Induct/Mutil.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/Mutil.ML Fri Oct 17 15:25:12 1997 +0200
@@ -94,7 +94,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 setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
qed "evnodd_insert";
@@ -110,7 +110,7 @@
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]
- setloop split_tac [expand_if]) 1
+ addsplits [expand_if]) 1
THEN Blast_tac 1));
qed "domino_singleton";
--- a/src/HOL/Induct/Perm.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/Perm.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop split_tac [expand_if])));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
val perm_mem_lemma = result();
bind_thm ("perm_mem", perm_mem_lemma RS mp);
--- a/src/HOL/Induct/PropLog.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/PropLog.ML Fri Oct 17 15:25:12 1997 +0200
@@ -142,7 +142,7 @@
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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Simp_tac 1);
by (Fast_tac 1);
qed "hyps_Diff";
@@ -152,7 +152,7 @@
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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Simp_tac 1);
by (Fast_tac 1);
qed "hyps_insert";
@@ -174,7 +174,7 @@
goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
by (PropLog.pl.induct_tac "p" 1);
-by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
by (Blast_tac 1);
qed "hyps_subset";
--- a/src/HOL/Induct/SList.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/SList.ML Fri Oct 17 15:25:12 1997 +0200
@@ -312,12 +312,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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
qed "mem_filter2";
--- a/src/HOL/Integ/Bin.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Integ/Bin.ML Fri Oct 17 15:25:12 1997 +0200
@@ -100,7 +100,7 @@
(**** The carry/borrow functions, bin_succ and bin_pred ****)
-val if_ss = !simpset setloop (split_tac [expand_if]) ;
+val if_ss = !simpset addsplits [expand_if];
(**** integ_of_bin ****)
--- a/src/HOL/Lambda/Eta.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Lambda/Eta.ML Fri Oct 17 15:25:12 1997 +0200
@@ -37,8 +37,7 @@
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
by (Blast_tac 2);
-by(simp_tac (!simpset addsimps [pred_def]
- setloop (split_tac [expand_nat_case])) 1);
+by(simp_tac (!simpset addsimps [pred_def] addsplits [expand_nat_case]) 1);
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
qed "free_lift";
@@ -51,7 +50,7 @@
by (Blast_tac 2);
by (asm_full_simp_tac (addsplit (!simpset)) 2);
by(simp_tac (!simpset addsimps [pred_def,subst_Var]
- setloop (split_tac [expand_if,expand_nat_case])) 1);
+ addsplits [expand_if,expand_nat_case]) 1);
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
qed "free_subst";
@@ -169,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 setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (SELECT_GOAL(safe_tac HOL_cs)1);
by(etac nat_neqE 1);
by (res_inst_tac [("x","Var nat")] exI 1);
@@ -180,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 setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
by (Simp_tac 1);
by (Simp_tac 1);
@@ -196,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 setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Simp_tac 1);
by (Blast_tac 1);
by (Simp_tac 1);
@@ -210,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 setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Blast_tac 1);
--- a/src/HOL/Lambda/Lambda.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Lambda/Lambda.ML Fri Oct 17 15:25:12 1997 +0200
@@ -45,8 +45,8 @@
(*** subst and lift ***)
-fun addsplit ss = ss addsimps [subst_Var]
- setloop (split_inside_tac [expand_if]);
+fun addsplit ss = ss addsimps [subst_Var]
+ setloop (split_inside_tac [expand_if]);
goal Lambda.thy "(Var k)[u/k] = u";
by (asm_full_simp_tac(addsplit(!simpset)) 1);
@@ -66,7 +66,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 setloop (split_tac [expand_if])
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if]
addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
@@ -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 [pred_def,subst_Var,lift_lift]
- setloop (split_tac [expand_if,expand_nat_case])
+ addsplits [expand_if,expand_nat_case]
addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
@@ -88,7 +88,7 @@
\ 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]
- setloop (split_tac [expand_if])
+ addsplits [expand_if]
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
@@ -96,7 +96,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 setloop (split_tac[expand_if]))));
+by (ALLGOALS (asm_full_simp_tac (!simpset addsplits [expand_if])));
qed "subst_lift";
Addsimps [subst_lift];
@@ -106,7 +106,7 @@
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac
(!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
- setloop (split_tac [expand_if,expand_nat_case])
+ addsplits [expand_if,expand_nat_case]
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
--- a/src/HOL/Lex/AutoChopper.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Lex/AutoChopper.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 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 setloop (split_tac[expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 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] setloop (split_tac [expand_if])) 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (list.induct_tac "xs" 1);
- by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
by (Fast_tac 1);
-by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (list.induct_tac "xs" 1);
- by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
by (Fast_tac 1);
-by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (list.induct_tac "xs" 1);
- by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
by (Fast_tac 1);
-by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (list.induct_tac "xs" 1);
- by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
by (Fast_tac 1);
-by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (rtac conjI 1);
by (rtac mp 1);
by (etac step2_c 2);
- by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (rtac conjI 1);
- by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
+ by (asm_simp_tac (!simpset addsimps [step2_a] addsplits [expand_if]) 1);
by (rtac conjI 1);
by (rtac mp 1);
by (etac step2_d 2);
- by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (rtac mp 1);
by (etac step2_e 2);
- by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
qed"auto_chopper_is_auto_chopper";
--- a/src/HOL/List.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/List.ML Fri Oct 17 15:25:12 1997 +0200
@@ -203,17 +203,17 @@
goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
by (asm_simp_tac (!simpset addsimps [hd_append]
- setloop (split_tac [expand_list_case])) 1);
+ addsplits [expand_list_case]) 1);
qed "hd_append2";
Addsimps [hd_append2];
goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
-by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
+by (simp_tac (!simpset addsplits [expand_list_case]) 1);
qed "tl_append";
goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
by (asm_simp_tac (!simpset addsimps [tl_append]
- setloop (split_tac [expand_list_case])) 1);
+ addsplits [expand_list_case]) 1);
qed "tl_append2";
Addsimps [tl_append2];
@@ -309,13 +309,13 @@
goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
qed "mem_filter";
Addsimps[mem_filter];
@@ -331,7 +331,7 @@
goal thy "(x mem xs) = (x: set xs)";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
by (Blast_tac 1);
qed "set_mem_eq";
@@ -377,7 +377,7 @@
goal thy "list_all P xs = (!x. x mem xs --> P(x))";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
by (Blast_tac 1);
qed "list_all_mem_conv";
@@ -388,13 +388,13 @@
goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
by (induct_tac "xs" 1);
- by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+ by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
qed "filter_append";
Addsimps [filter_append];
goal thy "size (filter P xs) <= size xs";
by (induct_tac "xs" 1);
- by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+ by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
qed "filter_size";
@@ -489,7 +489,7 @@
(* case 0 *)
by (Asm_full_simp_tac 1);
(* case Suc x *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
qed_spec_mp "nth_mem";
Addsimps [nth_mem];
@@ -497,36 +497,36 @@
goal thy "last(xs@[x]) = x";
by(induct_tac "xs" 1);
-by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
+by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
qed "last_snoc";
Addsimps [last_snoc];
goal thy "butlast(xs@[x]) = xs";
by(induct_tac "xs" 1);
-by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
+by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
qed "butlast_snoc";
Addsimps [butlast_snoc];
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 setloop (split_tac[expand_if]))));
+by(ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac[expand_if]))));
+by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
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]
- setloop (split_tac[expand_if])) 1);
+ addsplits [expand_if]) 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]
- setloop (split_tac[expand_if])) 1);
+ addsplits [expand_if]) 1);
by(Clarify_tac 1);
by(Full_simp_tac 1);
qed "in_set_butlast_appendI2";
@@ -678,14 +678,14 @@
goal thy "takeWhile P xs @ dropWhile P xs = xs";
by (induct_tac "xs" 1);
by (Simp_tac 1);
-by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
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 setloop (split_tac[expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
bind_thm("takeWhile_append1", conjI RS (result() RS mp));
Addsimps [takeWhile_append1];
@@ -694,7 +694,7 @@
"(!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 setloop (split_tac[expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
bind_thm("takeWhile_append2", ballI RS (result() RS mp));
Addsimps [takeWhile_append2];
@@ -702,7 +702,7 @@
"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 setloop (split_tac[expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
bind_thm("dropWhile_append1", conjI RS (result() RS mp));
Addsimps [dropWhile_append1];
@@ -711,14 +711,14 @@
"(!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 setloop (split_tac[expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
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 setloop (split_tac[expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
qed_spec_mp"set_take_whileD";
(** replicate **)
--- a/src/HOL/MiniML/Generalize.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/MiniML/Generalize.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop (split_tac [expand_if])) 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
by (Fast_tac 1);
by (Asm_simp_tac 1);
by (Fast_tac 1);
@@ -99,7 +99,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 setloop (split_tac[expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Asm_simp_tac 1);
qed "gen_bound_typ_instance";
@@ -109,7 +109,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 setloop (split_tac[expand_if])) 1);
+ by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
by (Fast_tac 1);
by (Asm_simp_tac 1);
qed "free_tv_subset_gen_le";
@@ -123,8 +123,8 @@
by (typ.induct_tac "t" 1);
by (Simp_tac 1);
by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 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 Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/MiniML/Instance.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 (!claset));
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 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 setloop (split_tac [expand_if]) addsimps [leD]) 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [le_add2,diff_add_inverse2]) 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 (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 setloop (split_tac [expand_if]) addsimps [leD]) 1);
+by (simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1);
by (Asm_simp_tac 1);
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1);
val aux2 = result () RS mp;
--- a/src/HOL/MiniML/Maybe.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/MiniML/Maybe.ML Fri Oct 17 15:25:12 1997 +0200
@@ -25,7 +25,7 @@
goal thy
"((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
-by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by(simp_tac (!simpset addsplits [expand_option_bind]) 1);
qed "option_bind_eq_None";
Addsimps [option_bind_eq_None];
--- a/src/HOL/MiniML/MiniML.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/MiniML/MiniML.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 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 setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Fast_tac 1);
by (Simp_tac 1);
by (Fast_tac 1);
--- a/src/HOL/MiniML/Type.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/MiniML/Type.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
qed_spec_mp "subst_te_new_type_scheme";
Addsimps [subst_te_new_type_scheme];
@@ -546,13 +546,13 @@
Addsimps [new_tv_not_free_tv];
goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (safe_tac (!claset));
by (trans_tac 1);
qed "less_maxL";
goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1);
val less_maxR = result();
@@ -585,11 +585,11 @@
Addsimps [fresh_variable_type_schemes];
goalw thy [max_def] "!!n::nat. n <= (max n n')";
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
val le_maxL = result();
goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 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 Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/MiniML/W.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
by (strip_tac 1);
by (etac conjE 1);
by (etac conjE 1);
@@ -27,10 +27,10 @@
by (dtac sym 1);
by (Asm_full_simp_tac 1);
(* case Abs e *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
by (eres_inst_tac [("x","A")] allE 1);
@@ -50,7 +50,7 @@
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
(* case LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
by (REPEAT (etac conjE 1));
@@ -88,7 +88,7 @@
by (assume_tac 2);
by (rtac add_le_mono 1);
by (Simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1);
by (strip_tac 1);
by (rtac new_tv_le 1);
by (mp_tac 2);
@@ -96,7 +96,7 @@
by (assume_tac 2);
by (rtac add_le_mono 1);
by (Simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1);
by (strip_tac 1);
by (dtac not_leE 1);
by (rtac less_or_eq_imp_le 1);
@@ -111,7 +111,7 @@
\ new_tv m S & new_tv m t";
by (expr.induct_tac "e" 1);
(* case Var n *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
by (strip_tac 1);
by (REPEAT (etac conjE 1));
by (rtac conjI 1);
@@ -125,14 +125,14 @@
by (Asm_full_simp_tac 1);
(* case Abs e *)
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
- setloop (split_tac [expand_option_bind])) 1);
+ addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
by (fast_tac (HOL_cs addss (!simpset
addsimps [new_tv_subst,new_tv_Suc_list])) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
by (eres_inst_tac [("x","n")] allE 1);
@@ -174,7 +174,7 @@
[new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
addss (!simpset)) 1);
(* case LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
by (REPEAT (etac conjE 1));
@@ -239,7 +239,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (simp_tac (!simpset addsimps
- [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
+ [free_tv_subst] addsplits [expand_option_bind,expand_if]) 1);
by (strip_tac 1);
by (REPEAT (etac conjE 1));
by (hyp_subst_tac 1);
@@ -255,7 +255,7 @@
by (Asm_full_simp_tac 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps
- [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+ [free_tv_subst] addsplits [expand_option_bind] delsimps all_simps) 1);
by (strip_tac 1);
by (rename_tac "S t n1 S1 t1 m v" 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
@@ -267,7 +267,7 @@
by (best_tac (HOL_cs addIs [cod_app_subst]
addss (!simpset addsimps [less_Suc_eq])) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
by (strip_tac 1);
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
by (eres_inst_tac [("x","n")] allE 1);
@@ -303,7 +303,7 @@
addEs [UnE]
addss !simpset) 1);
(* LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
by (strip_tac 1);
by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
by (eres_inst_tac [("x","nat")] allE 1);
@@ -338,7 +338,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 setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
by (strip_tac 1);
by (rtac has_type.VarI 1);
by (Simp_tac 1);
@@ -347,7 +347,7 @@
by (rtac refl 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
- setloop (split_tac [expand_option_bind])) 1);
+ addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
by (Asm_full_simp_tac 1);
@@ -360,7 +360,7 @@
by (Asm_simp_tac 1);
by (assume_tac 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
@@ -392,7 +392,7 @@
by (mp_tac 1);
by (assume_tac 1);
(* case Let e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (strip_tac 1);
by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1);
by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
@@ -469,8 +469,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (strip_tac 1);
-by (simp_tac (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
by (eresolve_tac has_type_casesE 1);
by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
by (etac exE 1);
@@ -491,7 +490,7 @@
by (eres_inst_tac [("x","Suc n")] allE 1);
by (best_tac (HOL_cs addSDs [mk_scheme_injective]
addss (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_option_bind]))) 1);
+ addsplits [expand_option_bind])) 1);
(** LEVEL 19 **)
(* case App e1 e2 *)
@@ -531,8 +530,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
- setloop (split_tac [expand_if])) 3);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 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);
@@ -540,8 +538,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]
- setloop (split_tac [expand_if])) 3);
+by (asm_full_simp_tac (!simpset addsimps [dom_def] addsplits [expand_if]) 3);
(* na : dom Sa *)
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2);
@@ -553,7 +550,7 @@
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]
- setloop (split_tac [expand_if]))) 2);
+ addsplits [expand_if])) 2);
by (Simp_tac 2);
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2 );
@@ -564,16 +561,16 @@
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 setloop (split_tac [expand_if])) 3);
+by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3);
by (Fast_tac 3);
(* case na : free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 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);
(** LEVEL 75 **)
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_option_bind]) 1);
by (safe_tac HOL_cs );
by (dtac mgu_Some 1);
by ( fast_tac (HOL_cs addss !simpset) 1);
@@ -603,9 +600,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 setloop (split_tac [expand_if])) 2);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
(* case na : free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 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/Prod.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Prod.ML Fri Oct 17 15:25:12 1997 +0200
@@ -168,7 +168,7 @@
qed "expand_split";
(* could be done after split_tac has been speeded up significantly:
-simpset := (!simpset setloop split_tac[expand_split]);
+simpset := (!simpset addsplits [expand_split]);
precompute the constants involved and don't do anything unless
the current goal contains one of those constants
*)
--- a/src/HOL/Set.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Set.ML Fri Oct 17 15:25:12 1997 +0200
@@ -646,7 +646,7 @@
(** Rewrite rules for boolean case-splitting: faster than
- setloop split_tac[expand_if]
+ addsplits[expand_if]
**)
bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
@@ -669,7 +669,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 setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
qed "mem_if";
val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
--- a/src/HOL/Subst/Subst.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Subst/Subst.ML Fri Oct 17 15:25:12 1997 +0200
@@ -41,8 +41,7 @@
qed "agreement";
goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
-by (simp_tac (!simpset addsimps [agreement]
- setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addsimps [agreement] addsplits [expand_if]) 1);
qed_spec_mp"repl_invariance";
val asms = goal Subst.thy
@@ -112,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 setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
qed "subst_comp";
Addsimps [subst_comp];
@@ -131,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 setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_full_simp_tac (!simpset addsplits [expand_if])));
qed "Cons_trivial";
@@ -144,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 setloop (split_tac[expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
by (Blast_tac 1);
qed "sdom_iff";
@@ -204,7 +203,7 @@
goal Subst.thy "(M <| [(x, Var x)]) = M";
by (induct_tac "M" 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
qed "id_subst_lemma";
Addsimps [id_subst_lemma];
--- a/src/HOL/Subst/Unifier.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Subst/Unifier.ML Fri Oct 17 15:25:12 1997 +0200
@@ -83,7 +83,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]
- setloop (split_tac [expand_if])) 1);
+ addsplits [expand_if]) 1);
by (Blast_tac 1);
qed_spec_mp "Var_Idem";
--- a/src/HOL/Subst/Unify.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Subst/Unify.ML Fri Oct 17 15:25:12 1997 +0200
@@ -154,14 +154,14 @@
by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
- setloop (split_tac [expand_if]))));
+ addsplits [expand_if])));
(*Const-Const case*)
by (simp_tac
(!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
inv_image_def, less_eq]) 1);
(** LEVEL 7 **)
(*Comb-Comb case*)
-by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
by (strip_tac 1);
by (rtac (trans_unifyRel RS transD) 1);
by (Blast_tac 1);
@@ -184,7 +184,7 @@
\ of None => None \
\ | Some sigma => Some (theta <> sigma)))";
by (asm_simp_tac (!simpset addsimps (unify_TC::unifyRules0)
- setloop split_tac [expand_option_case]) 1);
+ addsplits [expand_option_case]) 1);
qed "unifyCombComb";
@@ -207,7 +207,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 setloop split_tac [expand_if])));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
(*Const-Const case*)
by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
(*Const-Var case*)
@@ -220,7 +220,7 @@
by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
(** LEVEL 8 **)
(*Comb-Comb case*)
-by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
by (strip_tac 1);
by (rotate_tac ~2 1);
by (asm_full_simp_tac
@@ -246,7 +246,7 @@
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [Var_Idem]
- setloop split_tac[expand_if, expand_option_case])));
+ addsplits [expand_if,expand_option_case])));
(*Comb-Comb case*)
by (safe_tac (!claset));
by (REPEAT (dtac spec 1 THEN mp_tac 1));
--- a/src/HOL/W0/I.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/W0/I.ML Fri Oct 17 15:25:12 1997 +0200
@@ -144,8 +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]
- setloop (split_tac [expand_if])) 1);
+ by (simp_tac (!simpset addsimps [app_subst_list] addsplits [expand_if]) 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/Maybe.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/W0/Maybe.ML Fri Oct 17 15:25:12 1997 +0200
@@ -26,7 +26,7 @@
goal Maybe.thy
"((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_bind]) 1);
qed "bind_eq_Fail";
Addsimps [bind_eq_Fail];
--- a/src/HOL/W0/Type.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/W0/Type.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))) 1);
+by (fast_tac (set_cs addss(!simpset addsplits [expand_if])) 1);
qed_spec_mp "ftv_mem_sub_ftv_list";
Addsimps [ftv_mem_sub_ftv_list];
--- a/src/HOL/W0/W.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/W0/W.ML Fri Oct 17 15:25:12 1997 +0200
@@ -14,15 +14,15 @@
"!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 setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
- setloop (split_tac [expand_bind])) 1);
+ addsplits [expand_bind]) 1);
by (strip_tac 1);
by (dtac sym 1);
by (fast_tac (HOL_cs addss !simpset) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_bind]) 1);
by (strip_tac 1);
by ( rename_tac "sa ta na sb tb nb sc" 1);
by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
@@ -45,12 +45,12 @@
"!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 setloop (split_tac [expand_if]))) 1);
+by (fast_tac (HOL_cs addss(!simpset addsplits [expand_if])) 1);
(* case Abs e *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_bind]) 1);
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_bind]) 1);
by (strip_tac 1);
by (rename_tac "s t na sa ta nb sb sc tb m" 1);
by (eres_inst_tac [("x","a")] allE 1);
@@ -93,10 +93,10 @@
(* case Var n *)
by (fast_tac (HOL_cs addDs [list_all_nth] addss (!simpset
addsimps [id_subst_def,new_tv_list,new_tv_subst]
- setloop (split_tac [expand_if]))) 1);
+ addsplits [expand_if])) 1);
(* case Abs e *)
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
- setloop (split_tac [expand_bind])) 1);
+ addsplits [expand_bind]) 1);
by (strip_tac 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
@@ -104,7 +104,7 @@
addsimps [new_tv_subst,new_tv_Suc_list])) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_bind]) 1);
by (strip_tac 1);
by (rename_tac "s t na sa ta nb sb sc tb m" 1);
by (eres_inst_tac [("x","n")] allE 1);
@@ -160,11 +160,11 @@
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 setloop (split_tac [expand_if]))) 1);
+ addss (!simpset addsplits [expand_if])) 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps
- [free_tv_subst] setloop (split_tac [expand_bind])) 1);
+ [free_tv_subst] addsplits [expand_bind]) 1);
by (strip_tac 1);
by (rename_tac "s t na sa ta m v" 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
@@ -178,7 +178,7 @@
addss (!simpset addsimps [less_Suc_eq])) 1);
(** LEVEL 12 **)
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_bind]) 1);
by (strip_tac 1);
by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
by (eres_inst_tac [("x","n")] allE 1);
@@ -227,7 +227,7 @@
(* case Var n *)
by (strip_tac 1);
by (simp_tac (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_if])) 1);
+ addsplits [expand_if]) 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);
@@ -242,7 +242,7 @@
by (eres_inst_tac [("x","t2")] allE 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_bind]))) 1);
+ addsplits [expand_bind])) 1);
(** LEVEL 17 **)
(* case App e1 e2 *)
@@ -285,7 +285,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 setloop (split_tac [expand_if])) 3);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 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);
@@ -295,7 +295,7 @@
(* na ~: dom sa *)
(** LEVEL 50 **)
by (asm_full_simp_tac (!simpset addsimps [dom_def]
- setloop (split_tac [expand_if])) 3);
+ addsplits [expand_if]) 3);
(* na : dom sa *)
by (rtac eq_free_eq_subst_te 2);
by (strip_tac 2);
@@ -307,7 +307,7 @@
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]
- setloop (split_tac [expand_if]))) 2);
+ addsplits [expand_if])) 2);
(** LEVEL 60 **)
by (Simp_tac 2);
@@ -321,16 +321,16 @@
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 setloop (split_tac [expand_if])) 3);
+by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3);
(* case na : free_tv t - free_tv sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 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);
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
by (Fast_tac 2);
(** LEVEL 76 **)
-by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_bind]) 1);
by (safe_tac HOL_cs);
by (dtac mgu_Ok 1);
by ( fast_tac (HOL_cs addss !simpset) 1);
@@ -359,9 +359,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 setloop (split_tac [expand_if])) 2);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
(* case na : free_tv t - free_tv sa *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 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 Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/WF.ML Fri Oct 17 15:25:12 1997 +0200
@@ -151,8 +151,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]
- setloop (split_tac [expand_if])) 1);
+by (simp_tac (HOL_ss addsimps [expand_fun_eq] addsplits [expand_if]) 1);
qed "cuts_eq";
goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
@@ -193,7 +192,7 @@
by (cut_facts_tac prems 1);
by (rtac ext 1);
by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
- setloop (split_tac [expand_if])) 1);
+ addsplits [expand_if]) 1);
qed "is_recfun_cut";
(*** Main Existence Lemma -- Basic Properties of the_recfun ***)
--- a/src/HOL/equalities.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/equalities.ML Fri Oct 17 15:25:12 1997 +0200
@@ -239,13 +239,13 @@
goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
\ else B Int C)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
qed "Int_insert_left";
goal Set.thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
\ else A Int B)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
qed "Int_insert_right";
@@ -568,7 +568,7 @@
qed "Diff_insert2";
goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
-by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
qed "insert_Diff_if";
--- a/src/HOL/ex/Fib.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/ex/Fib.ML Fri Oct 17 15:25:12 1997 +0200
@@ -53,7 +53,7 @@
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]
- setloop split_tac[expand_if])));
+ addsplits [expand_if])));
by (safe_tac (!claset addSDs [mod2_neq_0]));
by (ALLGOALS
(asm_full_simp_tac
--- a/src/HOL/ex/InSort.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/ex/InSort.ML Fri Oct 17 15:25:12 1997 +0200
@@ -9,7 +9,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 setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
qed "mset_ins";
Addsimps [mset_ins];
@@ -20,7 +20,7 @@
goal thy "set(ins f x xs) = insert x (set xs)";
by (asm_simp_tac (!simpset addsimps [set_via_mset]
- setloop (split_tac [expand_if])) 1);
+ addsplits [expand_if]) 1);
by (Fast_tac 1);
qed "set_ins";
Addsimps [set_ins];
@@ -28,7 +28,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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
by (cut_facts_tac prems 1);
by (Fast_tac 1);
qed "sorted_ins";
--- a/src/HOL/ex/Primes.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/ex/Primes.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
qed "gcd_less_0";
Addsimps [gcd_0, gcd_less_0];
--- a/src/HOL/ex/Qsort.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/ex/Qsort.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
qed"Ball_set_filter";
Addsimps [Ball_set_filter];
--- a/src/HOL/ex/Recdef.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/ex/Recdef.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop split_tac[expand_if])));
+by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
by (Blast_tac 1);
qed "qsort_mem_stable";
--- a/src/HOL/ex/Sorting.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/ex/Sorting.ML Fri Oct 17 15:25:12 1997 +0200
@@ -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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
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 setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
by (Fast_tac 1);
qed "set_via_mset";
@@ -30,7 +30,7 @@
val prems = goalw Sorting.thy [transf_def]
"transf(le) ==> sorted1 le xs = sorted le xs";
by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_list_case]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_list_case])));
by (cut_facts_tac prems 1);
by (Fast_tac 1);
qed "sorted1_is_sorted";
--- a/src/HOL/ex/set.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/ex/set.ML Fri Oct 17 15:25:12 1997 +0200
@@ -77,7 +77,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 setloop split_tac [expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
by (Blast_tac 1);
qed "range_if_then_else";
--- a/src/HOL/simpdata.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/simpdata.ML Fri Oct 17 15:25:12 1997 +0200
@@ -328,6 +328,9 @@
fun split_inside_tac splits = mktac (map mk_meta_eq splits)
end;
+infix 4 addsplits;
+fun ss addsplits splits = ss addloop (split_tac splits);
+
qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
(fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]);