--- a/src/HOL/BNF_Wellorder_Relation.thy Thu Jan 30 10:00:53 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Relation.thy Thu Jan 30 13:31:56 2014 +0100
@@ -34,6 +34,8 @@
abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r"
abbreviation Above where "Above \<equiv> Order_Relation.Above r"
abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS r"
+abbreviation ofilter where "ofilter \<equiv> Order_Relation.ofilter r"
+lemmas ofilter_def = Order_Relation.ofilter_def[of r]
subsection {* Auxiliaries *}
@@ -139,10 +141,6 @@
definition suc :: "'a set \<Rightarrow> 'a"
where "suc A \<equiv> minim (AboveS A)"
-definition ofilter :: "'a set \<Rightarrow> bool"
-where
-"ofilter A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under a \<le> A)"
-
subsubsection {* Properties of max2 *}
@@ -438,7 +436,7 @@
hence 2: "?a \<in> Field r" using minim_inField[of ?B] by blast
have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast
hence 4: "?a \<notin> A" by blast
- have 5: "A \<le> Field r" using * ofilter_def[of A] by auto
+ have 5: "A \<le> Field r" using * ofilter_def by auto
(* *)
moreover
have "A = underS ?a"
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Thu Jan 30 10:00:53 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Thu Jan 30 13:31:56 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
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jan 30 10:00:53 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jan 30 13:31:56 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 *}
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Thu Jan 30 10:00:53 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Thu Jan 30 13:31:56 2014 +0100
@@ -530,6 +530,5 @@
abbreviation "max2 \<equiv> wo_rel.max2"
abbreviation "supr \<equiv> wo_rel.supr"
abbreviation "suc \<equiv> wo_rel.suc"
-abbreviation "ofilter \<equiv> wo_rel.ofilter"
end
--- a/src/HOL/Order_Relation.thy Thu Jan 30 10:00:53 2014 +0100
+++ b/src/HOL/Order_Relation.thy Thu Jan 30 13:31:56 2014 +0100
@@ -210,6 +210,9 @@
definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
+definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
+where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
+
text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
we bounded comprehension by @{text "Field r"} in order to properly cover
the case of @{text "A"} being empty. *}