1.1 --- a/src/HOL/Arith.ML Fri Oct 17 15:23:14 1997 +0200
1.2 +++ b/src/HOL/Arith.ML Fri Oct 17 15:25:12 1997 +0200
1.3 @@ -35,7 +35,7 @@
1.4 AddIffs [pred_le];
1.5
1.6 goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
1.7 -by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
1.8 +by(simp_tac (!simpset addsplits [expand_nat_case]) 1);
1.9 qed_spec_mp "pred_le_mono";
1.10
1.11 goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
1.12 @@ -434,7 +434,7 @@
1.13
1.14 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
1.15 by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
1.16 - setloop (split_tac [expand_if])) 1);
1.17 + addsplits [expand_if]) 1);
1.18 qed "if_Suc_diff_n";
1.19
1.20 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
2.1 --- a/src/HOL/Auth/Event.ML Fri Oct 17 15:23:14 1997 +0200
2.2 +++ b/src/HOL/Auth/Event.ML Fri Oct 17 15:25:12 1997 +0200
2.3 @@ -46,7 +46,7 @@
2.4 qed "spies_subset_spies_Says";
2.5
2.6 goal thy "spies evs <= spies (Notes A X # evs)";
2.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
2.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
2.9 by (Fast_tac 1);
2.10 qed "spies_subset_spies_Notes";
2.11
2.12 @@ -54,14 +54,14 @@
2.13 goal thy "Says A B X : set evs --> X : spies evs";
2.14 by (induct_tac "evs" 1);
2.15 by (ALLGOALS (asm_simp_tac
2.16 - (!simpset setloop split_tac [expand_event_case, expand_if])));
2.17 + (!simpset addsplits [expand_event_case, expand_if])));
2.18 qed_spec_mp "Says_imp_spies";
2.19
2.20 (*Spy sees Notes of bad agents*)
2.21 goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
2.22 by (induct_tac "evs" 1);
2.23 by (ALLGOALS (asm_simp_tac
2.24 - (!simpset setloop split_tac [expand_event_case, expand_if])));
2.25 + (!simpset addsplits [expand_event_case, expand_if])));
2.26 qed_spec_mp "Notes_imp_spies";
2.27
2.28 (*Use with addSEs to derive contradictions from old Says events containing
2.29 @@ -80,7 +80,7 @@
2.30 by (induct_tac "evs" 1);
2.31 by (ALLGOALS (asm_simp_tac
2.32 (!simpset addsimps [parts_insert_spies]
2.33 - setloop split_tac [expand_event_case, expand_if])));
2.34 + addsplits [expand_event_case, expand_if])));
2.35 by (ALLGOALS Blast_tac);
2.36 qed "parts_spies_subset_used";
2.37
2.38 @@ -91,7 +91,7 @@
2.39 by (induct_tac "evs" 1);
2.40 by (ALLGOALS (asm_simp_tac
2.41 (!simpset addsimps [parts_insert_spies]
2.42 - setloop split_tac [expand_event_case, expand_if])));
2.43 + addsplits [expand_event_case, expand_if])));
2.44 by (ALLGOALS Blast_tac);
2.45 bind_thm ("initState_into_used", impOfSubs (result()));
2.46
3.1 --- a/src/HOL/Auth/Message.ML Fri Oct 17 15:23:14 1997 +0200
3.2 +++ b/src/HOL/Auth/Message.ML Fri Oct 17 15:25:12 1997 +0200
3.3 @@ -899,7 +899,7 @@
3.4 (REPEAT o CHANGED)
3.5 (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
3.6 (*...allowing further simplifications*)
3.7 - simp_tac (!simpset setloop split_tac [expand_if]) 1,
3.8 + simp_tac (!simpset addsplits [expand_if]) 1,
3.9 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
3.10 DEPTH_SOLVE
3.11 (Fake_insert_simp_tac 1
4.1 --- a/src/HOL/Auth/NS_Public.ML Fri Oct 17 15:23:14 1997 +0200
4.2 +++ b/src/HOL/Auth/NS_Public.ML Fri Oct 17 15:25:12 1997 +0200
4.3 @@ -124,7 +124,7 @@
4.4 fun analz_induct_tac i =
4.5 etac ns_public.induct i THEN
4.6 ALLGOALS (asm_simp_tac
4.7 - (!simpset setloop split_tac [expand_if]));
4.8 + (!simpset addsplits [expand_if]));
4.9
4.10
4.11 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
5.1 --- a/src/HOL/Auth/NS_Public_Bad.ML Fri Oct 17 15:23:14 1997 +0200
5.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Oct 17 15:25:12 1997 +0200
5.3 @@ -126,8 +126,7 @@
5.4 (*Tactic for proving secrecy theorems*)
5.5 fun analz_induct_tac i =
5.6 etac ns_public.induct i THEN
5.7 - ALLGOALS (asm_simp_tac
5.8 - (!simpset setloop split_tac [expand_if]));
5.9 + ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]));
5.10
5.11
5.12 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
6.1 --- a/src/HOL/Auth/NS_Shared.ML Fri Oct 17 15:23:14 1997 +0200
6.2 +++ b/src/HOL/Auth/NS_Shared.ML Fri Oct 17 15:25:12 1997 +0200
6.3 @@ -267,7 +267,7 @@
6.4 by (ALLGOALS
6.5 (asm_simp_tac
6.6 (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
6.7 - setloop split_tac [expand_if])));
6.8 + addsplits [expand_if])));
6.9 (*Oops*)
6.10 by (blast_tac (!claset addDs [unique_session_keys]) 5);
6.11 (*NS3, replay sub-case*)
7.1 --- a/src/HOL/Auth/OtwayRees.ML Fri Oct 17 15:23:14 1997 +0200
7.2 +++ b/src/HOL/Auth/OtwayRees.ML Fri Oct 17 15:25:12 1997 +0200
7.3 @@ -339,7 +339,7 @@
7.4 by (ALLGOALS
7.5 (asm_simp_tac (!simpset addcongs [conj_cong]
7.6 addsimps [analz_insert_eq, analz_insert_freshK]
7.7 - setloop split_tac [expand_if])));
7.8 + addsplits [expand_if])));
7.9 (*Oops*)
7.10 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
7.11 (*OR4*)
8.1 --- a/src/HOL/Auth/OtwayRees_AN.ML Fri Oct 17 15:23:14 1997 +0200
8.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Oct 17 15:25:12 1997 +0200
8.3 @@ -268,7 +268,7 @@
8.4 by (ALLGOALS
8.5 (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong]
8.6 addsimps [analz_insert_eq, analz_insert_freshK]
8.7 - setloop split_tac [expand_if])));
8.8 + addsplits [expand_if])));
8.9 (*Oops*)
8.10 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
8.11 (*OR4*)
9.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Oct 17 15:23:14 1997 +0200
9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Oct 17 15:25:12 1997 +0200
9.3 @@ -231,7 +231,7 @@
9.4 by (ALLGOALS
9.5 (asm_simp_tac (!simpset addcongs [conj_cong]
9.6 addsimps [analz_insert_eq, analz_insert_freshK]
9.7 - setloop split_tac [expand_if])));
9.8 + addsplits [expand_if])));
9.9 (*Oops*)
9.10 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
9.11 (*OR4*)
10.1 --- a/src/HOL/Auth/Public.ML Fri Oct 17 15:23:14 1997 +0200
10.2 +++ b/src/HOL/Auth/Public.ML Fri Oct 17 15:25:12 1997 +0200
10.3 @@ -58,7 +58,7 @@
10.4 by (induct_tac "evs" 1);
10.5 by (ALLGOALS (asm_simp_tac
10.6 (!simpset addsimps [imageI, spies_Cons]
10.7 - setloop split_tac [expand_event_case, expand_if])));
10.8 + addsplits [expand_event_case, expand_if])));
10.9 qed_spec_mp "spies_pubK";
10.10
10.11 (*Spy sees private keys of bad agents!*)
10.12 @@ -66,7 +66,7 @@
10.13 by (induct_tac "evs" 1);
10.14 by (ALLGOALS (asm_simp_tac
10.15 (!simpset addsimps [imageI, spies_Cons]
10.16 - setloop split_tac [expand_event_case, expand_if])));
10.17 + addsplits [expand_event_case, expand_if])));
10.18 qed "Spy_spies_bad";
10.19
10.20 AddIffs [spies_pubK, spies_pubK RS analz.Inj];
10.21 @@ -114,7 +114,7 @@
10.22 by (res_inst_tac [("x","0")] exI 1);
10.23 by (ALLGOALS (asm_simp_tac
10.24 (!simpset addsimps [used_Cons]
10.25 - setloop split_tac [expand_event_case, expand_if])));
10.26 + addsplits [expand_event_case, expand_if])));
10.27 by Safe_tac;
10.28 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
10.29 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
10.30 @@ -160,5 +160,5 @@
10.31 rangeI,
10.32 insert_Key_singleton,
10.33 insert_Key_image, Un_assoc RS sym]
10.34 - setloop split_tac [expand_if];
10.35 + addsplits [expand_if];
10.36
11.1 --- a/src/HOL/Auth/Recur.ML Fri Oct 17 15:23:14 1997 +0200
11.2 +++ b/src/HOL/Auth/Recur.ML Fri Oct 17 15:25:12 1997 +0200
11.3 @@ -455,7 +455,7 @@
11.4 (asm_simp_tac
11.5 (!simpset addsimps [analz_insert_eq, parts_insert_spies,
11.6 analz_insert_freshK]
11.7 - setloop split_tac [expand_if])));
11.8 + addsplits [expand_if])));
11.9 (*RA4*)
11.10 by (spy_analz_tac 5);
11.11 (*RA2*)
12.1 --- a/src/HOL/Auth/Shared.ML Fri Oct 17 15:23:14 1997 +0200
12.2 +++ b/src/HOL/Auth/Shared.ML Fri Oct 17 15:25:12 1997 +0200
12.3 @@ -36,7 +36,7 @@
12.4 by (induct_tac "evs" 1);
12.5 by (ALLGOALS (asm_simp_tac
12.6 (!simpset addsimps [imageI, spies_Cons]
12.7 - setloop split_tac [expand_event_case, expand_if])));
12.8 + addsplits [expand_event_case, expand_if])));
12.9 qed "Spy_spies_bad";
12.10
12.11 AddSIs [Spy_spies_bad];
12.12 @@ -111,7 +111,7 @@
12.13 by (res_inst_tac [("x","0")] exI 1);
12.14 by (ALLGOALS (asm_simp_tac
12.15 (!simpset addsimps [used_Cons]
12.16 - setloop split_tac [expand_event_case, expand_if])));
12.17 + addsplits [expand_event_case, expand_if])));
12.18 by Safe_tac;
12.19 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
12.20 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
12.21 @@ -238,7 +238,7 @@
12.22 insert_Key_singleton, subset_Compl_range,
12.23 Key_not_used, insert_Key_image, Un_assoc RS sym]
12.24 @disj_comms)
12.25 - setloop split_tac [expand_if];
12.26 + addsplits [expand_if];
12.27
12.28 (*Lemma for the trivial direction of the if-and-only-if*)
12.29 goal thy
13.1 --- a/src/HOL/Auth/TLS.ML Fri Oct 17 15:23:14 1997 +0200
13.2 +++ b/src/HOL/Auth/TLS.ML Fri Oct 17 15:25:12 1997 +0200
13.3 @@ -146,7 +146,7 @@
13.4 REPEAT (FIRSTGOAL analz_mono_contra_tac)
13.5 THEN
13.6 fast_tac (!claset addss (!simpset)) i THEN
13.7 - ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]));
13.8 + ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]));
13.9
13.10
13.11 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
13.12 @@ -198,13 +198,13 @@
13.13 ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*)
13.14 ALLGOALS (asm_simp_tac
13.15 (!simpset addcongs [if_weak_cong]
13.16 - setloop split_tac [expand_if])) THEN
13.17 + addsplits [expand_if])) THEN
13.18 (*Remove instances of pubK B: the Spy already knows all public keys.
13.19 Combining the two simplifier calls makes them run extremely slowly.*)
13.20 ALLGOALS (asm_simp_tac
13.21 (!simpset addcongs [if_weak_cong]
13.22 addsimps [insert_absorb]
13.23 - setloop split_tac [expand_if]));
13.24 + addsplits [expand_if]));
13.25
13.26
13.27 (*** Properties of items found in Notes ***)
14.1 --- a/src/HOL/Auth/Yahalom.ML Fri Oct 17 15:23:14 1997 +0200
14.2 +++ b/src/HOL/Auth/Yahalom.ML Fri Oct 17 15:25:12 1997 +0200
14.3 @@ -227,7 +227,7 @@
14.4 by (ALLGOALS
14.5 (asm_simp_tac
14.6 (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
14.7 - setloop split_tac [expand_if])));
14.8 + addsplits [expand_if])));
14.9 (*Oops*)
14.10 by (blast_tac (!claset addDs [unique_session_keys]) 3);
14.11 (*YM3*)
14.12 @@ -499,7 +499,7 @@
14.13 by (ALLGOALS
14.14 (asm_simp_tac
14.15 (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
14.16 - setloop split_tac [expand_if])));
14.17 + addsplits [expand_if])));
14.18 (*Prove YM3 by showing that no NB can also be an NA*)
14.19 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
14.20 addSEs [MPair_parts]
15.1 --- a/src/HOL/Auth/Yahalom2.ML Fri Oct 17 15:23:14 1997 +0200
15.2 +++ b/src/HOL/Auth/Yahalom2.ML Fri Oct 17 15:25:12 1997 +0200
15.3 @@ -227,7 +227,7 @@
15.4 by (ALLGOALS
15.5 (asm_simp_tac
15.6 (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
15.7 - setloop split_tac [expand_if])));
15.8 + addsplits [expand_if])));
15.9 (*Oops*)
15.10 by (blast_tac (!claset addDs [unique_session_keys]) 3);
15.11 (*YM3*)
16.1 --- a/src/HOL/Divides.ML Fri Oct 17 15:23:14 1997 +0200
16.2 +++ b/src/HOL/Divides.ML Fri Oct 17 15:25:12 1997 +0200
16.3 @@ -222,7 +222,7 @@
16.4 goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
16.5 by (subgoal_tac "k mod 2 < 2" 1);
16.6 by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
16.7 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
16.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
16.9 by (Blast_tac 1);
16.10 qed "mod2_cases";
16.11
17.1 --- a/src/HOL/Finite.ML Fri Oct 17 15:23:14 1997 +0200
17.2 +++ b/src/HOL/Finite.ML Fri Oct 17 15:25:12 1997 +0200
17.3 @@ -176,7 +176,7 @@
17.4 by (Asm_simp_tac 1);
17.5 by (rtac iffI 1);
17.6 by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
17.7 - by (simp_tac (!simpset setloop (split_tac[expand_split])) 1);
17.8 + by (simp_tac (!simpset addsplits [expand_split]) 1);
17.9 by (etac finite_imageI 1);
17.10 by (simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
17.11 by (Auto_tac());
17.12 @@ -244,7 +244,7 @@
17.13 by (SELECT_GOAL(safe_tac (!claset))1);
17.14 by (res_inst_tac [("x","k")] exI 1);
17.15 by (Asm_simp_tac 1);
17.16 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
17.17 + by (simp_tac (!simpset addsplits [expand_if]) 1);
17.18 by (Blast_tac 1);
17.19 by (dtac sym 1);
17.20 by (rotate_tac ~1 1);
17.21 @@ -258,7 +258,7 @@
17.22 by (SELECT_GOAL(safe_tac (!claset))1);
17.23 by (res_inst_tac [("x","k")] exI 1);
17.24 by (Asm_simp_tac 1);
17.25 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
17.26 + by (simp_tac (!simpset addsplits [expand_if]) 1);
17.27 by (Blast_tac 1);
17.28 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
17.29 by (SELECT_GOAL(safe_tac (!claset))1);
17.30 @@ -272,7 +272,7 @@
17.31 by (SELECT_GOAL(safe_tac (!claset))1);
17.32 by (res_inst_tac [("x","k")] exI 1);
17.33 by (Asm_simp_tac 1);
17.34 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
17.35 +by (simp_tac (!simpset addsplits [expand_if]) 1);
17.36 by (Blast_tac 1);
17.37 val lemma = result();
17.38
17.39 @@ -330,7 +330,7 @@
17.40 by (etac finite_induct 1);
17.41 by (ALLGOALS
17.42 (asm_simp_tac (!simpset addsimps [Int_insert_left]
17.43 - setloop split_tac [expand_if])));
17.44 + addsplits [expand_if])));
17.45 qed_spec_mp "card_Un_disjoint";
17.46
17.47 goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
18.1 --- a/src/HOL/IMP/Hoare.ML Fri Oct 17 15:23:14 1997 +0200
18.2 +++ b/src/HOL/IMP/Hoare.ML Fri Oct 17 15:25:12 1997 +0200
18.3 @@ -61,13 +61,13 @@
18.4 (*Not suitable for rewriting: LOOPS!*)
18.5 goal Hoare.thy "wp (WHILE b DO c) Q s = \
18.6 \ (if b s then wp (c;WHILE b DO c) Q s else Q s)";
18.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
18.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
18.9 qed "wp_While_if";
18.10
18.11 goal thy
18.12 "wp (WHILE b DO c) Q s = \
18.13 \ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
18.14 -by (simp_tac (!simpset setloop(split_tac[expand_if])) 1);
18.15 +by (simp_tac (!simpset addsplits [expand_if]) 1);
18.16 by (rtac iffI 1);
18.17 by (rtac weak_coinduct 1);
18.18 by (etac CollectI 1);
19.1 --- a/src/HOL/IOA/IOA.ML Fri Oct 17 15:23:14 1997 +0200
19.2 +++ b/src/HOL/IOA/IOA.ML Fri Oct 17 15:25:12 1997 +0200
19.3 @@ -32,7 +32,7 @@
19.4 by (rtac ext 1);
19.5 by (exhaust_tac "s(i)" 1);
19.6 by (Asm_simp_tac 1);
19.7 - by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
19.8 + by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
19.9 qed "filter_oseq_idemp";
19.10
19.11 goalw IOA.thy [mk_trace_def,filter_oseq_def]
19.12 @@ -42,7 +42,7 @@
19.13 \ (mk_trace A s n = Some(a)) = \
19.14 \ (s(n)=Some(a) & a : externals(asig_of(A)))";
19.15 by (exhaust_tac "s(n)" 1);
19.16 - by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
19.17 + by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
19.18 by (Fast_tac 1);
19.19 qed "mk_trace_thm";
19.20
19.21 @@ -135,7 +135,7 @@
19.22 \ else snd(snd(snd(t)))=snd(snd(snd(s)))))";
19.23 by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
19.24 ioa_projections)
19.25 - setloop (split_tac [expand_if])) 1);
19.26 + addsplits [expand_if]) 1);
19.27 qed "trans_of_par4";
19.28
19.29 goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
20.1 --- a/src/HOL/IOA/Solve.ML Fri Oct 17 15:23:14 1997 +0200
20.2 +++ b/src/HOL/IOA/Solve.ML Fri Oct 17 15:25:12 1997 +0200
20.3 @@ -78,7 +78,7 @@
20.4 by (asm_full_simp_tac
20.5 (!simpset addsimps [executions_def,is_execution_fragment_def,
20.6 par_def,starts_of_def,trans_of_def,filter_oseq_def]
20.7 - setloop (split_tac[expand_if,expand_option_case])) 1);
20.8 + addsplits [expand_if,expand_option_case]) 1);
20.9 qed"comp1_reachable";
20.10
20.11
20.12 @@ -98,7 +98,7 @@
20.13 by (asm_full_simp_tac
20.14 (!simpset addsimps [executions_def,is_execution_fragment_def,
20.15 par_def,starts_of_def,trans_of_def,filter_oseq_def]
20.16 - setloop (split_tac[expand_if,expand_option_case])) 1);
20.17 + addsplits [expand_if,expand_option_case]) 1);
20.18 qed"comp2_reachable";
20.19
20.20
20.21 @@ -141,7 +141,7 @@
20.22 by (Asm_full_simp_tac 2);
20.23 by (Fast_tac 2);
20.24 by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong]
20.25 - setloop (split_tac [expand_if])) 1);
20.26 + addsplits [expand_if]) 1);
20.27 by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
20.28 asm_full_simp_tac(!simpset addsimps[comp1_reachable,
20.29 comp2_reachable])1));
20.30 @@ -160,7 +160,7 @@
20.31 by (asm_full_simp_tac
20.32 (!simpset addsimps [executions_def,is_execution_fragment_def,
20.33 par_def,starts_of_def,trans_of_def,rename_def]
20.34 - setloop (split_tac[expand_option_case])) 1);
20.35 + addsplits [expand_option_case]) 1);
20.36 by (best_tac (!claset addSDs [spec] addDs [sym] addss (!simpset)) 1);
20.37 qed"reachable_rename_ioa";
20.38
21.1 --- a/src/HOL/Induct/Com.ML Fri Oct 17 15:23:14 1997 +0200
21.2 +++ b/src/HOL/Induct/Com.ML Fri Oct 17 15:25:12 1997 +0200
21.3 @@ -53,7 +53,7 @@
21.4
21.5 goalw thy [assign_def] "s[s x/x] = s";
21.6 by (rtac ext 1);
21.7 -by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
21.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
21.9 qed "assign_triv";
21.10
21.11 Addsimps [assign_same, assign_different, assign_triv];
22.1 --- a/src/HOL/Induct/LFilter.ML Fri Oct 17 15:23:14 1997 +0200
22.2 +++ b/src/HOL/Induct/LFilter.ML Fri Oct 17 15:25:12 1997 +0200
22.3 @@ -96,7 +96,7 @@
22.4
22.5 goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
22.6 by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
22.7 - setloop split_tac[expand_if]) 1);
22.8 + addsplits [expand_if]) 1);
22.9 qed "find_LCons";
22.10
22.11
22.12 @@ -141,7 +141,7 @@
22.13 goal thy "lfilter p (LCons x l) = \
22.14 \ (if p x then LCons x (lfilter p l) else lfilter p l)";
22.15 by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
22.16 - setloop split_tac[expand_if]) 1);
22.17 + addsplits [expand_if]) 1);
22.18 qed "lfilter_LCons";
22.19
22.20 AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
22.21 @@ -186,7 +186,7 @@
22.22
22.23 goal thy "lfilter p (lfilter p l) = lfilter p l";
22.24 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
22.25 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
22.26 +by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
22.27 by Safe_tac;
22.28 (*Cases: p x is true or false*)
22.29 by (Blast_tac 1);
22.30 @@ -244,7 +244,7 @@
22.31 \ ==> l'' = LCons y l' --> \
22.32 \ (lfilter q l, LCons y (lfilter q l')) : findRel p";
22.33 by (etac findRel.induct 1);
22.34 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
22.35 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
22.36 by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
22.37 qed_spec_mp "findRel_conj_lfilter";
22.38
22.39 @@ -288,7 +288,7 @@
22.40
22.41 goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
22.42 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
22.43 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
22.44 +by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
22.45 by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
22.46 qed "lfilter_conj";
22.47
22.48 @@ -326,7 +326,7 @@
22.49
22.50 goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
22.51 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
22.52 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
22.53 +by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
22.54 by Safe_tac;
22.55 by (Blast_tac 1);
22.56 by (case_tac "lmap f l : Domain (findRel p)" 1);
23.1 --- a/src/HOL/Induct/LList.ML Fri Oct 17 15:23:14 1997 +0200
23.2 +++ b/src/HOL/Induct/LList.ML Fri Oct 17 15:25:12 1997 +0200
23.3 @@ -10,7 +10,7 @@
23.4
23.5 (** Simplification **)
23.6
23.7 -simpset := !simpset setloop split_tac [expand_split, expand_sum_case];
23.8 +simpset := !simpset addsplits [expand_split, expand_sum_case];
23.9
23.10 (*For adding _eqI rules to a simpset; we must remove Pair_eq because
23.11 it may turn an instance of reflexivity into a conjunction!*)
23.12 @@ -68,11 +68,11 @@
23.13
23.14 (*UNUSED; obsolete?
23.15 goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
23.16 -by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
23.17 +by (simp_tac (!simpset addsplits [expand_split]) 1);
23.18 qed "split_UN1";
23.19
23.20 goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
23.21 -by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
23.22 +by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
23.23 qed "sum_case2_UN1";
23.24 *)
23.25
23.26 @@ -310,7 +310,7 @@
23.27 by (rename_tac "y" 1);
23.28 by (stac prem1 1);
23.29 by (stac prem2 1);
23.30 -by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
23.31 +by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
23.32 by (strip_tac 1);
23.33 by (res_inst_tac [("n", "n")] natE 1);
23.34 by (rename_tac "m" 2);
24.1 --- a/src/HOL/Induct/Mutil.ML Fri Oct 17 15:23:14 1997 +0200
24.2 +++ b/src/HOL/Induct/Mutil.ML Fri Oct 17 15:25:12 1997 +0200
24.3 @@ -94,7 +94,7 @@
24.4 goalw thy [evnodd_def]
24.5 "evnodd (insert (i,j) C) b = \
24.6 \ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
24.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
24.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
24.9 by (Blast_tac 1);
24.10 qed "evnodd_insert";
24.11
24.12 @@ -110,7 +110,7 @@
24.13 by (REPEAT_FIRST assume_tac);
24.14 (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
24.15 by (REPEAT (asm_full_simp_tac (!simpset addsimps [less_Suc_eq, mod_Suc]
24.16 - setloop split_tac [expand_if]) 1
24.17 + addsplits [expand_if]) 1
24.18 THEN Blast_tac 1));
24.19 qed "domino_singleton";
24.20
25.1 --- a/src/HOL/Induct/Perm.ML Fri Oct 17 15:23:14 1997 +0200
25.2 +++ b/src/HOL/Induct/Perm.ML Fri Oct 17 15:25:12 1997 +0200
25.3 @@ -41,7 +41,7 @@
25.4 goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
25.5 by (etac perm.induct 1);
25.6 by (Fast_tac 4);
25.7 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
25.8 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
25.9 val perm_mem_lemma = result();
25.10
25.11 bind_thm ("perm_mem", perm_mem_lemma RS mp);
26.1 --- a/src/HOL/Induct/PropLog.ML Fri Oct 17 15:23:14 1997 +0200
26.2 +++ b/src/HOL/Induct/PropLog.ML Fri Oct 17 15:25:12 1997 +0200
26.3 @@ -142,7 +142,7 @@
26.4 goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
26.5 by (PropLog.pl.induct_tac "p" 1);
26.6 by (Simp_tac 1);
26.7 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
26.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
26.9 by (Simp_tac 1);
26.10 by (Fast_tac 1);
26.11 qed "hyps_Diff";
26.12 @@ -152,7 +152,7 @@
26.13 goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
26.14 by (PropLog.pl.induct_tac "p" 1);
26.15 by (Simp_tac 1);
26.16 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
26.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
26.18 by (Simp_tac 1);
26.19 by (Fast_tac 1);
26.20 qed "hyps_insert";
26.21 @@ -174,7 +174,7 @@
26.22
26.23 goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
26.24 by (PropLog.pl.induct_tac "p" 1);
26.25 -by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
26.26 +by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
26.27 by (Blast_tac 1);
26.28 qed "hyps_subset";
26.29
27.1 --- a/src/HOL/Induct/SList.ML Fri Oct 17 15:23:14 1997 +0200
27.2 +++ b/src/HOL/Induct/SList.ML Fri Oct 17 15:25:12 1997 +0200
27.3 @@ -312,12 +312,12 @@
27.4
27.5 goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
27.6 by (list_ind_tac "xs" 1);
27.7 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
27.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
27.9 qed "mem_append2";
27.10
27.11 goal SList.thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
27.12 by (list_ind_tac "xs" 1);
27.13 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
27.14 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
27.15 qed "mem_filter2";
27.16
27.17
28.1 --- a/src/HOL/Integ/Bin.ML Fri Oct 17 15:23:14 1997 +0200
28.2 +++ b/src/HOL/Integ/Bin.ML Fri Oct 17 15:25:12 1997 +0200
28.3 @@ -100,7 +100,7 @@
28.4
28.5 (**** The carry/borrow functions, bin_succ and bin_pred ****)
28.6
28.7 -val if_ss = !simpset setloop (split_tac [expand_if]) ;
28.8 +val if_ss = !simpset addsplits [expand_if];
28.9
28.10
28.11 (**** integ_of_bin ****)
29.1 --- a/src/HOL/Lambda/Eta.ML Fri Oct 17 15:23:14 1997 +0200
29.2 +++ b/src/HOL/Lambda/Eta.ML Fri Oct 17 15:25:12 1997 +0200
29.3 @@ -37,8 +37,7 @@
29.4 by (dB.induct_tac "t" 1);
29.5 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
29.6 by (Blast_tac 2);
29.7 -by(simp_tac (!simpset addsimps [pred_def]
29.8 - setloop (split_tac [expand_nat_case])) 1);
29.9 +by(simp_tac (!simpset addsimps [pred_def] addsplits [expand_nat_case]) 1);
29.10 by (safe_tac HOL_cs);
29.11 by (ALLGOALS trans_tac);
29.12 qed "free_lift";
29.13 @@ -51,7 +50,7 @@
29.14 by (Blast_tac 2);
29.15 by (asm_full_simp_tac (addsplit (!simpset)) 2);
29.16 by(simp_tac (!simpset addsimps [pred_def,subst_Var]
29.17 - setloop (split_tac [expand_if,expand_nat_case])) 1);
29.18 + addsplits [expand_if,expand_nat_case]) 1);
29.19 by (safe_tac (HOL_cs addSEs [nat_neqE]));
29.20 by (ALLGOALS trans_tac);
29.21 qed "free_subst";
29.22 @@ -169,7 +168,7 @@
29.23
29.24 goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
29.25 by (dB.induct_tac "s" 1);
29.26 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
29.27 + by (simp_tac (!simpset addsplits [expand_if]) 1);
29.28 by (SELECT_GOAL(safe_tac HOL_cs)1);
29.29 by(etac nat_neqE 1);
29.30 by (res_inst_tac [("x","Var nat")] exI 1);
29.31 @@ -180,7 +179,7 @@
29.32 by (assume_tac 2);
29.33 by (etac thin_rl 1);
29.34 by (res_inst_tac [("dB","t")] dB_case_distinction 1);
29.35 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
29.36 + by (simp_tac (!simpset addsplits [expand_if]) 1);
29.37 by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
29.38 by (Simp_tac 1);
29.39 by (Simp_tac 1);
29.40 @@ -196,7 +195,7 @@
29.41 by (etac exE 1);
29.42 by (etac rev_mp 1);
29.43 by (res_inst_tac [("dB","t")] dB_case_distinction 1);
29.44 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
29.45 + by (simp_tac (!simpset addsplits [expand_if]) 1);
29.46 by (Simp_tac 1);
29.47 by (Blast_tac 1);
29.48 by (Simp_tac 1);
29.49 @@ -210,7 +209,7 @@
29.50 by (etac exE 1);
29.51 by (etac rev_mp 1);
29.52 by (res_inst_tac [("dB","t")] dB_case_distinction 1);
29.53 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
29.54 + by (simp_tac (!simpset addsplits [expand_if]) 1);
29.55 by (Simp_tac 1);
29.56 by (Simp_tac 1);
29.57 by (Blast_tac 1);
30.1 --- a/src/HOL/Lambda/Lambda.ML Fri Oct 17 15:23:14 1997 +0200
30.2 +++ b/src/HOL/Lambda/Lambda.ML Fri Oct 17 15:25:12 1997 +0200
30.3 @@ -45,8 +45,8 @@
30.4
30.5 (*** subst and lift ***)
30.6
30.7 -fun addsplit ss = ss addsimps [subst_Var]
30.8 - setloop (split_inside_tac [expand_if]);
30.9 +fun addsplit ss = ss addsimps [subst_Var]
30.10 + setloop (split_inside_tac [expand_if]);
30.11
30.12 goal Lambda.thy "(Var k)[u/k] = u";
30.13 by (asm_full_simp_tac(addsplit(!simpset)) 1);
30.14 @@ -66,7 +66,7 @@
30.15 goal Lambda.thy
30.16 "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
30.17 by (dB.induct_tac "t" 1);
30.18 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
30.19 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if]
30.20 addSolver cut_trans_tac)));
30.21 by (safe_tac HOL_cs);
30.22 by (ALLGOALS trans_tac);
30.23 @@ -76,7 +76,7 @@
30.24 \ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
30.25 by (dB.induct_tac "t" 1);
30.26 by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
30.27 - setloop (split_tac [expand_if,expand_nat_case])
30.28 + addsplits [expand_if,expand_nat_case]
30.29 addSolver cut_trans_tac)));
30.30 by (safe_tac HOL_cs);
30.31 by (ALLGOALS trans_tac);
30.32 @@ -88,7 +88,7 @@
30.33 \ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
30.34 by (dB.induct_tac "t" 1);
30.35 by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
30.36 - setloop (split_tac [expand_if])
30.37 + addsplits [expand_if]
30.38 addSolver cut_trans_tac)));
30.39 by (safe_tac (HOL_cs addSEs [nat_neqE]));
30.40 by (ALLGOALS trans_tac);
30.41 @@ -96,7 +96,7 @@
30.42
30.43 goal Lambda.thy "!k s. (lift t k)[s/k] = t";
30.44 by (dB.induct_tac "t" 1);
30.45 -by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if]))));
30.46 +by (ALLGOALS (asm_full_simp_tac (!simpset addsplits [expand_if])));
30.47 qed "subst_lift";
30.48 Addsimps [subst_lift];
30.49
30.50 @@ -106,7 +106,7 @@
30.51 by (dB.induct_tac "t" 1);
30.52 by (ALLGOALS(asm_simp_tac
30.53 (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
30.54 - setloop (split_tac [expand_if,expand_nat_case])
30.55 + addsplits [expand_if,expand_nat_case]
30.56 addSolver cut_trans_tac)));
30.57 by (safe_tac (HOL_cs addSEs [nat_neqE]));
30.58 by (ALLGOALS trans_tac);
31.1 --- a/src/HOL/Lex/AutoChopper.ML Fri Oct 17 15:23:14 1997 +0200
31.2 +++ b/src/HOL/Lex/AutoChopper.ML Fri Oct 17 15:25:12 1997 +0200
31.3 @@ -18,7 +18,7 @@
31.4 goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
31.5 by (list.induct_tac "xs" 1);
31.6 by (Simp_tac 1);
31.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
31.9 val accept_not_Nil = result() repeat_RS spec;
31.10 Addsimps [accept_not_Nil];
31.11
31.12 @@ -27,7 +27,7 @@
31.13 \ zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
31.14 by (list.induct_tac "xs" 1);
31.15 by (simp_tac (!simpset addcongs [conj_cong]) 1);
31.16 -by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
31.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
31.18 by (strip_tac 1);
31.19 by (rtac conjI 1);
31.20 by (Fast_tac 1);
31.21 @@ -53,17 +53,17 @@
31.22 \ acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
31.23 \ ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
31.24 by (list.induct_tac "xs" 1);
31.25 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.26 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.27 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.28 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
31.29 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
31.30 by (rename_tac "vss lrst" 1);
31.31 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.32 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
31.33 by (res_inst_tac[("xs","vss")] list_eq_cases 1);
31.34 by (hyp_subst_tac 1);
31.35 by (Simp_tac 1);
31.36 by (fast_tac (!claset addSDs [no_acc]) 1);
31.37 by (hyp_subst_tac 1);
31.38 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.39 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
31.40 val step2_a = (result() repeat_RS spec) RS mp;
31.41
31.42
31.43 @@ -73,11 +73,11 @@
31.44 \ (if acc_prefix A st xs \
31.45 \ then ys ~= [] \
31.46 \ else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
31.47 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.48 +by (simp_tac (!simpset addsplits [expand_if]) 1);
31.49 by (list.induct_tac "xs" 1);
31.50 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.51 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.52 by (Fast_tac 1);
31.53 -by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.54 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.55 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
31.56 by (rename_tac "vss lrst" 1);
31.57 by (Asm_simp_tac 1);
31.58 @@ -96,11 +96,11 @@
31.59 \ (if acc_prefix A st xs \
31.60 \ then ? g. ys=r@g & fin A (nexts A st g) \
31.61 \ else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
31.62 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.63 +by (simp_tac (!simpset addsplits [expand_if]) 1);
31.64 by (list.induct_tac "xs" 1);
31.65 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.66 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.67 by (Fast_tac 1);
31.68 -by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.69 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.70 by (strip_tac 1);
31.71 by (rtac conjI 1);
31.72 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
31.73 @@ -135,11 +135,11 @@
31.74 \ (if acc_prefix A st xs \
31.75 \ then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
31.76 \ else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
31.77 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.78 +by (simp_tac (!simpset addsplits [expand_if]) 1);
31.79 by (list.induct_tac "xs" 1);
31.80 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.81 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.82 by (Fast_tac 1);
31.83 -by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.84 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.85 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
31.86 by (rename_tac "vss lrst" 1);
31.87 by (Asm_simp_tac 1);
31.88 @@ -164,7 +164,7 @@
31.89 by (Simp_tac 1);
31.90 by (rtac trans 1);
31.91 by (etac step2_a 1);
31.92 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.93 +by (simp_tac (!simpset addsplits [expand_if]) 1);
31.94 val step2_d = (result() repeat_RS spec) RS mp;
31.95
31.96 Delsimps [split_paired_All];
31.97 @@ -174,11 +174,11 @@
31.98 \ (if acc_prefix A st xs \
31.99 \ then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
31.100 \ else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
31.101 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.102 +by (simp_tac (!simpset addsplits [expand_if]) 1);
31.103 by (list.induct_tac "xs" 1);
31.104 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.105 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.106 by (Fast_tac 1);
31.107 -by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
31.108 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
31.109 by (strip_tac 1);
31.110 by (case_tac "acc_prefix A (next A st a) list" 1);
31.111 by (rtac conjI 1);
31.112 @@ -225,18 +225,18 @@
31.113 by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
31.114 by (rtac mp 1);
31.115 by (etac step2_b 2);
31.116 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.117 + by (simp_tac (!simpset addsplits [expand_if]) 1);
31.118 by (rtac conjI 1);
31.119 by (rtac mp 1);
31.120 by (etac step2_c 2);
31.121 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.122 + by (simp_tac (!simpset addsplits [expand_if]) 1);
31.123 by (rtac conjI 1);
31.124 - by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
31.125 + by (asm_simp_tac (!simpset addsimps [step2_a] addsplits [expand_if]) 1);
31.126 by (rtac conjI 1);
31.127 by (rtac mp 1);
31.128 by (etac step2_d 2);
31.129 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.130 + by (simp_tac (!simpset addsplits [expand_if]) 1);
31.131 by (rtac mp 1);
31.132 by (etac step2_e 2);
31.133 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
31.134 + by (simp_tac (!simpset addsplits [expand_if]) 1);
31.135 qed"auto_chopper_is_auto_chopper";
32.1 --- a/src/HOL/List.ML Fri Oct 17 15:23:14 1997 +0200
32.2 +++ b/src/HOL/List.ML Fri Oct 17 15:25:12 1997 +0200
32.3 @@ -203,17 +203,17 @@
32.4
32.5 goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
32.6 by (asm_simp_tac (!simpset addsimps [hd_append]
32.7 - setloop (split_tac [expand_list_case])) 1);
32.8 + addsplits [expand_list_case]) 1);
32.9 qed "hd_append2";
32.10 Addsimps [hd_append2];
32.11
32.12 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
32.13 -by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
32.14 +by (simp_tac (!simpset addsplits [expand_list_case]) 1);
32.15 qed "tl_append";
32.16
32.17 goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
32.18 by (asm_simp_tac (!simpset addsimps [tl_append]
32.19 - setloop (split_tac [expand_list_case])) 1);
32.20 + addsplits [expand_list_case]) 1);
32.21 qed "tl_append2";
32.22 Addsimps [tl_append2];
32.23
32.24 @@ -309,13 +309,13 @@
32.25
32.26 goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
32.27 by (induct_tac "xs" 1);
32.28 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
32.29 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.30 qed "mem_append";
32.31 Addsimps[mem_append];
32.32
32.33 goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
32.34 by (induct_tac "xs" 1);
32.35 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
32.36 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.37 qed "mem_filter";
32.38 Addsimps[mem_filter];
32.39
32.40 @@ -331,7 +331,7 @@
32.41
32.42 goal thy "(x mem xs) = (x: set xs)";
32.43 by (induct_tac "xs" 1);
32.44 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
32.45 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.46 by (Blast_tac 1);
32.47 qed "set_mem_eq";
32.48
32.49 @@ -377,7 +377,7 @@
32.50
32.51 goal thy "list_all P xs = (!x. x mem xs --> P(x))";
32.52 by (induct_tac "xs" 1);
32.53 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
32.54 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.55 by (Blast_tac 1);
32.56 qed "list_all_mem_conv";
32.57
32.58 @@ -388,13 +388,13 @@
32.59
32.60 goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
32.61 by (induct_tac "xs" 1);
32.62 - by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
32.63 + by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.64 qed "filter_append";
32.65 Addsimps [filter_append];
32.66
32.67 goal thy "size (filter P xs) <= size xs";
32.68 by (induct_tac "xs" 1);
32.69 - by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
32.70 + by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.71 qed "filter_size";
32.72
32.73
32.74 @@ -489,7 +489,7 @@
32.75 (* case 0 *)
32.76 by (Asm_full_simp_tac 1);
32.77 (* case Suc x *)
32.78 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
32.79 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
32.80 qed_spec_mp "nth_mem";
32.81 Addsimps [nth_mem];
32.82
32.83 @@ -497,36 +497,36 @@
32.84
32.85 goal thy "last(xs@[x]) = x";
32.86 by(induct_tac "xs" 1);
32.87 -by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
32.88 +by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.89 qed "last_snoc";
32.90 Addsimps [last_snoc];
32.91
32.92 goal thy "butlast(xs@[x]) = xs";
32.93 by(induct_tac "xs" 1);
32.94 -by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
32.95 +by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.96 qed "butlast_snoc";
32.97 Addsimps [butlast_snoc];
32.98
32.99 goal thy
32.100 "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
32.101 by(induct_tac "xs" 1);
32.102 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
32.103 +by(ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
32.104 qed_spec_mp "butlast_append";
32.105
32.106 goal thy "x:set(butlast xs) --> x:set xs";
32.107 by(induct_tac "xs" 1);
32.108 -by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
32.109 +by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
32.110 qed_spec_mp "in_set_butlastD";
32.111
32.112 goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
32.113 by(asm_simp_tac (!simpset addsimps [butlast_append]
32.114 - setloop (split_tac[expand_if])) 1);
32.115 + addsplits [expand_if]) 1);
32.116 by(blast_tac (!claset addDs [in_set_butlastD]) 1);
32.117 qed "in_set_butlast_appendI1";
32.118
32.119 goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
32.120 by(asm_simp_tac (!simpset addsimps [butlast_append]
32.121 - setloop (split_tac[expand_if])) 1);
32.122 + addsplits [expand_if]) 1);
32.123 by(Clarify_tac 1);
32.124 by(Full_simp_tac 1);
32.125 qed "in_set_butlast_appendI2";
32.126 @@ -678,14 +678,14 @@
32.127 goal thy "takeWhile P xs @ dropWhile P xs = xs";
32.128 by (induct_tac "xs" 1);
32.129 by (Simp_tac 1);
32.130 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
32.131 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
32.132 qed "takeWhile_dropWhile_id";
32.133 Addsimps [takeWhile_dropWhile_id];
32.134
32.135 goal thy "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
32.136 by (induct_tac "xs" 1);
32.137 by (Simp_tac 1);
32.138 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
32.139 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
32.140 by (Blast_tac 1);
32.141 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
32.142 Addsimps [takeWhile_append1];
32.143 @@ -694,7 +694,7 @@
32.144 "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
32.145 by (induct_tac "xs" 1);
32.146 by (Simp_tac 1);
32.147 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
32.148 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
32.149 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
32.150 Addsimps [takeWhile_append2];
32.151
32.152 @@ -702,7 +702,7 @@
32.153 "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
32.154 by (induct_tac "xs" 1);
32.155 by (Simp_tac 1);
32.156 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
32.157 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
32.158 by (Blast_tac 1);
32.159 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
32.160 Addsimps [dropWhile_append1];
32.161 @@ -711,14 +711,14 @@
32.162 "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
32.163 by (induct_tac "xs" 1);
32.164 by (Simp_tac 1);
32.165 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
32.166 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
32.167 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
32.168 Addsimps [dropWhile_append2];
32.169
32.170 goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
32.171 by (induct_tac "xs" 1);
32.172 by (Simp_tac 1);
32.173 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
32.174 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
32.175 qed_spec_mp"set_take_whileD";
32.176
32.177 (** replicate **)
33.1 --- a/src/HOL/MiniML/Generalize.ML Fri Oct 17 15:23:14 1997 +0200
33.2 +++ b/src/HOL/MiniML/Generalize.ML Fri Oct 17 15:25:12 1997 +0200
33.3 @@ -45,8 +45,8 @@
33.4 by (typ.induct_tac "t1" 1);
33.5 by (Simp_tac 1);
33.6 by (case_tac "nat : free_tv A" 1);
33.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
33.8 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
33.9 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
33.10 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
33.11 by (Fast_tac 1);
33.12 by (Asm_simp_tac 1);
33.13 by (Fast_tac 1);
33.14 @@ -99,7 +99,7 @@
33.15 by (rename_tac "R" 1);
33.16 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
33.17 by (typ.induct_tac "t" 1);
33.18 - by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
33.19 + by (simp_tac (!simpset addsplits [expand_if]) 1);
33.20 by (Asm_simp_tac 1);
33.21 qed "gen_bound_typ_instance";
33.22
33.23 @@ -109,7 +109,7 @@
33.24 by (rename_tac "S" 1);
33.25 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
33.26 by (typ.induct_tac "t" 1);
33.27 - by (asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
33.28 + by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
33.29 by (Fast_tac 1);
33.30 by (Asm_simp_tac 1);
33.31 qed "free_tv_subset_gen_le";
33.32 @@ -123,8 +123,8 @@
33.33 by (typ.induct_tac "t" 1);
33.34 by (Simp_tac 1);
33.35 by (case_tac "nat : free_tv A" 1);
33.36 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
33.37 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
33.38 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
33.39 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
33.40 by (subgoal_tac "n <= n + nat" 1);
33.41 by (forw_inst_tac [("t","A")] new_tv_le 1);
33.42 by (assume_tac 1);
34.1 --- a/src/HOL/MiniML/Instance.ML Fri Oct 17 15:23:14 1997 +0200
34.2 +++ b/src/HOL/MiniML/Instance.ML Fri Oct 17 15:25:12 1997 +0200
34.3 @@ -66,8 +66,8 @@
34.4 by (rename_tac "S1 S2" 1);
34.5 by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
34.6 by (safe_tac (!claset));
34.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
34.8 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
34.9 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
34.10 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
34.11 by (strip_tac 1);
34.12 by (dres_inst_tac [("x","x")] bspec 1);
34.13 by (assume_tac 1);
34.14 @@ -82,8 +82,8 @@
34.15 goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
34.16 \ (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
34.17 by (type_scheme.induct_tac "sch" 1);
34.18 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
34.19 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [le_add2,diff_add_inverse2]) 1);
34.20 +by (simp_tac (!simpset addsimps [leD] addsplits [expand_if]) 1);
34.21 +by (simp_tac (!simpset addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1);
34.22 by (Asm_simp_tac 1);
34.23 qed_spec_mp "subst_to_scheme_inverse";
34.24
34.25 @@ -96,9 +96,9 @@
34.26 \ (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
34.27 \ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
34.28 by (type_scheme.induct_tac "sch" 1);
34.29 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
34.30 +by (simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1);
34.31 by (Asm_simp_tac 1);
34.32 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
34.33 +by (asm_full_simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1);
34.34 val aux2 = result () RS mp;
34.35
34.36
35.1 --- a/src/HOL/MiniML/Maybe.ML Fri Oct 17 15:23:14 1997 +0200
35.2 +++ b/src/HOL/MiniML/Maybe.ML Fri Oct 17 15:25:12 1997 +0200
35.3 @@ -25,7 +25,7 @@
35.4
35.5 goal thy
35.6 "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
35.7 -by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
35.8 +by(simp_tac (!simpset addsplits [expand_option_bind]) 1);
35.9 qed "option_bind_eq_None";
35.10
35.11 Addsimps [option_bind_eq_None];
36.1 --- a/src/HOL/MiniML/MiniML.ML Fri Oct 17 15:23:14 1997 +0200
36.2 +++ b/src/HOL/MiniML/MiniML.ML Fri Oct 17 15:25:12 1997 +0200
36.3 @@ -82,7 +82,7 @@
36.4 goalw thy [free_tv_subst,dom_def]
36.5 "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
36.6 \ free_tv A Un free_tv t";
36.7 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
36.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
36.9 by (Fast_tac 1);
36.10 qed "dom_S'";
36.11
36.12 @@ -110,7 +110,7 @@
36.13 \ (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
36.14 \ {x. ? y. x = n + y}";
36.15 by (typ.induct_tac "t1" 1);
36.16 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
36.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
36.18 by (Fast_tac 1);
36.19 by (Simp_tac 1);
36.20 by (Fast_tac 1);
37.1 --- a/src/HOL/MiniML/Type.ML Fri Oct 17 15:23:14 1997 +0200
37.2 +++ b/src/HOL/MiniML/Type.ML Fri Oct 17 15:25:12 1997 +0200
37.3 @@ -352,7 +352,7 @@
37.4
37.5 goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
37.6 by (type_scheme.induct_tac "sch" 1);
37.7 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
37.8 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
37.9 by (strip_tac 1);
37.10 by (Fast_tac 1);
37.11 qed "free_tv_ML_scheme";
37.12 @@ -423,14 +423,14 @@
37.13 goal thy
37.14 "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
37.15 by (typ.induct_tac "t" 1);
37.16 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
37.17 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
37.18 qed "subst_te_new_tv";
37.19 Addsimps [subst_te_new_tv];
37.20
37.21 goal thy
37.22 "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
37.23 by (type_scheme.induct_tac "sch" 1);
37.24 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
37.25 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
37.26 qed_spec_mp "subst_te_new_type_scheme";
37.27 Addsimps [subst_te_new_type_scheme];
37.28
37.29 @@ -546,13 +546,13 @@
37.30 Addsimps [new_tv_not_free_tv];
37.31
37.32 goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
37.33 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
37.34 +by (simp_tac (!simpset addsplits [expand_if]) 1);
37.35 by (safe_tac (!claset));
37.36 by (trans_tac 1);
37.37 qed "less_maxL";
37.38
37.39 goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
37.40 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
37.41 +by (simp_tac (!simpset addsplits [expand_if]) 1);
37.42 by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1);
37.43 val less_maxR = result();
37.44
37.45 @@ -585,11 +585,11 @@
37.46 Addsimps [fresh_variable_type_schemes];
37.47
37.48 goalw thy [max_def] "!!n::nat. n <= (max n n')";
37.49 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
37.50 +by (simp_tac (!simpset addsplits [expand_if]) 1);
37.51 val le_maxL = result();
37.52
37.53 goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
37.54 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
37.55 +by (simp_tac (!simpset addsplits [expand_if]) 1);
37.56 by (fast_tac (!claset addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
37.57 val le_maxR = result();
37.58
38.1 --- a/src/HOL/MiniML/W.ML Fri Oct 17 15:23:14 1997 +0200
38.2 +++ b/src/HOL/MiniML/W.ML Fri Oct 17 15:25:12 1997 +0200
38.3 @@ -18,7 +18,7 @@
38.4 "!A n S t m. W e A n = Some (S,t,m) --> n<=m";
38.5 by (expr.induct_tac "e" 1);
38.6 (* case Var(n) *)
38.7 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
38.8 +by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
38.9 by (strip_tac 1);
38.10 by (etac conjE 1);
38.11 by (etac conjE 1);
38.12 @@ -27,10 +27,10 @@
38.13 by (dtac sym 1);
38.14 by (Asm_full_simp_tac 1);
38.15 (* case Abs e *)
38.16 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
38.17 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
38.18 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
38.19 (* case App e1 e2 *)
38.20 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
38.21 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
38.22 by (strip_tac 1);
38.23 by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
38.24 by (eres_inst_tac [("x","A")] allE 1);
38.25 @@ -50,7 +50,7 @@
38.26 by (Asm_simp_tac 1);
38.27 by (Asm_simp_tac 1);
38.28 (* case LET e1 e2 *)
38.29 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
38.30 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
38.31 by (strip_tac 1);
38.32 by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
38.33 by (REPEAT (etac conjE 1));
38.34 @@ -88,7 +88,7 @@
38.35 by (assume_tac 2);
38.36 by (rtac add_le_mono 1);
38.37 by (Simp_tac 1);
38.38 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
38.39 +by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1);
38.40 by (strip_tac 1);
38.41 by (rtac new_tv_le 1);
38.42 by (mp_tac 2);
38.43 @@ -96,7 +96,7 @@
38.44 by (assume_tac 2);
38.45 by (rtac add_le_mono 1);
38.46 by (Simp_tac 1);
38.47 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
38.48 +by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1);
38.49 by (strip_tac 1);
38.50 by (dtac not_leE 1);
38.51 by (rtac less_or_eq_imp_le 1);
38.52 @@ -111,7 +111,7 @@
38.53 \ new_tv m S & new_tv m t";
38.54 by (expr.induct_tac "e" 1);
38.55 (* case Var n *)
38.56 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
38.57 +by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
38.58 by (strip_tac 1);
38.59 by (REPEAT (etac conjE 1));
38.60 by (rtac conjI 1);
38.61 @@ -125,14 +125,14 @@
38.62 by (Asm_full_simp_tac 1);
38.63 (* case Abs e *)
38.64 by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
38.65 - setloop (split_tac [expand_option_bind])) 1);
38.66 + addsplits [expand_option_bind]) 1);
38.67 by (strip_tac 1);
38.68 by (eres_inst_tac [("x","Suc n")] allE 1);
38.69 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
38.70 by (fast_tac (HOL_cs addss (!simpset
38.71 addsimps [new_tv_subst,new_tv_Suc_list])) 1);
38.72 (* case App e1 e2 *)
38.73 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
38.74 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
38.75 by (strip_tac 1);
38.76 by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
38.77 by (eres_inst_tac [("x","n")] allE 1);
38.78 @@ -174,7 +174,7 @@
38.79 [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
38.80 addss (!simpset)) 1);
38.81 (* case LET e1 e2 *)
38.82 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
38.83 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
38.84 by (strip_tac 1);
38.85 by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
38.86 by (REPEAT (etac conjE 1));
38.87 @@ -239,7 +239,7 @@
38.88 by (expr.induct_tac "e" 1);
38.89 (* case Var n *)
38.90 by (simp_tac (!simpset addsimps
38.91 - [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
38.92 + [free_tv_subst] addsplits [expand_option_bind,expand_if]) 1);
38.93 by (strip_tac 1);
38.94 by (REPEAT (etac conjE 1));
38.95 by (hyp_subst_tac 1);
38.96 @@ -255,7 +255,7 @@
38.97 by (Asm_full_simp_tac 1);
38.98 (* case Abs e *)
38.99 by (asm_full_simp_tac (!simpset addsimps
38.100 - [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
38.101 + [free_tv_subst] addsplits [expand_option_bind] delsimps all_simps) 1);
38.102 by (strip_tac 1);
38.103 by (rename_tac "S t n1 S1 t1 m v" 1);
38.104 by (eres_inst_tac [("x","Suc n")] allE 1);
38.105 @@ -267,7 +267,7 @@
38.106 by (best_tac (HOL_cs addIs [cod_app_subst]
38.107 addss (!simpset addsimps [less_Suc_eq])) 1);
38.108 (* case App e1 e2 *)
38.109 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
38.110 +by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
38.111 by (strip_tac 1);
38.112 by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
38.113 by (eres_inst_tac [("x","n")] allE 1);
38.114 @@ -303,7 +303,7 @@
38.115 addEs [UnE]
38.116 addss !simpset) 1);
38.117 (* LET e1 e2 *)
38.118 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
38.119 +by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
38.120 by (strip_tac 1);
38.121 by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
38.122 by (eres_inst_tac [("x","nat")] allE 1);
38.123 @@ -338,7 +338,7 @@
38.124 "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
38.125 by (expr.induct_tac "e" 1);
38.126 (* case Var n *)
38.127 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
38.128 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
38.129 by (strip_tac 1);
38.130 by (rtac has_type.VarI 1);
38.131 by (Simp_tac 1);
38.132 @@ -347,7 +347,7 @@
38.133 by (rtac refl 1);
38.134 (* case Abs e *)
38.135 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
38.136 - setloop (split_tac [expand_option_bind])) 1);
38.137 + addsplits [expand_option_bind]) 1);
38.138 by (strip_tac 1);
38.139 by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
38.140 by (Asm_full_simp_tac 1);
38.141 @@ -360,7 +360,7 @@
38.142 by (Asm_simp_tac 1);
38.143 by (assume_tac 1);
38.144 (* case App e1 e2 *)
38.145 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
38.146 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
38.147 by (strip_tac 1);
38.148 by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
38.149 by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
38.150 @@ -392,7 +392,7 @@
38.151 by (mp_tac 1);
38.152 by (assume_tac 1);
38.153 (* case Let e1 e2 *)
38.154 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
38.155 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
38.156 by (strip_tac 1);
38.157 by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1);
38.158 by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
38.159 @@ -469,8 +469,7 @@
38.160 by (expr.induct_tac "e" 1);
38.161 (* case Var n *)
38.162 by (strip_tac 1);
38.163 -by (simp_tac (!simpset addcongs [conj_cong]
38.164 - setloop (split_tac [expand_if])) 1);
38.165 +by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
38.166 by (eresolve_tac has_type_casesE 1);
38.167 by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
38.168 by (etac exE 1);
38.169 @@ -491,7 +490,7 @@
38.170 by (eres_inst_tac [("x","Suc n")] allE 1);
38.171 by (best_tac (HOL_cs addSDs [mk_scheme_injective]
38.172 addss (!simpset addcongs [conj_cong]
38.173 - setloop (split_tac [expand_option_bind]))) 1);
38.174 + addsplits [expand_option_bind])) 1);
38.175 (** LEVEL 19 **)
38.176
38.177 (* case App e1 e2 *)
38.178 @@ -531,8 +530,7 @@
38.179 by (case_tac "na:free_tv Sa" 2);
38.180 (* n1 ~: free_tv S1 *)
38.181 by (forward_tac [not_free_impl_id] 3);
38.182 -by (asm_simp_tac (!simpset
38.183 - setloop (split_tac [expand_if])) 3);
38.184 +by (asm_simp_tac (!simpset addsplits [expand_if]) 3);
38.185 (* na : free_tv Sa *)
38.186 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
38.187 by (dtac eq_subst_scheme_list_eq_free 2);
38.188 @@ -540,8 +538,7 @@
38.189 by (Asm_simp_tac 2);
38.190 by (case_tac "na:dom Sa" 2);
38.191 (* na ~: dom Sa *)
38.192 -by (asm_full_simp_tac (!simpset addsimps [dom_def]
38.193 - setloop (split_tac [expand_if])) 3);
38.194 +by (asm_full_simp_tac (!simpset addsimps [dom_def] addsplits [expand_if]) 3);
38.195 (* na : dom Sa *)
38.196 by (rtac eq_free_eq_subst_te 2);
38.197 by (strip_tac 2);
38.198 @@ -553,7 +550,7 @@
38.199 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss
38.200 (!simpset addsimps [cod_def,free_tv_subst])) 3);
38.201 by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst]
38.202 - setloop (split_tac [expand_if]))) 2);
38.203 + addsplits [expand_if])) 2);
38.204 by (Simp_tac 2);
38.205 by (rtac eq_free_eq_subst_te 2);
38.206 by (strip_tac 2 );
38.207 @@ -564,16 +561,16 @@
38.208 by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
38.209 by (case_tac "na: free_tv t - free_tv Sa" 2);
38.210 (* case na ~: free_tv t - free_tv Sa *)
38.211 -by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
38.212 +by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3);
38.213 by (Fast_tac 3);
38.214 (* case na : free_tv t - free_tv Sa *)
38.215 -by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
38.216 +by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
38.217 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
38.218 by (dtac eq_subst_scheme_list_eq_free 2);
38.219 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
38.220 (** LEVEL 75 **)
38.221 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
38.222 -by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
38.223 +by (asm_simp_tac (!simpset addsplits [expand_option_bind]) 1);
38.224 by (safe_tac HOL_cs );
38.225 by (dtac mgu_Some 1);
38.226 by ( fast_tac (HOL_cs addss !simpset) 1);
38.227 @@ -603,9 +600,9 @@
38.228 new_tv_not_free_tv]) 2);
38.229 by (case_tac "na: free_tv t - free_tv Sa" 1);
38.230 (* case na ~: free_tv t - free_tv Sa *)
38.231 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
38.232 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
38.233 (* case na : free_tv t - free_tv Sa *)
38.234 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
38.235 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
38.236 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
38.237 by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
38.238 eq_subst_scheme_list_eq_free] addss ((!simpset addsimps
39.1 --- a/src/HOL/Prod.ML Fri Oct 17 15:23:14 1997 +0200
39.2 +++ b/src/HOL/Prod.ML Fri Oct 17 15:25:12 1997 +0200
39.3 @@ -168,7 +168,7 @@
39.4 qed "expand_split";
39.5
39.6 (* could be done after split_tac has been speeded up significantly:
39.7 -simpset := (!simpset setloop split_tac[expand_split]);
39.8 +simpset := (!simpset addsplits [expand_split]);
39.9 precompute the constants involved and don't do anything unless
39.10 the current goal contains one of those constants
39.11 *)
40.1 --- a/src/HOL/Set.ML Fri Oct 17 15:23:14 1997 +0200
40.2 +++ b/src/HOL/Set.ML Fri Oct 17 15:25:12 1997 +0200
40.3 @@ -646,7 +646,7 @@
40.4
40.5
40.6 (** Rewrite rules for boolean case-splitting: faster than
40.7 - setloop split_tac[expand_if]
40.8 + addsplits[expand_if]
40.9 **)
40.10
40.11 bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
40.12 @@ -669,7 +669,7 @@
40.13
40.14 (*Not for Addsimps -- it can cause goals to blow up!*)
40.15 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
40.16 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
40.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
40.18 qed "mem_if";
40.19
40.20 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
41.1 --- a/src/HOL/Subst/Subst.ML Fri Oct 17 15:23:14 1997 +0200
41.2 +++ b/src/HOL/Subst/Subst.ML Fri Oct 17 15:25:12 1997 +0200
41.3 @@ -41,8 +41,7 @@
41.4 qed "agreement";
41.5
41.6 goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
41.7 -by (simp_tac (!simpset addsimps [agreement]
41.8 - setloop (split_tac [expand_if])) 1);
41.9 +by (simp_tac (!simpset addsimps [agreement] addsplits [expand_if]) 1);
41.10 qed_spec_mp"repl_invariance";
41.11
41.12 val asms = goal Subst.thy
41.13 @@ -112,7 +111,7 @@
41.14 by (induct_tac "t" 1);
41.15 by (ALLGOALS Asm_simp_tac);
41.16 by (alist_ind_tac "r" 1);
41.17 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
41.18 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
41.19 qed "subst_comp";
41.20
41.21 Addsimps [subst_comp];
41.22 @@ -131,7 +130,7 @@
41.23 by (simp_tac (!simpset addsimps [subst_eq_iff]) 1);
41.24 by (rtac allI 1);
41.25 by (induct_tac "t" 1);
41.26 -by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]))));
41.27 +by (ALLGOALS (asm_full_simp_tac (!simpset addsplits [expand_if])));
41.28 qed "Cons_trivial";
41.29
41.30
41.31 @@ -144,7 +143,7 @@
41.32
41.33 goal Subst.thy "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
41.34 by (alist_ind_tac "s" 1);
41.35 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
41.36 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
41.37 by (Blast_tac 1);
41.38 qed "sdom_iff";
41.39
41.40 @@ -204,7 +203,7 @@
41.41
41.42 goal Subst.thy "(M <| [(x, Var x)]) = M";
41.43 by (induct_tac "M" 1);
41.44 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
41.45 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
41.46 qed "id_subst_lemma";
41.47
41.48 Addsimps [id_subst_lemma];
42.1 --- a/src/HOL/Subst/Unifier.ML Fri Oct 17 15:23:14 1997 +0200
42.2 +++ b/src/HOL/Subst/Unifier.ML Fri Oct 17 15:25:12 1997 +0200
42.3 @@ -83,7 +83,7 @@
42.4 goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
42.5 by (simp_tac (!simpset addsimps [vars_iff_occseq, Idem_iff, srange_iff,
42.6 empty_iff_all_not]
42.7 - setloop (split_tac [expand_if])) 1);
42.8 + addsplits [expand_if]) 1);
42.9 by (Blast_tac 1);
42.10 qed_spec_mp "Var_Idem";
42.11
43.1 --- a/src/HOL/Subst/Unify.ML Fri Oct 17 15:23:14 1997 +0200
43.2 +++ b/src/HOL/Subst/Unify.ML Fri Oct 17 15:25:12 1997 +0200
43.3 @@ -154,14 +154,14 @@
43.4 by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
43.5 by (ALLGOALS
43.6 (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
43.7 - setloop (split_tac [expand_if]))));
43.8 + addsplits [expand_if])));
43.9 (*Const-Const case*)
43.10 by (simp_tac
43.11 (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
43.12 inv_image_def, less_eq]) 1);
43.13 (** LEVEL 7 **)
43.14 (*Comb-Comb case*)
43.15 -by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
43.16 +by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
43.17 by (strip_tac 1);
43.18 by (rtac (trans_unifyRel RS transD) 1);
43.19 by (Blast_tac 1);
43.20 @@ -184,7 +184,7 @@
43.21 \ of None => None \
43.22 \ | Some sigma => Some (theta <> sigma)))";
43.23 by (asm_simp_tac (!simpset addsimps (unify_TC::unifyRules0)
43.24 - setloop split_tac [expand_option_case]) 1);
43.25 + addsplits [expand_option_case]) 1);
43.26 qed "unifyCombComb";
43.27
43.28
43.29 @@ -207,7 +207,7 @@
43.30
43.31 goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
43.32 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
43.33 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
43.34 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
43.35 (*Const-Const case*)
43.36 by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
43.37 (*Const-Var case*)
43.38 @@ -220,7 +220,7 @@
43.39 by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
43.40 (** LEVEL 8 **)
43.41 (*Comb-Comb case*)
43.42 -by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
43.43 +by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
43.44 by (strip_tac 1);
43.45 by (rotate_tac ~2 1);
43.46 by (asm_full_simp_tac
43.47 @@ -246,7 +246,7 @@
43.48 by (ALLGOALS
43.49 (asm_simp_tac
43.50 (!simpset addsimps [Var_Idem]
43.51 - setloop split_tac[expand_if, expand_option_case])));
43.52 + addsplits [expand_if,expand_option_case])));
43.53 (*Comb-Comb case*)
43.54 by (safe_tac (!claset));
43.55 by (REPEAT (dtac spec 1 THEN mp_tac 1));
44.1 --- a/src/HOL/W0/I.ML Fri Oct 17 15:23:14 1997 +0200
44.2 +++ b/src/HOL/W0/I.ML Fri Oct 17 15:25:12 1997 +0200
44.3 @@ -144,8 +144,7 @@
44.4 goal I.thy "!a m s. \
44.5 \ new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
44.6 by (expr.induct_tac "e" 1);
44.7 - by (simp_tac (!simpset addsimps [app_subst_list]
44.8 - setloop (split_tac [expand_if])) 1);
44.9 + by (simp_tac (!simpset addsimps [app_subst_list] addsplits [expand_if]) 1);
44.10 by (Simp_tac 1);
44.11 by (strip_tac 1);
44.12 by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
45.1 --- a/src/HOL/W0/Maybe.ML Fri Oct 17 15:23:14 1997 +0200
45.2 +++ b/src/HOL/W0/Maybe.ML Fri Oct 17 15:25:12 1997 +0200
45.3 @@ -26,7 +26,7 @@
45.4
45.5 goal Maybe.thy
45.6 "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
45.7 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
45.8 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
45.9 qed "bind_eq_Fail";
45.10
45.11 Addsimps [bind_eq_Fail];
46.1 --- a/src/HOL/W0/Type.ML Fri Oct 17 15:23:14 1997 +0200
46.2 +++ b/src/HOL/W0/Type.ML Fri Oct 17 15:25:12 1997 +0200
46.3 @@ -157,7 +157,7 @@
46.4 goal thy
46.5 "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
46.6 by (typ.induct_tac "t" 1);
46.7 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
46.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
46.9 qed "subst_te_new_tv";
46.10 Addsimps [subst_te_new_tv];
46.11
46.12 @@ -259,7 +259,7 @@
46.13 (* case [] *)
46.14 by (Simp_tac 1);
46.15 (* case x#xl *)
46.16 -by (fast_tac (set_cs addss(!simpset setloop (split_tac [expand_if]))) 1);
46.17 +by (fast_tac (set_cs addss(!simpset addsplits [expand_if])) 1);
46.18 qed_spec_mp "ftv_mem_sub_ftv_list";
46.19 Addsimps [ftv_mem_sub_ftv_list];
46.20
47.1 --- a/src/HOL/W0/W.ML Fri Oct 17 15:23:14 1997 +0200
47.2 +++ b/src/HOL/W0/W.ML Fri Oct 17 15:25:12 1997 +0200
47.3 @@ -14,15 +14,15 @@
47.4 "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
47.5 by (expr.induct_tac "e" 1);
47.6 (* case Var n *)
47.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
47.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
47.9 (* case Abs e *)
47.10 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
47.11 - setloop (split_tac [expand_bind])) 1);
47.12 + addsplits [expand_bind]) 1);
47.13 by (strip_tac 1);
47.14 by (dtac sym 1);
47.15 by (fast_tac (HOL_cs addss !simpset) 1);
47.16 (* case App e1 e2 *)
47.17 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
47.18 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
47.19 by (strip_tac 1);
47.20 by ( rename_tac "sa ta na sb tb nb sc" 1);
47.21 by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
47.22 @@ -45,12 +45,12 @@
47.23 "!a n s t m. W e a n = Ok (s,t,m) --> n<=m";
47.24 by (expr.induct_tac "e" 1);
47.25 (* case Var(n) *)
47.26 -by (fast_tac (HOL_cs addss(!simpset setloop (split_tac [expand_if]))) 1);
47.27 +by (fast_tac (HOL_cs addss(!simpset addsplits [expand_if])) 1);
47.28 (* case Abs e *)
47.29 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
47.30 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
47.31 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
47.32 (* case App e1 e2 *)
47.33 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
47.34 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
47.35 by (strip_tac 1);
47.36 by (rename_tac "s t na sa ta nb sb sc tb m" 1);
47.37 by (eres_inst_tac [("x","a")] allE 1);
47.38 @@ -93,10 +93,10 @@
47.39 (* case Var n *)
47.40 by (fast_tac (HOL_cs addDs [list_all_nth] addss (!simpset
47.41 addsimps [id_subst_def,new_tv_list,new_tv_subst]
47.42 - setloop (split_tac [expand_if]))) 1);
47.43 + addsplits [expand_if])) 1);
47.44 (* case Abs e *)
47.45 by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
47.46 - setloop (split_tac [expand_bind])) 1);
47.47 + addsplits [expand_bind]) 1);
47.48 by (strip_tac 1);
47.49 by (eres_inst_tac [("x","Suc n")] allE 1);
47.50 by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
47.51 @@ -104,7 +104,7 @@
47.52 addsimps [new_tv_subst,new_tv_Suc_list])) 1);
47.53
47.54 (* case App e1 e2 *)
47.55 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
47.56 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
47.57 by (strip_tac 1);
47.58 by (rename_tac "s t na sa ta nb sb sc tb m" 1);
47.59 by (eres_inst_tac [("x","n")] allE 1);
47.60 @@ -160,11 +160,11 @@
47.61 by (expr.induct_tac "e" 1);
47.62 (* case Var n *)
47.63 by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list]
47.64 - addss (!simpset setloop (split_tac [expand_if]))) 1);
47.65 + addss (!simpset addsplits [expand_if])) 1);
47.66
47.67 (* case Abs e *)
47.68 by (asm_full_simp_tac (!simpset addsimps
47.69 - [free_tv_subst] setloop (split_tac [expand_bind])) 1);
47.70 + [free_tv_subst] addsplits [expand_bind]) 1);
47.71 by (strip_tac 1);
47.72 by (rename_tac "s t na sa ta m v" 1);
47.73 by (eres_inst_tac [("x","Suc n")] allE 1);
47.74 @@ -178,7 +178,7 @@
47.75 addss (!simpset addsimps [less_Suc_eq])) 1);
47.76 (** LEVEL 12 **)
47.77 (* case App e1 e2 *)
47.78 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
47.79 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
47.80 by (strip_tac 1);
47.81 by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
47.82 by (eres_inst_tac [("x","n")] allE 1);
47.83 @@ -227,7 +227,7 @@
47.84 (* case Var n *)
47.85 by (strip_tac 1);
47.86 by (simp_tac (!simpset addcongs [conj_cong]
47.87 - setloop (split_tac [expand_if])) 1);
47.88 + addsplits [expand_if]) 1);
47.89 by (eresolve_tac has_type_casesE 1);
47.90 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
47.91 by (res_inst_tac [("x","s'")] exI 1);
47.92 @@ -242,7 +242,7 @@
47.93 by (eres_inst_tac [("x","t2")] allE 1);
47.94 by (eres_inst_tac [("x","Suc n")] allE 1);
47.95 by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
47.96 - setloop (split_tac [expand_bind]))) 1);
47.97 + addsplits [expand_bind])) 1);
47.98
47.99 (** LEVEL 17 **)
47.100 (* case App e1 e2 *)
47.101 @@ -285,7 +285,7 @@
47.102 by (case_tac "na:free_tv sa" 2);
47.103 (* na ~: free_tv sa *)
47.104 by (forward_tac [not_free_impl_id] 3);
47.105 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
47.106 +by (asm_simp_tac (!simpset addsplits [expand_if]) 3);
47.107 (* na : free_tv sa *)
47.108 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
47.109 by (dtac eq_subst_tel_eq_free 2);
47.110 @@ -295,7 +295,7 @@
47.111 (* na ~: dom sa *)
47.112 (** LEVEL 50 **)
47.113 by (asm_full_simp_tac (!simpset addsimps [dom_def]
47.114 - setloop (split_tac [expand_if])) 3);
47.115 + addsplits [expand_if]) 3);
47.116 (* na : dom sa *)
47.117 by (rtac eq_free_eq_subst_te 2);
47.118 by (strip_tac 2);
47.119 @@ -307,7 +307,7 @@
47.120 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss
47.121 (!simpset addsimps [cod_def,free_tv_subst])) 3);
47.122 by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst]
47.123 - setloop (split_tac [expand_if]))) 2);
47.124 + addsplits [expand_if])) 2);
47.125
47.126 (** LEVEL 60 **)
47.127 by (Simp_tac 2);
47.128 @@ -321,16 +321,16 @@
47.129 by (case_tac "na: free_tv t - free_tv sa" 2);
47.130 (** LEVEL 69 **)
47.131 (* case na ~: free_tv t - free_tv sa *)
47.132 -by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
47.133 +by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3);
47.134 (* case na : free_tv t - free_tv sa *)
47.135 -by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
47.136 +by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
47.137 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
47.138 by (dtac eq_subst_tel_eq_free 2);
47.139 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
47.140 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
47.141 by (Fast_tac 2);
47.142 (** LEVEL 76 **)
47.143 -by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
47.144 +by (asm_simp_tac (!simpset addsplits [expand_bind]) 1);
47.145 by (safe_tac HOL_cs);
47.146 by (dtac mgu_Ok 1);
47.147 by ( fast_tac (HOL_cs addss !simpset) 1);
47.148 @@ -359,9 +359,9 @@
47.149 new_tv_not_free_tv]) 2);
47.150 by (case_tac "na: free_tv t - free_tv sa" 1);
47.151 (* case na ~: free_tv t - free_tv sa *)
47.152 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
47.153 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
47.154 (* case na : free_tv t - free_tv sa *)
47.155 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
47.156 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
47.157 by (dtac (free_tv_app_subst_tel RS subsetD) 1);
47.158 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
47.159 eq_subst_tel_eq_free]
48.1 --- a/src/HOL/WF.ML Fri Oct 17 15:23:14 1997 +0200
48.2 +++ b/src/HOL/WF.ML Fri Oct 17 15:25:12 1997 +0200
48.3 @@ -151,8 +151,7 @@
48.4 H_cong to expose the equality*)
48.5 goalw WF.thy [cut_def]
48.6 "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
48.7 -by (simp_tac (HOL_ss addsimps [expand_fun_eq]
48.8 - setloop (split_tac [expand_if])) 1);
48.9 +by (simp_tac (HOL_ss addsimps [expand_fun_eq] addsplits [expand_if]) 1);
48.10 qed "cuts_eq";
48.11
48.12 goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
48.13 @@ -193,7 +192,7 @@
48.14 by (cut_facts_tac prems 1);
48.15 by (rtac ext 1);
48.16 by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
48.17 - setloop (split_tac [expand_if])) 1);
48.18 + addsplits [expand_if]) 1);
48.19 qed "is_recfun_cut";
48.20
48.21 (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
49.1 --- a/src/HOL/equalities.ML Fri Oct 17 15:23:14 1997 +0200
49.2 +++ b/src/HOL/equalities.ML Fri Oct 17 15:25:12 1997 +0200
49.3 @@ -239,13 +239,13 @@
49.4
49.5 goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
49.6 \ else B Int C)";
49.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
49.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
49.9 by (Blast_tac 1);
49.10 qed "Int_insert_left";
49.11
49.12 goal Set.thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
49.13 \ else A Int B)";
49.14 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
49.15 +by (simp_tac (!simpset addsplits [expand_if]) 1);
49.16 by (Blast_tac 1);
49.17 qed "Int_insert_right";
49.18
49.19 @@ -568,7 +568,7 @@
49.20 qed "Diff_insert2";
49.21
49.22 goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
49.23 -by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
49.24 +by (simp_tac (!simpset addsplits [expand_if]) 1);
49.25 by (Blast_tac 1);
49.26 qed "insert_Diff_if";
49.27
50.1 --- a/src/HOL/ex/Fib.ML Fri Oct 17 15:23:14 1997 +0200
50.2 +++ b/src/HOL/ex/Fib.ML Fri Oct 17 15:25:12 1997 +0200
50.3 @@ -53,7 +53,7 @@
50.4 by (ALLGOALS (*using fib.rules here results in a longer proof!*)
50.5 (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2,
50.6 mod_less, mod_Suc]
50.7 - setloop split_tac[expand_if])));
50.8 + addsplits [expand_if])));
50.9 by (safe_tac (!claset addSDs [mod2_neq_0]));
50.10 by (ALLGOALS
50.11 (asm_full_simp_tac
51.1 --- a/src/HOL/ex/InSort.ML Fri Oct 17 15:23:14 1997 +0200
51.2 +++ b/src/HOL/ex/InSort.ML Fri Oct 17 15:25:12 1997 +0200
51.3 @@ -9,7 +9,7 @@
51.4 goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
51.5 by (list.induct_tac "xs" 1);
51.6 by (Asm_simp_tac 1);
51.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
51.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
51.9 qed "mset_ins";
51.10 Addsimps [mset_ins];
51.11
51.12 @@ -20,7 +20,7 @@
51.13
51.14 goal thy "set(ins f x xs) = insert x (set xs)";
51.15 by (asm_simp_tac (!simpset addsimps [set_via_mset]
51.16 - setloop (split_tac [expand_if])) 1);
51.17 + addsplits [expand_if]) 1);
51.18 by (Fast_tac 1);
51.19 qed "set_ins";
51.20 Addsimps [set_ins];
51.21 @@ -28,7 +28,7 @@
51.22 val prems = goalw InSort.thy [total_def,transf_def]
51.23 "[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs";
51.24 by (list.induct_tac "xs" 1);
51.25 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
51.26 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
51.27 by (cut_facts_tac prems 1);
51.28 by (Fast_tac 1);
51.29 qed "sorted_ins";
52.1 --- a/src/HOL/ex/Primes.ML Fri Oct 17 15:23:14 1997 +0200
52.2 +++ b/src/HOL/ex/Primes.ML Fri Oct 17 15:25:12 1997 +0200
52.3 @@ -36,7 +36,7 @@
52.4
52.5 goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
52.6 by (rtac (gcd_eq RS trans) 1);
52.7 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
52.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
52.9 qed "gcd_less_0";
52.10 Addsimps [gcd_0, gcd_less_0];
52.11
53.1 --- a/src/HOL/ex/Qsort.ML Fri Oct 17 15:23:14 1997 +0200
53.2 +++ b/src/HOL/ex/Qsort.ML Fri Oct 17 15:25:12 1997 +0200
53.3 @@ -26,7 +26,7 @@
53.4
53.5 goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
53.6 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
53.7 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
53.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
53.9 qed "qsort_permutes";
53.10
53.11 goal Qsort.thy "set(qsort le xs) = set xs";
53.12 @@ -37,7 +37,7 @@
53.13 goal List.thy
53.14 "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
53.15 by (list.induct_tac "xs" 1);
53.16 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
53.17 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
53.18 qed"Ball_set_filter";
53.19 Addsimps [Ball_set_filter];
53.20
54.1 --- a/src/HOL/ex/Recdef.ML Fri Oct 17 15:23:14 1997 +0200
54.2 +++ b/src/HOL/ex/Recdef.ML Fri Oct 17 15:25:12 1997 +0200
54.3 @@ -13,7 +13,7 @@
54.4
54.5 goal thy "(x mem qsort (ord,l)) = (x mem l)";
54.6 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
54.7 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
54.8 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
54.9 by (Blast_tac 1);
54.10 qed "qsort_mem_stable";
54.11
55.1 --- a/src/HOL/ex/Sorting.ML Fri Oct 17 15:23:14 1997 +0200
55.2 +++ b/src/HOL/ex/Sorting.ML Fri Oct 17 15:25:12 1997 +0200
55.3 @@ -8,20 +8,20 @@
55.4
55.5 goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
55.6 by (list.induct_tac "xs" 1);
55.7 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
55.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
55.9 qed "mset_append";
55.10
55.11 goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
55.12 \ mset xs x";
55.13 by (list.induct_tac "xs" 1);
55.14 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
55.15 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
55.16 qed "mset_compl_add";
55.17
55.18 Addsimps [mset_append, mset_compl_add];
55.19
55.20 goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
55.21 by (list.induct_tac "xs" 1);
55.22 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
55.23 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
55.24 by (Fast_tac 1);
55.25 qed "set_via_mset";
55.26
55.27 @@ -30,7 +30,7 @@
55.28 val prems = goalw Sorting.thy [transf_def]
55.29 "transf(le) ==> sorted1 le xs = sorted le xs";
55.30 by (list.induct_tac "xs" 1);
55.31 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_list_case]))));
55.32 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_list_case])));
55.33 by (cut_facts_tac prems 1);
55.34 by (Fast_tac 1);
55.35 qed "sorted1_is_sorted";
56.1 --- a/src/HOL/ex/set.ML Fri Oct 17 15:23:14 1997 +0200
56.2 +++ b/src/HOL/ex/set.ML Fri Oct 17 15:25:12 1997 +0200
56.3 @@ -77,7 +77,7 @@
56.4
56.5 goalw Lfp.thy [image_def]
56.6 "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
56.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
56.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
56.9 by (Blast_tac 1);
56.10 qed "range_if_then_else";
56.11
57.1 --- a/src/HOL/simpdata.ML Fri Oct 17 15:23:14 1997 +0200
57.2 +++ b/src/HOL/simpdata.ML Fri Oct 17 15:25:12 1997 +0200
57.3 @@ -328,6 +328,9 @@
57.4 fun split_inside_tac splits = mktac (map mk_meta_eq splits)
57.5 end;
57.6
57.7 +infix 4 addsplits;
57.8 +fun ss addsplits splits = ss addloop (split_tac splits);
57.9 +
57.10
57.11 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
57.12 (fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]);