# HG changeset patch # User paulson # Date 899395092 -7200 # Node ID 8eb343ab57489c7c3f3f5c37fdef4c7fee09d637 # Parent caf39b7b7a126e30e08f5ee83456898ebe66ee25 Renamed expand_if to split_if and setloop split_tac to addsplits, as in HOL diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/AC/AC16_WO4.ML --- 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] diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/AC/AC18_AC19.ML --- 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); diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/AC/Cardinal_aux.ML --- 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/AC/HH.ML --- 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 diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/AC/WO2_AC16.ML --- 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 diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/AC/WO6_WO1.ML --- 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 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] diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/AC/recfunAC16.ML --- 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/Arith.ML --- 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/Cardinal.ML --- 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/CardinalArith.ML --- 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/Cardinal_AC.ML --- 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/Coind/Map.ML --- 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); diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/Epsilon.ML --- 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 \ \ 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/ex/Mutil.ML --- 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(,C), b) = \ \ if((i#+j) mod 2 = b, cons(, 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/ex/PropLog.ML --- 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"; diff -r caf39b7b7a12 -r 8eb343ab5748 src/ZF/upair.ML --- 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 ***)