# HG changeset patch # User paulson # Date 880635925 -3600 # Node ID 63844406913c9b9ea50df1dc122bfc00fae4a1b2 # Parent e220fb9bd4e53107f2fc64a589a9216dbb1fe53b Tidying, mostly indentation diff -r e220fb9bd4e5 -r 63844406913c src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Thu Nov 27 13:58:51 1997 +0100 +++ b/src/ZF/CardinalArith.ML Thu Nov 27 14:05:25 1997 +0100 @@ -58,7 +58,7 @@ goalw CardinalArith.thy [cadd_def] "!!K. Card(K) ==> 0 |+| K = K"; by (asm_simp_tac (simpset() addsimps [sum_0_eqpoll RS cardinal_cong, - Card_cardinal_eq]) 1); + Card_cardinal_eq]) 1); qed "cadd_0"; (** Addition by another cardinal **) @@ -108,7 +108,7 @@ lam_bijective 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [succI2, mem_imp_not_eq] - setloop eresolve_tac [sumE,succE]))); + setloop eresolve_tac [sumE,succE]))); qed "sum_succ_eqpoll"; (*Pulling the succ(...) outside the |...| requires m, n: nat *) @@ -127,7 +127,7 @@ by (nat_ind_tac "m" [mnat] 1); by (asm_simp_tac (simpset() addsimps [nat_into_Card RS cadd_0]) 1); by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cadd_succ_lemma, - nat_into_Card RS Card_cardinal_eq]) 1); + nat_into_Card RS Card_cardinal_eq]) 1); qed "nat_cadd_eq_add"; @@ -182,8 +182,8 @@ 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 (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"; @@ -197,7 +197,7 @@ goalw CardinalArith.thy [cmult_def] "0 |*| i = 0"; by (asm_simp_tac (simpset() addsimps [prod_0_eqpoll RS cardinal_cong, - Card_0 RS Card_cardinal_eq]) 1); + Card_0 RS Card_cardinal_eq]) 1); qed "cmult_0"; (** 1 is the identity for multiplication **) @@ -209,7 +209,7 @@ goalw CardinalArith.thy [cmult_def, succ_def] "!!K. Card(K) ==> 1 |*| K = K"; by (asm_simp_tac (simpset() addsimps [prod_singleton_eqpoll RS cardinal_cong, - Card_cardinal_eq]) 1); + Card_cardinal_eq]) 1); qed "cmult_1"; (*** Some inequalities for multiplication ***) @@ -225,7 +225,8 @@ 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); +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 **) @@ -291,14 +292,14 @@ by (nat_ind_tac "m" [mnat] 1); by (asm_simp_tac (simpset() addsimps [cmult_0]) 1); by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cmult_succ_lemma, - nat_cadd_eq_add]) 1); + nat_cadd_eq_add]) 1); qed "nat_cmult_eq_mult"; goal CardinalArith.thy "!!m n. Card(n) ==> 2 |*| n = n |+| n"; by (asm_simp_tac (simpset() addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, - Card_is_Ord, - read_instantiate [("j","0")] cadd_commute, cadd_0]) 1); + Card_is_Ord, cadd_0, + read_instantiate [("j","0")] cadd_commute]) 1); qed "cmult_2"; @@ -321,11 +322,11 @@ 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, - left_inverse, right_inverse, nat_0I, nat_succI, - nat_case_0, nat_case_succ] - setloop split_tac [expand_if]) 1); + inj_converse_fun RS apply_rangeI, + 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); qed "nat_cons_lepoll"; goal CardinalArith.thy "!!i. nat lepoll A ==> cons(u,A) eqpoll A"; @@ -349,7 +350,7 @@ goalw CardinalArith.thy [InfCard_def] "!!K L. [| 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); + Card_is_Ord]) 1); qed "InfCard_Un"; (*Kunen's Lemma 10.11*) @@ -383,7 +384,7 @@ goalw CardinalArith.thy [inj_def] "!!K. Ord(K) ==> (lam :K*K. ) : inj(K*K, K*K*K)"; by (fast_tac (claset() addss (simpset()) - addIs [lam_type, Un_least_lt RS ltD, ltI]) 1); + addIs [lam_type, Un_least_lt RS ltD, ltI]) 1); qed "csquare_lam_inj"; goalw CardinalArith.thy [csquare_rel_def] @@ -399,9 +400,9 @@ \ <, > : csquare_rel(K) --> x le z & y le z"; by (REPEAT (etac ltE 1)); by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff, - Un_absorb, Un_least_mem_iff, ltD]) 1); + Un_absorb, Un_least_mem_iff, ltD]) 1); by (safe_tac (claset() addSEs [mem_irrefl] - addSIs [Un_upper1_le, Un_upper2_le])); + addSIs [Un_upper1_le, Un_upper2_le])); by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2, Ord_succ]))); qed_spec_mp "csquareD"; @@ -420,7 +421,7 @@ by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2)); by (REPEAT (etac ltE 1)); by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff, - Un_absorb, Un_least_mem_iff, ltD]) 1); + Un_absorb, Un_least_mem_iff, ltD]) 1); qed "csquare_ltI"; (*Part of the traditional proof. UNUSED since it's harder to prove & apply *) @@ -431,11 +432,11 @@ by (REPEAT (eresolve_tac [asm_rl, lt_trans1] 2)); by (REPEAT (etac ltE 1)); by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff, - Un_absorb, Un_least_mem_iff, ltD]) 1); + Un_absorb, Un_least_mem_iff, ltD]) 1); by (REPEAT_FIRST (etac succE)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [subset_Un_iff RS iff_sym, - subset_Un_iff2 RS iff_sym, OrdmemD]))); + subset_Un_iff2 RS iff_sym, OrdmemD]))); qed "csquare_or_eqI"; (** The cardinality of initial segments **) @@ -451,7 +452,7 @@ by (etac well_ord_is_wf 4); by (ALLGOALS (blast_tac (claset() addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap] - addSEs [ltE]))); + addSEs [ltE]))); qed "ordermap_z_lt"; (*Kunen: "each : K*K has no more than z*z predecessors..." (page 29) *) @@ -498,13 +499,13 @@ 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); + nat_into_Card RS Card_cardinal_eq, Ord_nat]) 1); (*case nat le (xb Un y) *) 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); + 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*) @@ -520,9 +521,9 @@ 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); + 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)*) @@ -532,7 +533,8 @@ 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); +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) **) @@ -556,7 +558,7 @@ 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]))); + subset_Un_iff2 RS iffD1, le_imp_subset]))); qed "InfCard_cmult_eq"; (*This proof appear to be the simplest!*) @@ -587,7 +589,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps [InfCard_le_cadd_eq, - subset_Un_iff2 RS iffD1, le_imp_subset]))); + 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 @@ -643,7 +645,7 @@ 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); + 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*) @@ -701,7 +703,7 @@ goalw CardinalArith.thy [InfCard_def] "!!K. 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); + lt_csucc RS leI RSN (2,le_trans)]) 1); qed "InfCard_csucc"; @@ -742,9 +744,9 @@ goal CardinalArith.thy "!!A. [| 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); + addSDs [Finite_into_Fin] + addIs [Un_upper1 RS Fin_mono RS subsetD, + Un_upper2 RS Fin_mono RS subsetD]) 1); qed "Finite_Un"; @@ -767,8 +769,8 @@ 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); + addSEs [mem_irrefl] + addSDs [Finite_imp_well_ord]) 1); by (blast_tac (claset() addIs [Ord_succ, 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); @@ -792,27 +794,24 @@ goal CardinalArith.thy "!!a A. [| Finite(A); a:A |] ==> |A-{a}| < |A|"; by (rtac succ_leE 1); by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, - Ord_cardinal RS le_refl]) 1); + Ord_cardinal RS le_refl]) 1); qed "Finite_imp_cardinal_Diff"; -(** Thanks to Krzysztof Grabczewski **) +(** Theorems by Krzysztof Grabczewski, proofs by lcp **) val nat_implies_well_ord = (transfer CardinalArith.thy 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 (simpset() addsimps [cadd_def, eqpoll_refl]) 1); +by (resolve_tac [well_ord_radd RS well_ord_cardinal_eqpoll RS eqpoll_sym] 1); +by (REPEAT (eresolve_tac [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"; goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat"; -by (blast_tac (claset() addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))] - addSEs [ltE]) 1); +by (blast_tac (claset() addSIs [nat_succI] addSDs [lt_nat_in_nat]) 1); qed "le_in_nat";