# HG changeset patch # User paulson # Date 1024221534 -7200 # Node ID 6104bd4088a2d3215edbf931c86170787946410a # Parent 072a77989ce0d1c3c2fb6e7cb91e1e7787152d3f conversion of CardinalArith to Isar script diff -r 072a77989ce0 -r 6104bd4088a2 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Sat Jun 15 22:57:33 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,909 +0,0 @@ -(* Title: ZF/CardinalArith.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Cardinal arithmetic -- WITHOUT the Axiom of Choice - -Note: Could omit proving the algebraic laws for cardinal addition and -multiplication. On finite cardinals these operations coincide with -addition and multiplication of natural numbers; on infinite cardinals they -coincide with union (maximum). Either way we get most laws for free. -*) - -val InfCard_def = thm "InfCard_def"; -val cmult_def = thm "cmult_def"; -val cadd_def = thm "cadd_def"; -val csquare_rel_def = thm "csquare_rel_def"; -val jump_cardinal_def = thm "jump_cardinal_def"; -val csucc_def = thm "csucc_def"; - - -(*** Cardinal addition ***) - -(** Cardinal addition is commutative **) - -Goalw [eqpoll_def] "A+B eqpoll B+A"; -by (rtac exI 1); -by (res_inst_tac [("c", "case(Inr, Inl)"), ("d", "case(Inr, Inl)")] - lam_bijective 1); -by Auto_tac; -qed "sum_commute_eqpoll"; - -Goalw [cadd_def] "i |+| j = j |+| i"; -by (rtac (sum_commute_eqpoll RS cardinal_cong) 1); -qed "cadd_commute"; - -(** Cardinal addition is associative **) - -Goalw [eqpoll_def] "(A+B)+C eqpoll A+(B+C)"; -by (rtac exI 1); -by (rtac sum_assoc_bij 1); -qed "sum_assoc_eqpoll"; - -(*Unconditional version requires AC*) -Goalw [cadd_def] - "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ -\ (i |+| j) |+| k = i |+| (j |+| k)"; -by (rtac cardinal_cong 1); -by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS sum_eqpoll_cong RS - eqpoll_trans) 1); -by (rtac (sum_assoc_eqpoll RS eqpoll_trans) 2); -by (rtac ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong RS - eqpoll_sym) 2); -by (REPEAT (ares_tac [well_ord_radd] 1)); -qed "well_ord_cadd_assoc"; - -(** 0 is the identity for addition **) - -Goalw [eqpoll_def] "0+A eqpoll A"; -by (rtac exI 1); -by (rtac bij_0_sum 1); -qed "sum_0_eqpoll"; - -Goalw [cadd_def] "Card(K) ==> 0 |+| K = K"; -by (asm_simp_tac (simpset() addsimps [sum_0_eqpoll RS cardinal_cong, - Card_cardinal_eq]) 1); -qed "cadd_0"; -Addsimps [cadd_0]; - -(** Addition by another cardinal **) - -Goalw [lepoll_def, inj_def] "A lepoll A+B"; -by (res_inst_tac [("x", "lam x:A. Inl(x)")] exI 1); -by (Asm_simp_tac 1); -qed "sum_lepoll_self"; - -(*Could probably weaken the premises to well_ord(K,r), or removing using AC*) -Goalw [cadd_def] - "[| Card(K); Ord(L) |] ==> K le (K |+| L)"; -by (rtac ([Card_cardinal_le, well_ord_lepoll_imp_Card_le] MRS le_trans) 1); -by (rtac sum_lepoll_self 3); -by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Card_is_Ord] 1)); -qed "cadd_le_self"; - -(** Monotonicity of addition **) - -Goalw [lepoll_def] - "[| A lepoll C; B lepoll D |] ==> A + B lepoll C + D"; -by (REPEAT (etac exE 1)); -by (res_inst_tac [("x", "lam z:A+B. case(%w. Inl(f`w), %y. Inr(fa`y), z)")] - exI 1); -by (res_inst_tac - [("d", "case(%w. Inl(converse(f)`w), %y. Inr(converse(fa)`y))")] - lam_injective 1); -by (typecheck_tac (tcset() addTCs [inj_is_fun])); -by Auto_tac; -qed "sum_lepoll_mono"; - -Goalw [cadd_def] - "[| K' le K; L' le L |] ==> (K' |+| L') le (K |+| L)"; -by (safe_tac (claset() addSDs [le_subset_iff RS iffD1])); -by (rtac well_ord_lepoll_imp_Card_le 1); -by (REPEAT (ares_tac [sum_lepoll_mono, subset_imp_lepoll] 2)); -by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1)); -qed "cadd_le_mono"; - -(** Addition of finite cardinals is "ordinary" addition **) - -Goalw [eqpoll_def] "succ(A)+B eqpoll succ(A+B)"; -by (rtac exI 1); -by (res_inst_tac [("c", "%z. if z=Inl(A) then A+B else z"), - ("d", "%z. if z=A+B then Inl(A) else z")] - lam_bijective 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [succI2, mem_imp_not_eq] - setloop eresolve_tac [sumE,succE]))); -qed "sum_succ_eqpoll"; - -(*Pulling the succ(...) outside the |...| requires m, n: nat *) -(*Unconditional version requires AC*) -Goalw [cadd_def] - "[| Ord(m); Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|"; -by (rtac (sum_succ_eqpoll RS cardinal_cong RS trans) 1); -by (rtac (succ_eqpoll_cong RS cardinal_cong) 1); -by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1); -by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1)); -qed "cadd_succ_lemma"; - -Goal "[| m: nat; n: nat |] ==> m |+| n = m#+n"; -by (induct_tac "m" 1); -by (asm_simp_tac (simpset() addsimps [nat_into_Card RS cadd_0]) 1); -by (asm_simp_tac (simpset() addsimps [cadd_succ_lemma, - nat_into_Card RS Card_cardinal_eq]) 1); -qed "nat_cadd_eq_add"; - - -(*** Cardinal multiplication ***) - -(** Cardinal multiplication is commutative **) - -(*Easier to prove the two directions separately*) -Goalw [eqpoll_def] "A*B eqpoll B*A"; -by (rtac exI 1); -by (res_inst_tac [("c", "%."), ("d", "%.")] - lam_bijective 1); -by Safe_tac; -by (ALLGOALS (Asm_simp_tac)); -qed "prod_commute_eqpoll"; - -Goalw [cmult_def] "i |*| j = j |*| i"; -by (rtac (prod_commute_eqpoll RS cardinal_cong) 1); -qed "cmult_commute"; - -(** Cardinal multiplication is associative **) - -Goalw [eqpoll_def] "(A*B)*C eqpoll A*(B*C)"; -by (rtac exI 1); -by (rtac prod_assoc_bij 1); -qed "prod_assoc_eqpoll"; - -(*Unconditional version requires AC*) -Goalw [cmult_def] - "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ -\ (i |*| j) |*| k = i |*| (j |*| k)"; -by (rtac cardinal_cong 1); -by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS - eqpoll_trans) 1); -by (rtac (prod_assoc_eqpoll RS eqpoll_trans) 2); -by (rtac ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS prod_eqpoll_cong RS - eqpoll_sym) 2); -by (REPEAT (ares_tac [well_ord_rmult] 1)); -qed "well_ord_cmult_assoc"; - -(** Cardinal multiplication distributes over addition **) - -Goalw [eqpoll_def] "(A+B)*C eqpoll (A*C)+(B*C)"; -by (rtac exI 1); -by (rtac sum_prod_distrib_bij 1); -qed "sum_prod_distrib_eqpoll"; - -Goalw [cadd_def, cmult_def] - "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ -\ (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"; -by (rtac cardinal_cong 1); -by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS - eqpoll_trans) 1); -by (rtac (sum_prod_distrib_eqpoll RS eqpoll_trans) 2); -by (rtac ([well_ord_cardinal_eqpoll, well_ord_cardinal_eqpoll] MRS - sum_eqpoll_cong RS eqpoll_sym) 2); -by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd] 1)); -qed "well_ord_cadd_cmult_distrib"; - -(** Multiplication by 0 yields 0 **) - -Goalw [eqpoll_def] "0*A eqpoll 0"; -by (rtac exI 1); -by (rtac lam_bijective 1); -by Safe_tac; -qed "prod_0_eqpoll"; - -Goalw [cmult_def] "0 |*| i = 0"; -by (asm_simp_tac (simpset() addsimps [prod_0_eqpoll RS cardinal_cong, - Card_0 RS Card_cardinal_eq]) 1); -qed "cmult_0"; -Addsimps [cmult_0]; - -(** 1 is the identity for multiplication **) - -Goalw [eqpoll_def] "{x}*A eqpoll A"; -by (rtac exI 1); -by (resolve_tac [singleton_prod_bij RS bij_converse_bij] 1); -qed "prod_singleton_eqpoll"; - -Goalw [cmult_def, succ_def] "Card(K) ==> 1 |*| K = K"; -by (asm_simp_tac (simpset() addsimps [prod_singleton_eqpoll RS cardinal_cong, - Card_cardinal_eq]) 1); -qed "cmult_1"; -Addsimps [cmult_1]; - -(*** Some inequalities for multiplication ***) - -Goalw [lepoll_def, inj_def] "A lepoll A*A"; -by (res_inst_tac [("x", "lam x:A. ")] exI 1); -by (Simp_tac 1); -qed "prod_square_lepoll"; - -(*Could probably weaken the premise to well_ord(K,r), or remove using AC*) -Goalw [cmult_def] "Card(K) ==> K le K |*| K"; -by (rtac le_trans 1); -by (rtac well_ord_lepoll_imp_Card_le 2); -by (rtac prod_square_lepoll 3); -by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord] 2)); -by (asm_simp_tac (simpset() - addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); -qed "cmult_square_le"; - -(** Multiplication by a non-zero cardinal **) - -Goalw [lepoll_def, inj_def] "b: B ==> A lepoll A*B"; -by (res_inst_tac [("x", "lam x:A. ")] exI 1); -by (Asm_simp_tac 1); -qed "prod_lepoll_self"; - -(*Could probably weaken the premises to well_ord(K,r), or removing using AC*) -Goalw [cmult_def] - "[| Card(K); Ord(L); 0 K le (K |*| L)"; -by (rtac ([Card_cardinal_le, well_ord_lepoll_imp_Card_le] MRS le_trans) 1); -by (rtac prod_lepoll_self 3); -by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord, ltD] 1)); -qed "cmult_le_self"; - -(** Monotonicity of multiplication **) - -Goalw [lepoll_def] - "[| A lepoll C; B lepoll D |] ==> A * B lepoll C * D"; -by (REPEAT (etac exE 1)); -by (res_inst_tac [("x", "lam :A*B. ")] exI 1); -by (res_inst_tac [("d", "%.")] - lam_injective 1); -by (typecheck_tac (tcset() addTCs [inj_is_fun])); -by Auto_tac; -qed "prod_lepoll_mono"; - -Goalw [cmult_def] - "[| K' le K; L' le L |] ==> (K' |*| L') le (K |*| L)"; -by (safe_tac (claset() addSDs [le_subset_iff RS iffD1])); -by (rtac well_ord_lepoll_imp_Card_le 1); -by (REPEAT (ares_tac [prod_lepoll_mono, subset_imp_lepoll] 2)); -by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); -qed "cmult_le_mono"; - -(*** Multiplication of finite cardinals is "ordinary" multiplication ***) - -Goalw [eqpoll_def] "succ(A)*B eqpoll B + A*B"; -by (rtac exI 1); -by (res_inst_tac [("c", "%. if x=A then Inl(y) else Inr()"), - ("d", "case(%y. , %z. z)")] - lam_bijective 1); -by Safe_tac; -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [succI2, if_type, mem_imp_not_eq]))); -qed "prod_succ_eqpoll"; - -(*Unconditional version requires AC*) -Goalw [cmult_def, cadd_def] - "[| Ord(m); Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"; -by (rtac (prod_succ_eqpoll RS cardinal_cong RS trans) 1); -by (rtac (cardinal_cong RS sym) 1); -by (rtac ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong) 1); -by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); -qed "cmult_succ_lemma"; - -Goal "[| m: nat; n: nat |] ==> m |*| n = m#*n"; -by (induct_tac "m" 1); -by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addsimps [cmult_succ_lemma, nat_cadd_eq_add]) 1); -qed "nat_cmult_eq_mult"; - -Goal "Card(n) ==> 2 |*| n = n |+| n"; -by (asm_simp_tac - (simpset() addsimps [cmult_succ_lemma, Card_is_Ord, - inst "j" "0" cadd_commute]) 1); -qed "cmult_2"; - - -bind_thm ("sum_lepoll_prod", [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll, - asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans)) - |> standard); - -Goal "[| A lepoll B; 2 lepoll A |] ==> A+B lepoll A*B"; -by (REPEAT (ares_tac [[sum_lepoll_mono, sum_lepoll_prod] - MRS lepoll_trans, lepoll_refl] 1)); -qed "lepoll_imp_sum_lepoll_prod"; - - -(*** Infinite Cardinals are Limit Ordinals ***) - -(*This proof is modelled upon one assuming nat<=A, with injection - lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z - and inverse %y. if y:nat then nat_case(u, %z. z, y) else y. \ - If f: inj(nat,A) then range(f) behaves like the natural numbers.*) -Goalw [lepoll_def] "nat lepoll A ==> cons(u,A) lepoll A"; -by (etac exE 1); -by (res_inst_tac [("x", - "lam z:cons(u,A). if z=u then f`0 \ -\ else if z: range(f) then f`succ(converse(f)`z) \ -\ else z")] exI 1); -by (res_inst_tac [("d", "%y. if y: range(f) \ -\ then nat_case(u, %z. f`z, converse(f)`y) \ -\ else y")] - lam_injective 1); -by (fast_tac (claset() addSIs [if_type, apply_type] - addIs [inj_is_fun, inj_converse_fun]) 1); -by (asm_simp_tac - (simpset() addsimps [inj_is_fun RS apply_rangeI, - inj_converse_fun RS apply_rangeI, - inj_converse_fun RS apply_funtype]) 1); -qed "nat_cons_lepoll"; - -Goal "nat lepoll A ==> cons(u,A) eqpoll A"; -by (etac (nat_cons_lepoll RS eqpollI) 1); -by (rtac (subset_consI RS subset_imp_lepoll) 1); -qed "nat_cons_eqpoll"; - -(*Specialized version required below*) -Goalw [succ_def] "nat <= A ==> succ(A) eqpoll A"; -by (eresolve_tac [subset_imp_lepoll RS nat_cons_eqpoll] 1); -qed "nat_succ_eqpoll"; - -Goalw [InfCard_def] "InfCard(nat)"; -by (blast_tac (claset() addIs [Card_nat, le_refl, Card_is_Ord]) 1); -qed "InfCard_nat"; - -Goalw [InfCard_def] "InfCard(K) ==> Card(K)"; -by (etac conjunct1 1); -qed "InfCard_is_Card"; - -Goalw [InfCard_def] - "[| InfCard(K); Card(L) |] ==> InfCard(K Un L)"; -by (asm_simp_tac (simpset() addsimps [Card_Un, Un_upper1_le RSN (2,le_trans), - Card_is_Ord]) 1); -qed "InfCard_Un"; - -(*Kunen's Lemma 10.11*) -Goalw [InfCard_def] "InfCard(K) ==> Limit(K)"; -by (etac conjE 1); -by (ftac Card_is_Ord 1); -by (rtac (ltI RS non_succ_LimitI) 1); -by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1); -by (safe_tac (claset() addSDs [Limit_nat RS Limit_le_succD])); -by (rewtac Card_def); -by (dtac trans 1); -by (etac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1); -by (etac (Ord_cardinal_le RS lt_trans2 RS lt_irrefl) 1); -by (REPEAT (ares_tac [le_eqI, Ord_cardinal] 1)); -qed "InfCard_is_Limit"; - - -(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***) - -(*A general fact about ordermap*) -Goalw [eqpoll_def] - "[| well_ord(A,r); x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)"; -by (rtac exI 1); -by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, well_ord_is_wf]) 1); -by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1); -by (rtac pred_subset 1); -qed "ordermap_eqpoll_pred"; - -(** Establishing the well-ordering **) - -Goalw [inj_def] "Ord(K) ==> (lam :K*K. ) : inj(K*K, K*K*K)"; -by (force_tac (claset() addIs [lam_type, Un_least_lt RS ltD, ltI], - simpset()) 1); -qed "csquare_lam_inj"; - -Goalw [csquare_rel_def] "Ord(K) ==> well_ord(K*K, csquare_rel(K))"; -by (rtac (csquare_lam_inj RS well_ord_rvimage) 1); -by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); -qed "well_ord_csquare"; - -(** Characterising initial segments of the well-ordering **) - -Goalw [csquare_rel_def] - "[| <, > : csquare_rel(K); x x le z & y le z"; -by (etac rev_mp 1); -by (REPEAT (etac ltE 1)); -by (asm_simp_tac (simpset() addsimps [rvimage_iff, - Un_absorb, Un_least_mem_iff, ltD]) 1); -by (safe_tac (claset() addSEs [mem_irrefl] - addSIs [Un_upper1_le, Un_upper2_le])); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2]))); -qed "csquareD"; - -Goalw [thm "Order.pred_def"] - "z pred(K*K, , csquare_rel(K)) <= succ(z)*succ(z)"; -by (safe_tac (claset() delrules [SigmaI, succCI])); -by (etac (csquareD RS conjE) 1); -by (rewtac lt_def); -by (ALLGOALS Blast_tac); -qed "pred_csquare_subset"; - -Goalw [csquare_rel_def] - "[| x <, > : csquare_rel(K)"; -by (subgoals_tac ["x \ -\ <, > : csquare_rel(K) | x=z & y=z"; -by (subgoals_tac ["x \ -\ ordermap(K*K, csquare_rel(K)) ` < \ -\ ordermap(K*K, csquare_rel(K)) ` "; -by (subgoals_tac ["z: K*K has no more than z*z predecessors..." (page 29) *) -Goalw [cmult_def] - "[| Limit(K); x \ -\ | ordermap(K*K, csquare_rel(K)) ` | le |succ(z)| |*| |succ(z)|"; -by (rtac (well_ord_rmult RS well_ord_lepoll_imp_Card_le) 1); -by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1)); -by (subgoals_tac ["z y |*| y = y |] ==> \ -\ ordertype(K*K, csquare_rel(K)) le K"; -by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); -by (rtac all_lt_imp_le 1); -by (assume_tac 1); -by (etac (well_ord_csquare RS Ord_ordertype) 1); -by (rtac Card_lt_imp_lt 1); -by (etac InfCard_is_Card 3); -by (etac ltE 2 THEN assume_tac 2); -by (asm_full_simp_tac (simpset() addsimps [ordertype_unfold]) 1); -by (safe_tac (claset() addSEs [ltE])); -by (subgoals_tac ["Ord(xa)", "Ord(ya)"] 1); -by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 2)); -by (rtac (InfCard_is_Limit RS ordermap_csquare_le RS lt_trans1) 1 THEN - REPEAT (ares_tac [refl] 1 ORELSE etac ltI 1)); -by (res_inst_tac [("i","xa Un ya"), ("j","nat")] Ord_linear2 1 THEN - REPEAT (ares_tac [Ord_Un, Ord_nat] 1)); -(*the finite case: xa Un ya < nat *) -by (res_inst_tac [("j", "nat")] lt_trans2 1); -by (asm_full_simp_tac (simpset() addsimps [InfCard_def]) 2); -by (asm_full_simp_tac - (simpset() addsimps [lt_def, nat_cmult_eq_mult, nat_succI, mult_type, - nat_into_Card RS Card_cardinal_eq, Ord_nat]) 1); -(*case nat le (xa Un ya) *) -by (asm_full_simp_tac - (simpset() addsimps [le_imp_subset RS nat_succ_eqpoll RS cardinal_cong, - le_succ_iff, InfCard_def, Card_cardinal, Un_least_lt, - Ord_Un, ltI, nat_le_cardinal, - Ord_cardinal_le RS lt_trans1 RS ltD]) 1); -qed "ordertype_csquare_le"; - -(*Main result: Kunen's Theorem 10.12*) -Goal "InfCard(K) ==> K |*| K = K"; -by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); -by (etac rev_mp 1); -by (trans_ind_tac "K" [] 1); -by (rtac impI 1); -by (rtac le_anti_sym 1); -by (etac (InfCard_is_Card RS cmult_square_le) 2); -by (rtac (ordertype_csquare_le RSN (2, le_trans)) 1); -by (assume_tac 2); -by (assume_tac 2); -by (asm_simp_tac - (simpset() addsimps [cmult_def, Ord_cardinal_le, - well_ord_csquare RS ordermap_bij RS - bij_imp_eqpoll RS cardinal_cong, - well_ord_csquare RS Ord_ordertype]) 1); -qed "InfCard_csquare_eq"; - -(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*) -Goal "[| well_ord(A,r); InfCard(|A|) |] ==> A*A eqpoll A"; -by (resolve_tac [prod_eqpoll_cong RS eqpoll_trans] 1); -by (REPEAT (etac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1)); -by (rtac well_ord_cardinal_eqE 1); -by (REPEAT (ares_tac [Ord_cardinal, well_ord_rmult, well_ord_Memrel] 1)); -by (asm_simp_tac (simpset() - addsimps [symmetric cmult_def, InfCard_csquare_eq]) 1); -qed "well_ord_InfCard_square_eq"; - -(** Toward's Kunen's Corollary 10.13 (1) **) - -Goal "[| InfCard(K); L le K; 0 K |*| L = K"; -by (rtac le_anti_sym 1); -by (etac ltE 2 THEN - REPEAT (ares_tac [cmult_le_self, InfCard_is_Card] 2)); -by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1); -by (resolve_tac [cmult_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1)); -by (asm_full_simp_tac (simpset() addsimps [InfCard_csquare_eq]) 1); -qed "InfCard_le_cmult_eq"; - -(*Corollary 10.13 (1), for cardinal multiplication*) -Goal "[| InfCard(K); InfCard(L) |] ==> K |*| L = K Un L"; -by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1); -by (typecheck_tac (tcset() addTCs [InfCard_is_Card, Card_is_Ord])); -by (resolve_tac [cmult_commute RS ssubst] 1); -by (resolve_tac [Un_commute RS ssubst] 1); -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps [InfCard_is_Limit RS Limit_has_0, InfCard_le_cmult_eq, - subset_Un_iff2 RS iffD1, le_imp_subset]))); -qed "InfCard_cmult_eq"; - -Goal "InfCard(K) ==> K |+| K = K"; -by (asm_simp_tac - (simpset() addsimps [cmult_2 RS sym, InfCard_is_Card, cmult_commute]) 1); -by (asm_simp_tac - (simpset() addsimps [InfCard_le_cmult_eq, InfCard_is_Limit, - Limit_has_0, Limit_has_succ]) 1); -qed "InfCard_cdouble_eq"; - -(*Corollary 10.13 (1), for cardinal addition*) -Goal "[| InfCard(K); L le K |] ==> K |+| L = K"; -by (rtac le_anti_sym 1); -by (etac ltE 2 THEN - REPEAT (ares_tac [cadd_le_self, InfCard_is_Card] 2)); -by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1); -by (resolve_tac [cadd_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1)); -by (asm_full_simp_tac (simpset() addsimps [InfCard_cdouble_eq]) 1); -qed "InfCard_le_cadd_eq"; - -Goal "[| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L"; -by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1); -by (typecheck_tac (tcset() addTCs [InfCard_is_Card, Card_is_Ord])); -by (resolve_tac [cadd_commute RS ssubst] 1); -by (resolve_tac [Un_commute RS ssubst] 1); -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps [InfCard_le_cadd_eq, - subset_Un_iff2 RS iffD1, le_imp_subset]))); -qed "InfCard_cadd_eq"; - -(*The other part, Corollary 10.13 (2), refers to the cardinality of the set - of all n-tuples of elements of K. A better version for the Isabelle theory - might be InfCard(K) ==> |list(K)| = K. -*) - -(*** For every cardinal number there exists a greater one - [Kunen's Theorem 10.16, which would be trivial using AC] ***) - -Goalw [jump_cardinal_def] "Ord(jump_cardinal(K))"; -by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); -by (blast_tac (claset() addSIs [Ord_ordertype]) 2); -by (rewtac Transset_def); -by (safe_tac subset_cs); -by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold]) 1); -by Safe_tac; -by (rtac UN_I 1); -by (rtac ReplaceI 2); -by (ALLGOALS (blast_tac (claset() addIs [well_ord_subset] addSEs [predE]))); -qed "Ord_jump_cardinal"; - -(*Allows selective unfolding. Less work than deriving intro/elim rules*) -Goalw [jump_cardinal_def] - "i : jump_cardinal(K) <-> \ -\ (EX r X. r <= K*K & X <= K & well_ord(X,r) & i = ordertype(X,r))"; -by (fast_tac subset_cs 1); (*It's vital to avoid reasoning about <=*) -qed "jump_cardinal_iff"; - -(*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*) -Goal "Ord(K) ==> K < jump_cardinal(K)"; -by (resolve_tac [Ord_jump_cardinal RSN (2,ltI)] 1); -by (resolve_tac [jump_cardinal_iff RS iffD2] 1); -by (REPEAT_FIRST (ares_tac [exI, conjI, well_ord_Memrel])); -by (rtac subset_refl 2); -by (asm_simp_tac (simpset() addsimps [Memrel_def, subset_iff]) 1); -by (asm_simp_tac (simpset() addsimps [ordertype_Memrel]) 1); -qed "K_lt_jump_cardinal"; - -(*The proof by contradiction: the bijection f yields a wellordering of X - whose ordertype is jump_cardinal(K). *) -Goal "[| well_ord(X,r); r <= K * K; X <= K; \ -\ f : bij(ordertype(X,r), jump_cardinal(K)) \ -\ |] ==> jump_cardinal(K) : jump_cardinal(K)"; -by (subgoal_tac "f O ordermap(X,r): bij(X, jump_cardinal(K))" 1); -by (REPEAT (ares_tac [comp_bij, ordermap_bij] 2)); -by (resolve_tac [jump_cardinal_iff RS iffD2] 1); -by (REPEAT_FIRST (resolve_tac [exI, conjI])); -by (rtac ([rvimage_type, Sigma_mono] MRS subset_trans) 1); -by (REPEAT (assume_tac 1)); -by (etac (bij_is_inj RS well_ord_rvimage) 1); -by (rtac (Ord_jump_cardinal RS well_ord_Memrel) 1); -by (asm_simp_tac - (simpset() addsimps [well_ord_Memrel RSN (2, bij_ordertype_vimage), - ordertype_Memrel, Ord_jump_cardinal]) 1); -qed "Card_jump_cardinal_lemma"; - -(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*) -Goal "Card(jump_cardinal(K))"; -by (rtac (Ord_jump_cardinal RS CardI) 1); -by (rewtac eqpoll_def); -by (safe_tac (claset() addSDs [ltD, jump_cardinal_iff RS iffD1])); -by (REPEAT (ares_tac [Card_jump_cardinal_lemma RS mem_irrefl] 1)); -qed "Card_jump_cardinal"; - -(*** Basic properties of successor cardinals ***) - -Goalw [csucc_def] - "Ord(K) ==> Card(csucc(K)) & K < csucc(K)"; -by (rtac LeastI 1); -by (REPEAT (ares_tac [conjI, Card_jump_cardinal, K_lt_jump_cardinal, - Ord_jump_cardinal] 1)); -qed "csucc_basic"; - -bind_thm ("Card_csucc", csucc_basic RS conjunct1); - -bind_thm ("lt_csucc", csucc_basic RS conjunct2); - -Goal "Ord(K) ==> 0 < csucc(K)"; -by (resolve_tac [[Ord_0_le, lt_csucc] MRS lt_trans1] 1); -by (REPEAT (assume_tac 1)); -qed "Ord_0_lt_csucc"; - -Goalw [csucc_def] - "[| Card(L); K csucc(K) le L"; -by (rtac Least_le 1); -by (REPEAT (ares_tac [conjI, Card_is_Ord] 1)); -qed "csucc_le"; - -Goal "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K"; -by (rtac iffI 1); -by (rtac Card_lt_imp_lt 2); -by (etac lt_trans1 2); -by (REPEAT (ares_tac [lt_csucc, Card_csucc, Card_is_Ord] 2)); -by (resolve_tac [notI RS not_lt_imp_le] 1); -by (resolve_tac [Card_cardinal RS csucc_le RS lt_trans1 RS lt_irrefl] 1); -by (assume_tac 1); -by (resolve_tac [Ord_cardinal_le RS lt_trans1] 1); -by (REPEAT (ares_tac [Ord_cardinal] 1 - ORELSE eresolve_tac [ltE, Card_is_Ord] 1)); -qed "lt_csucc_iff"; - -Goal "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"; -by (asm_simp_tac - (simpset() addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1); -qed "Card_lt_csucc_iff"; - -Goalw [InfCard_def] - "InfCard(K) ==> InfCard(csucc(K))"; -by (asm_simp_tac (simpset() addsimps [Card_csucc, Card_is_Ord, - lt_csucc RS leI RSN (2,le_trans)]) 1); -qed "InfCard_csucc"; - - -(*** Finite sets ***) - -Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)"; -by (induct_tac "n" 1); -by (simp_tac (simpset() addsimps [eqpoll_0_iff]) 1); -by (Clarify_tac 1); -by (subgoal_tac "EX u. u:A" 1); -by (etac 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 [thm "Fin.consI"] 1); -by (Blast_tac 1); -by (blast_tac (claset() addIs [subset_consI RS Fin_mono RS subsetD]) 1); -(*Now for the lemma assumed above*) -by (rewtac eqpoll_def); -by (blast_tac (claset() addIs [bij_converse_bij RS bij_is_fun RS apply_type]) 1); -val lemma = result(); - -Goalw [Finite_def] "Finite(A) ==> A : Fin(A)"; -by (blast_tac (claset() addIs [lemma RS spec RS mp]) 1); -qed "Finite_into_Fin"; - -Goal "A : Fin(U) ==> Finite(A)"; -by (fast_tac (claset() addSIs [Finite_0, Finite_cons] addEs [Fin_induct]) 1); -qed "Fin_into_Finite"; - -Goal "Finite(A) <-> A : Fin(A)"; -by (blast_tac (claset() addIs [Finite_into_Fin, Fin_into_Finite]) 1); -qed "Finite_Fin_iff"; - -Goal "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"; -by (blast_tac (claset() addSIs [Fin_into_Finite, Fin_UnI] - addSDs [Finite_into_Fin] - addIs [Un_upper1 RS Fin_mono RS subsetD, - Un_upper2 RS Fin_mono RS subsetD]) 1); -qed "Finite_Un"; - -Goal "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))"; -by (asm_full_simp_tac (simpset() addsimps [Finite_Fin_iff]) 1); -by (rtac Fin_UnionI 1); -by (etac Fin_induct 1); -by (Simp_tac 1); -by (blast_tac (claset() addIs [thm "Fin.consI", impOfSubs Fin_mono]) 1); -qed "Finite_Union"; - -(* Induction principle for Finite(A), by Sidi Ehmety *) -val major::prems = Goal -"[| Finite(A); P(0); \ -\ !! x B. [| Finite(B); x ~: B; P(B) |] \ -\ ==> P(cons(x, B)) |] \ -\ ==> P(A)"; -by (resolve_tac [major RS Finite_into_Fin RS Fin_induct] 1); -by (ALLGOALS(resolve_tac prems)); -by (ALLGOALS(asm_simp_tac (simpset() addsimps [Fin_into_Finite]))); -qed "Finite_induct"; - - -(** Removing elements from a finite set decreases its cardinality **) - -Goal "A: Fin(U) ==> x~:A --> ~ cons(x,A) lepoll A"; -by (etac Fin_induct 1); -by (simp_tac (simpset() addsimps [lepoll_0_iff]) 1); -by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1); -by (Asm_simp_tac 1); -by (blast_tac (claset() addSDs [cons_lepoll_consD]) 1); -by (Blast_tac 1); -qed "Fin_imp_not_cons_lepoll"; - -Goal "[| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)"; -by (rewtac cardinal_def); -by (rtac Least_equality 1); -by (fold_tac [cardinal_def]); -by (simp_tac (simpset() addsimps [succ_def]) 1); -by (blast_tac (claset() addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll] - addSEs [mem_irrefl] - addSDs [Finite_imp_well_ord]) 1); -by (blast_tac (claset() addIs [Card_cardinal, Card_is_Ord]) 1); -by (rtac 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 (blast_tac (claset() addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll] - addSDs [Finite_imp_well_ord]) 1); -qed "Finite_imp_cardinal_cons"; - - -Goal "[| Finite(A); a:A |] ==> succ(|A-{a}|) = |A|"; -by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1); -by (assume_tac 1); -by (asm_simp_tac (simpset() addsimps [Finite_imp_cardinal_cons, - Diff_subset RS subset_Finite]) 1); -by (asm_simp_tac (simpset() addsimps [cons_Diff]) 1); -qed "Finite_imp_succ_cardinal_Diff"; - -Goal "[| Finite(A); a:A |] ==> |A-{a}| < |A|"; -by (rtac succ_leE 1); -by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff]) 1); -qed "Finite_imp_cardinal_Diff"; - - -(** Theorems by Krzysztof Grabczewski, proofs by lcp **) - -bind_thm ("nat_implies_well_ord", - (transfer (the_context ()) nat_into_Ord) RS well_ord_Memrel); - -Goal "[| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; -by (rtac eqpoll_trans 1); -by (resolve_tac [well_ord_radd RS well_ord_cardinal_eqpoll RS eqpoll_sym] 1); -by (REPEAT (etac nat_implies_well_ord 1)); -by (asm_simp_tac (simpset() - addsimps [nat_cadd_eq_add RS sym, cadd_def, eqpoll_refl]) 1); -qed "nat_sum_eqpoll_sum"; - - -(*** Theorems by Sidi Ehmety ***) - -(*The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) -Goalw [Finite_def] "Finite(A - {a}) ==> Finite(A)"; -by (case_tac "a:A" 1); -by (subgoal_tac "A-{a}=A" 2); -by Auto_tac; -by (res_inst_tac [("x", "succ(n)")] bexI 1); -by (subgoal_tac "cons(a, A - {a}) = A & cons(n, n) = succ(n)" 1); -by (dres_inst_tac [("a", "a"), ("b", "n")] cons_eqpoll_cong 1); -by (auto_tac (claset() addDs [mem_irrefl], simpset())); -qed "Diff_sing_Finite"; - -(*And the contrapositive of this says - [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *) -Goal "Finite(B) ==> Finite(A-B) --> Finite(A)"; -by (etac Finite_induct 1); -by Auto_tac; -by (case_tac "x:A" 1); - by (subgoal_tac "A-cons(x, B) = A - B" 2); -by (subgoal_tac "A - cons(x, B) = (A - B) - {x}" 1); -by (rotate_tac ~1 1); -by (Asm_full_simp_tac 1); -by (dtac Diff_sing_Finite 1); -by Auto_tac; -qed_spec_mp "Diff_Finite"; - -Goal "Ord(i) ==> i <= nat --> i : nat | i=nat"; -by (etac trans_induct3 1); -by Auto_tac; -by (blast_tac (claset() addSDs [nat_le_Limit RS le_imp_subset]) 1); -qed_spec_mp "Ord_subset_natD"; - -Goal "[| Ord(i); i <= nat |] ==> Card(i)"; -by (blast_tac (claset() addDs [Ord_subset_natD] - addIs [Card_nat, nat_into_Card]) 1); -qed "Ord_nat_subset_into_Card"; - -Goal "Finite(A) ==> |A| : nat"; -by (etac Finite_induct 1); -by (auto_tac (claset(), - simpset() addsimps - [cardinal_0, Finite_imp_cardinal_cons])); -qed "Finite_cardinal_in_nat"; -Addsimps [Finite_cardinal_in_nat]; - -Goal "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1"; -by (rtac succ_inject 1); -by (res_inst_tac [("b", "|A|")] trans 1); -by (asm_simp_tac (simpset() addsimps - [Finite_imp_succ_cardinal_Diff]) 1); -by (subgoal_tac "1 lepoll A" 1); -by (blast_tac (claset() addIs [not_0_is_lepoll_1]) 2); -by (forward_tac [Finite_imp_well_ord] 1); -by (Clarify_tac 1); -by (rotate_tac ~1 1); -by (dtac well_ord_lepoll_imp_Card_le 1); -by (auto_tac (claset(), simpset() addsimps [cardinal_1])); -by (rtac trans 1); -by (rtac diff_succ 2); -by (auto_tac (claset(), simpset() addsimps [Finite_cardinal_in_nat])); -qed "Finite_Diff_sing_eq_diff_1"; - -Goal "Finite(B) ==> ALL A. |B|<|A| --> A - B ~= 0"; -by (etac Finite_induct 1); -by (ALLGOALS(Clarify_tac)); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps - [cardinal_0,Finite_imp_cardinal_cons]))); -by (case_tac "Finite(A)" 1); -by (subgoal_tac "Finite(cons(x, B))" 2); -by (dres_inst_tac [("B", "cons(x, B)")] Diff_Finite 2); -by (auto_tac (claset(), simpset() addsimps [Finite_0, Finite_cons])); -by (subgoal_tac "|B|<|A|" 1); -by (blast_tac (claset() addIs [lt_trans, Ord_cardinal]) 2); -by (case_tac "x:A" 1); -by (subgoal_tac "A - cons(x, B)= A - B" 2); -by Auto_tac; -by (subgoal_tac "|A| le |cons(x, B)|" 1); -by (blast_tac (claset() addDs [Finite_cons RS Finite_imp_well_ord] - addIs [well_ord_lepoll_imp_Card_le, subset_imp_lepoll]) 2); -by (auto_tac (claset(), simpset() addsimps [Finite_imp_cardinal_cons])); -by (auto_tac (claset() addSDs [Finite_cardinal_in_nat], - simpset() addsimps [le_iff])); -by (blast_tac (claset() addIs [lt_trans]) 1); -qed_spec_mp "cardinal_lt_imp_Diff_not_0"; diff -r 072a77989ce0 -r 6104bd4088a2 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Sat Jun 15 22:57:33 2002 +0200 +++ b/src/ZF/CardinalArith.thy Sun Jun 16 11:58:54 2002 +0200 @@ -3,7 +3,12 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Cardinal Arithmetic +Cardinal arithmetic -- WITHOUT the Axiom of Choice + +Note: Could omit proving the algebraic laws for cardinal addition and +multiplication. On finite cardinals these operations coincide with +addition and multiplication of natural numbers; on infinite cardinals they +coincide with union (maximum). Either way we get most laws for free. *) theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite: @@ -123,7 +128,7 @@ apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) apply (drule lesspoll_trans1, assumption) -apply (subgoal_tac "B lepoll \A") +apply (subgoal_tac "B \ \A") apply (drule lesspoll_trans1, assumption, blast) apply (blast intro: subset_imp_lepoll) done @@ -192,4 +197,985 @@ apply (blast intro: eqpoll_trans eqpoll_sym) done + +(*** Cardinal addition ***) + +(** Cardinal addition is commutative **) + +lemma sum_commute_eqpoll: "A+B \ B+A" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule_tac c = "case(Inr,Inl)" and d = "case(Inr,Inl)" in lam_bijective) +apply auto +done + +lemma cadd_commute: "i |+| j = j |+| i" +apply (unfold cadd_def) +apply (rule sum_commute_eqpoll [THEN cardinal_cong]) +done + +(** Cardinal addition is associative **) + +lemma sum_assoc_eqpoll: "(A+B)+C \ A+(B+C)" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule sum_assoc_bij) +done + +(*Unconditional version requires AC*) +lemma well_ord_cadd_assoc: + "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] + ==> (i |+| j) |+| k = i |+| (j |+| k)" +apply (unfold cadd_def) +apply (rule cardinal_cong) +apply (rule eqpoll_trans) + apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) + apply (blast intro: well_ord_radd elim:) +apply (rule sum_assoc_eqpoll [THEN eqpoll_trans]) +apply (rule eqpoll_sym) +apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) +apply (blast intro: well_ord_radd elim:) +done + +(** 0 is the identity for addition **) + +lemma sum_0_eqpoll: "0+A \ A" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule bij_0_sum) +done + +lemma cadd_0 [simp]: "Card(K) ==> 0 |+| K = K" +apply (unfold cadd_def) +apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq) +done + +(** Addition by another cardinal **) + +lemma sum_lepoll_self: "A \ A+B" +apply (unfold lepoll_def inj_def) +apply (rule_tac x = "lam x:A. Inl (x) " in exI) +apply (simp (no_asm_simp)) +done + +(*Could probably weaken the premises to well_ord(K,r), or removing using AC*) + +lemma cadd_le_self: + "[| Card(K); Ord(L) |] ==> K le (K |+| L)" +apply (unfold cadd_def) +apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le]) +apply assumption; +apply (rule_tac [2] sum_lepoll_self) +apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord) +done + +(** Monotonicity of addition **) + +lemma sum_lepoll_mono: + "[| A \ C; B \ D |] ==> A + B \ C + D" +apply (unfold lepoll_def) +apply (elim exE); +apply (rule_tac x = "lam z:A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI) +apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) `y))" + in lam_injective) +apply (typecheck add: inj_is_fun) +apply auto +done + +lemma cadd_le_mono: + "[| K' le K; L' le L |] ==> (K' |+| L') le (K |+| L)" +apply (unfold cadd_def) +apply (safe dest!: le_subset_iff [THEN iffD1]) +apply (rule well_ord_lepoll_imp_Card_le) +apply (blast intro: well_ord_radd well_ord_Memrel) +apply (blast intro: sum_lepoll_mono subset_imp_lepoll) +done + +(** Addition of finite cardinals is "ordinary" addition **) + +(*????????????????upair.ML*) +lemma eq_imp_not_mem: "a=A ==> a ~: A" +apply (blast intro: elim: mem_irrefl); +done + +lemma sum_succ_eqpoll: "succ(A)+B \ succ(A+B)" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule_tac c = "%z. if z=Inl (A) then A+B else z" + and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective) + apply (simp_all) +apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+ +done + +(*Pulling the succ(...) outside the |...| requires m, n: nat *) +(*Unconditional version requires AC*) +lemma cadd_succ_lemma: + "[| Ord(m); Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|" +apply (unfold cadd_def) +apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans]) +apply (rule succ_eqpoll_cong [THEN cardinal_cong]) +apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym]) +apply (blast intro: well_ord_radd well_ord_Memrel) +done + +lemma nat_cadd_eq_add: "[| m: nat; n: nat |] ==> m |+| n = m#+n" +apply (induct_tac "m") +apply (simp add: nat_into_Card [THEN cadd_0]) +apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq]) +done + + +(*** Cardinal multiplication ***) + +(** Cardinal multiplication is commutative **) + +(*Easier to prove the two directions separately*) +lemma prod_commute_eqpoll: "A*B \ B*A" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule_tac c = "%." and d = "%." in lam_bijective) +apply (auto ); +done + +lemma cmult_commute: "i |*| j = j |*| i" +apply (unfold cmult_def) +apply (rule prod_commute_eqpoll [THEN cardinal_cong]) +done + +(** Cardinal multiplication is associative **) + +lemma prod_assoc_eqpoll: "(A*B)*C \ A*(B*C)" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule prod_assoc_bij) +done + +(*Unconditional version requires AC*) +lemma well_ord_cmult_assoc: + "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] + ==> (i |*| j) |*| k = i |*| (j |*| k)" +apply (unfold cmult_def) +apply (rule cardinal_cong) +apply (rule eqpoll_trans); + apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) + apply (blast intro: well_ord_rmult) +apply (rule prod_assoc_eqpoll [THEN eqpoll_trans]) +apply (rule eqpoll_sym); +apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) +apply (blast intro: well_ord_rmult) +done + +(** Cardinal multiplication distributes over addition **) + +lemma sum_prod_distrib_eqpoll: "(A+B)*C \ (A*C)+(B*C)" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule sum_prod_distrib_bij) +done + +lemma well_ord_cadd_cmult_distrib: + "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] + ==> (i |+| j) |*| k = (i |*| k) |+| (j |*| k)" +apply (unfold cadd_def cmult_def) +apply (rule cardinal_cong) +apply (rule eqpoll_trans); + apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) +apply (blast intro: well_ord_radd) +apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans]) +apply (rule eqpoll_sym); +apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll + well_ord_cardinal_eqpoll]) +apply (blast intro: well_ord_rmult)+ +done + +(** Multiplication by 0 yields 0 **) + +lemma prod_0_eqpoll: "0*A \ 0" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule lam_bijective) +apply safe +done + +lemma cmult_0 [simp]: "0 |*| i = 0" +apply (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong]) +done + +(** 1 is the identity for multiplication **) + +lemma prod_singleton_eqpoll: "{x}*A \ A" +apply (unfold eqpoll_def) +apply (rule exI) +apply (rule singleton_prod_bij [THEN bij_converse_bij]) +done + +lemma cmult_1 [simp]: "Card(K) ==> 1 |*| K = K" +apply (unfold cmult_def succ_def) +apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq) +done + +(*** Some inequalities for multiplication ***) + +lemma prod_square_lepoll: "A \ A*A" +apply (unfold lepoll_def inj_def) +apply (rule_tac x = "lam x:A. " in exI) +apply (simp (no_asm)) +done + +(*Could probably weaken the premise to well_ord(K,r), or remove using AC*) +lemma cmult_square_le: "Card(K) ==> K le K |*| K" +apply (unfold cmult_def) +apply (rule le_trans) +apply (rule_tac [2] well_ord_lepoll_imp_Card_le) +apply (rule_tac [3] prod_square_lepoll) +apply (simp (no_asm_simp) add: le_refl Card_is_Ord Card_cardinal_eq) +apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord); +done + +(** Multiplication by a non-zero cardinal **) + +lemma prod_lepoll_self: "b: B ==> A \ A*B" +apply (unfold lepoll_def inj_def) +apply (rule_tac x = "lam x:A. " in exI) +apply (simp (no_asm_simp)) +done + +(*Could probably weaken the premises to well_ord(K,r), or removing using AC*) +lemma cmult_le_self: + "[| Card(K); Ord(L); 0 K le (K |*| L)" +apply (unfold cmult_def) +apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le]) + apply assumption; + apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) +apply (blast intro: prod_lepoll_self ltD) +done + +(** Monotonicity of multiplication **) + +lemma prod_lepoll_mono: + "[| A \ C; B \ D |] ==> A * B \ C * D" +apply (unfold lepoll_def) +apply (elim exE); +apply (rule_tac x = "lam :A*B. " in exI) +apply (rule_tac d = "%. " + in lam_injective) +apply (typecheck add: inj_is_fun) +apply auto +done + +lemma cmult_le_mono: + "[| K' le K; L' le L |] ==> (K' |*| L') le (K |*| L)" +apply (unfold cmult_def) +apply (safe dest!: le_subset_iff [THEN iffD1]) +apply (rule well_ord_lepoll_imp_Card_le) + apply (blast intro: well_ord_rmult well_ord_Memrel) +apply (blast intro: prod_lepoll_mono subset_imp_lepoll) +done + +(*** Multiplication of finite cardinals is "ordinary" multiplication ***) + +lemma prod_succ_eqpoll: "succ(A)*B \ B + A*B" +apply (unfold eqpoll_def) +apply (rule exI); +apply (rule_tac c = "%. if x=A then Inl (y) else Inr ()" + and d = "case (%y. , %z. z)" in lam_bijective) +apply safe +apply (simp_all add: succI2 if_type mem_imp_not_eq) +done + +(*Unconditional version requires AC*) +lemma cmult_succ_lemma: + "[| Ord(m); Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)" +apply (unfold cmult_def cadd_def) +apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans]) +apply (rule cardinal_cong [symmetric]) +apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) +apply (blast intro: well_ord_rmult well_ord_Memrel) +done + +lemma nat_cmult_eq_mult: "[| m: nat; n: nat |] ==> m |*| n = m#*n" +apply (induct_tac "m") +apply (simp (no_asm_simp)) +apply (simp (no_asm_simp) add: cmult_succ_lemma nat_cadd_eq_add) +done + +lemma cmult_2: "Card(n) ==> 2 |*| n = n |+| n" +apply (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0]) +done + +lemma sum_lepoll_prod: "2 \ C ==> B+B \ C*B" +apply (rule lepoll_trans); +apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll]) +apply (erule prod_lepoll_mono) +apply (rule lepoll_refl); +done + +lemma lepoll_imp_sum_lepoll_prod: "[| A \ B; 2 \ A |] ==> A+B \ A*B" +apply (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl) +done + + +(*** Infinite Cardinals are Limit Ordinals ***) + +(*This proof is modelled upon one assuming nat<=A, with injection + lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z + and inverse %y. if y:nat then nat_case(u, %z. z, y) else y. \ + If f: inj(nat,A) then range(f) behaves like the natural numbers.*) +lemma nat_cons_lepoll: "nat \ A ==> cons(u,A) \ A" +apply (unfold lepoll_def) +apply (erule exE) +apply (rule_tac x = + "lam z:cons (u,A). + if z=u then f`0 + else if z: range (f) then f`succ (converse (f) `z) else z" + in exI) +apply (rule_tac d = + "%y. if y: range(f) then nat_case (u, %z. f`z, converse(f) `y) + else y" + in lam_injective) +apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun) +apply (simp add: inj_is_fun [THEN apply_rangeI] + inj_converse_fun [THEN apply_rangeI] + inj_converse_fun [THEN apply_funtype]) +done + +lemma nat_cons_eqpoll: "nat \ A ==> cons(u,A) \ A" +apply (erule nat_cons_lepoll [THEN eqpollI]) +apply (rule subset_consI [THEN subset_imp_lepoll]) +done + +(*Specialized version required below*) +lemma nat_succ_eqpoll: "nat <= A ==> succ(A) \ A" +apply (unfold succ_def) +apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll]) +done + +lemma InfCard_nat: "InfCard(nat)" +apply (unfold InfCard_def) +apply (blast intro: Card_nat le_refl Card_is_Ord) +done + +lemma InfCard_is_Card: "InfCard(K) ==> Card(K)" +apply (unfold InfCard_def) +apply (erule conjunct1) +done + +lemma InfCard_Un: + "[| InfCard(K); Card(L) |] ==> InfCard(K Un L)" +apply (unfold InfCard_def) +apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans] Card_is_Ord) +done + +(*Kunen's Lemma 10.11*) +lemma InfCard_is_Limit: "InfCard(K) ==> Limit(K)" +apply (unfold InfCard_def) +apply (erule conjE) +apply (frule Card_is_Ord) +apply (rule ltI [THEN non_succ_LimitI]) +apply (erule le_imp_subset [THEN subsetD]) +apply (safe dest!: Limit_nat [THEN Limit_le_succD]) +apply (unfold Card_def) +apply (drule trans) +apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong]) +apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl]) +apply (rule le_eqI) +apply assumption; +apply (rule Ord_cardinal) +done + + +(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***) + +(*A general fact about ordermap*) +lemma ordermap_eqpoll_pred: + "[| well_ord(A,r); x:A |] ==> ordermap(A,r)`x \ pred(A,x,r)" +apply (unfold eqpoll_def) +apply (rule exI) +apply (simp (no_asm_simp) add: ordermap_eq_image well_ord_is_wf) +apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, THEN bij_converse_bij]) +apply (rule pred_subset) +done + +(** Establishing the well-ordering **) + +lemma csquare_lam_inj: + "Ord(K) ==> (lam :K*K. ) : inj(K*K, K*K*K)" +apply (unfold inj_def) +apply (force intro: lam_type Un_least_lt [THEN ltD] ltI) +done + +lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))" +apply (unfold csquare_rel_def) +apply (rule csquare_lam_inj [THEN well_ord_rvimage]) +apply assumption; +apply (blast intro: well_ord_rmult well_ord_Memrel) +done + +(** Characterising initial segments of the well-ordering **) + +lemma csquareD: + "[| <, > : csquare_rel(K); x x le z & y le z" +apply (unfold csquare_rel_def) +apply (erule rev_mp) +apply (elim ltE) +apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD) +apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le) +apply (simp_all (no_asm_simp) add: lt_def succI2) +done + +lemma pred_csquare_subset: + "z pred(K*K, , csquare_rel(K)) <= succ(z)*succ(z)" +apply (unfold Order.pred_def) +apply (safe del: SigmaI succCI) +apply (erule csquareD [THEN conjE]) +apply (unfold lt_def) +apply (auto ); +done + +lemma csquare_ltI: + "[| x <, > : csquare_rel(K)" +apply (unfold csquare_rel_def) +apply (subgoal_tac "x <, > : csquare_rel(K) | x=z & y=z" +apply (unfold csquare_rel_def) +apply (subgoal_tac "x + ordermap(K*K, csquare_rel(K)) ` < + ordermap(K*K, csquare_rel(K)) ` " +apply (subgoal_tac "z: K*K has no more than z*z predecessors..." (page 29) *) +lemma ordermap_csquare_le: + "[| Limit(K); x + | ordermap(K*K, csquare_rel(K)) ` | le |succ(z)| |*| |succ(z)|" +apply (unfold cmult_def) +apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le]) +apply (rule Ord_cardinal [THEN well_ord_Memrel])+ +apply (subgoal_tac "z y |*| y = y |] + ==> ordertype(K*K, csquare_rel(K)) le K" +apply (frule InfCard_is_Card [THEN Card_is_Ord]) +apply (rule all_lt_imp_le) +apply assumption +apply (erule well_ord_csquare [THEN Ord_ordertype]) +apply (rule Card_lt_imp_lt) +apply (erule_tac [3] InfCard_is_Card) +apply (erule_tac [2] ltE) +apply (simp add: ordertype_unfold) +apply (safe elim!: ltE) +apply (subgoal_tac "Ord (xa) & Ord (ya)") + prefer 2 apply (blast intro: Ord_in_Ord) +apply (clarify ); +(*??WHAT A MESS!*) +apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1], + (assumption | rule refl | erule ltI)+) +apply (rule_tac i = "xa Un ya" and j = "nat" in Ord_linear2, + simp_all add: Ord_Un Ord_nat) +prefer 2 (*case nat le (xa Un ya) *) + apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] + le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un + ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD]) +(*the finite case: xa Un ya < nat *) +apply (rule_tac j = "nat" in lt_trans2) + apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type + nat_into_Card [THEN Card_cardinal_eq] Ord_nat) +apply (simp add: InfCard_def) +done + +(*Main result: Kunen's Theorem 10.12*) +lemma InfCard_csquare_eq: "InfCard(K) ==> K |*| K = K" +apply (frule InfCard_is_Card [THEN Card_is_Ord]) +apply (erule rev_mp) +apply (erule_tac i=K in trans_induct) +apply (rule impI) +apply (rule le_anti_sym) +apply (erule_tac [2] InfCard_is_Card [THEN cmult_square_le]) +apply (rule ordertype_csquare_le [THEN [2] le_trans]) +prefer 2 apply (assumption) +prefer 2 apply (assumption) +apply (simp (no_asm_simp) add: cmult_def Ord_cardinal_le well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll, THEN cardinal_cong] well_ord_csquare [THEN Ord_ordertype]) +done + +(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*) +lemma well_ord_InfCard_square_eq: + "[| well_ord(A,r); InfCard(|A|) |] ==> A*A \ A" +apply (rule prod_eqpoll_cong [THEN eqpoll_trans]) +apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+ +apply (rule well_ord_cardinal_eqE) +apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel) +apply assumption; +apply (simp (no_asm_simp) add: cmult_def [symmetric] InfCard_csquare_eq) +done + +(** Toward's Kunen's Corollary 10.13 (1) **) + +lemma InfCard_le_cmult_eq: "[| InfCard(K); L le K; 0 K |*| L = K" +apply (rule le_anti_sym) + prefer 2 + apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card) +apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl]) +apply (rule cmult_le_mono [THEN le_trans], assumption+) +apply (simp add: InfCard_csquare_eq) +done + +(*Corollary 10.13 (1), for cardinal multiplication*) +lemma InfCard_cmult_eq: "[| InfCard(K); InfCard(L) |] ==> K |*| L = K Un L" +apply (rule_tac i = "K" and j = "L" in Ord_linear_le) +apply (typecheck add: InfCard_is_Card Card_is_Ord) +apply (rule cmult_commute [THEN ssubst]) +apply (rule Un_commute [THEN ssubst]) +apply (simp_all (no_asm_simp) add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) +done + +lemma InfCard_cdouble_eq: "InfCard(K) ==> K |+| K = K" +apply (simp (no_asm_simp) add: cmult_2 [symmetric] InfCard_is_Card cmult_commute) +apply (simp (no_asm_simp) add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ) +done + +(*Corollary 10.13 (1), for cardinal addition*) +lemma InfCard_le_cadd_eq: "[| InfCard(K); L le K |] ==> K |+| L = K" +apply (rule le_anti_sym) + prefer 2 + apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card) +apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl]) +apply (rule cadd_le_mono [THEN le_trans], assumption+) +apply (simp add: InfCard_cdouble_eq) +done + +lemma InfCard_cadd_eq: "[| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L" +apply (rule_tac i = "K" and j = "L" in Ord_linear_le) +apply (typecheck add: InfCard_is_Card Card_is_Ord) +apply (rule cadd_commute [THEN ssubst]) +apply (rule Un_commute [THEN ssubst]) +apply (simp_all (no_asm_simp) add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) +done + +(*The other part, Corollary 10.13 (2), refers to the cardinality of the set + of all n-tuples of elements of K. A better version for the Isabelle theory + might be InfCard(K) ==> |list(K)| = K. +*) + +(*** For every cardinal number there exists a greater one + [Kunen's Theorem 10.16, which would be trivial using AC] ***) + +lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))" +apply (unfold jump_cardinal_def) +apply (rule Ord_is_Transset [THEN [2] OrdI]) + prefer 2 apply (blast intro!: Ord_ordertype) +apply (unfold Transset_def) +apply (safe del: subsetI) +apply (simp add: ordertype_pred_unfold) +apply safe +apply (rule UN_I) +apply (rule_tac [2] ReplaceI) + prefer 4 apply (blast intro: well_ord_subset elim!: predE)+ +done + +(*Allows selective unfolding. Less work than deriving intro/elim rules*) +lemma jump_cardinal_iff: + "i : jump_cardinal(K) <-> + (EX r X. r <= K*K & X <= K & well_ord(X,r) & i = ordertype(X,r))" +apply (unfold jump_cardinal_def) +apply (blast del: subsetI) +done + +(*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*) +lemma K_lt_jump_cardinal: "Ord(K) ==> K < jump_cardinal(K)" +apply (rule Ord_jump_cardinal [THEN [2] ltI]) +apply (rule jump_cardinal_iff [THEN iffD2]) +apply (rule_tac x="Memrel(K)" in exI) +apply (rule_tac x=K in exI) +apply (simp add: ordertype_Memrel well_ord_Memrel) +apply (simp add: Memrel_def subset_iff) +done + +(*The proof by contradiction: the bijection f yields a wellordering of X + whose ordertype is jump_cardinal(K). *) +lemma Card_jump_cardinal_lemma: + "[| well_ord(X,r); r <= K * K; X <= K; + f : bij(ordertype(X,r), jump_cardinal(K)) |] + ==> jump_cardinal(K) : jump_cardinal(K)" +apply (subgoal_tac "f O ordermap (X,r) : bij (X, jump_cardinal (K))") + prefer 2 apply (blast intro: comp_bij ordermap_bij) +apply (rule jump_cardinal_iff [THEN iffD2]) +apply (intro exI conjI) +apply (rule subset_trans [OF rvimage_type Sigma_mono]) +apply assumption+ +apply (erule bij_is_inj [THEN well_ord_rvimage]) +apply (rule Ord_jump_cardinal [THEN well_ord_Memrel]) +apply (simp add: well_ord_Memrel [THEN [2] bij_ordertype_vimage] + ordertype_Memrel Ord_jump_cardinal) +done + +(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*) +lemma Card_jump_cardinal: "Card(jump_cardinal(K))" +apply (rule Ord_jump_cardinal [THEN CardI]) +apply (unfold eqpoll_def) +apply (safe dest!: ltD jump_cardinal_iff [THEN iffD1]) +apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl]) +done + +(*** Basic properties of successor cardinals ***) + +lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)" +apply (unfold csucc_def) +apply (rule LeastI) +apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ +done + +lemmas Card_csucc = csucc_basic [THEN conjunct1, standard] + +lemmas lt_csucc = csucc_basic [THEN conjunct2, standard] + +lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)" +apply (blast intro: Ord_0_le lt_csucc lt_trans1) +done + +lemma csucc_le: "[| Card(L); K csucc(K) le L" +apply (unfold csucc_def) +apply (rule Least_le) +apply (blast intro: Card_is_Ord)+ +done + +lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K" +apply (rule iffI) +apply (rule_tac [2] Card_lt_imp_lt) +apply (erule_tac [2] lt_trans1) +apply (simp_all add: lt_csucc Card_csucc Card_is_Ord) +apply (rule notI [THEN not_lt_imp_le]) +apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl]) +apply assumption +apply (rule Ord_cardinal_le [THEN lt_trans1]) +apply (simp_all add: Ord_cardinal Card_is_Ord) +done + +lemma Card_lt_csucc_iff: + "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K" +by (simp (no_asm_simp) add: lt_csucc_iff Card_cardinal_eq Card_is_Ord) + +lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))" +by (simp add: InfCard_def Card_csucc Card_is_Ord + lt_csucc [THEN leI, THEN [2] le_trans]) + + +(*** Finite sets ***) + +lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \ n --> A : Fin(A)" +apply (induct_tac "n") +apply (simp (no_asm) add: eqpoll_0_iff) +apply clarify +apply (subgoal_tac "EX u. u:A") +apply (erule exE) +apply (rule Diff_sing_eqpoll [THEN revcut_rl]) +prefer 2 apply (assumption) +apply assumption +apply (rule_tac b = "A" in cons_Diff [THEN subst]) +apply assumption +apply (rule Fin.consI) +apply blast +apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD]) +(*Now for the lemma assumed above*) +apply (unfold eqpoll_def) +apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type]) +done + +lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)" +apply (unfold Finite_def) +apply (blast intro: Fin_lemma) +done + +lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)" +apply (fast intro!: Finite_0 Finite_cons elim: Fin_induct) +done + +lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)" +apply (blast intro: Finite_into_Fin Fin_into_Finite) +done + +lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)" +by (blast intro!: Fin_into_Finite Fin_UnI + dest!: Finite_into_Fin + intro: Un_upper1 [THEN Fin_mono, THEN subsetD] + Un_upper2 [THEN Fin_mono, THEN subsetD]) + +lemma Finite_Union: "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))" +apply (simp add: Finite_Fin_iff) +apply (rule Fin_UnionI) +apply (erule Fin_induct) +apply (simp (no_asm)) +apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD]) +done + +(* Induction principle for Finite(A), by Sidi Ehmety *) +lemma Finite_induct: +"[| Finite(A); P(0); + !! x B. [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |] + ==> P(A)" +apply (erule Finite_into_Fin [THEN Fin_induct]) +apply (blast intro: Fin_into_Finite)+ +done + + +(** Removing elements from a finite set decreases its cardinality **) + +lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x~:A --> ~ cons(x,A) \ A" +apply (erule Fin_induct) +apply (simp (no_asm) add: lepoll_0_iff) +apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))") +apply (simp (no_asm_simp)) +apply (blast dest!: cons_lepoll_consD) +apply blast +done + +lemma Finite_imp_cardinal_cons: "[| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)" +apply (unfold cardinal_def) +apply (rule Least_equality) +apply (fold cardinal_def) +apply (simp (no_asm) add: succ_def) +apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll + elim!: mem_irrefl dest!: Finite_imp_well_ord) +apply (blast intro: Card_cardinal Card_is_Ord) +apply (rule notI) +apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE]) +apply assumption +apply assumption +apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) +apply (erule le_imp_lepoll [THEN lepoll_trans]) +apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll] + dest!: Finite_imp_well_ord) +done + + +lemma Finite_imp_succ_cardinal_Diff: "[| Finite(A); a:A |] ==> succ(|A-{a}|) = |A|" +apply (rule_tac b = "A" in cons_Diff [THEN subst]) +apply assumption +apply (simp (no_asm_simp) add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite]) +apply (simp (no_asm_simp) add: cons_Diff) +done + +lemma Finite_imp_cardinal_Diff: "[| Finite(A); a:A |] ==> |A-{a}| < |A|" +apply (rule succ_leE) +apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff) +done + + +(** Theorems by Krzysztof Grabczewski, proofs by lcp **) + +lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard] + +lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \ m #+ n" +apply (rule eqpoll_trans) +apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym]) +apply (erule nat_implies_well_ord)+ +apply (simp (no_asm_simp) add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl) +done + + +(*** Theorems by Sidi Ehmety ***) + +(*The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) +lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)" +apply (unfold Finite_def) +apply (case_tac "a:A") +apply (subgoal_tac [2] "A-{a}=A") +apply auto +apply (rule_tac x = "succ (n) " in bexI) +apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ") +apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong) +apply (auto dest: mem_irrefl) +done + +(*And the contrapositive of this says + [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *) +lemma Diff_Finite [rule_format (no_asm)]: "Finite(B) ==> Finite(A-B) --> Finite(A)" +apply (erule Finite_induct) +apply auto +apply (case_tac "x:A") + apply (subgoal_tac [2] "A-cons (x, B) = A - B") +apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}") +apply (rotate_tac -1) +apply simp +apply (drule Diff_sing_Finite) +apply auto +done + +lemma Ord_subset_natD [rule_format (no_asm)]: "Ord(i) ==> i <= nat --> i : nat | i=nat" +apply (erule trans_induct3) +apply auto +apply (blast dest!: nat_le_Limit [THEN le_imp_subset]) +done + +lemma Ord_nat_subset_into_Card: "[| Ord(i); i <= nat |] ==> Card(i)" +apply (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) +done + +lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| : nat" +apply (erule Finite_induct) +apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons) +done + +lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1" +apply (rule succ_inject) +apply (rule_tac b = "|A|" in trans) +apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff) +apply (subgoal_tac "1 \ A") +prefer 2 apply (blast intro: not_0_is_lepoll_1) +apply (frule Finite_imp_well_ord) +apply clarify +apply (rotate_tac -1) +apply (drule well_ord_lepoll_imp_Card_le) +apply (auto simp add: cardinal_1) +apply (rule trans) +apply (rule_tac [2] diff_succ) +apply (auto simp add: Finite_cardinal_in_nat) +done + +lemma cardinal_lt_imp_Diff_not_0 [rule_format (no_asm)]: "Finite(B) ==> ALL A. |B|<|A| --> A - B ~= 0" +apply (erule Finite_induct) +apply auto +apply (simp_all add: Finite_imp_cardinal_cons) +apply (case_tac "Finite (A) ") +apply (subgoal_tac [2] "Finite (cons (x, B))") +apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite) +apply (auto simp add: Finite_0 Finite_cons) +apply (subgoal_tac "|B|<|A|") +prefer 2 apply (blast intro: lt_trans Ord_cardinal) +apply (case_tac "x:A") +apply (subgoal_tac [2] "A - cons (x, B) = A - B") +apply auto +apply (subgoal_tac "|A| le |cons (x, B) |") +prefer 2 + apply (blast dest: Finite_cons [THEN Finite_imp_well_ord] + intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll) +apply (auto simp add: Finite_imp_cardinal_cons) +apply (auto dest!: Finite_cardinal_in_nat simp add: le_iff) +apply (blast intro: lt_trans) +done + + +ML{* +val InfCard_def = thm "InfCard_def" +val cmult_def = thm "cmult_def" +val cadd_def = thm "cadd_def" +val jump_cardinal_def = thm "jump_cardinal_def" +val csucc_def = thm "csucc_def" + +val sum_commute_eqpoll = thm "sum_commute_eqpoll"; +val cadd_commute = thm "cadd_commute"; +val sum_assoc_eqpoll = thm "sum_assoc_eqpoll"; +val well_ord_cadd_assoc = thm "well_ord_cadd_assoc"; +val sum_0_eqpoll = thm "sum_0_eqpoll"; +val cadd_0 = thm "cadd_0"; +val sum_lepoll_self = thm "sum_lepoll_self"; +val cadd_le_self = thm "cadd_le_self"; +val sum_lepoll_mono = thm "sum_lepoll_mono"; +val cadd_le_mono = thm "cadd_le_mono"; +val eq_imp_not_mem = thm "eq_imp_not_mem"; +val sum_succ_eqpoll = thm "sum_succ_eqpoll"; +val nat_cadd_eq_add = thm "nat_cadd_eq_add"; +val prod_commute_eqpoll = thm "prod_commute_eqpoll"; +val cmult_commute = thm "cmult_commute"; +val prod_assoc_eqpoll = thm "prod_assoc_eqpoll"; +val well_ord_cmult_assoc = thm "well_ord_cmult_assoc"; +val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll"; +val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib"; +val prod_0_eqpoll = thm "prod_0_eqpoll"; +val cmult_0 = thm "cmult_0"; +val prod_singleton_eqpoll = thm "prod_singleton_eqpoll"; +val cmult_1 = thm "cmult_1"; +val prod_lepoll_self = thm "prod_lepoll_self"; +val cmult_le_self = thm "cmult_le_self"; +val prod_lepoll_mono = thm "prod_lepoll_mono"; +val cmult_le_mono = thm "cmult_le_mono"; +val prod_succ_eqpoll = thm "prod_succ_eqpoll"; +val nat_cmult_eq_mult = thm "nat_cmult_eq_mult"; +val cmult_2 = thm "cmult_2"; +val sum_lepoll_prod = thm "sum_lepoll_prod"; +val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod"; +val nat_cons_lepoll = thm "nat_cons_lepoll"; +val nat_cons_eqpoll = thm "nat_cons_eqpoll"; +val nat_succ_eqpoll = thm "nat_succ_eqpoll"; +val InfCard_nat = thm "InfCard_nat"; +val InfCard_is_Card = thm "InfCard_is_Card"; +val InfCard_Un = thm "InfCard_Un"; +val InfCard_is_Limit = thm "InfCard_is_Limit"; +val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred"; +val ordermap_z_lt = thm "ordermap_z_lt"; +val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq"; +val InfCard_cmult_eq = thm "InfCard_cmult_eq"; +val InfCard_cdouble_eq = thm "InfCard_cdouble_eq"; +val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq"; +val InfCard_cadd_eq = thm "InfCard_cadd_eq"; +val Ord_jump_cardinal = thm "Ord_jump_cardinal"; +val jump_cardinal_iff = thm "jump_cardinal_iff"; +val K_lt_jump_cardinal = thm "K_lt_jump_cardinal"; +val Card_jump_cardinal = thm "Card_jump_cardinal"; +val csucc_basic = thm "csucc_basic"; +val Card_csucc = thm "Card_csucc"; +val lt_csucc = thm "lt_csucc"; +val Ord_0_lt_csucc = thm "Ord_0_lt_csucc"; +val csucc_le = thm "csucc_le"; +val lt_csucc_iff = thm "lt_csucc_iff"; +val Card_lt_csucc_iff = thm "Card_lt_csucc_iff"; +val InfCard_csucc = thm "InfCard_csucc"; +val Finite_into_Fin = thm "Finite_into_Fin"; +val Fin_into_Finite = thm "Fin_into_Finite"; +val Finite_Fin_iff = thm "Finite_Fin_iff"; +val Finite_Un = thm "Finite_Un"; +val Finite_Union = thm "Finite_Union"; +val Finite_induct = thm "Finite_induct"; +val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll"; +val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons"; +val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff"; +val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff"; +val nat_implies_well_ord = thm "nat_implies_well_ord"; +val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum"; +val Diff_sing_Finite = thm "Diff_sing_Finite"; +val Diff_Finite = thm "Diff_Finite"; +val Ord_subset_natD = thm "Ord_subset_natD"; +val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card"; +val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat"; +val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1"; +val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0"; +*} + end diff -r 072a77989ce0 -r 6104bd4088a2 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Sat Jun 15 22:57:33 2002 +0200 +++ b/src/ZF/IsaMakefile Sun Jun 16 11:58:54 2002 +0200 @@ -30,7 +30,7 @@ $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML \ ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \ - CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \ + CardinalArith.thy Cardinal_AC.thy \ Datatype.ML Datatype.thy Epsilon.thy Finite.thy \ Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy \ InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \