--- a/src/ZF/AC/AC16_WO4.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/AC/AC16_WO4.ML Thu Jul 02 17:58:12 1998 +0200
@@ -91,7 +91,7 @@
by (ALLGOALS
(asm_simp_tac
(simpset() addsimps [inj_is_fun RS apply_type, left_inverse]
- setloop (split_tac [expand_if] ORELSE' Step_tac))));
+ setloop (split_tac [split_if] ORELSE' Step_tac))));
qed "succ_not_lepoll_lemma";
Goalw [lepoll_def, eqpoll_def, bij_def, surj_def]
--- a/src/ZF/AC/AC18_AC19.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/AC/AC18_AC19.ML Thu Jul 02 17:58:12 1998 +0200
@@ -85,7 +85,7 @@
by (res_inst_tac
[("x","lam a:A. if(f`(u_(a)) : a, f`(u_(a)), f`(u_(a))-{0})")] exI 1);
by (rtac lam_type 1);
-by (split_tac [expand_if] 1);
+by (split_tac [split_if] 1);
by (rtac conjI 1);
by (Fast_tac 1);
by (fast_tac (claset() addSEs [lemma1_2]) 1);
--- a/src/ZF/AC/Cardinal_aux.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML Thu Jul 02 17:58:12 1998 +0200
@@ -66,14 +66,14 @@
qed "Un_eqpoll_Inf_Ord";
val ss = (simpset()) addsimps [inj_is_fun RS apply_type, left_inverse]
- setloop (split_tac [expand_if] ORELSE' etac UnE);
+ setloop (split_tac [split_if] ORELSE' etac UnE);
goal ZF.thy "{x, y} - {y} = {x} - {y}";
by (Fast_tac 1);
qed "double_Diff_sing";
goal ZF.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
-by (split_tac [expand_if] 1);
+by (split_tac [split_if] 1);
by (asm_full_simp_tac (simpset() addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
by (fast_tac (claset() addSIs [the_equality] addEs [equalityE]) 1);
qed "paired_bij_lemma";
@@ -190,7 +190,7 @@
by (res_inst_tac [("d","%z. case(%x. x, %x. x, z)")] lam_bijective 1);
by (fast_tac (claset() addSIs [if_type, InlI, InrI]) 1);
by (TRYALL (etac sumE ));
-by (TRYALL (split_tac [expand_if]));
+by (TRYALL (split_tac [split_if]));
by (TRYALL Asm_simp_tac);
by (fast_tac (claset() addDs [equals0D]) 1);
qed "disj_Un_eqpoll_sum";
--- a/src/ZF/AC/HH.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/AC/HH.ML Thu Jul 02 17:58:12 1998 +0200
@@ -24,7 +24,7 @@
Goal "HH(f,x,a) : Pow(x)-{0} | HH(f,x,a)={x}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (Fast_tac 1);
qed "HH_values";
@@ -76,8 +76,8 @@
by (dresolve_tac [HH_def_satisfies_eq RS subst] 1);
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1);
-by (dresolve_tac [expand_if RS iffD1] 1);
-by (simp_tac (simpset() setloop split_tac [expand_if] ) 1);
+by (dresolve_tac [split_if RS iffD1] 1);
+by (simp_tac (simpset() addsplits [split_if] ) 1);
by (fast_tac (subset_cs addSEs [mem_irrefl]) 1);
qed "HH_subset_x_imp_subset_Diff_UN";
@@ -177,7 +177,7 @@
Goal "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
qed "HH_values2";
Goal
--- a/src/ZF/AC/WO2_AC16.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/AC/WO2_AC16.ML Thu Jul 02 17:58:12 1998 +0200
@@ -206,7 +206,7 @@
by (asm_simp_tac (simpset() addsimps [recfunAC16_Limit,
Diff_cancel, empty_subsetI RS subset_imp_lepoll]) 2);
by (asm_simp_tac (simpset() addsimps [recfunAC16_succ]) 1);
-by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
+by (resolve_tac [conjI RS (split_if RS iffD2)] 1);
by (fast_tac (claset() addSIs [empty_subsetI RS subset_imp_lepoll]
addSEs [Diff_UN_succ_empty RS ssubst]) 1);
by (fast_tac (claset() addSEs [Diff_UN_succ_subset RS subset_imp_lepoll RS
@@ -259,7 +259,7 @@
by (etac Ord_cases 1);
by (asm_simp_tac (simpset() addsimps [recfunAC16_0, lepoll_refl]) 1);
by (asm_simp_tac (simpset() addsimps [recfunAC16_succ]) 1);
-by (fast_tac (claset() addIs [conjI RS (expand_if RS iffD2)]
+by (fast_tac (claset() addIs [conjI RS (split_if RS iffD2)]
addSDs [succI1 RSN (2, bspec)]
addSEs [subset_succI RS subset_imp_lepoll RSN (2, lepoll_trans),
Un_lepoll_succ]) 1);
@@ -509,7 +509,7 @@
by (hyp_subst_tac 1);
by (eresolve_tac [lemma6 RS conjE] 1 THEN (assume_tac 1));
by (asm_simp_tac (simpset() addsimps [recfunAC16_succ]) 1);
-by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
+by (resolve_tac [conjI RS (split_if RS iffD2)] 1);
by (etac lemma7 1 THEN (REPEAT (assume_tac 1)));
by (rtac impI 1);
by (resolve_tac [ex_next_Ord RS oexE] 1
--- a/src/ZF/AC/WO6_WO1.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Thu Jul 02 17:58:12 1998 +0200
@@ -84,7 +84,7 @@
Goalw [vv1_def] "vv1(f,m,b) <= f`b";
by (rtac (LetI RS LetI) 1);
-by (split_tac [expand_if] 1);
+by (split_tac [split_if] 1);
by (simp_tac (simpset() addsimps [domain_uu_subset]) 1);
qed "vv1_subset";
@@ -133,7 +133,7 @@
by (safe_tac (claset() addSEs [lt_oadd_odiff_cases]));
(*Case b<a : show vv1(f,m,b) lepoll m *)
by (asm_simp_tac (simpset() addsimps [vv1_def, Let_def]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (fast_tac (claset() addIs [nested_Least_instance RS conjunct2]
addSEs [lt_Ord]
addSIs [empty_lepollI]) 1);
@@ -231,7 +231,7 @@
\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
\ (UN b<a. f`b)=y; b<a; g<a; m:nat; s:f`b \
\ |] ==> vv2(f,b,g,s) <= f`g";
-by (split_tac [expand_if] 1);
+by (split_tac [split_if] 1);
by Safe_tac;
by (etac (uu_Least_is_fun RS apply_type) 1);
by (REPEAT_SOME (fast_tac (claset() addSIs [not_emptyI, singleton_subsetI])));
@@ -265,7 +265,7 @@
Goalw [vv2_def]
"!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
by (asm_simp_tac (simpset() addsimps [empty_lepollI]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (fast_tac (claset()
addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0]
addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
@@ -281,7 +281,7 @@
by (dtac ospec 1 THEN (assume_tac 1));
by (rtac Diff_lepoll 1
THEN (TRYALL assume_tac));
-by (asm_simp_tac (simpset() addsimps [vv2_def, expand_if, not_emptyI]) 1);
+by (asm_simp_tac (simpset() addsimps [vv2_def, split_if, not_emptyI]) 1);
qed "ww2_lepoll";
Goalw [gg2_def]
--- a/src/ZF/AC/recfunAC16.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/AC/recfunAC16.ML Thu Jul 02 17:58:12 1998 +0200
@@ -60,6 +60,6 @@
Goalw [recfunAC16_def]
"!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)";
by (rtac transrec2_mono 1);
-by (REPEAT (fast_tac (claset() addIs [expand_if RS iffD2]) 1));
+by (REPEAT (fast_tac (claset() addIs [split_if RS iffD2]) 1));
qed "recfunAC16_mono";
--- a/src/ZF/Arith.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Arith.ML Thu Jul 02 17:58:12 1998 +0200
@@ -427,7 +427,7 @@
by (subgoal_tac "k mod 2: 2" 1);
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
by (dtac ltD 1);
-by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [split_if]) 1);
by (Blast_tac 1);
qed "mod2_cases";
--- a/src/ZF/Cardinal.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Cardinal.ML Thu Jul 02 17:58:12 1998 +0200
@@ -162,7 +162,7 @@
by (best_tac (claset() addSIs [if_type RS lam_type]
addEs [apply_funtype RS succE]) 1);
(*Proving it's injective*)
-by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [split_if]) 1);
by (blast_tac (claset() delrules [equalityI]) 1);
qed "inj_not_surj_succ";
@@ -441,7 +441,7 @@
by (blast_tac (claset() addEs [apply_funtype RS consE]) 1);
by (blast_tac (claset() addSEs [mem_irrefl] addEs [apply_funtype RS consE]) 1);
(*Proving it's injective*)
-by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [split_if]) 1);
by (Blast_tac 1);
qed "cons_lepoll_consD";
@@ -631,12 +631,12 @@
by (blast_tac (claset() addSIs [if_type, inj_is_fun RS apply_type]) 1);
by (asm_simp_tac
(simpset() addsimps [inj_converse_fun RS apply_funtype]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI, left_inverse]
setloop etac UnE') 1);
by (asm_simp_tac
(simpset() addsimps [inj_converse_fun RS apply_funtype, right_inverse]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (blast_tac (claset() addEs [equals0D]) 1);
qed "inj_disjoint_eqpoll";
@@ -677,10 +677,10 @@
Goalw [lepoll_def] "A Un B lepoll A+B";
by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1);
by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1);
-by (split_tac [expand_if] 1);
+by (split_tac [split_if] 1);
by (blast_tac (claset() addSIs [InlI, InrI]) 1);
by (asm_full_simp_tac (simpset() addsimps [Inl_def, Inr_def]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
qed "Un_lepoll_sum";
--- a/src/ZF/CardinalArith.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/CardinalArith.ML Thu Jul 02 17:58:12 1998 +0200
@@ -326,7 +326,7 @@
inj_converse_fun RS apply_funtype,
left_inverse, right_inverse, nat_0I, nat_succI,
nat_case_0, nat_case_succ]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
qed "nat_cons_lepoll";
Goal "!!i. nat lepoll A ==> cons(u,A) eqpoll A";
--- a/src/ZF/Cardinal_AC.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Cardinal_AC.ML Thu Jul 02 17:58:12 1998 +0200
@@ -193,6 +193,6 @@
by (REPEAT (assume_tac 1));
by (blast_tac (claset() addSIs [Ord_UN] addEs [ltE]) 2);
by (asm_simp_tac (simpset() addsimps [inj_converse_fun RS apply_type]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
qed "le_UN_Ord_lt_csucc";
--- a/src/ZF/Coind/Map.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Coind/Map.ML Thu Jul 02 17:58:12 1998 +0200
@@ -114,7 +114,7 @@
by (etac image_Sigma1 1);
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
by (asm_full_simp_tac
- (simpset() addsimps [qbeta] setloop split_tac [expand_if]) 1);
+ (simpset() addsimps [qbeta] addsplits [split_if]) 1);
by Safe_tac;
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
by (ALLGOALS Asm_full_simp_tac);
--- a/src/ZF/Epsilon.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Epsilon.ML Thu Jul 02 17:58:12 1998 +0200
@@ -305,13 +305,13 @@
Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
by (rtac (transrec2_def RS def_transrec RS trans) 1);
by (simp_tac (simpset() addsimps [succ_not_0, THE_eq, if_P]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (Blast_tac 1);
qed "transrec2_succ";
Goal "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
by (rtac (transrec2_def RS def_transrec RS trans) 1);
-by (simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (simp_tac (simpset() addsplits [split_if]) 1);
by (blast_tac (claset() addSDs [Limit_has_0] addSEs [succ_LimitE]) 1);
qed "transrec2_Limit";
--- a/src/ZF/OrderArith.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/OrderArith.ML Thu Jul 02 17:58:12 1998 +0200
@@ -142,7 +142,7 @@
by (blast_tac (claset() addSIs [if_type]) 2);
by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
by Safe_tac;
-by (ALLGOALS (asm_simp_tac (simpset() setloop split_tac [expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [split_if])));
by (blast_tac (claset() addEs [equalityE]) 1);
qed "sum_disjoint_bij";
--- a/src/ZF/OrderType.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/OrderType.ML Thu Jul 02 17:58:12 1998 +0200
@@ -596,7 +596,7 @@
by (blast_tac (claset() addSIs [if_type]) 1);
by (fast_tac (claset() addSIs [case_type]) 1);
by (etac sumE 2);
-by (ALLGOALS (asm_simp_tac (simpset() setloop split_tac [expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [split_if])));
qed "bij_sum_Diff";
Goal
@@ -608,7 +608,7 @@
by (etac well_ord_Memrel 3);
by (assume_tac 1);
by (asm_simp_tac
- (simpset() setloop split_tac [expand_if] addsimps [Memrel_iff]) 1);
+ (simpset() addsplits [split_if] addsimps [Memrel_iff]) 1);
by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
by (asm_simp_tac (simpset() addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
--- a/src/ZF/Perm.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Perm.ML Thu Jul 02 17:58:12 1998 +0200
@@ -461,7 +461,7 @@
lam_injective 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse]
- setloop (split_tac [expand_if] ORELSE' etac UnE))));
+ setloop (split_tac [split_if] ORELSE' etac UnE))));
by (blast_tac (claset() addIs [inj_is_fun RS apply_type] addDs [equals0D]) 1);
qed "inj_disjoint_Un";
--- a/src/ZF/Resid/Substitution.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Resid/Substitution.ML Thu Jul 02 17:58:12 1998 +0200
@@ -108,7 +108,7 @@
by (asm_full_simp_tac (simpset()) 1);
qed "subst_App";
-fun addsplit ss = (ss setloop (split_inside_tac [expand_if])
+fun addsplit ss = (ss setloop (split_inside_tac [split_if])
addsimps [lift_rec_Var,subst_Var]);
--- a/src/ZF/Zorn.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/Zorn.ML Thu Jul 02 17:58:12 1998 +0200
@@ -199,13 +199,13 @@
by (rewtac increasing_def);
by (rtac CollectI 1);
by (rtac lam_type 1);
-by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [split_if]) 1);
by (fast_tac (claset() addSIs [super_subset_chain RS subsetD,
chain_subset_Pow RS subsetD,
choice_super]) 1);
(*Now, verify that it increases*)
by (asm_simp_tac (simpset() addsimps [Pow_iff, subset_refl]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by Safe_tac;
by (dtac choice_super 1);
by (REPEAT (assume_tac 1));
@@ -225,7 +225,7 @@
by (asm_simp_tac
(simpset() addsimps [chain_subset_Pow RS subsetD,
choice_super RS (super_subset_chain RS subsetD)]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (rewtac chain_def);
by (rtac CollectI 1 THEN Blast_tac 1);
by Safe_tac;
@@ -250,7 +250,7 @@
by (asm_full_simp_tac
(simpset() addsimps [subset_refl RS TFin_UnionI RS
(TFin.dom_subset RS subsetD)]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (eresolve_tac [choice_not_equals RS notE] 1);
by (REPEAT (assume_tac 1));
qed "Hausdorff";
@@ -359,10 +359,10 @@
by (rtac allI 2);
by (rtac impI 2);
by (asm_simp_tac (simpset() addsimps [Pow_iff, subset_consI, subset_refl]
- setloop split_tac [expand_if]) 2);
+ addsplits [split_if]) 2);
(*Type checking is surprisingly hard!*)
by (asm_simp_tac (simpset() addsimps [Pow_iff, cons_subset_iff, subset_refl]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (blast_tac (claset() addSIs [choice_Diff RS DiffD1]) 1);
qed "Zermelo_next_exists";
@@ -392,14 +392,14 @@
addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
Pow_iff, cons_subset_iff, subset_refl,
choice_Diff RS DiffD2]
- setloop split_tac [expand_if]) 2);
+ addsplits [split_if]) 2);
by (subgoal_tac "x : next ` Union({y: TFin(S,next). x~: y})" 1);
by (blast_tac (subset_cs addSIs [Collect_subset RS TFin_UnionI, TFin_nextI]) 2);
(*End of the lemmas!*)
by (asm_full_simp_tac
(simpset() addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
Pow_iff, cons_subset_iff, subset_refl]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
by (REPEAT (eresolve_tac [asm_rl, consE, sym, notE] 1));
qed "choice_imp_injection";
--- a/src/ZF/equalities.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/equalities.ML Thu Jul 02 17:58:12 1998 +0200
@@ -601,7 +601,7 @@
qed "Collect_Diff";
goal ZF.thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
-by (simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (simp_tac (simpset() addsplits [split_if]) 1);
by (Blast_tac 1);
qed "Collect_cons";
--- a/src/ZF/ex/Limit.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/ex/Limit.ML Thu Jul 02 17:58:12 1998 +0200
@@ -2028,7 +2028,7 @@
val prems = goalw Limit.thy [eps_def] (* eps_fun *)
"[|emb_chain(DD,ee); m:nat; n:nat|] ==> \
\ eps(DD,ee,m,n): set(DD`m)->set(DD`n)";
-by (rtac (expand_if RS iffD2) 1);
+by (rtac (split_if RS iffD2) 1);
by Safe_tac;
brr((e_less_cont RS cont_fun)::prems) 1;
brr((not_le_iff_lt RS iffD1 RS leI)::e_gr_fun::nat_into_Ord::prems) 1;
@@ -2050,7 +2050,7 @@
val prems = goalw Limit.thy [eps_def] (* eps_e_gr_add *)
"[|n:nat; k:nat|] ==> eps(DD,ee,n#+k,n) = e_gr(DD,ee,n#+k,n)";
-by (rtac (expand_if RS iffD2) 1);
+by (rtac (split_if RS iffD2) 1);
by Safe_tac;
by (etac leE 1);
(* Must control rewriting by instantiating a variable. *)
@@ -2363,7 +2363,7 @@
val prems = goalw Limit.thy [eps_def] (* eps1 *)
"[|emb_chain(DD,ee); x:set(Dinf(DD,ee)); m:nat; n:nat|] ==> \
\ rel(DD`n,eps(DD,ee,m,n)`(x`m),x`n)";
-by (split_tac [expand_if] 1);
+by (split_tac [split_if] 1);
brr(conjI::impI::lemma1::
(not_le_iff_lt RS iffD1 RS leI RS lemma2)::nat_into_Ord::prems) 1;
qed "eps1";
--- a/src/ZF/ex/Mutil.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/ex/Mutil.ML Thu Jul 02 17:58:12 1998 +0200
@@ -34,7 +34,7 @@
"evnodd(cons(<i,j>,C), b) = \
\ if((i#+j) mod 2 = b, cons(<i,j>, evnodd(C,b)), evnodd(C,b))";
by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]
- setloop split_tac [expand_if]) 1);
+ addsplits [split_if]) 1);
qed "evnodd_cons";
Goalw [evnodd_def] "evnodd(0, b) = 0";
@@ -56,7 +56,7 @@
by (REPEAT_FIRST (ares_tac [add_type]));
(*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
by (REPEAT (asm_simp_tac (simpset() addsimps [mod_succ, succ_neq_self]
- setloop split_tac [expand_if]) 1
+ addsplits [split_if]) 1
THEN blast_tac (claset() addDs [ltD]) 1));
qed "domino_singleton";
--- a/src/ZF/ex/PropLog.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/ex/PropLog.ML Thu Jul 02 17:58:12 1998 +0200
@@ -46,12 +46,12 @@
Goalw [is_true_def] "is_true(#v,t) <-> v:t";
by (simp_tac (simpset() addsimps [one_not_0 RS not_sym]
- setloop (split_tac [expand_if])) 1);
+ setloop (split_tac [split_if])) 1);
qed "is_true_Var";
Goalw [is_true_def]
"is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
-by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (simp_tac (simpset() setloop (split_tac [split_if])) 1);
qed "is_true_Imp";
(** The function hyps **)
@@ -171,7 +171,7 @@
(*Typical example of strengthening the induction formula*)
val [major] = goal PropLog.thy
"p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
-by (rtac (expand_if RS iffD2) 1);
+by (rtac (split_if RS iffD2) 1);
by (rtac (major RS prop.induct) 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1,
@@ -216,7 +216,7 @@
"p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
by (rtac (major RS prop.induct) 1);
by (Simp_tac 1);
-by (asm_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
by (fast_tac (claset() addSEs prop.free_SEs) 1);
by (Asm_simp_tac 1);
by (Fast_tac 1);
@@ -228,7 +228,7 @@
"p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
by (rtac (major RS prop.induct) 1);
by (Simp_tac 1);
-by (asm_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
by (fast_tac (claset() addSEs prop.free_SEs) 1);
by (Asm_simp_tac 1);
by (Fast_tac 1);
@@ -250,7 +250,7 @@
"p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
by (rtac (major RS prop.induct) 1);
by (asm_simp_tac (simpset() addsimps [UN_I]
- setloop (split_tac [expand_if])) 2);
+ setloop (split_tac [split_if])) 2);
by (ALLGOALS Asm_simp_tac);
by (fast_tac (claset() addIs Fin.intrs) 1);
qed "hyps_finite";
--- a/src/ZF/upair.ML Thu Jul 02 17:56:06 1998 +0200
+++ b/src/ZF/upair.ML Thu Jul 02 17:58:12 1998 +0200
@@ -255,33 +255,33 @@
Addsimps [if_true, if_false];
-qed_goal "expand_if" ZF.thy
+qed_goal "split_if" ZF.thy
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
(fn _=> [ (excluded_middle_tac "Q" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1) ]);
(** Rewrite rules for boolean case-splitting: faster than
- setloop split_tac[expand_if]
+ addsplits[split_if]
**)
-bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
-bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if);
+bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
+bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
-bind_thm ("expand_if_mem1", read_instantiate [("P", "%x. x : ?b")] expand_if);
-bind_thm ("expand_if_mem2", read_instantiate [("P", "%x. ?a : x")] expand_if);
+bind_thm ("split_if_mem1", read_instantiate [("P", "%x. x : ?b")] split_if);
+bind_thm ("split_if_mem2", read_instantiate [("P", "%x. ?a : x")] split_if);
-val expand_ifs = [expand_if_eq1, expand_if_eq2,
- expand_if_mem1, expand_if_mem2];
+val split_ifs = [split_if_eq1, split_if_eq2,
+ split_if_mem1, split_if_mem2];
-(*Logically equivalent to expand_if_mem2*)
+(*Logically equivalent to split_if_mem2*)
qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
- (fn _=> [ (simp_tac (simpset() setloop split_tac [expand_if]) 1) ]);
+ (fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]);
qed_goal "if_type" ZF.thy
"[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A"
(fn prems=> [ (simp_tac
- (simpset() addsimps prems setloop split_tac [expand_if]) 1) ]);
+ (simpset() addsimps prems addsplits [split_if]) 1) ]);
(*** Foundation lemmas ***)