--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Wed Jan 22 10:13:40 2014 +0100
@@ -5,7 +5,7 @@
Cardinal arithmetic.
*)
-header {* Cardinal Arithmetic *}
+header {* Cardinal Arithmetic *}
theory Cardinal_Arithmetic
imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
@@ -201,7 +201,6 @@
"\<lbrakk>Cinfinite r; |I| \<le>o r; \<forall>i \<in> I. |A i| \<le>o r\<rbrakk> \<Longrightarrow> |SIGMA i : I. A i| \<le>o r"
unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field)
-
lemma card_order_cexp:
assumes "card_order r1" "card_order r2"
shows "card_order (r1 ^c r2)"
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Wed Jan 22 10:13:40 2014 +0100
@@ -376,13 +376,11 @@
ultimately show ?thesis using ordLeq_transitive by blast
qed
-
lemma ordLeq_Sigma_mono1:
assumes "\<forall>i \<in> I. p i \<le>o r i"
shows "|SIGMA i : I. Field(p i)| \<le>o |SIGMA i : I. Field(r i)|"
using assms by (auto simp add: card_of_Sigma_mono1)
-
lemma ordLeq_Sigma_mono:
assumes "inj_on f I" and "f ` I \<le> J" and
"\<forall>j \<in> J. p j \<le>o r j"
@@ -390,13 +388,11 @@
using assms card_of_mono2 card_of_Sigma_mono
[of f I J "\<lambda> i. Field(p i)" "\<lambda> j. Field(r j)"] by metis
-
lemma card_of_Sigma_cong1:
assumes "\<forall>i \<in> I. |A i| =o |B i|"
shows "|SIGMA i : I. A i| =o |SIGMA i : I. B i|"
using assms by (auto simp add: card_of_Sigma_mono1 ordIso_iff_ordLeq)
-
lemma card_of_Sigma_cong2:
assumes "bij_betw f (I::'i set) (J::'j set)"
shows "|SIGMA i : I. (A::'j \<Rightarrow> 'a set) (f i)| =o |SIGMA j : J. A j|"
@@ -884,7 +880,7 @@
using lists_UNIV by auto
-subsection {* Cardinals versus the set-of-finite-sets operator *}
+subsection {* Cardinals versus the set-of-finite-sets operator *}
definition Fpow :: "'a set \<Rightarrow> 'a set set"
where "Fpow A \<equiv> {X. X \<le> A \<and> finite X}"
@@ -997,7 +993,7 @@
using assms card_of_Fpow_infinite card_of_ordIso by blast
-subsection {* The cardinal $\omega$ and the finite cardinals *}
+subsection {* The cardinal $\omega$ and the finite cardinals *}
subsubsection {* First as well-orders *}
@@ -1119,13 +1115,11 @@
"natLeq =o |A| \<Longrightarrow> \<not>finite A"
using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
-
lemma ordIso_natLeq_on_imp_finite:
"|A| =o natLeq_on n \<Longrightarrow> finite A"
unfolding ordIso_def iso_def[abs_def]
by (auto simp: Field_natLeq_on bij_betw_finite)
-
lemma natLeq_on_Card_order: "Card_order (natLeq_on n)"
proof(unfold card_order_on_def,
auto simp add: natLeq_on_Well_order, simp add: Field_natLeq_on)
@@ -1135,20 +1129,17 @@
finite_well_order_on_ordIso ordIso_iff_ordLeq by blast
qed
-
corollary card_of_Field_natLeq_on:
"|Field (natLeq_on n)| =o natLeq_on n"
using Field_natLeq_on natLeq_on_Card_order
Card_order_iff_ordIso_card_of[of "natLeq_on n"]
ordIso_symmetric[of "natLeq_on n"] by blast
-
corollary card_of_less:
"|{0 ..< n}| =o natLeq_on n"
using Field_natLeq_on card_of_Field_natLeq_on
unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by auto
-
lemma natLeq_on_ordLeq_less_eq:
"((natLeq_on m) \<le>o (natLeq_on n)) = (m \<le> n)"
proof
@@ -1167,7 +1158,6 @@
using card_of_less ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
qed
-
lemma natLeq_on_ordLeq_less:
"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
using not_ordLeq_iff_ordLess[OF natLeq_on_Well_order natLeq_on_Well_order, of n m]
@@ -1204,7 +1194,6 @@
using finite_imp_card_of_natLeq_on[of A]
by(auto simp add: ordIso_natLeq_on_imp_finite)
-
lemma finite_card_of_iff_card:
assumes FIN: "finite A" and FIN': "finite B"
shows "( |A| =o |B| ) = (card A = card B)"
@@ -1577,7 +1566,8 @@
shows "\<not>finite (Func A B)"
using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
-section {* Infinite cardinals are limit ordinals *}
+
+subsection {* Infinite cardinals are limit ordinals *}
lemma card_order_infinite_isLimOrd:
assumes c: "Card_order r" and i: "\<not>finite (Field r)"
@@ -1684,7 +1674,8 @@
ultimately show False unfolding card_of_ordLess[symmetric] by auto
qed
-section {* Regular vs. Stable Cardinals *}
+
+subsection {* Regular vs. stable cardinals *}
definition stable :: "'a rel \<Rightarrow> bool"
where
--- a/src/HOL/Cardinals/Cardinals.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Cardinals.thy Wed Jan 22 10:13:40 2014 +0100
@@ -6,7 +6,7 @@
Theory of ordinals and cardinals.
*)
-header {* Theory of Ordinals and Cardinals *}
+header {* Theory of Ordinals and Cardinals *}
theory Cardinals
imports Ordinal_Arithmetic Cardinal_Arithmetic Wellorder_Extension
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Wed Jan 22 10:13:40 2014 +0100
@@ -9,7 +9,8 @@
theory Constructions_on_Wellorders
imports
- BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union "../Library/Cardinal_Notations"
+ BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union
+ "../Library/Cardinal_Notations"
begin
declare
@@ -21,7 +22,8 @@
lemma Func_emp2[simp]: "A \<noteq> {} \<Longrightarrow> Func A {} = {}" by auto
-subsection {* Restriction to a set *}
+
+subsection {* Restriction to a set *}
lemma Restr_incr2:
"r <= r' \<Longrightarrow> Restr r A <= Restr r' A"
@@ -53,7 +55,7 @@
by blast
-subsection {* Order filters versus restrictions and embeddings *}
+subsection {* Order filters versus restrictions and embeddings *}
lemma ofilter_Restr:
assumes WELL: "Well_order r" and
@@ -167,7 +169,7 @@
by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def)
-subsection {* Copy via direct images *}
+subsection {* Copy via direct images *}
lemma Id_dir_image: "dir_image Id f \<le> Id"
unfolding dir_image_def by auto
@@ -273,7 +275,7 @@
qed
-subsection {* The maxim among a finite set of ordinals *}
+subsection {* The maxim among a finite set of ordinals *}
text {* The correct phrasing would be ``a maxim of ...", as @{text "\<le>o"} is only a preorder. *}
@@ -435,8 +437,7 @@
qed
-
-section {* Limit and Succesor Ordinals *}
+subsection {* Limit and succesor ordinals *}
lemma embed_underS2:
assumes r: "Well_order r" and s: "Well_order s" and g: "embed r s g" and a: "a \<in> Field r"
@@ -547,7 +548,7 @@
by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: Field_def)
qed
-subsection {* Successor and limit elements of an ordinal *}
+subsubsection {* Successor and limit elements of an ordinal *}
definition "succ i \<equiv> suc {i}"
@@ -723,7 +724,7 @@
else L f i"
-subsection {* Well-order recursion with (zero), succesor, and limit *}
+subsubsection {* Well-order recursion with (zero), succesor, and limit *}
definition worecSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where "worecSL S L \<equiv> worec (mergeSL S L)"
@@ -818,7 +819,7 @@
qed
-subsection {* Well-order succ-lim induction: *}
+subsubsection {* Well-order succ-lim induction *}
lemma ord_cases:
obtains j where "i = succ j" and "aboveS j \<noteq> {}" | "isLim i"
@@ -886,7 +887,6 @@
by (metis (lifting, full_types) a mem_Collect_eq succ_diff succ_in)
qed
-
end (* context wo_rel *)
abbreviation "zero \<equiv> wo_rel.zero"
@@ -900,7 +900,8 @@
abbreviation "worecSL \<equiv> wo_rel.worecSL"
abbreviation "worecZSL \<equiv> wo_rel.worecZSL"
-section {* Projections of Wellorders *}
+
+subsection {* Projections of wellorders *}
definition "oproj r s f \<equiv> Field s \<subseteq> f ` (Field r) \<and> compat r s f"
--- a/src/HOL/Cardinals/Fun_More.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Fun_More.thy Wed Jan 22 10:13:40 2014 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-subsection {* Purely functional properties *}
+subsection {* Purely functional properties *}
(* unused *)
(*1*)lemma notIn_Un_bij_betw2:
@@ -130,7 +130,6 @@
subsection {* Properties involving Hilbert choice *}
-
(*1*)lemma bij_betw_inv_into_LEFT:
assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A"
shows "(inv_into A f)`(f ` B) = B"
@@ -169,12 +168,10 @@
card_atLeastLessThan[of m] card_atLeastLessThan[of n]
bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto
-
(*2*)lemma atLeastLessThan_less_eq:
"({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)"
unfolding ivl_subset by arith
-
(*2*)lemma atLeastLessThan_less_eq2:
assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}"
shows "m \<le> n"
--- a/src/HOL/Cardinals/Order_Relation_More.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More.thy Wed Jan 22 10:13:40 2014 +0100
@@ -11,7 +11,7 @@
imports Main
begin
-subsection {* The upper and lower bounds operators *}
+subsection {* The upper and lower bounds operators *}
lemma aboveS_subset_above: "aboveS r a \<le> above r a"
by(auto simp add: aboveS_def above_def)
@@ -572,7 +572,7 @@
qed
-subsection {* Properties depending on more than one relation *}
+subsection {* Properties depending on more than one relation *}
lemma under_incr2:
"r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Wed Jan 22 10:13:40 2014 +0100
@@ -589,7 +589,6 @@
qed
qed
-
definition oexp where
"oexp = {(f, g) . f \<in> FINFUNC \<and> g \<in> FINFUNC \<and>
((let m = s.max_fun_diff f g in (f m, g m) \<in> r) \<or> f = g)}"
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy Wed Jan 22 10:13:40 2014 +0100
@@ -103,7 +103,7 @@
using one_set_greater[of UNIV UNIV] by auto
-subsection {* Uniqueness of embeddings *}
+subsection {* Uniqueness of embeddings *}
lemma comp_embedS:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Wed Jan 22 10:13:40 2014 +0100
@@ -29,7 +29,7 @@
using TOTALS by auto
-subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
+subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
lemma worec_unique_fixpoint:
assumes ADM: "adm_wo H" and fp: "f = H f"
@@ -60,7 +60,7 @@
qed
-subsubsection{* Properties of minim *}
+subsubsection {* Properties of minim *}
lemma minim_Under:
"\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
@@ -166,7 +166,7 @@
qed
-subsubsection{* Properties of supr *}
+subsubsection {* Properties of supr *}
lemma supr_Above:
assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
@@ -287,7 +287,7 @@
qed
-subsubsection{* Properties of successor *}
+subsubsection {* Properties of successor *}
lemma suc_least:
"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
@@ -454,7 +454,7 @@
by(unfold Union_eq, auto)
-subsubsection{* Other properties *}
+subsubsection {* Other properties *}
lemma Trans_Under_regressive:
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"