src/ZF/CardinalArith.thy
changeset 13356 c9cfe1638bf2
parent 13328 703de709a64b
child 13615 449a70d88b38
     1.1 --- a/src/ZF/CardinalArith.thy	Sun Jul 14 15:11:21 2002 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Sun Jul 14 15:14:43 2002 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4  done
     1.5  
     1.6  
     1.7 -(*** Cardinal addition ***)
     1.8 +subsection{*Cardinal addition*}
     1.9  
    1.10  text{*Note: Could omit proving the algebraic laws for cardinal addition and
    1.11  multiplication.  On finite cardinals these operations coincide with
    1.12 @@ -214,7 +214,7 @@
    1.13  done
    1.14  
    1.15  
    1.16 -(*** Cardinal multiplication ***)
    1.17 +subsection{*Cardinal multiplication*}
    1.18  
    1.19  (** Cardinal multiplication is commutative **)
    1.20  
    1.21 @@ -301,7 +301,7 @@
    1.22  apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
    1.23  done
    1.24  
    1.25 -(*** Some inequalities for multiplication ***)
    1.26 +subsection{*Some inequalities for multiplication*}
    1.27  
    1.28  lemma prod_square_lepoll: "A \<lesssim> A*A"
    1.29  apply (unfold lepoll_def inj_def)
    1.30 @@ -356,7 +356,7 @@
    1.31  apply (blast intro: prod_lepoll_mono subset_imp_lepoll)
    1.32  done
    1.33  
    1.34 -(*** Multiplication of finite cardinals is "ordinary" multiplication ***)
    1.35 +subsection{*Multiplication of finite cardinals is "ordinary" multiplication*}
    1.36  
    1.37  lemma prod_succ_eqpoll: "succ(A)*B \<approx> B + A*B"
    1.38  apply (unfold eqpoll_def)
    1.39 @@ -396,7 +396,7 @@
    1.40  by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)
    1.41  
    1.42  
    1.43 -(*** Infinite Cardinals are Limit Ordinals ***)
    1.44 +subsection{*Infinite Cardinals are Limit Ordinals*}
    1.45  
    1.46  (*This proof is modelled upon one assuming nat<=A, with injection
    1.47    lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z
    1.48 @@ -623,6 +623,15 @@
    1.49  apply (simp add: cmult_def [symmetric] InfCard_csquare_eq)
    1.50  done
    1.51  
    1.52 +lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K"
    1.53 +apply (rule well_ord_InfCard_square_eq)  
    1.54 + apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) 
    1.55 +apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) 
    1.56 +done
    1.57 +
    1.58 +lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)"
    1.59 +by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord])
    1.60 +
    1.61  (** Toward's Kunen's Corollary 10.13 (1) **)
    1.62  
    1.63  lemma InfCard_le_cmult_eq: "[| InfCard(K);  L le K;  0<L |] ==> K |*| L = K"
    1.64 @@ -672,8 +681,9 @@
    1.65    might be  InfCard(K) ==> |list(K)| = K.
    1.66  *)
    1.67  
    1.68 -(*** For every cardinal number there exists a greater one
    1.69 -     [Kunen's Theorem 10.16, which would be trivial using AC] ***)
    1.70 +subsection{*For Every Cardinal Number There Exists A Greater One}
    1.71 +
    1.72 +text{*This result is Kunen's Theorem 10.16, which would be trivial using AC*}
    1.73  
    1.74  lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))"
    1.75  apply (unfold jump_cardinal_def)
    1.76 @@ -730,7 +740,7 @@
    1.77  apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl])
    1.78  done
    1.79  
    1.80 -(*** Basic properties of successor cardinals ***)
    1.81 +subsection{*Basic Properties of Successor Cardinals*}
    1.82  
    1.83  lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)"
    1.84  apply (unfold csucc_def)