# HG changeset patch
# User traytel
# Date 1391081285 -3600
# Node ID 2e8fe898fa7173cb3a6ea6ddb4ae63ea6c6ef840
# Parent  5556470a02b703de06aefd841631c276eb7a2974
extended cardinals library

diff -r 5556470a02b7 -r 2e8fe898fa71 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Thu Jan 30 12:27:42 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Thu Jan 30 12:28:05 2014 +0100
@@ -400,4 +400,40 @@
 
 end
 
+lemma Card_order_cmax:
+assumes r: "Card_order r" and s: "Card_order s"
+shows "Card_order (cmax r s)"
+unfolding cmax_def by (auto simp: Card_order_csum)
+
+lemma ordLeq_cmax:
+assumes r: "Card_order r" and s: "Card_order s"
+shows "r \<le>o cmax r s \<and> s \<le>o cmax r s"
+proof-
+  {assume "r \<le>o s"
+   hence ?thesis by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s)
+  }
+  moreover
+  {assume "s \<le>o r"
+   hence ?thesis using cmax_com by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s)
+  }
+  ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto
+qed
+
+lemmas ordLeq_cmax1 = ordLeq_cmax[THEN conjunct1] and
+       ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2]
+
+lemma finite_cmax:
+assumes r: "Card_order r" and s: "Card_order s"
+shows "finite (Field (cmax r s)) \<longleftrightarrow> finite (Field r) \<and> finite (Field s)"
+proof-
+  {assume "r \<le>o s"
+   hence ?thesis by (metis cmax2 ordIso_finite_Field ordLeq_finite_Field r s)
+  }
+  moreover
+  {assume "s \<le>o r"
+   hence ?thesis by (metis cmax1 ordIso_finite_Field ordLeq_finite_Field r s)
+  }
+  ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto
+qed
+
 end
diff -r 5556470a02b7 -r 2e8fe898fa71 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jan 30 12:27:42 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jan 30 12:28:05 2014 +0100
@@ -652,6 +652,16 @@
   thus ?thesis using 1 ordLess_ordIso_trans by blast
 qed
 
+lemma ordLeq_finite_Field:
+assumes "r \<le>o s" and "finite (Field s)"
+shows "finite (Field r)"
+by (metis assms card_of_mono2 card_of_ordLeq_infinite)
+
+lemma ordIso_finite_Field:
+assumes "r =o s"
+shows "finite (Field r) \<longleftrightarrow> finite (Field s)"
+by (metis assms ordIso_iff_ordLeq ordLeq_finite_Field)
+
 
 subsection {* Cardinals versus set operations involving infinite sets *}