# HG changeset patch
# User blanchet
# Date 1390382020 -3600
# Node ID 761e40ce91bc2bb55ec991df548afe94b4ab79a5
# Parent  57c875e488bd60d7c6a78e25d75fdb6f9947d1a9
whitespace tuning

diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- 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)"
diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- 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
diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Cardinals.thy
--- 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
diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Constructions_on_Wellorders.thy
--- 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"
 
diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Fun_More.thy
--- 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"
diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Order_Relation_More.thy
--- 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"
diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- 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)}"
diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Wellorder_Embedding.thy
--- 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''"
diff -r 57c875e488bd -r 761e40ce91bc src/HOL/Cardinals/Wellorder_Relation.thy
--- 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"