# HG changeset patch
# User blanchet
# Date 1390380330 -3600
# Node ID 57c875e488bd60d7c6a78e25d75fdb6f9947d1a9
# Parent  697b41533e1a25965851de5158dabf313749030d
whitespace tuning

diff -r 697b41533e1a -r 57c875e488bd src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Jan 22 09:45:30 2014 +0100
@@ -38,7 +38,7 @@
 
 text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
 order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
-strict order-embedding relation, @{text "<o"}), among all the well-orders on its field.  *}
+strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *}
 
 definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
 where
@@ -115,7 +115,7 @@
 
 text{* We define the cardinal of set to be {\em some} cardinal order on that set.
 We shall prove that this notion is unique up to order isomorphism, meaning
-that order isomorphism shall be the true identity of cardinals.  *}
+that order isomorphism shall be the true identity of cardinals. *}
 
 definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
 where "card_of A = (SOME r. card_order_on A r)"
@@ -827,7 +827,7 @@
 theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
 does not increase cardinality -- the proof of this fact adapts a standard
 set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
-at page 47 in \cite{card-book}. Then everything else follows fairly easily.  *}
+at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
 
 lemma infinite_iff_card_of_nat:
 "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
@@ -1141,13 +1141,13 @@
 qed
 
 
-subsection {* The cardinal $\omega$ and the finite cardinals  *}
+subsection {* The cardinal $\omega$ and the finite cardinals *}
 
 text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
 order relation on
 @{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals
 shall be the restrictions of these relations to the numbers smaller than
-fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}.  *}
+fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
 
 abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
 abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
@@ -1263,7 +1263,7 @@
 
 text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
 being a successor cardinal of @{text "r"}. Although the definition does
-not require @{text "r"} to be a cardinal, only this case will be meaningful.  *}
+not require @{text "r"} to be a cardinal, only this case will be meaningful. *}
 
 definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
 where
@@ -1314,7 +1314,7 @@
 using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
 
 text{* The minimality property of @{text "cardSuc"} originally present in its definition
-is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}:  *}
+is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}
 
 lemma cardSuc_least_aux:
 "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
diff -r 697b41533e1a -r 57c875e488bd src/HOL/BNF_Constructions_on_Wellorders.thy
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Wed Jan 22 09:45:30 2014 +0100
@@ -11,7 +11,6 @@
 imports BNF_Wellorder_Embedding
 begin
 
-
 text {* In this section, we study basic constructions on well-orders, such as restriction to
 a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,
 and bounded square.  We also define between well-orders
@@ -19,59 +18,48 @@
 @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and
 @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).  We study the
 connections between these relations, order filters, and the aforementioned constructions.
-A main result of this section is that @{text "<o"} is well-founded.  *}
+A main result of this section is that @{text "<o"} is well-founded. *}
 
 
-subsection {* Restriction to a set  *}
-
+subsection {* Restriction to a set *}
 
 abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel"
 where "Restr r A \<equiv> r Int (A \<times> A)"
 
-
 lemma Restr_subset:
 "A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"
 by blast
 
-
 lemma Restr_Field: "Restr r (Field r) = r"
 unfolding Field_def by auto
 
-
 lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
 unfolding refl_on_def Field_def by auto
 
-
 lemma antisym_Restr:
 "antisym r \<Longrightarrow> antisym(Restr r A)"
 unfolding antisym_def Field_def by auto
 
-
 lemma Total_Restr:
 "Total r \<Longrightarrow> Total(Restr r A)"
 unfolding total_on_def Field_def by auto
 
-
 lemma trans_Restr:
 "trans r \<Longrightarrow> trans(Restr r A)"
 unfolding trans_def Field_def by blast
 
-
 lemma Preorder_Restr:
 "Preorder r \<Longrightarrow> Preorder(Restr r A)"
 unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)
 
-
 lemma Partial_order_Restr:
 "Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
 unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)
 
-
 lemma Linear_order_Restr:
 "Linear_order r \<Longrightarrow> Linear_order(Restr r A)"
 unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)
 
-
 lemma Well_order_Restr:
 assumes "Well_order r"
 shows "Well_order(Restr r A)"
@@ -83,21 +71,17 @@
   by (simp add: Linear_order_Restr)
 qed
 
-
 lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
 by (auto simp add: Field_def)
 
-
 lemma Refl_Field_Restr:
 "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
 unfolding refl_on_def Field_def by blast
 
-
 lemma Refl_Field_Restr2:
 "\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
 by (auto simp add: Refl_Field_Restr)
 
-
 lemma well_order_on_Restr:
 assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
 shows "well_order_on A (Restr r A)"
@@ -106,14 +90,12 @@
      order_on_defs[of "Field r" r] by auto
 
 
-subsection {* Order filters versus restrictions and embeddings  *}
-
+subsection {* Order filters versus restrictions and embeddings *}
 
 lemma Field_Restr_ofilter:
 "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
 by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2)
 
-
 lemma ofilter_Restr_under:
 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
 shows "under (Restr r A) a = under r a"
@@ -125,7 +107,6 @@
   thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
 qed
 
-
 lemma ofilter_embed:
 assumes "Well_order r"
 shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"
@@ -159,7 +140,6 @@
   thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)
 qed
 
-
 lemma ofilter_Restr_Int:
 assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A"
 shows "wo_rel.ofilter (Restr r B) (A Int B)"
@@ -183,7 +163,6 @@
   qed
 qed
 
-
 lemma ofilter_Restr_subset:
 assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B"
 shows "wo_rel.ofilter (Restr r B) A"
@@ -192,7 +171,6 @@
   thus ?thesis using assms ofilter_Restr_Int[of r A B] by auto
 qed
 
-
 lemma ofilter_subset_embed:
 assumes WELL: "Well_order r" and
         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
@@ -231,7 +209,6 @@
   qed
 qed
 
-
 lemma ofilter_subset_embedS_iso:
 assumes WELL: "Well_order r" and
         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
@@ -255,14 +232,12 @@
         FieldA FieldB bij_betw_id_iff[of A B] by auto
 qed
 
-
 lemma ofilter_subset_embedS:
 assumes WELL: "Well_order r" and
         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
 shows "(A < B) = embedS (Restr r A) (Restr r B) id"
 using assms by (simp add: ofilter_subset_embedS_iso)
 
-
 lemma embed_implies_iso_Restr:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r' r f"
@@ -288,13 +263,11 @@
 
 subsection {* The strict inclusion on proper ofilters is well-founded *}
 
-
 definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel"
 where
 "ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and>
                          wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}"
 
-
 lemma wf_ofilterIncl:
 assumes WELL: "Well_order r"
 shows "wf(ofilterIncl r)"
@@ -329,10 +302,8 @@
 qed
 
 
-
 subsection {* Ordering the well-orders by existence of embeddings *}
 
-
 text {* We define three relations between well-orders:
 \begin{itemize}
 \item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"});
@@ -345,20 +316,16 @@
 @{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set.
 *}
 
-
 definition ordLeq :: "('a rel * 'a' rel) set"
 where
 "ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}"
 
-
 abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50)
 where "r <=o r' \<equiv> (r,r') \<in> ordLeq"
 
-
 abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50)
 where "r \<le>o r' \<equiv> r <=o r'"
 
-
 definition ordLess :: "('a rel * 'a' rel) set"
 where
 "ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"
@@ -366,7 +333,6 @@
 abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
 where "r <o r' \<equiv> (r,r') \<in> ordLess"
 
-
 definition ordIso :: "('a rel * 'a' rel) set"
 where
 "ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"
@@ -374,7 +340,6 @@
 abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
 where "r =o r' \<equiv> (r,r') \<in> ordIso"
 
-
 lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def
 
 lemma ordLeq_Well_order_simp:
@@ -382,18 +347,15 @@
 shows "Well_order r \<and> Well_order r'"
 using assms unfolding ordLeq_def by simp
 
-
 text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
 on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
 restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,
-to @{text "'a rel rel"}.  *}
-
+to @{text "'a rel rel"}. *}
 
 lemma ordLeq_reflexive:
 "Well_order r \<Longrightarrow> r \<le>o r"
 unfolding ordLeq_def using id_embed[of r] by blast
 
-
 lemma ordLeq_transitive[trans]:
 assumes *: "r \<le>o r'" and **: "r' \<le>o r''"
 shows "r \<le>o r''"
@@ -407,17 +369,14 @@
   thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto
 qed
 
-
 lemma ordLeq_total:
 "\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r"
 unfolding ordLeq_def using wellorders_totally_ordered by blast
 
-
 lemma ordIso_reflexive:
 "Well_order r \<Longrightarrow> r =o r"
 unfolding ordIso_def using id_iso[of r] by blast
 
-
 lemma ordIso_transitive[trans]:
 assumes *: "r =o r'" and **: "r' =o r''"
 shows "r =o r''"
@@ -431,7 +390,6 @@
   thus "r =o r''" unfolding ordIso_def using 1 by auto
 qed
 
-
 lemma ordIso_symmetric:
 assumes *: "r =o r'"
 shows "r' =o r"
@@ -445,7 +403,6 @@
   thus "r' =o r" unfolding ordIso_def using 1 by (auto simp add: iso_def)
 qed
 
-
 lemma ordLeq_ordLess_trans[trans]:
 assumes "r \<le>o r'" and " r' <o r''"
 shows "r <o r''"
@@ -456,7 +413,6 @@
   using embed_comp_embedS by blast
 qed
 
-
 lemma ordLess_ordLeq_trans[trans]:
 assumes "r <o r'" and " r' \<le>o r''"
 shows "r <o r''"
@@ -467,7 +423,6 @@
   using embedS_comp_embed by blast
 qed
 
-
 lemma ordLeq_ordIso_trans[trans]:
 assumes "r \<le>o r'" and " r' =o r''"
 shows "r \<le>o r''"
@@ -478,7 +433,6 @@
   using embed_comp_iso by blast
 qed
 
-
 lemma ordIso_ordLeq_trans[trans]:
 assumes "r =o r'" and " r' \<le>o r''"
 shows "r \<le>o r''"
@@ -489,7 +443,6 @@
   using iso_comp_embed by blast
 qed
 
-
 lemma ordLess_ordIso_trans[trans]:
 assumes "r <o r'" and " r' =o r''"
 shows "r <o r''"
@@ -500,7 +453,6 @@
   using embedS_comp_iso by blast
 qed
 
-
 lemma ordIso_ordLess_trans[trans]:
 assumes "r =o r'" and " r' <o r''"
 shows "r <o r''"
@@ -511,7 +463,6 @@
   using iso_comp_embedS by blast
 qed
 
-
 lemma ordLess_not_embed:
 assumes "r <o r'"
 shows "\<not>(\<exists>f'. embed r' r f')"
@@ -527,7 +478,6 @@
   thus ?thesis by blast
 qed
 
-
 lemma ordLess_Field:
 assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f"
 shows "\<not> (f`(Field r1) = Field r2)"
@@ -546,7 +496,6 @@
   ultimately show ?thesis by (simp add: bij_betw_def)
 qed
 
-
 lemma ordLess_iff:
 "r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))"
 proof
@@ -568,7 +517,6 @@
   unfolding ordLess_def using * by (fastforce simp add: embedS_def)
 qed
 
-
 lemma ordLess_irreflexive: "\<not> r <o r"
 proof
   assume "r <o r"
@@ -578,12 +526,10 @@
   ultimately show False by blast
 qed
 
-
 lemma ordLeq_iff_ordLess_or_ordIso:
 "r \<le>o r' = (r <o r' \<or> r =o r')"
 unfolding ordRels_def embedS_defs iso_defs by blast
 
-
 lemma ordIso_iff_ordLeq:
 "(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"
 proof
@@ -604,12 +550,10 @@
   thus "r =o r'" unfolding ordIso_def using 1 by auto
 qed
 
-
 lemma not_ordLess_ordLeq:
 "r <o r' \<Longrightarrow> \<not> r' \<le>o r"
 using ordLess_ordLeq_trans ordLess_irreflexive by blast
 
-
 lemma ordLess_or_ordLeq:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "r <o r' \<or> r' \<le>o r"
@@ -624,46 +568,37 @@
   ultimately show ?thesis by blast
 qed
 
-
 lemma not_ordLess_ordIso:
 "r <o r' \<Longrightarrow> \<not> r =o r'"
 using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
 
-
 lemma not_ordLeq_iff_ordLess:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "(\<not> r' \<le>o r) = (r <o r')"
 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
 
-
 lemma not_ordLess_iff_ordLeq:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "(\<not> r' <o r) = (r \<le>o r')"
 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
 
-
 lemma ordLess_transitive[trans]:
 "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
 using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
 
-
 corollary ordLess_trans: "trans ordLess"
 unfolding trans_def using ordLess_transitive by blast
 
-
 lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric
 
-
 lemma ordIso_imp_ordLeq:
 "r =o r' \<Longrightarrow> r \<le>o r'"
 using ordIso_iff_ordLeq by blast
 
-
 lemma ordLess_imp_ordLeq:
 "r <o r' \<Longrightarrow> r \<le>o r'"
 using ordLeq_iff_ordLess_or_ordIso by blast
 
-
 lemma ofilter_subset_ordLeq:
 assumes WELL: "Well_order r" and
         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
@@ -687,7 +622,6 @@
   wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast
 qed
 
-
 lemma ofilter_subset_ordLess:
 assumes WELL: "Well_order r" and
         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
@@ -705,13 +639,11 @@
   finally show ?thesis .
 qed
 
-
 lemma ofilter_ordLess:
 "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> (A < Field r) = (Restr r A <o r)"
 by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter
     wo_rel_def Restr_Field)
 
-
 corollary underS_Restr_ordLess:
 assumes "Well_order r" and "Field r \<noteq> {}"
 shows "Restr r (underS r a) <o r"
@@ -722,7 +654,6 @@
   by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
 qed
 
-
 lemma embed_ordLess_ofilterIncl:
 assumes
   OL12: "r1 <o r2" and OL23: "r2 <o r3" and
@@ -769,7 +700,6 @@
   unfolding ofilterIncl_def by auto
 qed
 
-
 lemma ordLess_iff_ordIso_Restr:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
@@ -795,7 +725,6 @@
   thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto
 qed
 
-
 lemma internalize_ordLess:
 "(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)"
 proof
@@ -816,7 +745,6 @@
   thus "r' <o r" using ordIso_ordLess_trans by blast
 qed
 
-
 lemma internalize_ordLeq:
 "(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)"
 proof
@@ -837,7 +765,6 @@
   thus "r' \<le>o r" using ordIso_ordLeq_trans by blast
 qed
 
-
 lemma ordLeq_iff_ordLess_Restr:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
@@ -858,7 +785,6 @@
   thus "r \<le>o r'" using ordLess_or_ordLeq assms by blast
 qed
 
-
 lemma finite_ordLess_infinite:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
@@ -872,7 +798,6 @@
   thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
 qed
 
-
 lemma finite_well_order_on_ordIso:
 assumes FIN: "finite A" and
         WELL: "well_order_on A r" and WELL': "well_order_on A r'"
@@ -897,21 +822,17 @@
   ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis
 qed
 
-
 subsection{* @{text "<o"} is well-founded *}
 
-
 text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded
 on the restricted type @{text "'a rel rel"}.  We prove this by first showing that, for any set
 of well-orders all embedded in a fixed well-order, the function mapping each well-order
 in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus
 {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded. *}
 
-
 definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"
 where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)"
 
-
 lemma ord_to_filter_compat:
 "compat (ordLess Int (ordLess^-1``{r0} \<times> ordLess^-1``{r0}))
         (ofilterIncl r0)
@@ -929,7 +850,6 @@
   using * ** by (simp add: embed_ordLess_ofilterIncl)
 qed
 
-
 theorem wf_ordLess: "wf ordLess"
 proof-
   {fix r0 :: "('a \<times> 'a) set"
@@ -963,30 +883,24 @@
 qed
 
 
-
-subsection {* Copy via direct images  *}
-
+subsection {* Copy via direct images *}
 
 text{* The direct image operator is the dual of the inverse image operator @{text "inv_image"}
 from @{text "Relation.thy"}.  It is useful for transporting a well-order between
 different types. *}
 
-
 definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"
 where
 "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
 
-
 lemma dir_image_Field:
 "Field(dir_image r f) \<le> f ` (Field r)"
 unfolding dir_image_def Field_def by auto
 
-
 lemma dir_image_minus_Id:
 "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
 unfolding inj_on_def Field_def dir_image_def by auto
 
-
 lemma Refl_dir_image:
 assumes "Refl r"
 shows "Refl(dir_image r f)"
@@ -1004,7 +918,6 @@
   by(unfold refl_on_def Field_def Domain_def Range_def, auto)
 qed
 
-
 lemma trans_dir_image:
 assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"
 shows "trans(dir_image r f)"
@@ -1022,12 +935,10 @@
   unfolding dir_image_def using 1 by auto
 qed
 
-
 lemma Preorder_dir_image:
 "\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)"
 by (simp add: preorder_on_def Refl_dir_image trans_dir_image)
 
-
 lemma antisym_dir_image:
 assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
 shows "antisym(dir_image r f)"
@@ -1043,12 +954,10 @@
   thus "a' = b'" using 1 by auto
 qed
 
-
 lemma Partial_order_dir_image:
 "\<lbrakk>Partial_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Partial_order (dir_image r f)"
 by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image)
 
-
 lemma Total_dir_image:
 assumes TOT: "Total r" and INJ: "inj_on f (Field r)"
 shows "Total(dir_image r f)"
@@ -1064,12 +973,10 @@
   using 1 unfolding dir_image_def by auto
 qed
 
-
 lemma Linear_order_dir_image:
 "\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)"
 by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image)
 
-
 lemma wf_dir_image:
 assumes WF: "wf r" and INJ: "inj_on f (Field r)"
 shows "wf(dir_image r f)"
@@ -1095,7 +1002,6 @@
   using A_def 1 by blast
 qed
 
-
 lemma Well_order_dir_image:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
 using assms unfolding well_order_on_def
@@ -1104,33 +1010,27 @@
   subset_inj_on[of f "Field r" "Field(r - Id)"]
   mono_Field[of "r - Id" r] by auto
 
-
 lemma dir_image_Field2:
 "Refl r \<Longrightarrow> Field(dir_image r f) = f ` (Field r)"
 unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast
 
-
 lemma dir_image_bij_betw:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
 unfolding bij_betw_def
 by (simp add: dir_image_Field2 order_on_defs)
 
-
 lemma dir_image_compat:
 "compat r (dir_image r f) f"
 unfolding compat_def dir_image_def by auto
 
-
 lemma dir_image_iso:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> iso r (dir_image r f) f"
 using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast
 
-
 lemma dir_image_ordIso:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> r =o dir_image r f"
 unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast
 
-
 lemma Well_order_iso_copy:
 assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'"
 shows "\<exists>r'. well_order_on A' r' \<and> r =o r'"
@@ -1149,9 +1049,7 @@
 qed
 
 
-
-subsection {* Bounded square  *}
-
+subsection {* Bounded square *}
 
 text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic
 order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the
@@ -1168,7 +1066,6 @@
 construction) is that any proper order filter of the product order is included in a rectangle, i.e.,
 in a product of proper filters on the original relation (assumed to be a well-order). *}
 
-
 definition bsqr :: "'a rel => ('a * 'a)rel"
 where
 "bsqr r = {((a1,a2),(b1,b2)).
@@ -1179,7 +1076,6 @@
             wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1  \<and> (a2,b2) \<in> r - Id
            )}"
 
-
 lemma Field_bsqr:
 "Field (bsqr r) = Field r \<times> Field r"
 proof
@@ -1202,11 +1098,9 @@
   qed
 qed
 
-
 lemma bsqr_Refl: "Refl(bsqr r)"
 by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
 
-
 lemma bsqr_Trans:
 assumes "Well_order r"
 shows "trans (bsqr r)"
@@ -1296,7 +1190,6 @@
   qed
 qed
 
-
 lemma bsqr_antisym:
 assumes "Well_order r"
 shows "antisym (bsqr r)"
@@ -1367,7 +1260,6 @@
   qed
 qed
 
-
 lemma bsqr_Total:
 assumes "Well_order r"
 shows "Total(bsqr r)"
@@ -1485,14 +1377,12 @@
   thus ?thesis unfolding total_on_def by fast
 qed
 
-
 lemma bsqr_Linear_order:
 assumes "Well_order r"
 shows "Linear_order(bsqr r)"
 unfolding order_on_defs
 using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast
 
-
 lemma bsqr_Well_order:
 assumes "Well_order r"
 shows "Well_order(bsqr r)"
@@ -1557,7 +1447,6 @@
   ultimately show "\<exists>d \<in> D. \<forall>d' \<in> D. (d,d') \<in> bsqr r" by fastforce
 qed
 
-
 lemma bsqr_max2:
 assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \<in> bsqr r"
 shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
@@ -1572,7 +1461,6 @@
   ultimately show ?thesis using WELL unfolding order_on_defs refl_on_def by auto
 qed
 
-
 lemma bsqr_ofilter:
 assumes WELL: "Well_order r" and
         OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
diff -r 697b41533e1a -r 57c875e488bd src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Wed Jan 22 09:45:30 2014 +0100
@@ -11,7 +11,6 @@
 imports Zorn BNF_Wellorder_Relation
 begin
 
-
 text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
 prove their basic properties.  The notion of embedding is considered from the point
 of view of the theory of ordinals, and therefore requires the source to be injected
@@ -36,7 +35,6 @@
   by (auto simp add: inj_on_UNION_chain)
 qed
 
-
 lemma under_underS_bij_betw:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
@@ -57,10 +55,8 @@
 qed
 
 
-
 subsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
-functions  *}
-
+functions *}
 
 text{* Standardly, a function is an embedding of a well-order in another if it injectively and
 order-compatibly maps the former into an order filter of the latter.
@@ -70,40 +66,32 @@
 and the set of strict lower bounds of its image.  (Later we prove equivalence with
 the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.)
 A {\em strict embedding} (operator @{text "embedS"})  is a non-bijective embedding
-and an isomorphism (operator @{text "iso"}) is a bijective embedding.   *}
-
+and an isomorphism (operator @{text "iso"}) is a bijective embedding. *}
 
 definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
 where
 "embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
 
-
 lemmas embed_defs = embed_def embed_def[abs_def]
 
-
 text {* Strict embeddings: *}
 
 definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
 where
 "embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')"
 
-
 lemmas embedS_defs = embedS_def embedS_def[abs_def]
 
-
 definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
 where
 "iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')"
 
-
 lemmas iso_defs = iso_def iso_def[abs_def]
 
-
 definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
 where
 "compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'"
 
-
 lemma compat_wf:
 assumes CMP: "compat r r' f" and WF: "wf r'"
 shows "wf r"
@@ -115,15 +103,12 @@
   using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto
 qed
 
-
 lemma id_embed: "embed r r id"
 by(auto simp add: id_def embed_def bij_betw_def)
 
-
 lemma id_iso: "iso r r id"
 by(auto simp add: id_def embed_def iso_def bij_betw_def)
 
-
 lemma embed_in_Field:
 assumes WELL: "Well_order r" and
         EMB: "embed r r' f" and IN: "a \<in> Field r"
@@ -140,7 +125,6 @@
   by (auto simp: under_def)
 qed
 
-
 lemma comp_embed:
 assumes WELL: "Well_order r" and
         EMB: "embed r r' f" and EMB': "embed r' r'' f'"
@@ -160,7 +144,6 @@
   by(auto simp add: bij_betw_trans)
 qed
 
-
 lemma comp_iso:
 assumes WELL: "Well_order r" and
         EMB: "iso r r' f" and EMB': "iso r' r'' f'"
@@ -168,15 +151,12 @@
 using assms unfolding iso_def
 by (auto simp add: comp_embed bij_betw_trans)
 
-
-text{* That @{text "embedS"} is also preserved by function composition shall be proved only later.  *}
-
+text{* That @{text "embedS"} is also preserved by function composition shall be proved only later. *}
 
 lemma embed_Field:
 "\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f`(Field r) \<le> Field r'"
 by (auto simp add: embed_in_Field)
 
-
 lemma embed_preserves_ofilter:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
@@ -204,7 +184,6 @@
   qed
 qed
 
-
 lemma embed_Field_ofilter:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f"
@@ -216,7 +195,6 @@
   show ?thesis by (auto simp add: embed_preserves_ofilter)
 qed
 
-
 lemma embed_compat:
 assumes EMB: "embed r r' f"
 shows "compat r r' f"
@@ -234,7 +212,6 @@
   by (auto simp add: under_def)
 qed
 
-
 lemma embed_inj_on:
 assumes WELL: "Well_order r" and EMB: "embed r r' f"
 shows "inj_on f (Field r)"
@@ -271,7 +248,6 @@
   by (auto simp add: total_on_def)
 qed
 
-
 lemma embed_underS:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f" and IN: "a \<in> Field r"
@@ -293,7 +269,6 @@
   by (auto simp add: notIn_Un_bij_betw3)
 qed
 
-
 lemma embed_iff_compat_inj_on_ofilter:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f`(Field r)))"
@@ -366,7 +341,6 @@
   qed
 qed
 
-
 lemma inv_into_ofilter_embed:
 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
         BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
@@ -442,7 +416,6 @@
   thus ?thesis unfolding embed_def .
 qed
 
-
 lemma inv_into_underS_embed:
 assumes WELL: "Well_order r" and
         BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
@@ -452,7 +425,6 @@
 using assms
 by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
 
-
 lemma inv_into_Field_embed:
 assumes WELL: "Well_order r" and EMB: "embed r r' f" and
         IMAGE: "Field r' \<le> f ` (Field r)"
@@ -468,7 +440,6 @@
   by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
 qed
 
-
 lemma inv_into_Field_embed_bij_betw:
 assumes WELL: "Well_order r" and
         EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"
@@ -481,12 +452,8 @@
 qed
 
 
-
-
-
 subsection {* Given any two well-orders, one can be embedded in the other *}
 
-
 text{* Here is an overview of the proof of of this fact, stated in theorem
 @{text "wellorders_totally_ordered"}:
 
@@ -506,7 +473,6 @@
    (lemma @{text "wellorders_totally_ordered_aux2"}).
 *}
 
-
 lemma wellorders_totally_ordered_aux:
 fixes r ::"'a rel"  and r'::"'a' rel" and
       f :: "'a \<Rightarrow> 'a'" and a::'a
@@ -616,7 +582,6 @@
   using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
 qed
 
-
 lemma wellorders_totally_ordered_aux2:
 fixes r ::"'a rel"  and r'::"'a' rel" and
       f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a
@@ -696,7 +661,6 @@
   unfolding embed_def by blast
 qed
 
-
 theorem wellorders_totally_ordered:
 fixes r ::"'a rel"  and r'::"'a' rel"
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
@@ -805,15 +769,13 @@
 qed
 
 
-subsection {* Uniqueness of embeddings  *}
-
+subsection {* Uniqueness of embeddings *}
 
 text{* Here we show a fact complementary to the one from the previous subsection -- namely,
 that between any two well-orders there is {\em at most} one embedding, and is the one
 definable by the expected well-order recursive equation.  As a consequence, any two
 embeddings of opposite directions are mutually inverse. *}
 
-
 lemma embed_determined:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f" and IN: "a \<in> Field r"
@@ -832,7 +794,6 @@
   ultimately show ?thesis by simp
 qed
 
-
 lemma embed_unique:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMBf: "embed r r' f" and EMBg: "embed r r' g"
@@ -848,7 +809,6 @@
   using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
 qed
 
-
 lemma embed_bothWays_inverse:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f" and EMB': "embed r' r f'"
@@ -871,7 +831,6 @@
   ultimately show ?thesis by blast
 qed
 
-
 lemma embed_bothWays_bij_betw:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f" and EMB': "embed r' r g"
@@ -899,7 +858,6 @@
   qed
 qed
 
-
 lemma embed_bothWays_iso:
 assumes WELL: "Well_order r"  and WELL': "Well_order r'" and
         EMB: "embed r r' f" and EMB': "embed r' r g"
@@ -907,8 +865,7 @@
 unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
 
 
-subsection {* More properties of embeddings, strict embeddings and isomorphisms  *}
-
+subsection {* More properties of embeddings, strict embeddings and isomorphisms *}
 
 lemma embed_bothWays_Field_bij_betw:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
@@ -924,7 +881,6 @@
   show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
 qed
 
-
 lemma embedS_comp_embed:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
         and  EMB: "embedS r r' f" and EMB': "embed r' r'' f'"
@@ -948,7 +904,6 @@
   ultimately show ?thesis unfolding embedS_def by auto
 qed
 
-
 lemma embed_comp_embedS:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
         and  EMB: "embed r r' f" and EMB': "embedS r' r'' f'"
@@ -972,7 +927,6 @@
   ultimately show ?thesis unfolding embedS_def by auto
 qed
 
-
 lemma embed_comp_iso:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
         and  EMB: "embed r r' f" and EMB': "iso r' r'' f'"
@@ -980,7 +934,6 @@
 using assms unfolding iso_def
 by (auto simp add: comp_embed)
 
-
 lemma iso_comp_embed:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
         and  EMB: "iso r r' f" and EMB': "embed r' r'' f'"
@@ -988,7 +941,6 @@
 using assms unfolding iso_def
 by (auto simp add: comp_embed)
 
-
 lemma embedS_comp_iso:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
         and  EMB: "embedS r r' f" and EMB': "iso r' r'' f'"
@@ -996,7 +948,6 @@
 using assms unfolding iso_def
 by (auto simp add: embedS_comp_embed)
 
-
 lemma iso_comp_embedS:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
         and  EMB: "iso r r' f" and EMB': "embedS r' r'' f'"
@@ -1004,7 +955,6 @@
 using assms unfolding iso_def  using embed_comp_embedS
 by (auto simp add: embed_comp_embedS)
 
-
 lemma embedS_Field:
 assumes WELL: "Well_order r" and EMB: "embedS r r' f"
 shows "f ` (Field r) < Field r'"
@@ -1020,7 +970,6 @@
   ultimately show ?thesis by blast
 qed
 
-
 lemma embedS_iff:
 assumes WELL: "Well_order r" and ISO: "embed r r' f"
 shows "embedS r r' f = (f ` (Field r) < Field r')"
@@ -1036,12 +985,10 @@
   using ISO by auto
 qed
 
-
 lemma iso_Field:
 "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
 using assms by (auto simp add: iso_def bij_betw_def)
 
-
 lemma iso_iff:
 assumes "Well_order r"
 shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')"
@@ -1057,7 +1004,6 @@
   with * show "iso r r' f" unfolding iso_def by auto
 qed
 
-
 lemma iso_iff2:
 assumes "Well_order r"
 shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
@@ -1110,7 +1056,6 @@
   thus "embed r r' f" unfolding embed_def using * by auto
 qed
 
-
 lemma iso_iff3:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)"
@@ -1140,6 +1085,4 @@
   qed
 qed
 
-
-
 end
diff -r 697b41533e1a -r 57c875e488bd src/HOL/BNF_Wellorder_Relation.thy
--- a/src/HOL/BNF_Wellorder_Relation.thy	Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Relation.thy	Wed Jan 22 09:45:30 2014 +0100
@@ -11,13 +11,11 @@
 imports Order_Relation
 begin
 
-
 text{* In this section, we develop basic concepts and results pertaining
 to well-order relations.  Note that we consider well-order relations
 as {\em non-strict relations},
 i.e., as containing the diagonals of their fields. *}
 
-
 locale wo_rel =
   fixes r :: "'a rel"
   assumes WELL: "Well_order r"
@@ -40,49 +38,39 @@
 
 subsection {* Auxiliaries *}
 
-
 lemma REFL: "Refl r"
 using WELL order_on_defs[of _ r] by auto
 
-
 lemma TRANS: "trans r"
 using WELL order_on_defs[of _ r] by auto
 
-
 lemma ANTISYM: "antisym r"
 using WELL order_on_defs[of _ r] by auto
 
-
 lemma TOTAL: "Total r"
 using WELL order_on_defs[of _ r] by auto
 
-
 lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
 using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
 
-
 lemma LIN: "Linear_order r"
 using WELL well_order_on_def[of _ r] by auto
 
-
 lemma WF: "wf (r - Id)"
 using WELL well_order_on_def[of _ r] by auto
 
-
 lemma cases_Total:
 "\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk>
              \<Longrightarrow> phi a b"
 using TOTALS by auto
 
-
 lemma cases_Total3:
 "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (b,a) \<in> r - Id \<Longrightarrow> phi a b);
               (a = b \<Longrightarrow> phi a b)\<rbrakk>  \<Longrightarrow> phi a b"
 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 *}
 
 text{* Here we provide induction and recursion principles specific to {\em non-strict}
 well-order relations.
@@ -90,7 +78,6 @@
 for doing away with the tediousness of
 having to take out the diagonal each time in order to switch to a well-founded relation. *}
 
-
 lemma well_order_induct:
 assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
 shows "P a"
@@ -100,19 +87,16 @@
   thus "P a" using WF wf_induct[of "r - Id" P a] by blast
 qed
 
-
 definition
 worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
 "worec F \<equiv> wfrec (r - Id) F"
 
-
 definition
 adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
 where
 "adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
 
-
 lemma worec_fixpoint:
 assumes ADM: "adm_wo H"
 shows "worec H = H (worec H)"
@@ -127,8 +111,7 @@
 qed
 
 
-subsection {* The notions of maximum, minimum, supremum, successor and order filter  *}
-
+subsection {* The notions of maximum, minimum, supremum, successor and order filter *}
 
 text{*
 We define the successor {\em of a set}, and not of an element (the latter is of course
@@ -141,18 +124,15 @@
 meaningful for sets for which strict upper bounds exist.
 Order filters for well-orders are also known as ``initial segments". *}
 
-
 definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
 
-
 definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
 where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
 
 definition minim :: "'a set \<Rightarrow> 'a"
 where "minim A \<equiv> THE b. isMinim A b"
 
-
 definition supr :: "'a set \<Rightarrow> 'a"
 where "supr A \<equiv> minim (Above A)"
 
@@ -166,7 +146,6 @@
 
 subsubsection {* Properties of max2 *}
 
-
 lemma max2_greater_among:
 assumes "a \<in> Field r" and "b \<in> Field r"
 shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
@@ -191,26 +170,22 @@
   total_on_def[of "Field r" r] by blast
 qed
 
-
 lemma max2_greater:
 assumes "a \<in> Field r" and "b \<in> Field r"
 shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
 using assms by (auto simp add: max2_greater_among)
 
-
 lemma max2_among:
 assumes "a \<in> Field r" and "b \<in> Field r"
 shows "max2 a b \<in> {a, b}"
 using assms max2_greater_among[of a b] by simp
 
-
 lemma max2_equals1:
 assumes "a \<in> Field r" and "b \<in> Field r"
 shows "(max2 a b = a) = ((b,a) \<in> r)"
 using assms ANTISYM unfolding antisym_def using TOTALS
 by(auto simp add: max2_def max2_among)
 
-
 lemma max2_equals2:
 assumes "a \<in> Field r" and "b \<in> Field r"
 shows "(max2 a b = b) = ((a,b) \<in> r)"
@@ -220,7 +195,6 @@
 
 subsubsection {* Existence and uniqueness for isMinim and well-definedness of minim *}
 
-
 lemma isMinim_unique:
 assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
 shows "a = a'"
@@ -240,7 +214,6 @@
   show ?thesis using ANTISYM antisym_def[of r] by blast
 qed
 
-
 lemma Well_order_isMinim_exists:
 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
 shows "\<exists>b. isMinim B b"
@@ -269,7 +242,6 @@
   qed
 qed
 
-
 lemma minim_isMinim:
 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
 shows "isMinim B (minim B)"
@@ -284,10 +256,8 @@
   unfolding minim_def using theI[of ?phi b] by blast
 qed
 
-
 subsubsection{* Properties of minim *}
 
-
 lemma minim_in:
 assumes "B \<le> Field r" and "B \<noteq> {}"
 shows "minim B \<in> B"
@@ -297,7 +267,6 @@
   thus ?thesis by (simp add: isMinim_def)
 qed
 
-
 lemma minim_inField:
 assumes "B \<le> Field r" and "B \<noteq> {}"
 shows "minim B \<in> Field r"
@@ -306,7 +275,6 @@
   thus ?thesis using assms by blast
 qed
 
-
 lemma minim_least:
 assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
 shows "(minim B, b) \<in> r"
@@ -316,7 +284,6 @@
   thus ?thesis by (auto simp add: isMinim_def IN)
 qed
 
-
 lemma equals_minim:
 assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
         LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
@@ -329,10 +296,8 @@
   using isMinim_unique by auto
 qed
 
-
 subsubsection{* Properties of successor *}
 
-
 lemma suc_AboveS:
 assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
 shows "suc B \<in> AboveS B"
@@ -343,7 +308,6 @@
   using assms by (simp add: minim_in)
 qed
 
-
 lemma suc_greater:
 assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
         IN: "b \<in> B"
@@ -354,7 +318,6 @@
   with IN AboveS_def[of r] show ?thesis by simp
 qed
 
-
 lemma suc_least_AboveS:
 assumes ABOVES: "a \<in> AboveS B"
 shows "(suc B,a) \<in> r"
@@ -365,7 +328,6 @@
   using assms minim_least by simp
 qed
 
-
 lemma suc_inField:
 assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
 shows "suc B \<in> Field r"
@@ -375,7 +337,6 @@
   using assms AboveS_Field[of r] by auto
 qed
 
-
 lemma equals_suc_AboveS:
 assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
         MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
@@ -388,7 +349,6 @@
   by simp
 qed
 
-
 lemma suc_underS:
 assumes IN: "a \<in> Field r"
 shows "a = suc (underS a)"
@@ -432,7 +392,6 @@
 
 subsubsection {* Properties of order filters *}
 
-
 lemma under_ofilter:
 "ofilter (under a)"
 proof(unfold ofilter_def under_def, auto simp add: Field_def)
@@ -442,7 +401,6 @@
   using TRANS trans_def[of r] by blast
 qed
 
-
 lemma underS_ofilter:
 "ofilter (underS a)"
 proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
@@ -456,12 +414,10 @@
   using TRANS trans_def[of r] by blast
 qed
 
-
 lemma Field_ofilter:
 "ofilter (Field r)"
 by(unfold ofilter_def under_def, auto simp add: Field_def)
 
-
 lemma ofilter_underS_Field:
 "ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
 proof
@@ -523,12 +479,10 @@
   qed
 qed
 
-
 lemma ofilter_UNION:
 "(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
 unfolding ofilter_def by blast
 
-
 lemma ofilter_under_UNION:
 assumes "ofilter A"
 shows "A = (\<Union> a \<in> A. under a)"
@@ -542,10 +496,8 @@
   thus "A \<le> (\<Union> a \<in> A. under a)" by blast
 qed
 
-
 subsubsection{* Other properties *}
 
-
 lemma ofilter_linord:
 assumes OF1: "ofilter A" and OF2: "ofilter B"
 shows "A \<le> B \<or> B \<le> A"
@@ -587,7 +539,6 @@
   qed
 qed
 
-
 lemma ofilter_AboveS_Field:
 assumes "ofilter A"
 shows "A \<union> (AboveS A) = Field r"
@@ -614,7 +565,6 @@
   thus "Field r \<le> A \<union> (AboveS A)" by blast
 qed
 
-
 lemma suc_ofilter_in:
 assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
         REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
@@ -633,10 +583,6 @@
   thus ?thesis by blast
 qed
 
-
-
 end (* context wo_rel *)
 
-
-
 end