src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 55851 3d40cf74726c
parent 55811 aa1acc25126b
child 55866 a6fa341a6d66
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 03:13:45 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 12:48:19 2014 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4    "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
     1.5  unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
     1.6  
     1.7 -lemma Cinfinite_csum_strong:
     1.8 +lemma Cinfinite_csum_weak:
     1.9    "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
    1.10  by (erule Cinfinite_csum1)
    1.11  
    1.12 @@ -335,6 +335,9 @@
    1.13  lemma cprod_mono2: "p2 \<le>o r2 \<Longrightarrow> q *c p2 \<le>o q *c r2"
    1.14  by (simp only: cprod_def ordLeq_Times_mono2)
    1.15  
    1.16 +lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
    1.17 +by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
    1.18 +
    1.19  lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
    1.20  unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
    1.21  
    1.22 @@ -347,6 +350,15 @@
    1.23  lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
    1.24  by (blast intro: cinfinite_cprod2 Card_order_cprod)
    1.25  
    1.26 +lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
    1.27 +by (metis cprod_mono ordIso_iff_ordLeq)
    1.28 +
    1.29 +lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
    1.30 +by (metis cprod_mono1 ordIso_iff_ordLeq)
    1.31 +
    1.32 +lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
    1.33 +by (metis cprod_mono2 ordIso_iff_ordLeq)
    1.34 +
    1.35  lemma cprod_com: "p1 *c p2 =o p2 *c p1"
    1.36  by (simp only: cprod_def card_of_Times_commute)
    1.37  
    1.38 @@ -514,6 +526,9 @@
    1.39  unfolding cinfinite_def cprod_def
    1.40  by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+
    1.41  
    1.42 +lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
    1.43 +using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
    1.44 +
    1.45  lemma cexp_cprod_ordLeq:
    1.46    assumes r1: "Card_order r1" and r2: "Cinfinite r2"
    1.47    and r3: "Cnotzero r3" "r3 \<le>o r2"