# HG changeset patch # User paulson # Date 827836956 -3600 # Node ID 5324067d993fcddaf9440d640ca8c0637b7cbe30 # Parent e15e8c0c1e37357576e689f2708a3bfb5a3a7689 New lemmas for Mutilated Checkerboard diff -r e15e8c0c1e37 -r 5324067d993f src/ZF/Arith.ML --- a/src/ZF/Arith.ML Tue Mar 26 11:38:17 1996 +0100 +++ b/src/ZF/Arith.ML Tue Mar 26 11:42:36 1996 +0100 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -For arith.thy. Arithmetic operators and their definitions +Arithmetic operators and their definitions Proofs about elementary arithmetic: addition, multiplication, etc. @@ -42,8 +42,6 @@ (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ])))); qed "rec_type"; -val nat_le_refl = nat_into_Ord RS le_refl; - val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]; val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff, @@ -170,7 +168,6 @@ by (rtac (eqn RS rev_mp) 1); by (nat_ind_tac "k" [knat] 1); by (ALLGOALS (simp_tac arith_ss)); -by (fast_tac ZF_cs 1); qed "add_left_cancel"; (*** Multiplication ***) @@ -247,6 +244,15 @@ by (ALLGOALS (asm_simp_tac arith_ss)); qed "add_diff_inverse"; +(*Proof is IDENTICAL to that above*) +goal Arith.thy "!!m n. [| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)"; +by (forward_tac [lt_nat_in_nat] 1); +by (etac nat_succI 1); +by (etac rev_mp 1); +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); +by (ALLGOALS (asm_simp_tac arith_ss)); +qed "diff_succ"; + (*Subtraction is the inverse of addition. *) val [mnat,nnat] = goal Arith.thy "[| m:nat; n:nat |] ==> (n#+m) #- n = m"; @@ -266,7 +272,6 @@ by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); qed "diff_add_0"; - (*** Remainder ***) goal Arith.thy "!!m n. [| 0 m #- n < m"; @@ -321,7 +326,7 @@ by (asm_simp_tac div_ss 1); qed "div_geq"; -(*Main Result.*) +(*A key result*) goal Arith.thy "!!m n. [| 0 (m div n)#*n #+ m mod n = m"; by (etac complete_induct 1); @@ -335,6 +340,59 @@ div_termination RS ltD, add_diff_inverse]) 1); qed "mod_div_equality"; +(*** Further facts about mod (mainly for mutilated checkerboard ***) + +goal Arith.thy + "!!m n. [| 0 \ +\ succ(m) mod n = if(succ(m mod n) = n, 0, succ(m mod n))"; +by (etac complete_induct 1); +by (excluded_middle_tac "succ(x) m mod n < n"; +by (etac complete_induct 1); +by (excluded_middle_tac "x k mod 2 = b | k mod 2 = if(b=1,0,1)"; +by (subgoal_tac "k mod 2: 2" 1); +by (asm_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD]) 2); +by (dresolve_tac [ltD] 1); +by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); +by (fast_tac ZF_cs 1); +qed "mod2_cases"; + +goal Arith.thy "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2"; +by (subgoal_tac "m mod 2: 2" 1); +by (asm_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD]) 2); +by (asm_simp_tac (arith_ss addsimps [mod_succ] setloop step_tac ZF_cs) 1); +qed "mod2_succ_succ"; + +goal Arith.thy "!!m. m:nat ==> (m#+m) mod 2 = 0"; +by (eresolve_tac [nat_induct] 1); +by (simp_tac (arith_ss addsimps [mod_less]) 1); +by (asm_simp_tac (arith_ss addsimps [mod2_succ_succ, add_succ_right]) 1); +qed "mod2_add_self"; + (**** Additional theorems about "le" ****) @@ -395,3 +453,8 @@ rtac add_le_mono1 5]); by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); qed "add_le_mono"; + +val arith_ss0 = arith_ss +and arith_ss = arith_ss addsimps [add_0_right, add_succ_right, + mult_0_right, mult_succ_right, + mod_less, mod_geq, div_less, div_geq]; diff -r e15e8c0c1e37 -r 5324067d993f src/ZF/Cardinal.ML --- a/src/ZF/Cardinal.ML Tue Mar 26 11:38:17 1996 +0100 +++ b/src/ZF/Cardinal.ML Tue Mar 26 11:42:36 1996 +0100 @@ -77,7 +77,9 @@ by (etac id_subset_inj 1); qed "subset_imp_lepoll"; -val lepoll_refl = subset_refl RS subset_imp_lepoll; +bind_thm ("lepoll_refl", subset_refl RS subset_imp_lepoll); + +bind_thm ("le_imp_lepoll", le_imp_subset RS subset_imp_lepoll); goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def] "!!X Y. X eqpoll Y ==> X lepoll Y"; @@ -114,12 +116,39 @@ (*0 lepoll Y*) bind_thm ("empty_lepollI", empty_subsetI RS subset_imp_lepoll); +goal Cardinal.thy "A lepoll 0 <-> A=0"; +by (fast_tac (ZF_cs addIs [lepoll_0_is_0, lepoll_refl]) 1); +qed "lepoll_0_iff"; + (*A eqpoll 0 ==> A=0*) bind_thm ("eqpoll_0_is_0", eqpoll_imp_lepoll RS lepoll_0_is_0); +goal Cardinal.thy "A eqpoll 0 <-> A=0"; +by (fast_tac (ZF_cs addIs [eqpoll_0_is_0, eqpoll_refl]) 1); +qed "eqpoll_0_iff"; + +goalw Cardinal.thy [eqpoll_def] + "!!A. [| A eqpoll B; C eqpoll D; A Int C = 0; B Int D = 0 |] ==> \ +\ A Un C eqpoll B Un D"; +by (fast_tac (ZF_cs addIs [bij_disjoint_Un]) 1); +qed "eqpoll_disjoint_Un"; + (*** lesspoll: contributions by Krzysztof Grabczewski ***) +goalw Cardinal.thy [lesspoll_def] "!!A. A lesspoll B ==> A lepoll B"; +by (fast_tac ZF_cs 1); +qed "lesspoll_imp_lepoll"; + +goalw Cardinal.thy [lepoll_def] + "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)"; +by (fast_tac (ZF_cs addSEs [well_ord_rvimage]) 1); +qed "lepoll_well_ord"; + +goalw Cardinal.thy [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B"; +by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE]) 1); +qed "lepoll_iff_leqpoll"; + goalw Cardinal.thy [inj_def, surj_def] "!!f. [| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)"; by (safe_tac lemmas_cs); @@ -221,8 +250,8 @@ by (simp_tac (FOL_ss addsimps prems) 1); qed "Least_cong"; -(*Need AC to prove X lepoll Y ==> |X| le |Y| ; - see well_ord_lepoll_imp_Card_le *) +(*Need AC to get X lepoll Y ==> |X| le |Y|; see well_ord_lepoll_imp_Card_le + Converse also requires AC, but see well_ord_cardinal_eqE*) goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|"; by (rtac Least_cong 1); by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); @@ -236,6 +265,7 @@ by (etac (ordermap_bij RS bij_converse_bij RS bij_imp_eqpoll) 1); qed "well_ord_cardinal_eqpoll"; +(* Ord(A) ==> |A| eqpoll A *) bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll); goal Cardinal.thy @@ -245,6 +275,11 @@ by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); qed "well_ord_cardinal_eqE"; +goal Cardinal.thy + "!!X Y. [| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y"; +by (fast_tac (ZF_cs addSEs [cardinal_cong, well_ord_cardinal_eqE]) 1); +qed "well_ord_cardinal_eqpoll_iff"; + (** Observations from Kunen, page 28 **) @@ -286,6 +321,11 @@ by (ALLGOALS assume_tac); qed "Card_iff_initial"; +goalw Cardinal.thy [lesspoll_def] "!!a. [| Card(a); i i lesspoll a"; +by (dresolve_tac [Card_iff_initial RS iffD1] 1); +by (fast_tac (ZF_cs addSEs [leI RS le_imp_lepoll]) 1); +qed "lt_Card_imp_lesspoll"; + goal Cardinal.thy "Card(0)"; by (rtac (Ord_0 RS CardI) 1); by (fast_tac (ZF_cs addSEs [ltE]) 1); @@ -316,9 +356,9 @@ (*Kunen's Lemma 10.5*) goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|"; by (rtac (eqpollI RS cardinal_cong) 1); -by (etac (le_imp_subset RS subset_imp_lepoll) 1); +by (etac le_imp_lepoll 1); by (rtac lepoll_trans 1); -by (etac (le_imp_subset RS subset_imp_lepoll) 2); +by (etac le_imp_lepoll 2); by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1); by (rtac Ord_cardinal_eqpoll 1); by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); @@ -357,6 +397,32 @@ not_lt_iff_le RS iff_sym]) 1); qed "Card_le_iff"; +(*Can use AC or finiteness to discharge first premise*) +goal Cardinal.thy + "!!A B. [| well_ord(B,r); A lepoll B |] ==> |A| le |B|"; +by (res_inst_tac [("i","|A|"),("j","|B|")] Ord_linear_le 1); +by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); +by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1); +by (rtac lepoll_trans 1); +by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll) 1); +by (assume_tac 1); +by (etac (le_imp_lepoll RS lepoll_trans) 1); +by (rtac eqpoll_imp_lepoll 1); +by (rewtac lepoll_def); +by (etac exE 1); +by (rtac well_ord_cardinal_eqpoll 1); +by (etac well_ord_rvimage 1); +by (assume_tac 1); +qed "well_ord_lepoll_imp_Card_le"; + + +goal Cardinal.thy "!!A. [| A lepoll i; Ord(i) |] ==> |A| le i"; +br le_trans 1; +be (well_ord_Memrel RS well_ord_lepoll_imp_Card_le) 1; +ba 1; +be Ord_cardinal_le 1; +qed "lepoll_cardinal_le"; + (*** The finite cardinals ***) @@ -395,7 +461,7 @@ by (asm_simp_tac (ZF_ss addsimps [lepoll_def, inj_def, succI1 RS Pi_empty2]) 1); by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1); -val nat_lepoll_imp_le_lemma = result(); +qed "nat_lepoll_imp_le_lemma"; bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp); @@ -407,6 +473,7 @@ addSEs [eqpollE]) 1); qed "nat_eqpoll_iff"; +(*The object of all this work: every natural number is a (finite) cardinal*) goalw Cardinal.thy [Card_def,cardinal_def] "!!n. n: nat ==> Card(n)"; by (rtac (Least_equality RS ssubst) 1); @@ -527,6 +594,11 @@ by (fast_tac (ZF_cs addSIs [eqpoll_refl RS cons_eqpoll_cong]) 1); qed "singleton_eqpoll_1"; +goal Cardinal.thy "|{a}| = 1"; +by (resolve_tac [singleton_eqpoll_1 RS cardinal_cong RS trans] 1); +by (simp_tac (arith_ss addsimps [nat_into_Card RS Card_cardinal_eq]) 1); +qed "cardinal_singleton"; + (*Congruence law for succ under equipollence*) goalw Cardinal.thy [succ_def] "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)"; @@ -597,9 +669,22 @@ by (fast_tac (eq_cs addEs [equalityE]) 1); qed "lepoll_1_is_sing"; +goalw Cardinal.thy [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 (fast_tac (ZF_cs addSIs [InlI, InrI]) 1); +by (asm_full_simp_tac (ZF_ss addsimps [Inl_def, Inr_def] + setloop split_tac [expand_if]) 1); +qed "Un_lepoll_sum"; + (*** Finite and infinite sets ***) +goalw Cardinal.thy [Finite_def] "Finite(0)"; +by (fast_tac (ZF_cs addSIs [eqpoll_refl, nat_0I]) 1); +qed "Finite_0"; + goalw Cardinal.thy [Finite_def] "!!A. [| A lepoll n; n:nat |] ==> Finite(A)"; by (etac rev_mp 1); @@ -615,6 +700,8 @@ rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1); qed "lepoll_Finite"; +bind_thm ("Finite_Diff", Diff_subset RS subset_imp_lepoll RS lepoll_Finite); + goalw Cardinal.thy [Finite_def] "!!x. Finite(x) ==> Finite(cons(y,x))"; by (excluded_middle_tac "y:x" 1); by (asm_simp_tac (ZF_ss addsimps [cons_absorb]) 2); @@ -623,11 +710,11 @@ by (etac nat_succI 2); by (asm_simp_tac (ZF_ss addsimps [succ_def, cons_eqpoll_cong, mem_not_refl]) 1); -qed "Finite_imp_cons_Finite"; +qed "Finite_cons"; goalw Cardinal.thy [succ_def] "!!x. Finite(x) ==> Finite(succ(x))"; -by (etac Finite_imp_cons_Finite 1); -qed "Finite_imp_succ_Finite"; +by (etac Finite_cons 1); +qed "Finite_succ"; goalw Cardinal.thy [Finite_def] "!!i. [| Ord(i); ~ Finite(i) |] ==> nat le i"; @@ -636,6 +723,12 @@ by (fast_tac (ZF_cs addSIs [eqpoll_refl] addSEs [ltE]) 1); qed "nat_le_infinite_Ord"; +goalw Cardinal.thy [Finite_def, eqpoll_def] + "!!A. Finite(A) ==> EX r. well_ord(A,r)"; +by (fast_tac (ZF_cs addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel, + nat_into_Ord]) 1); +qed "Finite_imp_well_ord"; + (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered set is well-ordered. Proofs simplified by lcp. *) diff -r e15e8c0c1e37 -r 5324067d993f src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Tue Mar 26 11:38:17 1996 +0100 +++ b/src/ZF/CardinalArith.ML Tue Mar 26 11:42:36 1996 +0100 @@ -13,36 +13,6 @@ open CardinalArith; -(*** Elementary properties ***) - -(*Use AC to discharge first premise*) -goal CardinalArith.thy - "!!A B. [| well_ord(B,r); A lepoll B |] ==> |A| le |B|"; -by (res_inst_tac [("i","|A|"),("j","|B|")] Ord_linear_le 1); -by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); -by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1); -by (rtac lepoll_trans 1); -by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll) 1); -by (assume_tac 1); -by (etac (le_imp_subset RS subset_imp_lepoll RS lepoll_trans) 1); -by (rtac eqpoll_imp_lepoll 1); -by (rewtac lepoll_def); -by (etac exE 1); -by (rtac well_ord_cardinal_eqpoll 1); -by (etac well_ord_rvimage 1); -by (assume_tac 1); -qed "well_ord_lepoll_imp_Card_le"; - -(*Each element of Fin(A) is equivalent to a natural number*) -goal CardinalArith.thy - "!!X A. X: Fin(A) ==> EX n:nat. X eqpoll n"; -by (etac Fin_induct 1); -by (fast_tac (ZF_cs addIs [eqpoll_refl, nat_0I]) 1); -by (fast_tac (ZF_cs addSIs [cons_eqpoll_cong, - rewrite_rule [succ_def] nat_succI] - addSEs [mem_irrefl]) 1); -qed "Fin_eqpoll"; - (*** Cardinal addition ***) (** Cardinal addition is commutative **) @@ -493,8 +463,7 @@ by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1)); by (subgoals_tac ["z ALL A. A eqpoll n --> A : Fin(A)"; +by (eresolve_tac [nat_induct] 1); +by (simp_tac (ZF_ss addsimps (eqpoll_0_iff::Fin.intrs)) 1); +by (step_tac ZF_cs 1); +by (subgoal_tac "EX u. u:A" 1); +by (eresolve_tac [exE] 1); +by (resolve_tac [Diff_sing_eqpoll RS revcut_rl] 1); +by (assume_tac 2); +by (assume_tac 1); +by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1); +by (assume_tac 1); +by (resolve_tac [Fin.consI] 1); +by (fast_tac ZF_cs 1); +by (deepen_tac (ZF_cs addIs [Fin_mono RS subsetD]) 0 1); (*SLOW*) +(*Now for the lemma assumed above*) +by (rewrite_goals_tac [eqpoll_def]); +by (fast_tac (ZF_cs addSEs [bij_converse_bij RS bij_is_fun RS apply_type]) 1); +val lemma = result(); + +goalw CardinalArith.thy [Finite_def] "!!A. Finite(A) ==> A : Fin(A)"; +by (fast_tac (ZF_cs addIs [lemma RS spec RS mp]) 1); +qed "Finite_into_Fin"; + +goal CardinalArith.thy "!!A. A : Fin(U) ==> Finite(A)"; +by (fast_tac (ZF_cs addSIs [Finite_0, Finite_cons] addEs [Fin.induct]) 1); +qed "Fin_into_Finite"; + +goal CardinalArith.thy "Finite(A) <-> A : Fin(A)"; +by (fast_tac (ZF_cs addIs [Finite_into_Fin] addEs [Fin_into_Finite]) 1); +qed "Finite_Fin_iff"; + +goal CardinalArith.thy + "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)"; +by (fast_tac (ZF_cs addSIs [Fin_into_Finite, Fin_UnI] + addSDs [Finite_into_Fin] + addSEs [Un_upper1 RS Fin_mono RS subsetD, + Un_upper2 RS Fin_mono RS subsetD]) 1); +qed "Finite_Un"; + + +(** Removing elements from a finite set decreases its cardinality **) + +goal CardinalArith.thy + "!!A. A: Fin(U) ==> x~:A --> ~ cons(x,A) lepoll A"; +by (eresolve_tac [Fin_induct] 1); +by (simp_tac (ZF_ss addsimps [lepoll_0_iff]) 1); +by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1); +by (asm_simp_tac ZF_ss 1); +by (fast_tac (ZF_cs addSDs [cons_lepoll_consD]) 1); +by (fast_tac eq_cs 1); +qed "Fin_imp_not_cons_lepoll"; + +goal CardinalArith.thy + "!!a A. [| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)"; +by (rewrite_goals_tac [cardinal_def]); +by (resolve_tac [Least_equality] 1); +by (fold_tac [cardinal_def]); +by (simp_tac (ZF_ss addsimps [succ_def]) 1); +by (fast_tac (ZF_cs addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll] + addSEs [mem_irrefl] + addSDs [Finite_imp_well_ord]) 1); +by (fast_tac (ZF_cs addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1); +by (resolve_tac [notI] 1); +by (resolve_tac [Finite_into_Fin RS Fin_imp_not_cons_lepoll RS mp RS notE] 1); +by (assume_tac 1); +by (assume_tac 1); +by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans] 1); +by (eresolve_tac [le_imp_lepoll RS lepoll_trans] 1); +by (fast_tac (ZF_cs addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll] + addSDs [Finite_imp_well_ord]) 1); +qed "Finite_imp_cardinal_cons"; + + +goal CardinalArith.thy "!!a A. [| Finite(A); a:A |] ==> |A-{a}| < |A|"; +by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1); +by (assume_tac 1); +by (asm_simp_tac (ZF_ss addsimps [Finite_imp_cardinal_cons, + Diff_subset RS subset_imp_lepoll RS + lepoll_Finite]) 1); +by (asm_simp_tac (ZF_ss addsimps [cons_Diff, Ord_cardinal RS le_refl]) 1); +qed "Finite_imp_cardinal_Diff"; + + +(** Thanks to Krzysztof Grabczewski **) + +val nat_implies_well_ord = nat_into_Ord RS well_ord_Memrel; + +goal CardinalArith.thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; +by (rtac eqpoll_trans 1); +by (eresolve_tac [nat_implies_well_ord RS ( + nat_implies_well_ord RSN (2, + well_ord_radd RS well_ord_cardinal_eqpoll)) RS eqpoll_sym] 1 + THEN (assume_tac 1)); +by (eresolve_tac [nat_cadd_eq_add RS subst] 1 THEN (assume_tac 1)); +by (asm_full_simp_tac (ZF_ss addsimps [cadd_def, eqpoll_refl]) 1); +qed "nat_sum_eqpoll_sum"; + +goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat"; +by (fast_tac (ZF_cs addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))] + addSEs [ltE]) 1); +qed "le_in_nat"; + diff -r e15e8c0c1e37 -r 5324067d993f src/ZF/Cardinal_AC.ML --- a/src/ZF/Cardinal_AC.ML Tue Mar 26 11:38:17 1996 +0100 +++ b/src/ZF/Cardinal_AC.ML Tue Mar 26 11:42:36 1996 +0100 @@ -26,6 +26,17 @@ by (REPEAT_SOME assume_tac); qed "cardinal_eqE"; +goal Cardinal_AC.thy "|X| = |Y| <-> X eqpoll Y"; +by (fast_tac (ZF_cs addSEs [cardinal_cong, cardinal_eqE]) 1); +qed "cardinal_eqpoll_iff"; + +goal Cardinal_AC.thy + "!!A. [| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> \ +\ |A Un C| = |B Un D|"; +by (asm_full_simp_tac (ZF_ss addsimps [cardinal_eqpoll_iff, + eqpoll_disjoint_Un]) 1); +qed "cardinal_disjoint_Un"; + goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|"; by (resolve_tac [AC_well_ord RS exE] 1); by (etac well_ord_lepoll_imp_Card_le 1); diff -r e15e8c0c1e37 -r 5324067d993f src/ZF/upair.ML --- a/src/ZF/upair.ML Tue Mar 26 11:38:17 1996 +0100 +++ b/src/ZF/upair.ML Tue Mar 26 11:42:36 1996 +0100 @@ -156,6 +156,15 @@ [ (rtac (disjCI RS (cons_iff RS iffD2)) 1), (etac prem 1) ]); +qed_goal "cons_neq_0" ZF.thy "cons(a,B)=0 ==> P" + (fn [major]=> + [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1), + (rtac consI1 1) ]); + +(*Useful for rewriting*) +qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0" + (fn _=> [ (rtac notI 1), (etac cons_neq_0 1) ]); + (*** Singletons - using cons ***) qed_goal "singletonI" ZF.thy "a : {a}" @@ -308,6 +317,10 @@ (* succ(c) <= B ==> c : B *) val succ_subsetD = succI1 RSN (2,subsetD); +(* succ(b) ~= b *) +bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym); + + qed_goal "succ_inject" ZF.thy "!!m n. succ(m) = succ(n) ==> m=n" (fn _ => [ (fast_tac (lemmas_cs addSEs [succE, equalityE, make_elim succ_subsetD]