# HG changeset patch # User nipkow # Date 877094712 -7200 # Node ID c036caebfc7540899f33f0e958c6a4cd024b5095 # Parent 94e0fdcb7b91c691dd543b4a0550402d47b3fdee setloop split_tac -> addsplits diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Arith.ML --- 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. P(Suc(n))--> P(n)) --> P(k-i)"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/Event.ML --- 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())); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/Message.ML --- 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 diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/NS_Public.ML --- 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*) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/NS_Public_Bad.ML --- 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*) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/NS_Shared.ML --- 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*) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/OtwayRees.ML --- 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*) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/OtwayRees_AN.ML --- 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*) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/OtwayRees_Bad.ML --- 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*) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/Public.ML --- 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]; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/Recur.ML --- 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*) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/Shared.ML --- 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 diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/TLS.ML --- 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 ***) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/Yahalom.ML --- 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] diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Auth/Yahalom2.ML --- 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*) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Divides.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Finite.ML --- 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)"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/IMP/Hoare.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/IOA/IOA.ML --- 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) & \ diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/IOA/Solve.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Induct/Com.ML --- 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]; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Induct/LFilter.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Induct/LList.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Induct/Mutil.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Induct/Perm.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Induct/PropLog.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Induct/SList.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Integ/Bin.ML --- 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 ****) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Lambda/Eta.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Lambda/Lambda.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Lex/AutoChopper.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/List.ML --- 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 **) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/MiniML/Generalize.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/MiniML/Instance.ML --- 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; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/MiniML/Maybe.ML --- 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]; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/MiniML/MiniML.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/MiniML/Type.ML --- 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(); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/MiniML/W.ML --- 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 diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Prod.ML --- 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 *) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Set.ML --- 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; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Subst/Subst.ML --- 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]; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Subst/Unifier.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Subst/Unify.ML --- 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)); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/W0/I.ML --- 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); diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/W0/Maybe.ML --- 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]; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/W0/Type.ML --- 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]; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/W0/W.ML --- 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] diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/WF.ML --- 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 ***) diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/equalities.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/ex/Fib.ML --- 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 diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/ex/InSort.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/ex/Primes.ML --- 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 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]; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/ex/Qsort.ML --- 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]; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/ex/Recdef.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/ex/Sorting.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/ex/set.ML --- 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"; diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/simpdata.ML --- 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]);