# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1673650060 0
# Node ID f881fd264929b1c0dfcf54b6460f678ab3691d0f
# Parent  ec4c38e156c703c0920b1dc1c145221e9887c6bb
More cleaning up proofs, plus a TeX fix

diff -r ec4c38e156c7 -r f881fd264929 src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Fri Jan 13 16:44:00 2023 +0000
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Fri Jan 13 22:47:40 2023 +0000
@@ -8,7 +8,7 @@
 section \<open>Constructions on Wellorders as Needed by Bounded Natural Functors\<close>
 
 theory BNF_Wellorder_Constructions
-imports BNF_Wellorder_Embedding
+  imports BNF_Wellorder_Embedding
 begin
 
 text \<open>In this section, we study basic constructions on well-orders, such as restriction to
@@ -70,13 +70,8 @@
 lemma Well_order_Restr:
   assumes "Well_order r"
   shows "Well_order(Restr r A)"
-proof-
-  have "Restr r A - Id \<le> r - Id" using Restr_subset by blast
-  hence "wf(Restr r A - Id)" using assms
-    using well_order_on_def wf_subset by blast
-  thus ?thesis using assms unfolding well_order_on_def
-    by (simp add: Linear_order_Restr)
-qed
+  using assms  
+  by (auto simp: well_order_on_def Linear_order_Restr elim: wf_subset)
 
 lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
   by (auto simp add: Field_def)
@@ -92,7 +87,7 @@
 lemma well_order_on_Restr:
   assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
   shows "well_order_on A (Restr r A)"
-  using assms
+  using assms 
   using Well_order_Restr[of r A] Refl_Field_Restr2[of r A]
     order_on_defs[of "Field r" r] by auto
 
@@ -100,12 +95,12 @@
 subsection \<open>Order filters versus restrictions and embeddings\<close>
 
 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)
+  "\<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"
+  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"
   unfolding wo_rel.ofilter_def under_def
 proof
   show "{b. (b, a) \<in> Restr r A} \<subseteq> {b. (b, a) \<in> r}"
@@ -125,51 +120,51 @@
 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)"
+  assumes "Well_order r"
+  shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"
 proof
   assume *: "wo_rel.ofilter r A"
   show "A \<le> Field r \<and> embed (Restr r A) r id"
-  unfolding embed_def
+    unfolding embed_def
   proof safe
     fix a assume "a \<in> A" thus "a \<in> Field r" using assms *
-    by (auto simp add: wo_rel_def wo_rel.ofilter_def)
+      by (auto simp add: wo_rel_def wo_rel.ofilter_def)
   next
     fix a assume "a \<in> Field (Restr r A)"
     thus "bij_betw id (under (Restr r A) a) (under r (id a))" using assms *
-    by (simp add: ofilter_Restr_under Field_Restr_ofilter)
+      by (simp add: ofilter_Restr_under Field_Restr_ofilter)
   qed
 next
   assume *: "A \<le> Field r \<and> embed (Restr r A) r id"
   hence "Field(Restr r A) \<le> Field r"
-  using assms  embed_Field[of "Restr r A" r id] id_def
-        Well_order_Restr[of r] by auto
+    using assms  embed_Field[of "Restr r A" r id] id_def
+      Well_order_Restr[of r] by auto
   {fix a assume "a \<in> A"
-   hence "a \<in> Field(Restr r A)" using * assms
-   by (simp add: order_on_defs Refl_Field_Restr2)
-   hence "bij_betw id (under (Restr r A) a) (under r a)"
-   using * unfolding embed_def by auto
-   hence "under r a \<le> under (Restr r A) a"
-   unfolding bij_betw_def by auto
-   also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
-   also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
-   finally have "under r a \<le> A" .
+    hence "a \<in> Field(Restr r A)" using * assms
+      by (simp add: order_on_defs Refl_Field_Restr2)
+    hence "bij_betw id (under (Restr r A) a) (under r a)"
+      using * unfolding embed_def by auto
+    hence "under r a \<le> under (Restr r A) a"
+      unfolding bij_betw_def by auto
+    also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
+    also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
+    finally have "under r a \<le> A" .
   }
   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)"
+  assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A"
+  shows "wo_rel.ofilter (Restr r B) (A Int B)"
 proof-
   let ?rB = "Restr r B"
   have Well: "wo_rel r" unfolding wo_rel_def using WELL .
   hence Refl: "Refl r" by (simp add: wo_rel.REFL)
   hence Field: "Field ?rB = Field r Int B"
-  using Refl_Field_Restr by blast
+    using Refl_Field_Restr by blast
   have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
-  by (simp add: Well_order_Restr wo_rel_def)
-  (* Main proof *)
+    by (simp add: Well_order_Restr wo_rel_def)
+      (* Main proof *)
   show ?thesis using WellB assms
     unfolding wo_rel.ofilter_def under_def ofilter_def
   proof safe
@@ -183,84 +178,84 @@
 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"
+  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"
 proof-
   have "A Int B = A" using SUB by blast
   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"
-shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)"
+  assumes WELL: "Well_order r" and
+    OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
+  shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)"
 proof-
   let ?rA = "Restr r A"  let ?rB = "Restr r B"
   have Well: "wo_rel r" unfolding wo_rel_def using WELL .
   hence Refl: "Refl r" by (simp add: wo_rel.REFL)
   hence FieldA: "Field ?rA = Field r Int A"
-  using Refl_Field_Restr by blast
+    using Refl_Field_Restr by blast
   have FieldB: "Field ?rB = Field r Int B"
-  using Refl Refl_Field_Restr by blast
+    using Refl Refl_Field_Restr by blast
   have WellA: "wo_rel ?rA \<and> Well_order ?rA" using WELL
-  by (simp add: Well_order_Restr wo_rel_def)
+    by (simp add: Well_order_Restr wo_rel_def)
   have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
-  by (simp add: Well_order_Restr wo_rel_def)
-  (* Main proof *)
+    by (simp add: Well_order_Restr wo_rel_def)
+      (* Main proof *)
   show ?thesis
   proof
     assume *: "A \<le> B"
     hence "wo_rel.ofilter (Restr r B) A" using assms
-    by (simp add: ofilter_Restr_subset)
+      by (simp add: ofilter_Restr_subset)
     hence "embed (Restr ?rB A) (Restr r B) id"
-    using WellB ofilter_embed[of "?rB" A] by auto
+      using WellB ofilter_embed[of "?rB" A] by auto
     thus "embed (Restr r A) (Restr r B) id"
-    using * by (simp add: Restr_subset)
+      using * by (simp add: Restr_subset)
   next
     assume *: "embed (Restr r A) (Restr r B) id"
     {fix a assume **: "a \<in> A"
-     hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def)
-     with ** FieldA have "a \<in> Field ?rA" by auto
-     hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto
-     hence "a \<in> B" using FieldB by auto
+      hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def)
+      with ** FieldA have "a \<in> Field ?rA" by auto
+      hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto
+      hence "a \<in> B" using FieldB by auto
     }
     thus "A \<le> B" by blast
   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"
-shows "((A < B) = (embedS (Restr r A) (Restr r B) id)) \<and>
+  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)) \<and>
        ((A = B) = (iso (Restr r A) (Restr r B) id))"
 proof-
   let ?rA = "Restr r A"  let ?rB = "Restr r B"
   have Well: "wo_rel r" unfolding wo_rel_def using WELL .
   hence Refl: "Refl r" by (simp add: wo_rel.REFL)
   hence "Field ?rA = Field r Int A"
-  using Refl_Field_Restr by blast
+    using Refl_Field_Restr by blast
   hence FieldA: "Field ?rA = A" using OFA Well
-  by (auto simp add: wo_rel.ofilter_def)
+    by (auto simp add: wo_rel.ofilter_def)
   have "Field ?rB = Field r Int B"
-  using Refl Refl_Field_Restr by blast
+    using Refl Refl_Field_Restr by blast
   hence FieldB: "Field ?rB = B" using OFB Well
-  by (auto simp add: wo_rel.ofilter_def)
-  (* Main proof *)
+    by (auto simp add: wo_rel.ofilter_def)
+      (* Main proof *)
   show ?thesis unfolding embedS_def iso_def
-  using assms ofilter_subset_embed[of r A B]
-        FieldA FieldB bij_betw_id_iff[of A B] by auto
+    using assms ofilter_subset_embed[of r A B]
+      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)
+  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"
-shows "iso r' (Restr r (f ` (Field r'))) f"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    EMB: "embed r' r f"
+  shows "iso r' (Restr r (f ` (Field r'))) f"
 proof-
   let ?A' = "Field r'"
   let ?r'' = "Restr r (f ` ?A')"
@@ -268,13 +263,13 @@
   have 1: "wo_rel.ofilter r (f ` ?A')" using assms embed_Field_ofilter  by blast
   hence "Field ?r'' = f ` (Field r')" using WELL Field_Restr_ofilter by blast
   hence "bij_betw f ?A' (Field ?r'')"
-  using EMB embed_inj_on WELL' unfolding bij_betw_def by blast
+    using EMB embed_inj_on WELL' unfolding bij_betw_def by blast
   moreover
   {have "\<forall>a b. (a,b) \<in> r' \<longrightarrow> a \<in> Field r' \<and> b \<in> Field r'"
-   unfolding Field_def by auto
-   hence "compat r' ?r'' f"
-   using assms embed_iff_compat_inj_on_ofilter
-   unfolding compat_def by blast
+      unfolding Field_def by auto
+    hence "compat r' ?r'' f"
+      using assms embed_iff_compat_inj_on_ofilter
+      unfolding compat_def by blast
   }
   ultimately show ?thesis using WELL' 0 iso_iff3 by blast
 qed
@@ -283,13 +278,13 @@
 subsection \<open>The strict inclusion on proper ofilters is well-founded\<close>
 
 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>
+  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)"
+  assumes WELL: "Well_order r"
+  shows "wf(ofilterIncl r)"
 proof-
   have Well: "wo_rel r" using WELL by (simp add: wo_rel_def)
   hence Lo: "Linear_order r" by (simp add: wo_rel.LIN)
@@ -299,23 +294,23 @@
   moreover
   have "compat (ofilterIncl r) ?rS ?h"
   proof(unfold compat_def ofilterIncl_def,
-        intro allI impI, simp, elim conjE)
+      intro allI impI, simp, elim conjE)
     fix A B
     assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and
-           **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
+      **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
     then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and
-                         1: "A = underS r a \<and> B = underS r b"
-    using Well by (auto simp add: wo_rel.ofilter_underS_Field)
+      1: "A = underS r a \<and> B = underS r b"
+      using Well by (auto simp add: wo_rel.ofilter_underS_Field)
     hence "a \<noteq> b" using *** by auto
     moreover
     have "(a,b) \<in> r" using 0 1 Lo ***
-    by (auto simp add: underS_incl_iff)
+      by (auto simp add: underS_incl_iff)
     moreover
     have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B"
-    using Well 0 1 by (simp add: wo_rel.suc_underS)
+      using Well 0 1 by (simp add: wo_rel.suc_underS)
     ultimately
     show "(wo_rel.suc r A, wo_rel.suc r B) \<in> r \<and> wo_rel.suc r A \<noteq> wo_rel.suc r B"
-    by simp
+      by simp
   qed
   ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf)
 qed
@@ -336,35 +331,35 @@
 \<close>
 
 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)}"
+  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"
+  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'"
+  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)}"
+  where
+    "ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"
 
 abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
-where "r <o r' \<equiv> (r,r') \<in> ordLess"
+  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)}"
+  where
+    "ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"
 
 abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
-where "r =o r' \<equiv> (r,r') \<in> ordIso"
+  where "r =o r' \<equiv> (r,r') \<in> ordIso"
 
 lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def
 
 lemma ordLeq_Well_order_simp:
-assumes "r \<le>o r'"
-shows "Well_order r \<and> Well_order r'"
-using assms unfolding ordLeq_def by simp
+  assumes "r \<le>o r'"
+  shows "Well_order r \<and> Well_order r'"
+  using assms unfolding ordLeq_def by simp
 
 text\<open>Notice that the relations \<open>\<le>o\<close>, \<open><o\<close>, \<open>=o\<close> connect well-orders
 on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
@@ -372,360 +367,313 @@
 to \<open>'a rel rel\<close>.\<close>
 
 lemma ordLeq_reflexive:
-"Well_order r \<Longrightarrow> r \<le>o r"
-unfolding ordLeq_def using id_embed[of r] by blast
+  "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''"
-proof-
-  obtain f and f'
-  where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
-        "embed r r' f" and "embed r' r'' f'"
-  using * ** unfolding ordLeq_def by blast
-  hence "embed r r'' (f' \<circ> f)"
-  using comp_embed[of r r' f r'' f'] by auto
-  thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto
-qed
+  assumes "r \<le>o r'" and "r' \<le>o r''"
+  shows "r \<le>o r''"
+  using assms by (auto simp: ordLeq_def intro: comp_embed)
 
 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
+  "\<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
+  "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''"
-proof-
-  obtain f and f'
-  where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
-        "iso r r' f" and 3: "iso r' r'' f'"
-  using * ** unfolding ordIso_def by auto
-  hence "iso r r'' (f' \<circ> f)"
-  using comp_iso[of r r' f r'' f'] by auto
-  thus "r =o r''" unfolding ordIso_def using 1 by auto
-qed
+  assumes *: "r =o r'" and **: "r' =o r''"
+  shows "r =o r''"
+  using assms by (auto simp: ordIso_def intro: comp_iso)
 
 lemma ordIso_symmetric:
-assumes *: "r =o r'"
-shows "r' =o r"
+  assumes *: "r =o r'"
+  shows "r' =o r"
 proof-
   obtain f where 1: "Well_order r \<and> Well_order r'" and
-                 2: "embed r r' f \<and> bij_betw f (Field r) (Field r')"
-  using * by (auto simp add: ordIso_def iso_def)
+    2: "embed r r' f \<and> bij_betw f (Field r) (Field r')"
+    using * by (auto simp add: ordIso_def iso_def)
   let ?f' = "inv_into (Field r) f"
   have "embed r' r ?f' \<and> bij_betw ?f' (Field r') (Field r)"
-  using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw)
+    using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw)
   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''"
+  assumes "r \<le>o r'" and " r' <o r''"
+  shows "r <o r''"
 proof-
   have "Well_order r \<and> Well_order r''"
-  using assms unfolding ordLeq_def ordLess_def by auto
+    using assms unfolding ordLeq_def ordLess_def by auto
   thus ?thesis using assms unfolding ordLeq_def ordLess_def
-  using embed_comp_embedS by blast
+    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''"
-proof-
-  have "Well_order r \<and> Well_order r''"
-  using assms unfolding ordLeq_def ordLess_def by auto
-  thus ?thesis using assms unfolding ordLeq_def ordLess_def
-  using embedS_comp_embed by blast
-qed
+  assumes "r <o r'" and " r' \<le>o r''"
+  shows "r <o r''"
+  using embedS_comp_embed assms by (force simp: ordLeq_def ordLess_def)
 
 lemma ordLeq_ordIso_trans[trans]:
-assumes "r \<le>o r'" and " r' =o r''"
-shows "r \<le>o r''"
-proof-
-  have "Well_order r \<and> Well_order r''"
-  using assms unfolding ordLeq_def ordIso_def by auto
-  thus ?thesis using assms unfolding ordLeq_def ordIso_def
-  using embed_comp_iso by blast
-qed
+  assumes "r \<le>o r'" and " r' =o r''"
+  shows "r \<le>o r''"
+  using embed_comp_iso assms by (force simp: ordLeq_def ordIso_def)
 
 lemma ordIso_ordLeq_trans[trans]:
-assumes "r =o r'" and " r' \<le>o r''"
-shows "r \<le>o r''"
-proof-
-  have "Well_order r \<and> Well_order r''"
-  using assms unfolding ordLeq_def ordIso_def by auto
-  thus ?thesis using assms unfolding ordLeq_def ordIso_def
-  using iso_comp_embed by blast
-qed
+  assumes "r =o r'" and " r' \<le>o r''"
+  shows "r \<le>o r''"
+  using iso_comp_embed assms by (force simp: ordLeq_def ordIso_def)
 
 lemma ordLess_ordIso_trans[trans]:
-assumes "r <o r'" and " r' =o r''"
-shows "r <o r''"
-proof-
-  have "Well_order r \<and> Well_order r''"
-  using assms unfolding ordLess_def ordIso_def by auto
-  thus ?thesis using assms unfolding ordLess_def ordIso_def
-  using embedS_comp_iso by blast
-qed
+  assumes "r <o r'" and " r' =o r''"
+  shows "r <o r''"
+  using embedS_comp_iso assms by (force simp: ordLess_def ordIso_def)
 
 lemma ordIso_ordLess_trans[trans]:
-assumes "r =o r'" and " r' <o r''"
-shows "r <o r''"
-proof-
-  have "Well_order r \<and> Well_order r''"
-  using assms unfolding ordLess_def ordIso_def by auto
-  thus ?thesis using assms unfolding ordLess_def ordIso_def
-  using iso_comp_embedS by blast
-qed
+  assumes "r =o r'" and " r' <o r''"
+  shows "r <o r''"
+  using iso_comp_embedS assms by (force simp: ordLess_def ordIso_def)
 
 lemma ordLess_not_embed:
-assumes "r <o r'"
-shows "\<not>(\<exists>f'. embed r' r f')"
+  assumes "r <o r'"
+  shows "\<not>(\<exists>f'. embed r' r f')"
 proof-
   obtain f where 1: "Well_order r \<and> Well_order r'" and 2: "embed r r' f" and
-                 3: " \<not> bij_betw f (Field r) (Field r')"
-  using assms unfolding ordLess_def by (auto simp add: embedS_def)
+    3: " \<not> bij_betw f (Field r) (Field r')"
+    using assms unfolding ordLess_def by (auto simp add: embedS_def)
   {fix f' assume *: "embed r' r f'"
-   hence "bij_betw f (Field r) (Field r')" using 1 2
-   by (simp add: embed_bothWays_Field_bij_betw)
-   with 3 have False by contradiction
+    hence "bij_betw f (Field r) (Field r')" using 1 2
+      by (simp add: embed_bothWays_Field_bij_betw)
+    with 3 have False by contradiction
   }
   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)"
+  assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f"
+  shows "\<not> (f`(Field r1) = Field r2)"
 proof-
   let ?A1 = "Field r1"  let ?A2 = "Field r2"
   obtain g where
-  0: "Well_order r1 \<and> Well_order r2" and
-  1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)"
-  using OL unfolding ordLess_def by (auto simp add: embedS_def)
+    0: "Well_order r1 \<and> Well_order r2" and
+    1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)"
+    using OL unfolding ordLess_def by (auto simp add: embedS_def)
   hence "\<forall>a \<in> ?A1. f a = g a"
-  using 0 EMB embed_unique[of r1] by auto
+    using 0 EMB embed_unique[of r1] by auto
   hence "\<not>(bij_betw f ?A1 ?A2)"
-  using 1 bij_betw_cong[of ?A1] by blast
+    using 1 bij_betw_cong[of ?A1] by blast
   moreover
   have "inj_on f ?A1" using EMB 0 by (simp add: embed_inj_on)
   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'))"
+  "r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))"
 proof
   assume *: "r <o r'"
   hence "\<not>(\<exists>f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp
   with * show "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"
-  unfolding ordLess_def by auto
+    unfolding ordLess_def by auto
 next
   assume *: "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"
   then obtain f where 1: "embed r r' f"
-  using wellorders_totally_ordered[of r r'] by blast
+    using wellorders_totally_ordered[of r r'] by blast
   moreover
   {assume "bij_betw f (Field r) (Field r')"
-   with * 1 have "embed r' r (inv_into (Field r) f) "
-   using inv_into_Field_embed_bij_betw[of r r' f] by auto
-   with * have False by blast
+    with * 1 have "embed r' r (inv_into (Field r) f) "
+      using inv_into_Field_embed_bij_betw[of r r' f] by auto
+    with * have False by blast
   }
   ultimately show "(r,r') \<in> ordLess"
-  unfolding ordLess_def using * by (fastforce simp add: embedS_def)
+    unfolding ordLess_def using * by (fastforce simp add: embedS_def)
 qed
 
 lemma ordLess_irreflexive: "\<not> r <o r"
-proof
-  assume "r <o r"
-  hence "Well_order r \<and>  \<not>(\<exists>f. embed r r f)"
-  unfolding ordLess_iff ..
-  moreover have "embed r r id" using id_embed[of r] .
-  ultimately show False by blast
-qed
+  using id_embed[of r] by (auto simp: ordLess_iff)
 
 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
+  "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)"
+  "(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"
 proof
   assume "r =o r'"
   then obtain f where 1: "Well_order r \<and> Well_order r' \<and>
                      embed r r' f \<and> bij_betw f (Field r) (Field r')"
-  unfolding ordIso_def iso_defs by auto
+    unfolding ordIso_def iso_defs by auto
   hence "embed r r' f \<and> embed r' r (inv_into (Field r) f)"
-  by (simp add: inv_into_Field_embed_bij_betw)
+    by (simp add: inv_into_Field_embed_bij_betw)
   thus  "r \<le>o r' \<and> r' \<le>o r"
-  unfolding ordLeq_def using 1 by auto
+    unfolding ordLeq_def using 1 by auto
 next
   assume "r \<le>o r' \<and> r' \<le>o r"
   then obtain f and g where 1: "Well_order r \<and> Well_order r' \<and>
                            embed r r' f \<and> embed r' r g"
-  unfolding ordLeq_def by auto
+    unfolding ordLeq_def by auto
   hence "iso r r' f" by (auto simp add: embed_bothWays_iso)
   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
+  "r <o r' \<Longrightarrow> \<not> r' \<le>o r"
+  using ordLess_ordLeq_trans ordLess_irreflexive by blast
 
 lemma not_ordLeq_ordLess:
-"r \<le>o r' \<Longrightarrow> \<not> r' <o r"
-using not_ordLess_ordLeq by blast
+  "r \<le>o r' \<Longrightarrow> \<not> r' <o r"
+  using not_ordLess_ordLeq 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"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'"
+  shows "r <o r' \<or> r' \<le>o r"
 proof-
   have "r \<le>o r' \<or> r' \<le>o r"
-  using assms by (simp add: ordLeq_total)
+    using assms by (simp add: ordLeq_total)
   moreover
   {assume "\<not> r <o r' \<and> r \<le>o r'"
-   hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast
-   hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast
+    hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast
+    hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast
   }
   ultimately show ?thesis by blast
 qed
 
 lemma not_ordLess_ordIso:
-"r <o r' \<Longrightarrow> \<not> r =o r'"
-using ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
+  "r <o r' \<Longrightarrow> \<not> r =o r'"
+  using 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
+  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
+  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 ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
+  "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
+  using ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
 
 corollary ordLess_trans: "trans ordLess"
-unfolding trans_def using ordLess_transitive by blast
+  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
+  "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
+  "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"
-shows "(A \<le> B) = (Restr r A \<le>o Restr r B)"
+  assumes WELL: "Well_order r" and
+    OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
+  shows "(A \<le> B) = (Restr r A \<le>o Restr r B)"
 proof
   assume "A \<le> B"
   thus "Restr r A \<le>o Restr r B"
-  unfolding ordLeq_def using assms
-  Well_order_Restr Well_order_Restr ofilter_subset_embed by blast
+    unfolding ordLeq_def using assms
+      Well_order_Restr Well_order_Restr ofilter_subset_embed by blast
 next
   assume *: "Restr r A \<le>o Restr r B"
   then obtain f where "embed (Restr r A) (Restr r B) f"
-  unfolding ordLeq_def by blast
+    unfolding ordLeq_def by blast
   {assume "B < A"
-   hence "Restr r B <o Restr r A"
-   unfolding ordLess_def using assms
-   Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast
-   hence False using * not_ordLess_ordLeq by blast
+    hence "Restr r B <o Restr r A"
+      unfolding ordLess_def using assms
+        Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast
+    hence False using * not_ordLess_ordLeq by blast
   }
   thus "A \<le> B" using OFA OFB WELL
-  wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast
+      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"
-shows "(A < B) = (Restr r A <o Restr r B)"
+  assumes WELL: "Well_order r" and
+    OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
+  shows "(A < B) = (Restr r A <o Restr r B)"
 proof-
   let ?rA = "Restr r A" let ?rB = "Restr r B"
   have 1: "Well_order ?rA \<and> Well_order ?rB"
-  using WELL Well_order_Restr by blast
+    using WELL Well_order_Restr by blast
   have "(A < B) = (\<not> B \<le> A)" using assms
-  wo_rel_def wo_rel.ofilter_linord[of r A B] by blast
+      wo_rel_def wo_rel.ofilter_linord[of r A B] by blast
   also have "\<dots> = (\<not> Restr r B \<le>o Restr r A)"
-  using assms ofilter_subset_ordLeq by blast
+    using assms ofilter_subset_ordLeq by blast
   also have "\<dots> = (Restr r A <o Restr r B)"
-  using 1 not_ordLeq_iff_ordLess by blast
+    using 1 not_ordLeq_iff_ordLess by blast
   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)
+  "\<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"
+  assumes "Well_order r" and "Field r \<noteq> {}"
+  shows "Restr r (underS r a) <o r"
 proof-
   have "underS r a < Field r" using assms
-  by (simp add: underS_Field3)
+    by (simp add: underS_Field3)
   thus ?thesis using assms
-  by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
+    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
-  EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23"
-shows "(f13`(Field r1), f23`(Field r2)) \<in> (ofilterIncl r3)"
+  assumes
+    OL12: "r1 <o r2" and OL23: "r2 <o r3" and
+    EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23"
+  shows "(f13`(Field r1), f23`(Field r2)) \<in> (ofilterIncl r3)"
 proof-
   have OL13: "r1 <o r3"
-  using OL12 OL23 using ordLess_transitive by auto
+    using OL12 OL23 using ordLess_transitive by auto
   let ?A1 = "Field r1"  let ?A2 ="Field r2" let ?A3 ="Field r3"
   obtain f12 g23 where
-  0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and
-  1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and
-  2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)"
-  using OL12 OL23 by (auto simp add: ordLess_def embedS_def)
+    0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and
+    1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and
+    2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)"
+    using OL12 OL23 by (auto simp add: ordLess_def embedS_def)
   hence "\<forall>a \<in> ?A2. f23 a = g23 a"
-  using EMB23 embed_unique[of r2 r3] by blast
+    using EMB23 embed_unique[of r2 r3] by blast
   hence 3: "\<not>(bij_betw f23 ?A2 ?A3)"
-  using 2 bij_betw_cong[of ?A2 f23 g23] by blast
-  (*  *)
+    using 2 bij_betw_cong[of ?A2 f23 g23] by blast
+      (*  *)
   have 4: "wo_rel.ofilter r2 (f12 ` ?A1) \<and> f12 ` ?A1 \<noteq> ?A2"
-  using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field)
+    using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field)
   have 5: "wo_rel.ofilter r3 (f23 ` ?A2) \<and> f23 ` ?A2 \<noteq> ?A3"
-  using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field)
+    using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field)
   have 6: "wo_rel.ofilter r3 (f13 ` ?A1)  \<and> f13 ` ?A1 \<noteq> ?A3"
-  using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field)
-  (*  *)
+    using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field)
+      (*  *)
   have "f12 ` ?A1 < ?A2"
-  using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def)
+    using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def)
   moreover have "inj_on f23 ?A2"
-  using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
+    using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
   ultimately
   have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: image_strict_mono)
   moreover
   {have "embed r1 r3 (f23 \<circ> f12)"
-   using 1 EMB23 0 by (auto simp add: comp_embed)
-   hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"
-   using EMB13 0 embed_unique[of r1 r3 "f23 \<circ> f12" f13] by auto
-   hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force
+      using 1 EMB23 0 by (auto simp add: comp_embed)
+    hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"
+      using EMB13 0 embed_unique[of r1 r3 "f23 \<circ> f12" f13] by auto
+    hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force
   }
   ultimately
   have "f13 ` ?A1 < f23 ` ?A2" by simp
-  (*  *)
+      (*  *)
   with 5 6 show ?thesis
-  unfolding ofilterIncl_def by auto
+    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))"
+  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))"
 proof safe
   fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"
   hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
@@ -733,112 +681,107 @@
 next
   assume "r' <o r"
   then obtain f where 1: "Well_order r \<and> Well_order r'" and
-                      2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
-  unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
+    2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
+    unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
   hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast
   then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')"
-  using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
+    using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
   have "iso r' (Restr r (f ` (Field r'))) f"
-  using embed_implies_iso_Restr 2 assms by blast
+    using embed_implies_iso_Restr 2 assms by blast
   moreover have "Well_order (Restr r (f ` (Field r')))"
-  using WELL Well_order_Restr by blast
+    using WELL Well_order_Restr by blast
   ultimately have "r' =o Restr r (f ` (Field r'))"
-  using WELL' unfolding ordIso_def by auto
+    using WELL' unfolding ordIso_def by auto
   hence "r' =o Restr r (underS r a)" using 4 by auto
   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)"
+  "(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)"
 proof
   assume *: "r' <o r"
   hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto
   with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)"
-  using ordLess_iff_ordIso_Restr by blast
+    using ordLess_iff_ordIso_Restr by blast
   let ?p = "Restr r (underS r a)"
   have "wo_rel.ofilter r (underS r a)" using 0
-  by (simp add: wo_rel_def wo_rel.underS_ofilter)
+    by (simp add: wo_rel_def wo_rel.underS_ofilter)
   hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast
   hence "Field ?p < Field r" using underS_Field2 1 by fast
   moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast
-  ultimately
-  show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
+  ultimately show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
 next
   assume "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r"
   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)"
+  "(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)"
 proof
   assume *: "r' \<le>o r"
   moreover
-  {assume "r' <o r"
-   then obtain p where "Field p < Field r \<and> r' =o p \<and> p <o r"
-   using internalize_ordLess[of r' r] by blast
-   hence "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
-   using ordLeq_iff_ordLess_or_ordIso by blast
-  }
+  have "r' <o r \<Longrightarrow> \<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
+    using ordLeq_iff_ordLess_or_ordIso internalize_ordLess[of r' r] by blast
   moreover
   have "r \<le>o r" using * ordLeq_def ordLeq_reflexive by blast
   ultimately show "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
-  using ordLeq_iff_ordLess_or_ordIso by blast
+    using ordLeq_iff_ordLess_or_ordIso by blast
 next
   assume "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
   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')"
+  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')"
 proof safe
   assume *: "r \<le>o r'"
   fix a assume "a \<in> Field r"
   hence "Restr r (underS r a) <o r"
-  using WELL underS_Restr_ordLess[of r] by blast
+    using WELL underS_Restr_ordLess[of r] by blast
   thus "Restr r (underS r a) <o r'"
-  using * ordLess_ordLeq_trans by blast
+    using * ordLess_ordLeq_trans by blast
 next
   assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'"
   {assume "r' <o r"
-   then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
-   using assms ordLess_iff_ordIso_Restr by blast
-   hence False using * not_ordLess_ordIso ordIso_symmetric by blast
+    then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
+      using assms ordLess_iff_ordIso_Restr by blast
+    hence False using * not_ordLess_ordIso ordIso_symmetric by blast
   }
   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')"
-shows "r <o r'"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
+  shows "r <o r'"
 proof-
   {assume "r' \<le>o r"
-   then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
-   unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
-   hence False using finite_imageD finite_subset FIN INF by blast
+    then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
+      unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
+    hence False using finite_imageD finite_subset FIN INF by blast
   }
   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'"
-shows "r =o r'"
+  assumes FIN: "finite A" and
+    WELL: "well_order_on A r" and WELL': "well_order_on A r'"
+  shows "r =o r'"
 proof-
   have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
-  using assms well_order_on_Well_order by blast
+    using assms well_order_on_Well_order by blast
   moreover
   have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r'
                   \<longrightarrow> r =o r'"
   proof(clarify)
     fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'"
     have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
-    using * ** well_order_on_Well_order by blast
+      using * ** well_order_on_Well_order by blast
     assume "r \<le>o r'"
     then obtain f where 1: "embed r r' f" and
-                        "inj_on f A \<and> f ` A \<le> A"
-    unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast
+      "inj_on f A \<and> f ` A \<le> A"
+      unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast
     hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast
     thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto
   qed
@@ -854,10 +797,10 @@
 {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.\<close>
 
 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)"
+  where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)"
 
 lemma ord_to_filter_compat:
-"compat (ordLess Int (ordLess\<inverse>``{r0} \<times> ordLess\<inverse>``{r0}))
+  "compat (ordLess Int (ordLess\<inverse>``{r0} \<times> ordLess\<inverse>``{r0}))
         (ofilterIncl r0)
         (ord_to_filter r0)"
 proof(unfold compat_def ord_to_filter_def, clarify)
@@ -867,41 +810,41 @@
   let ?phi20 = "\<lambda> f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f"
   assume *: "r1 <o r0" "r2 <o r0" and **: "r1 <o r2"
   hence "(\<exists>f. ?phi10 f) \<and> (\<exists>f. ?phi20 f)"
-  by (auto simp add: ordLess_def embedS_def)
+    by (auto simp add: ordLess_def embedS_def)
   hence "?phi10 ?f10 \<and> ?phi20 ?f20" by (auto simp add: someI_ex)
   thus "(?f10 ` ?A1, ?f20 ` ?A2) \<in> ofilterIncl r0"
-  using * ** by (simp add: embed_ordLess_ofilterIncl)
+    using * ** by (simp add: embed_ordLess_ofilterIncl)
 qed
 
 theorem wf_ordLess: "wf ordLess"
 proof-
   {fix r0 :: "('a \<times> 'a) set"
-   (* need to annotate here!*)
-   let ?ordLess = "ordLess::('d rel * 'd rel) set"
-   let ?R = "?ordLess Int (?ordLess\<inverse>``{r0} \<times> ?ordLess\<inverse>``{r0})"
-   {assume Case1: "Well_order r0"
-    hence "wf ?R"
-    using wf_ofilterIncl[of r0]
+      (* need to annotate here!*)
+    let ?ordLess = "ordLess::('d rel * 'd rel) set"
+    let ?R = "?ordLess Int (?ordLess\<inverse>``{r0} \<times> ?ordLess\<inverse>``{r0})"
+    {assume Case1: "Well_order r0"
+      hence "wf ?R"
+        using wf_ofilterIncl[of r0]
           compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"]
           ord_to_filter_compat[of r0] by auto
-   }
-   moreover
-   {assume Case2: "\<not> Well_order r0"
-    hence "?R = {}" unfolding ordLess_def by auto
-    hence "wf ?R" using wf_empty by simp
-   }
-   ultimately have "wf ?R" by blast
+    }
+    moreover
+    {assume Case2: "\<not> Well_order r0"
+      hence "?R = {}" unfolding ordLess_def by auto
+      hence "wf ?R" using wf_empty by simp
+    }
+    ultimately have "wf ?R" by blast
   }
   thus ?thesis by (simp add: trans_wf_iff ordLess_trans)
 qed
 
 corollary exists_minim_Well_order:
-assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r"
-shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
+  assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r"
+  shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
 proof-
   obtain r where "r \<in> R \<and> (\<forall>r' \<in> R. \<not> r' <o r)"
-  using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R]
-    equals0I[of R] by blast
+    using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R]
+      equals0I[of R] by blast
   with not_ordLeq_iff_ordLess WELL show ?thesis by blast
 qed
 
@@ -913,79 +856,79 @@
 different types.\<close>
 
 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}"
+  where
+    "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
 
 lemma dir_image_Field:
-"Field(dir_image r f) = f ` (Field r)"
-unfolding dir_image_def Field_def Range_def Domain_def by fast
+  "Field(dir_image r f) = f ` (Field r)"
+  unfolding dir_image_def Field_def Range_def Domain_def by fast
 
 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
+  "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)"
+  assumes "Refl r"
+  shows "Refl(dir_image r f)"
 proof-
   {fix a' b'
-   assume "(a',b') \<in> dir_image r f"
-   then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r"
-   unfolding dir_image_def by blast
-   hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce
-   hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def)
-   with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f"
-   unfolding dir_image_def by auto
+    assume "(a',b') \<in> dir_image r f"
+    then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r"
+      unfolding dir_image_def by blast
+    hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce
+    hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def)
+    with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f"
+      unfolding dir_image_def by auto
   }
   thus ?thesis
-  by(unfold refl_on_def Field_def Domain_def Range_def, auto)
+    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)"
-unfolding trans_def
+  assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"
+  shows "trans(dir_image r f)"
+  unfolding trans_def
 proof safe
   fix a' b' c'
   assume "(a',b') \<in> dir_image r f" "(b',c') \<in> dir_image r f"
   then obtain a b1 b2 c where 1: "a' = f a \<and> b' = f b1 \<and> b' = f b2 \<and> c' = f c" and
-                         2: "(a,b1) \<in> r \<and> (b2,c) \<in> r"
-  unfolding dir_image_def by blast
+    2: "(a,b1) \<in> r \<and> (b2,c) \<in> r"
+    unfolding dir_image_def by blast
   hence "b1 \<in> Field r \<and> b2 \<in> Field r"
-  unfolding Field_def by auto
+    unfolding Field_def by auto
   hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto
   hence "(a,c) \<in> r" using 2 TRANS unfolding trans_def by blast
   thus "(a',c') \<in> dir_image r f"
-  unfolding dir_image_def using 1 by auto
+    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)
+  "\<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)"
-unfolding antisym_def
+  assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
+  shows "antisym(dir_image r f)"
+  unfolding antisym_def
 proof safe
   fix a' b'
   assume "(a',b') \<in> dir_image r f" "(b',a') \<in> dir_image r f"
   then obtain a1 b1 a2 b2 where 1: "a' = f a1 \<and> a' = f a2 \<and> b' = f b1 \<and> b' = f b2" and
-                           2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and
-                           3: "{a1,a2,b1,b2} \<le> Field r"
-  unfolding dir_image_def Field_def by blast
+    2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and
+    3: "{a1,a2,b1,b2} \<le> Field r"
+    unfolding dir_image_def Field_def by blast
   hence "a1 = a2 \<and> b1 = b2" using INJ unfolding inj_on_def by auto
   hence "a1 = b2" using 2 AN unfolding antisym_def by auto
   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)
+  "\<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)"
+  assumes TOT: "Total r" and INJ: "inj_on f (Field r)"
+  shows "Total(dir_image r f)"
 proof(unfold total_on_def, intro ballI impI)
   fix a' b'
   assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)"
@@ -995,76 +938,76 @@
   ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto
   hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto
   thus "(a',b') \<in> dir_image r f \<or> (b',a') \<in> dir_image r f"
-  using 1 unfolding dir_image_def by auto
+    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)
+  "\<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)"
+  assumes WF: "wf r" and INJ: "inj_on f (Field r)"
+  shows "wf(dir_image r f)"
 proof(unfold wf_eq_minimal2, intro allI impI, elim conjE)
   fix A'::"'b set"
   assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"
   obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast
   have "A \<noteq> {} \<and> A \<le> Field r" using A_def SUB NE by (auto simp: dir_image_Field)
   then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
-  using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
+    using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
   have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
   proof(clarify)
     fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
     obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and
-                       3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r"
-    using ** unfolding dir_image_def Field_def by blast
+      3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r"
+      using ** unfolding dir_image_def Field_def by blast
     hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto
     hence "b1 \<in> A \<and> (b1,a) \<in> r" using 2 3 A_def * by auto
     with 1 show False by auto
   qed
   thus "\<exists>a'\<in>A'. \<forall>b'\<in>A'. (b', a') \<notin> dir_image r f"
-  using A_def 1 by blast
+    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)"
-unfolding well_order_on_def
-using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
-  dir_image_minus_Id[of f r]
-  subset_inj_on[of f "Field r" "Field(r - Id)"]
-  mono_Field[of "r - Id" r] by auto
+  "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
+  unfolding well_order_on_def
+  using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
+    dir_image_minus_Id[of f r]
+    subset_inj_on[of f "Field r" "Field(r - Id)"]
+    mono_Field[of "r - Id" r] by auto
 
 lemma dir_image_bij_betw:
-"\<lbrakk>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_Field order_on_defs)
+  "\<lbrakk>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_Field order_on_defs)
 
 lemma dir_image_compat:
-"compat r (dir_image r f) f"
-unfolding compat_def dir_image_def by auto
+  "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
+  "\<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
+  "\<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'"
+  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'"
 proof-
-   let ?r' = "dir_image r f"
-   have 1: "A = Field r \<and> Well_order r"
-   using WELL well_order_on_Well_order by blast
-   hence 2: "iso r ?r' f"
-   using dir_image_iso using BIJ unfolding bij_betw_def by auto
-   hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
-   hence "Field ?r' = A'"
-   using 1 BIJ unfolding bij_betw_def by auto
-   moreover have "Well_order ?r'"
-   using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast
-   ultimately show ?thesis unfolding ordIso_def using 1 2 by blast
+  let ?r' = "dir_image r f"
+  have 1: "A = Field r \<and> Well_order r"
+    using WELL well_order_on_Well_order by blast
+  hence 2: "iso r ?r' f"
+    using dir_image_iso using BIJ unfolding bij_betw_def by auto
+  hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
+  hence "Field ?r' = A'"
+    using 1 BIJ unfolding bij_betw_def by auto
+  moreover have "Well_order ?r'"
+    using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast
+  ultimately show ?thesis unfolding ordIso_def using 1 2 by blast
 qed
 
 
@@ -1086,8 +1029,8 @@
 in a product of proper filters on the original relation (assumed to be a well-order).\<close>
 
 definition bsqr :: "'a rel => ('a * 'a)rel"
-where
-"bsqr r = {((a1,a2),(b1,b2)).
+  where
+    "bsqr r = {((a1,a2),(b1,b2)).
            {a1,a2,b1,b2} \<le> Field r \<and>
            (a1 = b1 \<and> a2 = b2 \<or>
             (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
@@ -1096,15 +1039,15 @@
            )}"
 
 lemma Field_bsqr:
-"Field (bsqr r) = Field r \<times> Field r"
+  "Field (bsqr r) = Field r \<times> Field r"
 proof
   show "Field (bsqr r) \<le> Field r \<times> Field r"
   proof-
     {fix a1 a2 assume "(a1,a2) \<in> Field (bsqr r)"
-     moreover
-     have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow>
+      moreover
+      have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow>
                       a1 \<in> Field r \<and> a2 \<in> Field r" unfolding bsqr_def by auto
-     ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto
+      ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto
     }
     thus ?thesis unfolding Field_def by force
   qed
@@ -1118,101 +1061,101 @@
 qed
 
 lemma bsqr_Refl: "Refl(bsqr r)"
-by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
+  by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
 
 lemma bsqr_Trans:
-assumes "Well_order r"
-shows "trans (bsqr r)"
-unfolding trans_def
+  assumes "Well_order r"
+  shows "trans (bsqr r)"
+  unfolding trans_def
 proof safe
   (* Preliminary facts *)
   have Well: "wo_rel r" using assms wo_rel_def by auto
   hence Trans: "trans r" using wo_rel.TRANS by auto
   have Anti: "antisym r" using wo_rel.ANTISYM Well by auto
   hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)
-  (* Main proof *)
+      (* Main proof *)
   fix a1 a2 b1 b2 c1 c2
   assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(c1,c2)) \<in> bsqr r"
   hence 0: "{a1,a2,b1,b2,c1,c2} \<le> Field r" unfolding bsqr_def by auto
   have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
-  using * unfolding bsqr_def by auto
+    using * unfolding bsqr_def by auto
   have 2: "b1 = c1 \<and> b2 = c2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id \<or>
            wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id \<or>
            wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
-  using ** unfolding bsqr_def by auto
+    using ** unfolding bsqr_def by auto
   show "((a1,a2),(c1,c2)) \<in> bsqr r"
   proof-
     {assume Case1: "a1 = b1 \<and> a2 = b2"
-     hence ?thesis using ** by simp
+      hence ?thesis using ** by simp
     }
     moreover
     {assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"
-     {assume Case21: "b1 = c1 \<and> b2 = c2"
-      hence ?thesis using * by simp
-     }
-     moreover
-     {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
-      hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id"
-      using Case2 TransS trans_def[of "r - Id"] by blast
-      hence ?thesis using 0 unfolding bsqr_def by auto
-     }
-     moreover
-     {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2"
-      hence ?thesis using Case2 0 unfolding bsqr_def by auto
-     }
-     ultimately have ?thesis using 0 2 by auto
+      {assume Case21: "b1 = c1 \<and> b2 = c2"
+        hence ?thesis using * by simp
+      }
+      moreover
+      {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
+        hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id"
+          using Case2 TransS trans_def[of "r - Id"] by blast
+        hence ?thesis using 0 unfolding bsqr_def by auto
+      }
+      moreover
+      {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2"
+        hence ?thesis using Case2 0 unfolding bsqr_def by auto
+      }
+      ultimately have ?thesis using 0 2 by auto
     }
     moreover
     {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"
-     {assume Case31: "b1 = c1 \<and> b2 = c2"
-      hence ?thesis using * by simp
-     }
-     moreover
-     {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
-      hence ?thesis using Case3 0 unfolding bsqr_def by auto
-     }
-     moreover
-     {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
-      hence "(a1,c1) \<in> r - Id"
-      using Case3 TransS trans_def[of "r - Id"] by blast
-      hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto
-     }
-     moreover
-     {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1"
-      hence ?thesis using Case3 0 unfolding bsqr_def by auto
-     }
-     ultimately have ?thesis using 0 2 by auto
+      {assume Case31: "b1 = c1 \<and> b2 = c2"
+        hence ?thesis using * by simp
+      }
+      moreover
+      {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
+        hence ?thesis using Case3 0 unfolding bsqr_def by auto
+      }
+      moreover
+      {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
+        hence "(a1,c1) \<in> r - Id"
+          using Case3 TransS trans_def[of "r - Id"] by blast
+        hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto
+      }
+      moreover
+      {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1"
+        hence ?thesis using Case3 0 unfolding bsqr_def by auto
+      }
+      ultimately have ?thesis using 0 2 by auto
     }
     moreover
     {assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
-     {assume Case41: "b1 = c1 \<and> b2 = c2"
-      hence ?thesis using * by simp
-     }
-     moreover
-     {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
-      hence ?thesis using Case4 0 unfolding bsqr_def by force
-     }
-     moreover
-     {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
-      hence ?thesis using Case4 0 unfolding bsqr_def by auto
-     }
-     moreover
-     {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
-      hence "(a2,c2) \<in> r - Id"
-      using Case4 TransS trans_def[of "r - Id"] by blast
-      hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto
-     }
-     ultimately have ?thesis using 0 2 by auto
+      {assume Case41: "b1 = c1 \<and> b2 = c2"
+        hence ?thesis using * by simp
+      }
+      moreover
+      {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
+        hence ?thesis using Case4 0 unfolding bsqr_def by force
+      }
+      moreover
+      {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
+        hence ?thesis using Case4 0 unfolding bsqr_def by auto
+      }
+      moreover
+      {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
+        hence "(a2,c2) \<in> r - Id"
+          using Case4 TransS trans_def[of "r - Id"] by blast
+        hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto
+      }
+      ultimately have ?thesis using 0 2 by auto
     }
     ultimately show ?thesis using 0 1 by auto
   qed
 qed
 
 lemma bsqr_antisym:
-assumes "Well_order r"
-shows "antisym (bsqr r)"
+  assumes "Well_order r"
+  shows "antisym (bsqr r)"
 proof(unfold antisym_def, clarify)
   (* Preliminary facts *)
   have Well: "wo_rel r" using assms wo_rel_def by auto
@@ -1220,334 +1163,293 @@
   have Anti: "antisym r" using wo_rel.ANTISYM Well by auto
   hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)
   hence IrrS: "\<forall>a b. \<not>((a,b) \<in> r - Id \<and> (b,a) \<in> r - Id)"
-  using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast
-  (* Main proof *)
+    using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast
+      (* Main proof *)
   fix a1 a2 b1 b2
   assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(a1,a2)) \<in> bsqr r"
-  hence 0: "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto
-  have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
+  hence "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto
+  moreover
+  have "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
-  using * unfolding bsqr_def by auto
-  have 2: "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or>
+    using * unfolding bsqr_def by auto
+  moreover
+  have "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or>
            wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> (b1,a1) \<in> r - Id \<or>
            wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> b1 = a1 \<and> (b2,a2) \<in> r - Id"
-  using ** unfolding bsqr_def by auto
-  show "a1 = b1 \<and> a2 = b2"
-  proof-
-    {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"
-     {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
-      hence False using Case1 IrrS by blast
-     }
-     moreover
-     {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2"
-      hence False using Case1 by auto
-     }
-     ultimately have ?thesis using 0 2 by auto
-    }
-    moreover
-    {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"
-     {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
-       hence False using Case2 by auto
-     }
-     moreover
-     {assume Case22: "(b1,a1) \<in> r - Id"
-      hence False using Case2 IrrS by blast
-     }
-     moreover
-     {assume Case23: "b1 = a1"
-      hence False using Case2 by auto
-     }
-     ultimately have ?thesis using 0 2 by auto
-    }
-    moreover
-    {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
-     moreover
-     {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
-      hence False using Case3 by auto
-     }
-     moreover
-     {assume Case32: "(b1,a1) \<in> r - Id"
-      hence False using Case3 by auto
-     }
-     moreover
-     {assume Case33: "(b2,a2) \<in> r - Id"
-      hence False using Case3 IrrS by blast
-     }
-     ultimately have ?thesis using 0 2 by auto
-    }
-    ultimately show ?thesis using 0 1 by blast
-  qed
+    using ** unfolding bsqr_def by auto
+  ultimately show "a1 = b1 \<and> a2 = b2"
+    using IrrS by auto
 qed
 
 lemma bsqr_Total:
-assumes "Well_order r"
-shows "Total(bsqr r)"
+  assumes "Well_order r"
+  shows "Total(bsqr r)"
 proof-
   (* Preliminary facts *)
   have Well: "wo_rel r" using assms wo_rel_def by auto
   hence Total: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
-  using wo_rel.TOTALS by auto
-  (* Main proof *)
+    using wo_rel.TOTALS by auto
+      (* Main proof *)
   {fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \<le> Field(bsqr r)"
-   hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r"
-   using Field_bsqr by blast
-   have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)"
-   proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0)
-       (* Why didn't clarsimp simp add: Well 0 do the same job? *)
-     assume Case1: "(a1,a2) \<in> r"
-     hence 1: "wo_rel.max2 r a1 a2 = a2"
-     using Well 0 by (simp add: wo_rel.max2_equals2)
-     show ?thesis
-     proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
-       assume Case11: "(b1,b2) \<in> r"
-       hence 2: "wo_rel.max2 r b1 b2 = b2"
-       using Well 0 by (simp add: wo_rel.max2_equals2)
-       show ?thesis
-       proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
-         assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
-         thus ?thesis using 0 1 2 unfolding bsqr_def by auto
-       next
-         assume Case112: "a2 = b2"
-         show ?thesis
-         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
-           assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
-           thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto
-         next
-           assume Case1122: "a1 = b1"
-           thus ?thesis using Case112 by auto
-         qed
-       qed
-     next
-       assume Case12: "(b2,b1) \<in> r"
-       hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)
-       show ?thesis
-       proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0)
-         assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id"
-         thus ?thesis using 0 1 3 unfolding bsqr_def by auto
-       next
-         assume Case122: "a2 = b1"
-         show ?thesis
-         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
-           assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
-           thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto
-         next
-           assume Case1222: "a1 = b1"
-           show ?thesis
-           proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
-             assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
-             thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto
-           next
-             assume Case12222: "a2 = b2"
-             thus ?thesis using Case122 Case1222 by auto
-           qed
-         qed
-       qed
-     qed
-   next
-     assume Case2: "(a2,a1) \<in> r"
-     hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1)
-     show ?thesis
-     proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
-       assume Case21: "(b1,b2) \<in> r"
-       hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2)
-       show ?thesis
-       proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0)
-         assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id"
-         thus ?thesis using 0 1 2 unfolding bsqr_def by auto
-       next
-         assume Case212: "a1 = b2"
-         show ?thesis
-         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
-           assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
-           thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto
-         next
-           assume Case2122: "a1 = b1"
-           show ?thesis
-           proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
-             assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
-             thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto
-           next
-             assume Case21222: "a2 = b2"
-             thus ?thesis using Case2122 Case212 by auto
-           qed
-         qed
-       qed
-     next
-       assume Case22: "(b2,b1) \<in> r"
-       hence 3: "wo_rel.max2 r b1 b2 = b1"  using Well 0 by (simp add: wo_rel.max2_equals1)
-       show ?thesis
-       proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
-         assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
-         thus ?thesis using 0 1 3 unfolding bsqr_def by auto
-       next
-         assume Case222: "a1 = b1"
-         show ?thesis
-         proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
-           assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
-           thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto
-         next
-           assume Case2222: "a2 = b2"
-           thus ?thesis using Case222 by auto
-         qed
-       qed
-     qed
-   qed
+    hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r"
+      using Field_bsqr by blast
+    have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)"
+    proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0)
+      (* Why didn't clarsimp simp add: Well 0 do the same job? *)
+      assume Case1: "(a1,a2) \<in> r"
+      hence 1: "wo_rel.max2 r a1 a2 = a2"
+        using Well 0 by (simp add: wo_rel.max2_equals2)
+      show ?thesis
+      proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
+        assume Case11: "(b1,b2) \<in> r"
+        hence 2: "wo_rel.max2 r b1 b2 = b2"
+          using Well 0 by (simp add: wo_rel.max2_equals2)
+        show ?thesis
+        proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
+          assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
+          thus ?thesis using 0 1 2 unfolding bsqr_def by auto
+        next
+          assume Case112: "a2 = b2"
+          show ?thesis
+          proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
+            assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
+            thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto
+          next
+            assume Case1122: "a1 = b1"
+            thus ?thesis using Case112 by auto
+          qed
+        qed
+      next
+        assume Case12: "(b2,b1) \<in> r"
+        hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)
+        show ?thesis
+        proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0)
+          assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id"
+          thus ?thesis using 0 1 3 unfolding bsqr_def by auto
+        next
+          assume Case122: "a2 = b1"
+          show ?thesis
+          proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
+            assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
+            thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto
+          next
+            assume Case1222: "a1 = b1"
+            show ?thesis
+            proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
+              assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
+              thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto
+            next
+              assume Case12222: "a2 = b2"
+              thus ?thesis using Case122 Case1222 by auto
+            qed
+          qed
+        qed
+      qed
+    next
+      assume Case2: "(a2,a1) \<in> r"
+      hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1)
+      show ?thesis
+      proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
+        assume Case21: "(b1,b2) \<in> r"
+        hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2)
+        show ?thesis
+        proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0)
+          assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id"
+          thus ?thesis using 0 1 2 unfolding bsqr_def by auto
+        next
+          assume Case212: "a1 = b2"
+          show ?thesis
+          proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
+            assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
+            thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto
+          next
+            assume Case2122: "a1 = b1"
+            show ?thesis
+            proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
+              assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
+              thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto
+            next
+              assume Case21222: "a2 = b2"
+              thus ?thesis using Case2122 Case212 by auto
+            qed
+          qed
+        qed
+      next
+        assume Case22: "(b2,b1) \<in> r"
+        hence 3: "wo_rel.max2 r b1 b2 = b1"  using Well 0 by (simp add: wo_rel.max2_equals1)
+        show ?thesis
+        proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
+          assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
+          thus ?thesis using 0 1 3 unfolding bsqr_def by auto
+        next
+          assume Case222: "a1 = b1"
+          show ?thesis
+          proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
+            assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
+            thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto
+          next
+            assume Case2222: "a2 = b2"
+            thus ?thesis using Case222 by auto
+          qed
+        qed
+      qed
+    qed
   }
   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
+  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)"
-using assms
+  assumes "Well_order r"
+  shows "Well_order(bsqr r)"
+  using assms
 proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI)
   have 0: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
-  using assms well_order_on_def Linear_order_Well_order_iff by blast
+    using assms well_order_on_def Linear_order_Well_order_iff by blast
   fix D assume *: "D \<le> Field (bsqr r)" and **: "D \<noteq> {}"
   hence 1: "D \<le> Field r \<times> Field r" unfolding Field_bsqr by simp
-  (*  *)
+      (*  *)
   obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \<in> D}" by blast
   have "M \<noteq> {}" using 1 M_def ** by auto
   moreover
   have "M \<le> Field r" unfolding M_def
-  using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
+    using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
   ultimately obtain m where m_min: "m \<in> M \<and> (\<forall>a \<in> M. (m,a) \<in> r)"
-  using 0 by blast
-  (*  *)
+    using 0 by blast
+      (*  *)
   obtain A1 where A1_def: "A1 = {a1. \<exists>a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast
   have "A1 \<le> Field r" unfolding A1_def using 1 by auto
   moreover have "A1 \<noteq> {}" unfolding A1_def using m_min unfolding M_def by blast
   ultimately obtain a1 where a1_min: "a1 \<in> A1 \<and> (\<forall>a \<in> A1. (a1,a) \<in> r)"
-  using 0 by blast
-  (*  *)
+    using 0 by blast
+      (*  *)
   obtain A2 where A2_def: "A2 = {a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast
   have "A2 \<le> Field r" unfolding A2_def using 1 by auto
   moreover have "A2 \<noteq> {}" unfolding A2_def
-  using m_min a1_min unfolding A1_def M_def by blast
+    using m_min a1_min unfolding A1_def M_def by blast
   ultimately obtain a2 where a2_min: "a2 \<in> A2 \<and> (\<forall>a \<in> A2. (a2,a) \<in> r)"
-  using 0 by blast
-  (*   *)
+    using 0 by blast
+      (*   *)
   have 2: "wo_rel.max2 r a1 a2 = m"
-  using a1_min a2_min unfolding A1_def A2_def by auto
+    using a1_min a2_min unfolding A1_def A2_def by auto
   have 3: "(a1,a2) \<in> D" using a2_min unfolding A2_def by auto
-  (*  *)
+      (*  *)
   moreover
   {fix b1 b2 assume ***: "(b1,b2) \<in> D"
-   hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast
-   have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
-   using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto
-   have "((a1,a2),(b1,b2)) \<in> bsqr r"
-   proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2")
-     assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2"
-     thus ?thesis unfolding bsqr_def using 4 5 by auto
-   next
-     assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
-     hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto
-     hence 6: "(a1,b1) \<in> r" using a1_min by auto
-     show ?thesis
-     proof(cases "a1 = b1")
-       assume Case21: "a1 \<noteq> b1"
-       thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto
-     next
-       assume Case22: "a1 = b1"
-       hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto
-       hence 7: "(a2,b2) \<in> r" using a2_min by auto
-       thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto
-     qed
-   qed
+    hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast
+    have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
+      using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto
+    have "((a1,a2),(b1,b2)) \<in> bsqr r"
+    proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2")
+      assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2"
+      thus ?thesis unfolding bsqr_def using 4 5 by auto
+    next
+      assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
+      hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto
+      hence 6: "(a1,b1) \<in> r" using a1_min by auto
+      show ?thesis
+      proof(cases "a1 = b1")
+        assume Case21: "a1 \<noteq> b1"
+        thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto
+      next
+        assume Case22: "a1 = b1"
+        hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto
+        hence 7: "(a2,b2) \<in> r" using a2_min by auto
+        thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto
+      qed
+    qed
   }
-  (*  *)
+    (*  *)
   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"
+  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"
 proof-
   have "{(a1,a2),(b1,b2)} \<le> Field(bsqr r)"
-  using LEQ unfolding Field_def by auto
+    using LEQ unfolding Field_def by auto
   hence "{a1,a2,b1,b2} \<le> Field r" unfolding Field_bsqr by auto
   hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \<le> Field r"
-  using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
+    using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
   moreover have "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r \<or> wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
-  using LEQ unfolding bsqr_def by auto
+    using LEQ unfolding bsqr_def by auto
   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
-        NE: "\<not> (\<exists>a. Field r = under r a)"
-shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
+  assumes WELL: "Well_order r" and
+    OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
+    NE: "\<not> (\<exists>a. Field r = under r a)"
+  shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
 proof-
   let ?r' = "bsqr r"
   have Well: "wo_rel r" using WELL wo_rel_def by blast
   hence Trans: "trans r" using wo_rel.TRANS by blast
   have Well': "Well_order ?r' \<and> wo_rel ?r'"
-  using WELL bsqr_Well_order wo_rel_def by blast
-  (*  *)
+    using WELL bsqr_Well_order wo_rel_def by blast
+      (*  *)
   have "D < Field ?r'" unfolding Field_bsqr using SUB .
   with OF obtain a1 and a2 where
-  "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
-  using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
+    "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
+    using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
   hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto
   let ?m = "wo_rel.max2 r a1 a2"
   have "D \<le> (under r ?m) \<times> (under r ?m)"
   proof(unfold 1)
     {fix b1 b2
-     let ?n = "wo_rel.max2 r b1 b2"
-     assume "(b1,b2) \<in> underS ?r' (a1,a2)"
-     hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
-     unfolding underS_def by blast
-     hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
-     moreover
-     {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
-      hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto
-      hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r"
-      using Well by (simp add: wo_rel.max2_greater)
-     }
-     ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
-     using Trans trans_def[of r] by blast
-     hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
-     thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
+      let ?n = "wo_rel.max2 r b1 b2"
+      assume "(b1,b2) \<in> underS ?r' (a1,a2)"
+      hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
+        unfolding underS_def by blast
+      hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
+      moreover
+      {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
+        hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto
+        hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r"
+          using Well by (simp add: wo_rel.max2_greater)
+      }
+      ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
+        using Trans trans_def[of r] by blast
+      hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
+    thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
   qed
   moreover have "wo_rel.ofilter r (under r ?m)"
-  using Well by (simp add: wo_rel.under_ofilter)
+    using Well by (simp add: wo_rel.under_ofilter)
   moreover have "under r ?m < Field r"
-  using NE under_Field[of r ?m] by blast
+    using NE under_Field[of r ?m] by blast
   ultimately show ?thesis by blast
 qed
 
 definition Func where
-"Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
+  "Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
 
 lemma Func_empty:
-"Func {} B = {\<lambda>x. undefined}"
-unfolding Func_def by auto
+  "Func {} B = {\<lambda>x. undefined}"
+  unfolding Func_def by auto
 
 lemma Func_elim:
-assumes "g \<in> Func A B" and "a \<in> A"
-shows "\<exists> b. b \<in> B \<and> g a = b"
-using assms unfolding Func_def by (cases "g a = undefined") auto
+  assumes "g \<in> Func A B" and "a \<in> A"
+  shows "\<exists> b. b \<in> B \<and> g a = b"
+  using assms unfolding Func_def by (cases "g a = undefined") auto
 
 definition curr where
-"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
+  "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
 
 lemma curr_in:
-assumes f: "f \<in> Func (A \<times> B) C"
-shows "curr A f \<in> Func A (Func B C)"
-using assms unfolding curr_def Func_def by auto
+  assumes f: "f \<in> Func (A \<times> B) C"
+  shows "curr A f \<in> Func A (Func B C)"
+  using assms unfolding curr_def Func_def by auto
 
 lemma curr_inj:
-assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
-shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
+  assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
+  shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
 proof safe
   assume c: "curr A f1 = curr A f2"
   show "f1 = f2"
@@ -1559,14 +1461,14 @@
     next
       case True hence a: "a \<in> A" and b: "b \<in> B" by auto
       thus ?thesis
-      using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
+        using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
     qed
   qed
 qed
 
 lemma curr_surj:
-assumes "g \<in> Func A (Func B C)"
-shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
+  assumes "g \<in> Func A (Func B C)"
+  shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
 proof
   let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
   show "curr A ?f = g"
@@ -1579,7 +1481,7 @@
     next
       case True
       obtain g1 where "g1 \<in> Func B C" and "g a = g1"
-      using assms using Func_elim[OF assms True] by blast
+        using assms using Func_elim[OF assms True] by blast
       thus ?thesis using True unfolding Func_def curr_def by auto
     qed
   qed
@@ -1587,24 +1489,21 @@
 qed
 
 lemma bij_betw_curr:
-"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
-  unfolding bij_betw_def inj_on_def image_def
-  apply (intro impI conjI ballI)
-   apply (erule curr_inj[THEN iffD1], assumption+, safe)
-  using curr_surj curr_in apply blast+
-  done
+  "bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
+  unfolding bij_betw_def inj_on_def 
+  using curr_surj curr_in curr_inj by blast
 
 definition Func_map where
-"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
+  "Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
 
 lemma Func_map:
-assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
-shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
-using assms unfolding Func_def Func_map_def mem_Collect_eq by auto
+  assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
+  shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
+  using assms unfolding Func_def Func_map_def mem_Collect_eq by auto
 
 lemma Func_non_emp:
-assumes "B \<noteq> {}"
-shows "Func A B \<noteq> {}"
+  assumes "B \<noteq> {}"
+  shows "Func A B \<noteq> {}"
 proof-
   obtain b where b: "b \<in> B" using assms by auto
   hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto
@@ -1612,27 +1511,21 @@
 qed
 
 lemma Func_is_emp:
-"Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
+  "Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
 proof
-  assume L: ?L
-  moreover {assume "A = {}" hence False using L Func_empty by auto}
-  moreover {assume "B \<noteq> {}" hence False using L Func_non_emp[of B A] by simp }
-  ultimately show ?R by blast
+  assume ?L
+  then show ?R
+    using Func_empty Func_non_emp[of B A] by blast
 next
-  assume R: ?R
-  moreover
-  {fix f assume "f \<in> Func A B"
-   moreover obtain a where "a \<in> A" using R by blast
-   ultimately obtain b where "b \<in> B" unfolding Func_def by blast
-   with R have False by blast
-  }
-  thus ?L by blast
+  assume ?R
+  then show ?L
+    using Func_empty Func_non_emp[of B A] by (auto simp: Func_def)
 qed
 
 lemma Func_map_surj:
-assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
-and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
-shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
+  assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
+    and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
+  shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
 proof(cases "B2 = {}")
   case True
   thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def)
@@ -1646,15 +1539,15 @@
     then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2"
       by atomize_elim (rule bchoice)
     {fix b2 assume b2: "b2 \<in> B2"
-     hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
-     moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
-     ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
+      hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
+      moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
+      ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
     } note kk = this
     obtain b22 where b22: "b22 \<in> B2" using B2 by auto
     define j2 where [abs_def]: "j2 a2 = (if a2 \<in> f2 ` B2 then k a2 else b22)" for a2
     have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
     have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
-    using kk unfolding j2_def by auto
+      using kk unfolding j2_def by auto
     define g where "g = Func_map A2 j1 j2 h"
     have "Func_map B2 f1 f2 g = h"
     proof (rule ext)
@@ -1668,13 +1561,13 @@
           show ?thesis using A2 f_inv_into_f[OF b1]
             unfolding True g_def Func_map_def j1_def j2[OF \<open>b2 \<in> B2\<close>] by auto
         qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def,
-          auto intro: f_inv_into_f)
+            auto intro: f_inv_into_f)
       qed(insert h, unfold Func_def Func_map_def, auto)
     qed
     moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
-    using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+
+      using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+
     ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
-    unfolding Func_map_def[abs_def] by auto
+      unfolding Func_map_def[abs_def] by auto
   qed(use B1 Func_map[OF _ _ A2(2)] in auto)
 qed
 
diff -r ec4c38e156c7 -r f881fd264929 src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri Jan 13 16:44:00 2023 +0000
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri Jan 13 22:47:40 2023 +0000
@@ -8,7 +8,7 @@
 section \<open>Well-Order Embeddings as Needed by Bounded Natural Functors\<close>
 
 theory BNF_Wellorder_Embedding
-imports Hilbert_Choice BNF_Wellorder_Relation
+  imports Hilbert_Choice BNF_Wellorder_Relation
 begin
 
 text\<open>In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
@@ -23,35 +23,35 @@
 subsection \<open>Auxiliaries\<close>
 
 lemma UNION_inj_on_ofilter:
-assumes WELL: "Well_order r" and
-        OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
-       INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
-shows "inj_on f (\<Union>i \<in> I. A i)"
+  assumes WELL: "Well_order r" and
+    OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
+    INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
+  shows "inj_on f (\<Union>i \<in> I. A i)"
 proof-
   have "wo_rel r" using WELL by (simp add: wo_rel_def)
   hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"
-  using wo_rel.ofilter_linord[of r] OF by blast
+    using wo_rel.ofilter_linord[of r] OF by blast
   with WELL INJ show ?thesis
-  by (auto simp add: inj_on_UNION_chain)
+    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
-        BIJ: "bij_betw f (underS r a) (underS r' (f a))"
-shows "bij_betw f (under r a) (under r' (f a))"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
+    BIJ: "bij_betw f (underS r a) (underS r' (f a))"
+  shows "bij_betw f (under r a) (under r' (f a))"
 proof-
   have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
-  unfolding underS_def by auto
+    unfolding underS_def by auto
   moreover
   {have "Refl r \<and> Refl r'" using WELL WELL'
-   by (auto simp add: order_on_defs)
-   hence "under r a = underS r a \<union> {a} \<and>
+      by (auto simp add: order_on_defs)
+    hence "under r a = underS r a \<union> {a} \<and>
           under r' (f a) = underS r' (f a) \<union> {f a}"
-   using IN IN' by(auto simp add: Refl_under_underS)
+      using IN IN' by(auto simp add: Refl_under_underS)
   }
   ultimately show ?thesis
-  using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
+    using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
 qed
 
 
@@ -69,28 +69,28 @@
 and an isomorphism (operator \<open>iso\<close>) is a bijective embedding.\<close>
 
 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))"
+  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 \<open>Strict embeddings:\<close>
 
 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')"
+  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')"
+  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'"
+  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'"
@@ -168,46 +168,46 @@
   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"
-shows "wo_rel.ofilter r' (f`A)"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
+  shows "wo_rel.ofilter r' (f`A)"
 proof-
   (* Preliminary facts *)
   from WELL have Well: "wo_rel r" unfolding wo_rel_def .
   from WELL' have Well': "wo_rel r'" unfolding wo_rel_def .
   from OF have 0: "A \<le> Field r" by(auto simp add: Well wo_rel.ofilter_def)
-  (* Main proof *)
+      (* Main proof *)
   show ?thesis  using Well' WELL EMB 0 embed_Field[of r r' f]
   proof(unfold wo_rel.ofilter_def, auto simp add: image_def)
     fix a b'
     assume *: "a \<in> A" and **: "b' \<in> under r' (f a)"
     hence "a \<in> Field r" using 0 by auto
     hence "bij_betw f (under r a) (under r' (f a))"
-    using * EMB by (auto simp add: embed_def)
+      using * EMB by (auto simp add: embed_def)
     hence "f`(under r a) = under r' (f a)"
-    by (simp add: bij_betw_def)
+      by (simp add: bij_betw_def)
     with ** image_def[of f "under r a"] obtain b where
-    1: "b \<in> under r a \<and> b' = f b" by blast
+      1: "b \<in> under r a \<and> b' = f b" by blast
     hence "b \<in> A" using Well * OF
-    by (auto simp add: wo_rel.ofilter_def)
+      by (auto simp add: wo_rel.ofilter_def)
     with 1 show "\<exists>b \<in> A. b' = f b" by blast
   qed
 qed
 
 lemma embed_Field_ofilter:
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and
-        EMB: "embed r r' f"
-shows "wo_rel.ofilter r' (f`(Field r))"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    EMB: "embed r r' f"
+  shows "wo_rel.ofilter r' (f`(Field r))"
 proof-
   have "wo_rel.ofilter r (Field r)"
-  using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter)
+    using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter)
   with WELL WELL' EMB
   show ?thesis by (auto simp add: embed_preserves_ofilter)
 qed
 
 lemma embed_inj_on:
-assumes WELL: "Well_order r" and EMB: "embed r r' f"
-shows "inj_on f (Field r)"
+  assumes WELL: "Well_order r" and EMB: "embed r r' f"
+  shows "inj_on f (Field r)"
 proof(unfold inj_on_def, clarify)
   (* Preliminary facts *)
   from WELL have Well: "wo_rel r" unfolding wo_rel_def .
@@ -215,30 +215,30 @@
   have Total: "Total r" by simp
   from Well wo_rel.REFL[of r]
   have Refl: "Refl r" by simp
-  (* Main proof *)
+      (* Main proof *)
   fix a b
   assume *: "a \<in> Field r" and **: "b \<in> Field r" and
-         ***: "f a = f b"
+    ***: "f a = f b"
   hence 1: "a \<in> Field r \<and> b \<in> Field r"
-  unfolding Field_def by auto
+    unfolding Field_def by auto
   {assume "(a,b) \<in> r"
-   hence "a \<in> under r b \<and> b \<in> under r b"
-   using Refl by(auto simp add: under_def refl_on_def)
-   hence "a = b"
-   using EMB 1 ***
-   by (auto simp add: embed_def bij_betw_def inj_on_def)
+    hence "a \<in> under r b \<and> b \<in> under r b"
+      using Refl by(auto simp add: under_def refl_on_def)
+    hence "a = b"
+      using EMB 1 ***
+      by (auto simp add: embed_def bij_betw_def inj_on_def)
   }
   moreover
   {assume "(b,a) \<in> r"
-   hence "a \<in> under r a \<and> b \<in> under r a"
-   using Refl by(auto simp add: under_def refl_on_def)
-   hence "a = b"
-   using EMB 1 ***
-   by (auto simp add: embed_def bij_betw_def inj_on_def)
+    hence "a \<in> under r a \<and> b \<in> under r a"
+      using Refl by(auto simp add: under_def refl_on_def)
+    hence "a = b"
+      using EMB 1 ***
+      by (auto simp add: embed_def bij_betw_def inj_on_def)
   }
   ultimately
   show "a = b" using Total 1
-  by (auto simp add: total_on_def)
+    by (auto simp add: total_on_def)
 qed
 
 lemma embed_underS:
@@ -265,173 +265,173 @@
 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)))"
-using assms
+  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)))"
+  using assms
 proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter,
-      unfold embed_def, auto) (* get rid of one implication *)
+    unfold embed_def, auto) (* get rid of one implication *)
   fix a
   assume *: "inj_on f (Field r)" and
-         **: "compat r r' f" and
-         ***: "wo_rel.ofilter r' (f`(Field r))" and
-         ****: "a \<in> Field r"
-  (* Preliminary facts *)
+    **: "compat r r' f" and
+    ***: "wo_rel.ofilter r' (f`(Field r))" and
+    ****: "a \<in> Field r"
+    (* Preliminary facts *)
   have Well: "wo_rel r"
-  using WELL wo_rel_def[of r] by simp
+    using WELL wo_rel_def[of r] by simp
   hence Refl: "Refl r"
-  using wo_rel.REFL[of r] by simp
+    using wo_rel.REFL[of r] by simp
   have Total: "Total r"
-  using Well wo_rel.TOTAL[of r] by simp
+    using Well wo_rel.TOTAL[of r] by simp
   have Well': "wo_rel r'"
-  using WELL' wo_rel_def[of r'] by simp
+    using WELL' wo_rel_def[of r'] by simp
   hence Antisym': "antisym r'"
-  using wo_rel.ANTISYM[of r'] by simp
+    using wo_rel.ANTISYM[of r'] by simp
   have "(a,a) \<in> r"
-  using **** Well wo_rel.REFL[of r]
-        refl_on_def[of _ r] by auto
+    using **** Well wo_rel.REFL[of r]
+      refl_on_def[of _ r] by auto
   hence "(f a, f a) \<in> r'"
-  using ** by(auto simp add: compat_def)
+    using ** by(auto simp add: compat_def)
   hence 0: "f a \<in> Field r'"
-  unfolding Field_def by auto
+    unfolding Field_def by auto
   have "f a \<in> f`(Field r)"
-  using **** by auto
+    using **** by auto
   hence 2: "under r' (f a) \<le> f`(Field r)"
-  using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
-  (* Main proof *)
+    using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
+      (* Main proof *)
   show "bij_betw f (under r a) (under r' (f a))"
   proof(unfold bij_betw_def, auto)
     show  "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
   next
     fix b assume "b \<in> under r a"
     thus "f b \<in> under r' (f a)"
-    unfolding under_def using **
-    by (auto simp add: compat_def)
+      unfolding under_def using **
+      by (auto simp add: compat_def)
   next
     fix b' assume *****: "b' \<in> under r' (f a)"
     hence "b' \<in> f`(Field r)"
-    using 2 by auto
+      using 2 by auto
     with Field_def[of r] obtain b where
-    3: "b \<in> Field r" and 4: "b' = f b" by auto
+      3: "b \<in> Field r" and 4: "b' = f b" by auto
     have "(b,a) \<in> r"
     proof-
       {assume "(a,b) \<in> r"
-       with ** 4 have "(f a, b') \<in> r'"
-       by (auto simp add: compat_def)
-       with ***** Antisym' have "f a = b'"
-       by(auto simp add: under_def antisym_def)
-       with 3 **** 4 * have "a = b"
-       by(auto simp add: inj_on_def)
+        with ** 4 have "(f a, b') \<in> r'"
+          by (auto simp add: compat_def)
+        with ***** Antisym' have "f a = b'"
+          by(auto simp add: under_def antisym_def)
+        with 3 **** 4 * have "a = b"
+          by(auto simp add: inj_on_def)
       }
       moreover
       {assume "a = b"
-       hence "(b,a) \<in> r" using Refl **** 3
-       by (auto simp add: refl_on_def)
+        hence "(b,a) \<in> r" using Refl **** 3
+          by (auto simp add: refl_on_def)
       }
       ultimately
       show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
     qed
     with 4 show  "b' \<in> f`(under r a)"
-    unfolding under_def by auto
+      unfolding under_def by auto
   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
-        IMAGE: "f ` A = Field r'"
-shows "embed r' r (inv_into A f)"
+  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
+    IMAGE: "f ` A = Field r'"
+  shows "embed r' r (inv_into A f)"
 proof-
   (* Preliminary facts *)
   have Well: "wo_rel r"
-  using WELL wo_rel_def[of r] by simp
+    using WELL wo_rel_def[of r] by simp
   have Refl: "Refl r"
-  using Well wo_rel.REFL[of r] by simp
+    using Well wo_rel.REFL[of r] by simp
   have Total: "Total r"
-  using Well wo_rel.TOTAL[of r] by simp
-  (* Main proof *)
+    using Well wo_rel.TOTAL[of r] by simp
+      (* Main proof *)
   have 1: "bij_betw f A (Field r')"
   proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE)
     fix b1 b2
     assume *: "b1 \<in> A" and **: "b2 \<in> A" and
-           ***: "f b1 = f b2"
+      ***: "f b1 = f b2"
     have 11: "b1 \<in> Field r \<and> b2 \<in> Field r"
-    using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
+      using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
     moreover
     {assume "(b1,b2) \<in> r"
-     hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
-     unfolding under_def using 11 Refl
-     by (auto simp add: refl_on_def)
-     hence "b1 = b2" using BIJ * ** ***
-     by (simp add: bij_betw_def inj_on_def)
+      hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
+        unfolding under_def using 11 Refl
+        by (auto simp add: refl_on_def)
+      hence "b1 = b2" using BIJ * ** ***
+        by (simp add: bij_betw_def inj_on_def)
     }
     moreover
-     {assume "(b2,b1) \<in> r"
-     hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
-     unfolding under_def using 11 Refl
-     by (auto simp add: refl_on_def)
-     hence "b1 = b2" using BIJ * ** ***
-     by (simp add: bij_betw_def inj_on_def)
+    {assume "(b2,b1) \<in> r"
+      hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
+        unfolding under_def using 11 Refl
+        by (auto simp add: refl_on_def)
+      hence "b1 = b2" using BIJ * ** ***
+        by (simp add: bij_betw_def inj_on_def)
     }
     ultimately
     show "b1 = b2"
-    using Total by (auto simp add: total_on_def)
+      using Total by (auto simp add: total_on_def)
   qed
-  (*  *)
+    (*  *)
   let ?f' = "(inv_into A f)"
-  (*  *)
+    (*  *)
   have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)"
   proof(clarify)
     fix b assume *: "b \<in> A"
     hence "under r b \<le> A"
-    using Well OF by(auto simp add: wo_rel.ofilter_def)
+      using Well OF by(auto simp add: wo_rel.ofilter_def)
     moreover
     have "f ` (under r b) = under r' (f b)"
-    using * BIJ by (auto simp add: bij_betw_def)
+      using * BIJ by (auto simp add: bij_betw_def)
     ultimately
     show "bij_betw ?f' (under r' (f b)) (under r b)"
-    using 1 by (auto simp add: bij_betw_inv_into_subset)
+      using 1 by (auto simp add: bij_betw_inv_into_subset)
   qed
-  (*  *)
+    (*  *)
   have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))"
   proof(clarify)
     fix b' assume *: "b' \<in> Field r'"
     have "b' = f (?f' b')" using * 1
-    by (auto simp add: bij_betw_inv_into_right)
+      by (auto simp add: bij_betw_inv_into_right)
     moreover
     {obtain b where 31: "b \<in> A" and "f b = b'" using IMAGE * by force
-     hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)
-     with 31 have "?f' b' \<in> A" by auto
+      hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)
+      with 31 have "?f' b' \<in> A" by auto
     }
     ultimately
     show  "bij_betw ?f' (under r' b') (under r (?f' b'))"
-    using 2 by auto
+      using 2 by auto
   qed
-  (*  *)
+    (*  *)
   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
-        IN: "a \<in> Field r" and
-        IMAGE: "f ` (underS r a) = Field r'"
-shows "embed r' r (inv_into (underS r a) f)"
-using assms
-by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_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
+    IN: "a \<in> Field r" and
+    IMAGE: "f ` (underS r a) = Field r'"
+  shows "embed r' r (inv_into (underS r a) f)"
+  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)"
-shows "embed r' r (inv_into (Field r) f)"
+  assumes WELL: "Well_order r" and EMB: "embed r r' f" and
+    IMAGE: "Field r' \<le> f ` (Field r)"
+  shows "embed r' r (inv_into (Field r) f)"
 proof-
   have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))"
-  using EMB by (auto simp add: embed_def)
+    using EMB by (auto simp add: embed_def)
   moreover
   have "f ` (Field r) \<le> Field r'"
-  using EMB WELL by (auto simp add: embed_Field)
+    using EMB WELL by (auto simp add: embed_Field)
   ultimately
   show ?thesis using assms
-  by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
+    by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
 qed
 
 lemma inv_into_Field_embed_bij_betw:
@@ -487,12 +487,12 @@
 \<close>
 
 lemma wellorders_totally_ordered_aux:
-fixes r ::"'a rel"  and r'::"'a' rel" and
-      f :: "'a \<Rightarrow> 'a'" and a::'a
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
-        IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
-        NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
-shows "bij_betw f (under r a) (under r' (f a))"
+  fixes r ::"'a rel"  and r'::"'a' rel" and
+    f :: "'a \<Rightarrow> 'a'" and a::'a
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
+    IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
+    NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
+  shows "bij_betw f (under r a) (under r' (f a))"
 proof-
   (* Preliminary facts *)
   have Well: "wo_rel r" using WELL unfolding wo_rel_def .
@@ -500,197 +500,197 @@
   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
   have OF: "wo_rel.ofilter r (underS r a)"
-  by (auto simp add: Well wo_rel.underS_ofilter)
+    by (auto simp add: Well wo_rel.underS_ofilter)
   hence UN: "underS r a = (\<Union>b \<in> underS r a. under r b)"
-  using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
-  (* Gather facts about elements of underS r a *)
+    using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
+      (* Gather facts about elements of underS r a *)
   {fix b assume *: "b \<in> underS r a"
-   hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
-   have t1: "b \<in> Field r"
-   using * underS_Field[of r a] by auto
-   have t2: "f`(under r b) = under r' (f b)"
-   using IH * by (auto simp add: bij_betw_def)
-   hence t3: "wo_rel.ofilter r' (f`(under r b))"
-   using Well' by (auto simp add: wo_rel.under_ofilter)
-   have "f`(under r b) \<le> Field r'"
-   using t2 by (auto simp add: under_Field)
-   moreover
-   have "b \<in> under r b"
-   using t1 by(auto simp add: Refl Refl_under_in)
-   ultimately
-   have t4:  "f b \<in> Field r'" by auto
-   have "f`(under r b) = under r' (f b) \<and>
+    hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
+    have t1: "b \<in> Field r"
+      using * underS_Field[of r a] by auto
+    have t2: "f`(under r b) = under r' (f b)"
+      using IH * by (auto simp add: bij_betw_def)
+    hence t3: "wo_rel.ofilter r' (f`(under r b))"
+      using Well' by (auto simp add: wo_rel.under_ofilter)
+    have "f`(under r b) \<le> Field r'"
+      using t2 by (auto simp add: under_Field)
+    moreover
+    have "b \<in> under r b"
+      using t1 by(auto simp add: Refl Refl_under_in)
+    ultimately
+    have t4:  "f b \<in> Field r'" by auto
+    have "f`(under r b) = under r' (f b) \<and>
          wo_rel.ofilter r' (f`(under r b)) \<and>
          f b \<in> Field r'"
-   using t2 t3 t4 by auto
+      using t2 t3 t4 by auto
   }
   hence bFact:
-  "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and>
+    "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and>
                        wo_rel.ofilter r' (f`(under r b)) \<and>
                        f b \<in> Field r'" by blast
-  (*  *)
+    (*  *)
   have subField: "f`(underS r a) \<le> Field r'"
-  using bFact by blast
-  (*  *)
+    using bFact by blast
+      (*  *)
   have OF': "wo_rel.ofilter r' (f`(underS r a))"
   proof-
     have "f`(underS r a) = f`(\<Union>b \<in> underS r a. under r b)"
-    using UN by auto
+      using UN by auto
     also have "\<dots> = (\<Union>b \<in> underS r a. f`(under r b))" by blast
     also have "\<dots> = (\<Union>b \<in> underS r a. (under r' (f b)))"
-    using bFact by auto
+      using bFact by auto
     finally
     have "f`(underS r a) = (\<Union>b \<in> underS r a. (under r' (f b)))" .
     thus ?thesis
-    using Well' bFact
-          wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
+      using Well' bFact
+        wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
   qed
-  (*  *)
+    (*  *)
   have "f`(underS r a) \<union> AboveS r' (f`(underS r a)) = Field r'"
-  using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
+    using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
   hence NE: "AboveS r' (f`(underS r a)) \<noteq> {}"
-  using subField NOT by blast
-  (* Main proof *)
+    using subField NOT by blast
+      (* Main proof *)
   have INCL1: "f`(underS r a) \<le> underS r' (f a) "
   proof(auto)
     fix b assume *: "b \<in> underS r a"
     have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"
-    using subField Well' SUC NE *
-          wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force
+      using subField Well' SUC NE *
+        wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force
     thus "f b \<in> underS r' (f a)"
-    unfolding underS_def by simp
+      unfolding underS_def by simp
   qed
-  (*  *)
+    (*  *)
   have INCL2: "underS r' (f a) \<le> f`(underS r a)"
   proof
     fix b' assume "b' \<in> underS r' (f a)"
     hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"
-    unfolding underS_def by simp
+      unfolding underS_def by simp
     thus "b' \<in> f`(underS r a)"
-    using Well' SUC NE OF'
-          wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto
+      using Well' SUC NE OF'
+        wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto
   qed
-  (*  *)
+    (*  *)
   have INJ: "inj_on f (underS r a)"
   proof-
     have "\<forall>b \<in> underS r a. inj_on f (under r b)"
-    using IH by (auto simp add: bij_betw_def)
+      using IH by (auto simp add: bij_betw_def)
     moreover
     have "\<forall>b. wo_rel.ofilter r (under r b)"
-    using Well by (auto simp add: wo_rel.under_ofilter)
+      using Well by (auto simp add: wo_rel.under_ofilter)
     ultimately show  ?thesis
-    using WELL bFact UN
-          UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
-    by auto
+      using WELL bFact UN
+        UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
+      by auto
   qed
-  (*  *)
+    (*  *)
   have BIJ: "bij_betw f (underS r a) (underS r' (f a))"
-  unfolding bij_betw_def
-  using INJ INCL1 INCL2 by auto
-  (*  *)
+    unfolding bij_betw_def
+    using INJ INCL1 INCL2 by auto
+      (*  *)
   have "f a \<in> Field r'"
-  using Well' subField NE SUC
-  by (auto simp add: wo_rel.suc_inField)
+    using Well' subField NE SUC
+    by (auto simp add: wo_rel.suc_inField)
   thus ?thesis
-  using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
+    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
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and
-MAIN1:
-  "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r'
+  fixes r ::"'a rel"  and r'::"'a' rel" and
+    f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    MAIN1:
+    "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r'
           \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True)
          \<and>
          (\<not>(False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')
           \<longrightarrow> g a = False)" and
-MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
+    MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
               bij_betw f (under r a) (under r' (f a))" and
-Case: "a \<in> Field r \<and> False \<in> g`(under r a)"
-shows "\<exists>f'. embed r' r f'"
+    Case: "a \<in> Field r \<and> False \<in> g`(under r a)"
+  shows "\<exists>f'. embed r' r f'"
 proof-
   have Well: "wo_rel r" using WELL unfolding wo_rel_def .
   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
   have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto
   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
-  (*  *)
+      (*  *)
   have 0: "under r a = underS r a \<union> {a}"
-  using Refl Case by(auto simp add: Refl_under_underS)
-  (*  *)
+    using Refl Case by(auto simp add: Refl_under_underS)
+      (*  *)
   have 1: "g a = False"
   proof-
     {assume "g a \<noteq> False"
-     with 0 Case have "False \<in> g`(underS r a)" by blast
-     with MAIN1 have "g a = False" by blast}
+      with 0 Case have "False \<in> g`(underS r a)" by blast
+      with MAIN1 have "g a = False" by blast}
     thus ?thesis by blast
   qed
   let ?A = "{a \<in> Field r. g a = False}"
   let ?a = "(wo_rel.minim r ?A)"
-  (*  *)
+    (*  *)
   have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast
-  (*  *)
+      (*  *)
   have 3: "False \<notin> g`(underS r ?a)"
   proof
     assume "False \<in> g`(underS r ?a)"
     then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto
     hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"
-    by (auto simp add: underS_def)
+      by (auto simp add: underS_def)
     hence "b \<in> Field r" unfolding Field_def by auto
     with 31 have "b \<in> ?A" by auto
     hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce
-    (* again: why worked without type annotations? *)
+        (* again: why worked without type annotations? *)
     with 32 Antisym show False
-    by (auto simp add: antisym_def)
+      by (auto simp add: antisym_def)
   qed
   have temp: "?a \<in> ?A"
-  using Well 2 wo_rel.minim_in[of r ?A] by auto
+    using Well 2 wo_rel.minim_in[of r ?A] by auto
   hence 4: "?a \<in> Field r" by auto
-  (*   *)
+      (*   *)
   have 5: "g ?a = False" using temp by blast
-  (*  *)
+      (*  *)
   have 6: "f`(underS r ?a) = Field r'"
-  using MAIN1[of ?a] 3 5 by blast
-  (*  *)
+    using MAIN1[of ?a] 3 5 by blast
+      (*  *)
   have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))"
   proof
     fix b assume as: "b \<in> underS r ?a"
     moreover
     have "wo_rel.ofilter r (underS r ?a)"
-    using Well by (auto simp add: wo_rel.underS_ofilter)
+      using Well by (auto simp add: wo_rel.underS_ofilter)
     ultimately
     have "False \<notin> g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
     moreover have "b \<in> Field r"
-    unfolding Field_def using as by (auto simp add: underS_def)
+      unfolding Field_def using as by (auto simp add: underS_def)
     ultimately
     show "bij_betw f (under r b) (under r' (f b))"
-    using MAIN2 by auto
+      using MAIN2 by auto
   qed
-  (*  *)
+    (*  *)
   have "embed r' r (inv_into (underS r ?a) f)"
-  using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
+    using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
   thus ?thesis
-  unfolding embed_def by blast
+    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'"
-shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')"
+  fixes r ::"'a rel"  and r'::"'a' rel"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'"
+  shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')"
 proof-
   (* Preliminary facts *)
   have Well: "wo_rel r" using WELL unfolding wo_rel_def .
   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
-  (* Main proof *)
+      (* Main proof *)
   obtain H where H_def: "H =
   (\<lambda>h a. if False \<notin> (snd \<circ> h)`(underS r a) \<and> (fst \<circ> h)`(underS r a) \<noteq> Field r'
                 then (wo_rel.suc r' ((fst \<circ> h)`(underS r a)), True)
                 else (undefined, False))" by blast
   have Adm: "wo_rel.adm_wo r H"
-  using Well
+    using Well
   proof(unfold wo_rel.adm_wo_def, clarify)
     fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x
     assume "\<forall>y\<in>underS r x. h1 y = h2 y"
@@ -701,52 +701,52 @@
       by (auto simp add: image_def)
     thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
   qed
-  (* More constant definitions:  *)
+    (* More constant definitions:  *)
   obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"
-  where h_def: "h = wo_rel.worec r H" and
-        f_def: "f = fst \<circ> h" and g_def: "g = snd \<circ> h" by blast
+    where h_def: "h = wo_rel.worec r H" and
+      f_def: "f = fst \<circ> h" and g_def: "g = snd \<circ> h" by blast
   obtain test where test_def:
-  "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast
-  (*  *)
+    "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast
+      (*  *)
   have *: "\<And> a. h a  = H h a"
-  using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
+    using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
   have Main1:
-  "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
+    "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
          (\<not>(test a) \<longrightarrow> g a = False)"
   proof-  (* How can I prove this withou fixing a? *)
     fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
                 (\<not>(test a) \<longrightarrow> g a = False)"
-    using *[of a] test_def f_def g_def H_def by auto
+      using *[of a] test_def f_def g_def H_def by auto
   qed
-  (*  *)
+    (*  *)
   let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
                    bij_betw f (under r a) (under r' (f a))"
   have Main2: "\<And> a. ?phi a"
   proof-
     fix a show "?phi a"
     proof(rule wo_rel.well_order_induct[of r ?phi],
-          simp only: Well, clarify)
+        simp only: Well, clarify)
       fix a
       assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and
-             *: "a \<in> Field r" and
-             **: "False \<notin> g`(under r a)"
+        *: "a \<in> Field r" and
+        **: "False \<notin> g`(under r a)"
       have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))"
       proof(clarify)
         fix b assume ***: "b \<in> underS r a"
         hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
         moreover have "b \<in> Field r"
-        using *** underS_Field[of r a] by auto
+          using *** underS_Field[of r a] by auto
         moreover have "False \<notin> g`(under r b)"
-        using 0 ** Trans under_incr[of r b a] by auto
+          using 0 ** Trans under_incr[of r b a] by auto
         ultimately show "bij_betw f (under r b) (under r' (f b))"
-        using IH by auto
+          using IH by auto
       qed
-      (*  *)
+        (*  *)
       have 21: "False \<notin> g`(underS r a)"
-      using ** underS_subset_under[of r a] by auto
+        using ** underS_subset_under[of r a] by auto
       have 22: "g`(under r a) \<le> {True}" using ** by auto
       moreover have 23: "a \<in> under r a"
-      using Refl * by (auto simp add: Refl_under_in)
+        using Refl * by (auto simp add: Refl_under_in)
       ultimately have 24: "g a = True" by blast
       have 2: "f`(underS r a) \<noteq> Field r'"
       proof
@@ -754,29 +754,29 @@
         hence "g a = False" using Main1 test_def by blast
         with 24 show False using ** by blast
       qed
-      (*  *)
+        (*  *)
       have 3: "f a = wo_rel.suc r' (f`(underS r a))"
-      using 21 2 Main1 test_def by blast
-      (*  *)
+        using 21 2 Main1 test_def by blast
+          (*  *)
       show "bij_betw f (under r a) (under r' (f a))"
-      using WELL  WELL' 1 2 3 *
-            wellorders_totally_ordered_aux[of r r' a f] by auto
+        using WELL  WELL' 1 2 3 *
+          wellorders_totally_ordered_aux[of r r' a f] by auto
     qed
   qed
-  (*  *)
+    (*  *)
   let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(under r a))"
   show ?thesis
   proof(cases "\<exists>a. ?chi a")
     assume "\<not> (\<exists>a. ?chi a)"
     hence "\<forall>a \<in> Field r.  bij_betw f (under r a) (under r' (f a))"
-    using Main2 by blast
+      using Main2 by blast
     thus ?thesis unfolding embed_def by blast
   next
     assume "\<exists>a. ?chi a"
     then obtain a where "?chi a" by blast
     hence "\<exists>f'. embed r' r f'"
-    using wellorders_totally_ordered_aux2[of r r' g f a]
-          WELL WELL' Main1 Main2 test_def by fast
+      using wellorders_totally_ordered_aux2[of r r' g f a]
+        WELL WELL' Main1 Main2 test_def by fast
     thus ?thesis by blast
   qed
 qed
@@ -790,75 +790,75 @@
 embeddings of opposite directions are mutually inverse.\<close>
 
 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"
-shows "f a = wo_rel.suc r' (f`(underS r a))"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    EMB: "embed r r' f" and IN: "a \<in> Field r"
+  shows "f a = wo_rel.suc r' (f`(underS r a))"
 proof-
   have "bij_betw f (underS r a) (underS r' (f a))"
-  using assms by (auto simp add: embed_underS)
+    using assms by (auto simp add: embed_underS)
   hence "f`(underS r a) = underS r' (f a)"
-  by (auto simp add: bij_betw_def)
+    by (auto simp add: bij_betw_def)
   moreover
   {have "f a \<in> Field r'" using IN
-   using EMB WELL embed_Field[of r r' f] by auto
-   hence "f a = wo_rel.suc r' (underS r' (f a))"
-   using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
+      using EMB WELL embed_Field[of r r' f] by auto
+    hence "f a = wo_rel.suc r' (underS r' (f a))"
+      using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
   }
   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"
-shows "a \<in> Field r \<longrightarrow> f a = g a"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    EMBf: "embed r r' f" and EMBg: "embed r r' g"
+  shows "a \<in> Field r \<longrightarrow> f a = g a"
 proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def)
   fix a
   assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and
-         *: "a \<in> Field r"
+    *: "a \<in> Field r"
   hence "\<forall>b \<in> underS r a. f b = g b"
-  unfolding underS_def by (auto simp add: Field_def)
+    unfolding underS_def by (auto simp add: Field_def)
   hence "f`(underS r a) = g`(underS r a)" by force
   thus "f a = g a"
-  using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
+    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'"
-shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    EMB: "embed r r' f" and EMB': "embed r' r f'"
+  shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
 proof-
   have "embed r r (f' \<circ> f)" using assms
-  by(auto simp add: comp_embed)
+    by(auto simp add: comp_embed)
   moreover have "embed r r id" using assms
-  by (auto simp add: id_embed)
+    by (auto simp add: id_embed)
   ultimately have "\<forall>a \<in> Field r. f'(f a) = a"
-  using assms embed_unique[of r r "f' \<circ> f" id] id_def by auto
+    using assms embed_unique[of r r "f' \<circ> f" id] id_def by auto
   moreover
   {have "embed r' r' (f \<circ> f')" using assms
-   by(auto simp add: comp_embed)
-   moreover have "embed r' r' id" using assms
-   by (auto simp add: id_embed)
-   ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'"
-   using assms embed_unique[of r' r' "f \<circ> f'" id] id_def by auto
+      by(auto simp add: comp_embed)
+    moreover have "embed r' r' id" using assms
+      by (auto simp add: id_embed)
+    ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'"
+      using assms embed_unique[of r' r' "f \<circ> f'" id] id_def by auto
   }
   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"
-shows "bij_betw f (Field r) (Field r')"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    EMB: "embed r r' f" and EMB': "embed r' r g"
+  shows "bij_betw f (Field r) (Field r')"
 proof-
   let ?A = "Field r"  let ?A' = "Field r'"
   have "embed r r (g \<circ> f) \<and> embed r' r' (f \<circ> g)"
-  using assms by (auto simp add: comp_embed)
+    using assms by (auto simp add: comp_embed)
   hence 1: "(\<forall>a \<in> ?A. g(f a) = a) \<and> (\<forall>a' \<in> ?A'. f(g a') = a')"
-  using WELL id_embed[of r] embed_unique[of r r "g \<circ> f" id]
-        WELL' id_embed[of r'] embed_unique[of r' r' "f \<circ> g" id]
-        id_def by auto
+    using WELL id_embed[of r] embed_unique[of r r "g \<circ> f" id]
+      WELL' id_embed[of r'] embed_unique[of r' r' "f \<circ> g" id]
+      id_def by auto
   have 2: "(\<forall>a \<in> ?A. f a \<in> ?A') \<and> (\<forall>a' \<in> ?A'. g a' \<in> ?A)"
-  using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast
-  (*  *)
+    using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast
+      (*  *)
   show ?thesis
   proof(unfold bij_betw_def inj_on_def, auto simp add: 2)
     fix a b assume *: "a \<in> ?A" "b \<in> ?A" and **: "f a = f b"
@@ -872,24 +872,24 @@
 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"
-shows "iso r r' f"
-unfolding iso_def using assms by (auto simp add: 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"
+  shows "iso r r' f"
+  unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
 
 
 subsection \<open>More properties of embeddings, strict embeddings and isomorphisms\<close>
 
 lemma embed_bothWays_Field_bij_betw:
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and
-        EMB: "embed r r' f" and EMB': "embed r' r f'"
-shows "bij_betw f (Field r) (Field r')"
+  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+    EMB: "embed r r' f" and EMB': "embed r' r f'"
+  shows "bij_betw f (Field r) (Field r')"
 proof-
   have "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
-  using assms by (auto simp add: embed_bothWays_inverse)
+    using assms by (auto simp add: embed_bothWays_inverse)
   moreover
   have "f`(Field r) \<le> Field r' \<and> f' ` (Field r') \<le> Field r"
-  using assms by (auto simp add: embed_Field)
+    using assms by (auto simp add: embed_Field)
   ultimately
   show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
 qed
@@ -928,7 +928,7 @@
   hence 2: "embed r r'' ?g"
     using WELL EMB comp_embed[of r r' f r'' f'] by auto
   moreover have \<section>: "f' ` Field r' \<subseteq> Field r''"
-  by (simp add: "1" embed_Field)
+    by (simp add: "1" embed_Field)
   {assume \<section>: "bij_betw ?g (Field r) (Field r'')"
     hence "embed r'' r ?h" using 2 WELL
       by (auto simp add: inv_into_Field_embed_bij_betw)
@@ -974,57 +974,57 @@
   using assms unfolding iso_def 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'"
+  assumes WELL: "Well_order r" and EMB: "embedS r r' f"
+  shows "f ` (Field r) < Field r'"
 proof-
   have "f`(Field r) \<le> Field r'" using assms
-  by (auto simp add: embed_Field embedS_def)
+    by (auto simp add: embed_Field embedS_def)
   moreover
   {have "inj_on f (Field r)" using assms
-   by (auto simp add: embedS_def embed_inj_on)
-   hence "f`(Field r) \<noteq> Field r'" using EMB
-   by (auto simp add: embedS_def bij_betw_def)
+      by (auto simp add: embedS_def embed_inj_on)
+    hence "f`(Field r) \<noteq> Field r'" using EMB
+      by (auto simp add: embedS_def bij_betw_def)
   }
   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')"
+  assumes WELL: "Well_order r" and ISO: "embed r r' f"
+  shows "embedS r r' f = (f ` (Field r) < Field r')"
 proof
   assume "embedS r r' f"
   thus "f ` Field r \<subset> Field r'"
-  using WELL by (auto simp add: embedS_Field)
+    using WELL by (auto simp add: embedS_Field)
 next
   assume "f ` Field r \<subset> Field r'"
   hence "\<not> bij_betw f (Field r) (Field r')"
-  unfolding bij_betw_def by blast
+    unfolding bij_betw_def by blast
   thus "embedS r r' f" unfolding embedS_def
-  using ISO by auto
+    using ISO by auto
 qed
 
 lemma iso_Field: "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
   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')"
+  assumes "Well_order r"
+  shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')"
 proof
   assume "iso r r' f"
   thus "embed r r' f \<and> f ` (Field r) = Field r'"
-  by (auto simp add: iso_Field iso_def)
+    by (auto simp add: iso_Field iso_def)
 next
   assume *: "embed r r' f \<and> f ` Field r = Field r'"
   hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on)
   with * have "bij_betw f (Field r) (Field r')"
-  unfolding bij_betw_def by simp
+    unfolding bij_betw_def by simp
   with * show "iso r r' f" unfolding iso_def by auto
 qed
 
 lemma iso_iff2: "iso r r' f \<longleftrightarrow>
                  bij_betw f (Field r) (Field r') \<and> 
                  (\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a, b) \<in> r \<longleftrightarrow> (f a, f b) \<in> r')"
-    (is "?lhs = ?rhs")
+  (is "?lhs = ?rhs")
 proof
   assume L: ?lhs
   then have "bij_betw f (Field r) (Field r')" and emb: "embed r r' f"
@@ -1047,31 +1047,31 @@
 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)"
+  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)"
 proof
   assume "iso r r' f"
   thus "bij_betw f (Field r) (Field r') \<and> compat r r' f"
-  unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def)
+    unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def)
 next
   have Well: "wo_rel r \<and> wo_rel r'" using WELL WELL'
-  by (auto simp add: wo_rel_def)
+    by (auto simp add: wo_rel_def)
   assume *: "bij_betw f (Field r) (Field r') \<and> compat r r' f"
   thus "iso r r' f"
-  unfolding "compat_def" using assms
+    unfolding "compat_def" using assms
   proof(auto simp add: iso_iff2)
     fix a b assume **: "a \<in> Field r" "b \<in> Field r" and
-                  ***: "(f a, f b) \<in> r'"
+      ***: "(f a, f b) \<in> r'"
     {assume "(b,a) \<in> r \<or> b = a"
-     hence "(b,a) \<in> r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
-     hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto
-     hence "f a = f b"
-     using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast
-     hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto
-     hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
+      hence "(b,a) \<in> r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
+      hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto
+      hence "f a = f b"
+        using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast
+      hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto
+      hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
     }
     thus "(a,b) \<in> r"
-    using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast
+      using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast
   qed
 qed
 
@@ -1098,12 +1098,7 @@
 
 lemma iso_forward:
   assumes "(x,y) \<in> r" "iso r r' f" shows "(f x,f y) \<in> r'" 
-proof -
-  have "x \<in> Field r" "y \<in> Field r" 
-    using assms by (auto simp: Field_def)
-  with assms show ?thesis unfolding iso_iff2 by blast 
-qed
-
+  using assms by (auto simp: Field_def iso_iff2)
 
 lemma iso_trans:
   assumes "trans r" and iso: "iso r r' f" shows "trans r'"
@@ -1112,7 +1107,7 @@
   fix x y z
   assume xyz: "(x, y) \<in> r'" "(y, z) \<in> r'"
   then have *: "(inv_into (Field r) f x, inv_into (Field r) f y) \<in> r" 
-               "(inv_into (Field r) f y, inv_into (Field r) f z) \<in> r" 
+    "(inv_into (Field r) f y, inv_into (Field r) f z) \<in> r" 
     using iso_backward [OF _ iso] by blast+
   then have "inv_into (Field r) f x \<in> Field r" "inv_into (Field r) f y \<in> Field r"
     by (auto simp: Field_def)
diff -r ec4c38e156c7 -r f881fd264929 src/HOL/BNF_Wellorder_Relation.thy
--- a/src/HOL/BNF_Wellorder_Relation.thy	Fri Jan 13 16:44:00 2023 +0000
+++ b/src/HOL/BNF_Wellorder_Relation.thy	Fri Jan 13 22:47:40 2023 +0000
@@ -8,7 +8,7 @@
 section \<open>Well-Order Relations as Needed by Bounded Natural Functors\<close>
 
 theory BNF_Wellorder_Relation
-imports Order_Relation
+  imports Order_Relation
 begin
 
 text\<open>In this section, we develop basic concepts and results pertaining
@@ -41,35 +41,35 @@
 subsection \<open>Auxiliaries\<close>
 
 lemma REFL: "Refl r"
-using WELL order_on_defs[of _ r] by auto
+  using WELL order_on_defs[of _ r] by auto
 
 lemma TRANS: "trans r"
-using WELL order_on_defs[of _ r] by auto
+  using WELL order_on_defs[of _ r] by auto
 
 lemma ANTISYM: "antisym r"
-using WELL order_on_defs[of _ r] by auto
+  using WELL order_on_defs[of _ r] by auto
 
 lemma TOTAL: "Total r"
-using WELL order_on_defs[of _ r] by auto
+  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
+  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
+  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
+  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>
+  "\<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
+  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);
+  "\<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
+  using TOTALS by auto
 
 
 subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>
@@ -81,34 +81,34 @@
 having to take out the diagonal each time in order to switch to a well-founded relation.\<close>
 
 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"
+  assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
+  shows "P a"
 proof-
   have "\<And>x. \<forall>y. (y, x) \<in> r - Id \<longrightarrow> P y \<Longrightarrow> P x"
-  using IND by blast
+    using IND by blast
   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"
+  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"
+  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)"
+  assumes ADM: "adm_wo H"
+  shows "worec H = H (worec H)"
 proof-
   let ?rS = "r - Id"
   have "adm_wf (r - Id) H"
-  unfolding adm_wf_def
-  using ADM adm_wo_def[of H] underS_def[of r] by auto
+    unfolding adm_wf_def
+    using ADM adm_wo_def[of H] underS_def[of r] by auto
   hence "wfrec ?rS H = H (wfrec ?rS H)"
-  using WF wfrec_fixpoint[of ?rS H] by simp
+    using WF wfrec_fixpoint[of ?rS H] by simp
   thus ?thesis unfolding worec_def .
 qed
 
@@ -127,97 +127,83 @@
 Order filters for well-orders are also known as ``initial segments".\<close>
 
 definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-where "max2 a b \<equiv> if (a,b) \<in> r then b else 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)"
+  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"
+  where "minim A \<equiv> THE b. isMinim A b"
 
 definition supr :: "'a set \<Rightarrow> 'a"
-where "supr A \<equiv> minim (Above A)"
+  where "supr A \<equiv> minim (Above A)"
 
 definition suc :: "'a set \<Rightarrow> 'a"
-where "suc A \<equiv> minim (AboveS A)"
+  where "suc A \<equiv> minim (AboveS A)"
 
 
 subsubsection \<open>Properties of max2\<close>
 
 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}"
+  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}"
 proof-
   {assume "(a,b) \<in> r"
-   hence ?thesis using max2_def assms REFL refl_on_def
-   by (auto simp add: refl_on_def)
+    hence ?thesis using max2_def assms REFL refl_on_def
+      by (auto simp add: refl_on_def)
   }
   moreover
   {assume "a = b"
-   hence "(a,b) \<in> r" using REFL  assms
-   by (auto simp add: refl_on_def)
+    hence "(a,b) \<in> r" using REFL  assms
+      by (auto simp add: refl_on_def)
   }
   moreover
   {assume *: "a \<noteq> b \<and> (b,a) \<in> r"
-   hence "(a,b) \<notin> r" using ANTISYM
-   by (auto simp add: antisym_def)
-   hence ?thesis using * max2_def assms REFL refl_on_def
-   by (auto simp add: refl_on_def)
+    hence "(a,b) \<notin> r" using ANTISYM
+      by (auto simp add: antisym_def)
+    hence ?thesis using * max2_def assms REFL refl_on_def
+      by (auto simp add: refl_on_def)
   }
   ultimately show ?thesis using assms TOTAL
-  total_on_def[of "Field r" r] by blast
+      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)
+  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
+  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)
+  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)"
-using assms ANTISYM unfolding antisym_def using TOTALS
-unfolding max2_def by auto
+  assumes "a \<in> Field r" and "b \<in> Field r"
+  shows "(max2 a b = b) = ((a,b) \<in> r)"
+  using assms ANTISYM unfolding antisym_def using TOTALS
+  unfolding max2_def by auto
 
 lemma in_notinI:
-assumes "(j,i) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
-shows "(i,j) \<in> r" using assms max2_def max2_greater_among by fastforce
+  assumes "(j,i) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
+  shows "(i,j) \<in> r" using assms max2_def max2_greater_among by fastforce
 
 subsubsection \<open>Existence and uniqueness for isMinim and well-definedness of minim\<close>
 
 lemma isMinim_unique:
-assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
-shows "a = a'"
-proof-
-  {have "a \<in> B"
-   using MINIM isMinim_def by simp
-   hence "(a',a) \<in> r"
-   using MINIM' isMinim_def by simp
-  }
-  moreover
-  {have "a' \<in> B"
-   using MINIM' isMinim_def by simp
-   hence "(a,a') \<in> r"
-   using MINIM isMinim_def by simp
-  }
-  ultimately
-  show ?thesis using ANTISYM antisym_def[of r] by blast
-qed
+  assumes "isMinim B a" "isMinim B a'"
+  shows "a = a'"
+  using assms ANTISYM antisym_def[of r] by (auto simp: isMinim_def)
 
 lemma Well_order_isMinim_exists:
-assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
-shows "\<exists>b. isMinim B b"
+  assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
+  shows "\<exists>b. isMinim B b"
 proof-
   from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
     *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
@@ -232,52 +218,46 @@
       moreover have "b' = b \<Longrightarrow> (b, b') \<in> r"
         using ** REFL by (auto simp add: refl_on_def)
       moreover have "b' \<noteq> b \<and> (b',b) \<notin> r \<Longrightarrow> (b,b') \<in> r"
-         using ** TOTAL by (auto simp add: total_on_def)
+        using ** TOTAL by (auto simp add: total_on_def)
       ultimately show "(b,b') \<in> r" by blast
     qed
   qed
-  then have "isMinim B b"
+  then show ?thesis
     unfolding isMinim_def using * by auto
-  then show ?thesis
-    by auto
 qed
 
 lemma minim_isMinim:
-assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
-shows "isMinim B (minim B)"
+  assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
+  shows "isMinim B (minim B)"
 proof-
   let ?phi = "(\<lambda> b. isMinim B b)"
   from assms Well_order_isMinim_exists
   obtain b where *: "?phi b" by blast
   moreover
   have "\<And> b'. ?phi b' \<Longrightarrow> b' = b"
-  using isMinim_unique * by auto
+    using isMinim_unique * by auto
   ultimately show ?thesis
-  unfolding minim_def using theI[of ?phi b] by blast
+    unfolding minim_def using theI[of ?phi b] by blast
 qed
 
 subsubsection\<open>Properties of minim\<close>
 
 lemma minim_in:
-assumes "B \<le> Field r" and "B \<noteq> {}"
-shows "minim B \<in> B"
-proof-
-  from minim_isMinim[of B] assms
-  have "isMinim B (minim B)" by simp
-  thus ?thesis by (simp add: isMinim_def)
-qed
+  assumes "B \<le> Field r" and "B \<noteq> {}"
+  shows "minim B \<in> B"
+  using assms minim_isMinim[of B] by (auto simp: isMinim_def)
 
 lemma minim_inField:
-assumes "B \<le> Field r" and "B \<noteq> {}"
-shows "minim B \<in> Field r"
+  assumes "B \<le> Field r" and "B \<noteq> {}"
+  shows "minim B \<in> Field r"
 proof-
   have "minim B \<in> B" using assms by (simp add: minim_in)
   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"
+  assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
+  shows "(minim B, b) \<in> r"
 proof-
   from minim_isMinim[of B] assms
   have "isMinim B (minim B)" by auto
@@ -285,137 +265,104 @@
 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"
-shows "a = minim B"
+  assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
+    LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
+  shows "a = minim B"
 proof-
   from minim_isMinim[of B] assms
   have "isMinim B (minim B)" by auto
   moreover have "isMinim B a" using IN LEAST isMinim_def by auto
   ultimately show ?thesis
-  using isMinim_unique by auto
+    using isMinim_unique by auto
 qed
 
 subsubsection\<open>Properties of successor\<close>
 
 lemma suc_AboveS:
-assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
-shows "suc B \<in> AboveS B"
+  assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
+  shows "suc B \<in> AboveS B"
 proof(unfold suc_def)
   have "AboveS B \<le> Field r"
-  using AboveS_Field[of r] by auto
+    using AboveS_Field[of r] by auto
   thus "minim (AboveS B) \<in> AboveS B"
-  using assms by (simp add: minim_in)
+    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"
-shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
-proof-
-  from assms suc_AboveS
-  have "suc B \<in> AboveS B" by simp
-  with IN AboveS_def[of r] show ?thesis by simp
-qed
+  assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and IN: "b \<in> B"
+  shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
+  using IN AboveS_def[of r] assms suc_AboveS by auto
 
 lemma suc_least_AboveS:
-assumes ABOVES: "a \<in> AboveS B"
-shows "(suc B,a) \<in> r"
-proof(unfold suc_def)
-  have "AboveS B \<le> Field r"
-  using AboveS_Field[of r] by auto
-  thus "(minim (AboveS B),a) \<in> r"
-  using assms minim_least by simp
-qed
+  assumes ABOVES: "a \<in> AboveS B"
+  shows "(suc B,a) \<in> r"
+  using assms minim_least AboveS_Field[of r] by (auto simp: suc_def)
 
 lemma suc_inField:
-assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
-shows "suc B \<in> Field r"
-proof-
-  have "suc B \<in> AboveS B" using suc_AboveS assms by simp
-  thus ?thesis
-  using assms AboveS_Field[of r] by auto
-qed
+  assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
+  shows "suc B \<in> Field r"
+  using suc_AboveS assms AboveS_Field[of r] by auto
 
 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"
-shows "a = suc B"
-proof(unfold suc_def)
-  have "AboveS B \<le> Field r"
-  using AboveS_Field[of r B] by auto
-  thus "a = minim (AboveS B)"
-  using assms equals_minim
-  by simp
-qed
+  assumes "B \<le> Field r" and "a \<in> AboveS B" and "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
+  shows "a = suc B"
+  using assms equals_minim AboveS_Field[of r B] by (auto simp: suc_def)
 
 lemma suc_underS:
-assumes IN: "a \<in> Field r"
-shows "a = suc (underS a)"
+  assumes IN: "a \<in> Field r"
+  shows "a = suc (underS a)"
 proof-
   have "underS a \<le> Field r"
-  using underS_Field[of r] by auto
+    using underS_Field[of r] by auto
   moreover
   have "a \<in> AboveS (underS a)"
-  using in_AboveS_underS IN by fast
+    using in_AboveS_underS IN by fast
   moreover
   have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
   proof(clarify)
     fix a'
     assume *: "a' \<in> AboveS (underS a)"
     hence **: "a' \<in> Field r"
-    using AboveS_Field by fast
+      using AboveS_Field by fast
     {assume "(a,a') \<notin> r"
-     hence "a' = a \<or> (a',a) \<in> r"
-     using TOTAL IN ** by (auto simp add: total_on_def)
-     moreover
-     {assume "a' = a"
-      hence "(a,a') \<in> r"
-      using REFL IN ** by (auto simp add: refl_on_def)
-     }
-     moreover
-     {assume "a' \<noteq> a \<and> (a',a) \<in> r"
-      hence "a' \<in> underS a"
-      unfolding underS_def by simp
-      hence "a' \<notin> AboveS (underS a)"
-      using AboveS_disjoint by fast
-      with * have False by simp
-     }
-     ultimately have "(a,a') \<in> r" by blast
+      hence "a' = a \<or> (a',a) \<in> r"
+        using TOTAL IN ** by (auto simp add: total_on_def)
+      moreover
+      {assume "a' = a"
+        hence "(a,a') \<in> r"
+          using REFL IN ** by (auto simp add: refl_on_def)
+      }
+      moreover
+      {assume "a' \<noteq> a \<and> (a',a) \<in> r"
+        hence "a' \<in> underS a"
+          unfolding underS_def by simp
+        hence "a' \<notin> AboveS (underS a)"
+          using AboveS_disjoint by fast
+        with * have False by simp
+      }
+      ultimately have "(a,a') \<in> r" by blast
     }
     thus  "(a, a') \<in> r" by blast
   qed
   ultimately show ?thesis
-  using equals_suc_AboveS by auto
+    using equals_suc_AboveS by auto
 qed
 
 
 subsubsection \<open>Properties of order filters\<close>
 
-lemma under_ofilter:
-"ofilter (under a)"
-proof -
-  have "\<And>aa x. (aa, a) \<in> r \<Longrightarrow> (x, aa) \<in> r \<Longrightarrow> (x, a) \<in> r"
-  proof -
-    fix aa x
-    assume "(aa,a) \<in> r" "(x,aa) \<in> r"
-    then show "(x,a) \<in> r"
-      using TRANS trans_def[of r] by blast
-  qed
-  then show ?thesis unfolding ofilter_def under_def
-    by (auto simp add: Field_def)
-qed
+lemma under_ofilter: "ofilter (under a)"
+  using TRANS by (auto simp: ofilter_def under_def Field_iff trans_def)
 
-lemma underS_ofilter:
-"ofilter (underS a)"
+lemma underS_ofilter: "ofilter (underS a)"
   unfolding ofilter_def underS_def under_def
 proof safe
-  fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
+  fix b assume "(a, b) \<in> r" "(b, a) \<in> r" and DIFF: "b \<noteq> a"
   thus False
-  using ANTISYM antisym_def[of r] by blast
+    using ANTISYM antisym_def[of r] by blast
 next
-  fix aa x
-  assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
+  fix b x
+  assume "(b,a) \<in> r" "b \<noteq> a" "(x,b) \<in> r"
   thus "(x,a) \<in> r"
     using TRANS trans_def[of r] by blast
 next
@@ -427,15 +374,15 @@
 qed
 
 lemma Field_ofilter:
-"ofilter (Field r)"
-by(unfold ofilter_def under_def, auto simp add: Field_def)
+  "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))"
+  "ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
 proof
   assume "(\<exists>a\<in>Field r. A = underS a) \<or> A = Field r"
   thus "ofilter A"
-  by (auto simp: underS_ofilter Field_ofilter)
+    by (auto simp: underS_ofilter Field_ofilter)
 next
   assume *: "ofilter A"
   let ?One = "(\<exists>a\<in>Field r. A = underS a)"
@@ -451,7 +398,7 @@
     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 by auto
-    (*  *)
+        (*  *)
     moreover
     have "A = underS ?a"
     proof
@@ -462,12 +409,12 @@
         have 12: "x \<noteq> ?a" using 4 ** by auto
         have 13: "under x \<le> A" using * ofilter_def ** by auto
         {assume "(x,?a) \<notin> r"
-         hence "(?a,x) \<in> r"
-         using TOTAL total_on_def[of "Field r" r]
-               2 4 11 12 by auto
-         hence "?a \<in> under x" using under_def[of r] by auto
-         hence "?a \<in> A" using ** 13 by blast
-         with 4 have False by simp
+          hence "(?a,x) \<in> r"
+            using TOTAL total_on_def[of "Field r" r]
+              2 4 11 12 by auto
+          hence "?a \<in> under x" using under_def[of r] by auto
+          hence "?a \<in> A" using ** 13 by blast
+          with 4 have False by simp
         }
         then have "(x,?a) \<in> r" by blast
         thus "x \<in> underS ?a"
@@ -479,13 +426,13 @@
         fix x
         assume **: "x \<in> underS ?a"
         hence 11: "x \<in> Field r"
-         using Field_def unfolding underS_def by fastforce
-         {assume "x \<notin> A"
+          using Field_def unfolding underS_def by fastforce
+        {assume "x \<notin> A"
           hence "x \<in> ?B" using 11 by auto
           hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
           hence False
-          using ANTISYM antisym_def[of r] ** unfolding underS_def by auto
-         }
+            using ANTISYM antisym_def[of r] ** unfolding underS_def by auto
+        }
         thus "x \<in> A" by blast
       qed
     qed
@@ -499,27 +446,27 @@
 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
+  "(\<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)"
+  assumes "ofilter A"
+  shows "A = (\<Union>a \<in> A. under a)"
 proof
   have "\<forall>a \<in> A. under a \<le> A"
-  using assms ofilter_def by auto
+    using assms ofilter_def by auto
   thus "(\<Union>a \<in> A. under a) \<le> A" by blast
 next
   have "\<forall>a \<in> A. a \<in> under a"
-  using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
+    using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
   thus "A \<le> (\<Union>a \<in> A. under a)" by blast
 qed
 
 subsubsection\<open>Other properties\<close>
 
 lemma ofilter_linord:
-assumes OF1: "ofilter A" and OF2: "ofilter B"
-shows "A \<le> B \<or> B \<le> A"
+  assumes OF1: "ofilter A" and OF2: "ofilter B"
+  shows "A \<le> B \<or> B \<le> A"
 proof(cases "A = Field r")
   assume Case1: "A = Field r"
   hence "B \<le> A" using OF2 ofilter_def by auto
@@ -527,7 +474,7 @@
 next
   assume Case2: "A \<noteq> Field r"
   with ofilter_underS_Field OF1 obtain a where
-  1: "a \<in> Field r \<and> A = underS a" by auto
+    1: "a \<in> Field r \<and> A = underS a" by auto
   show ?thesis
   proof(cases "B = Field r")
     assume Case21: "B = Field r"
@@ -536,68 +483,68 @@
   next
     assume Case22: "B \<noteq> Field r"
     with ofilter_underS_Field OF2 obtain b where
-    2: "b \<in> Field r \<and> B = underS b" by auto
+      2: "b \<in> Field r \<and> B = underS b" by auto
     have "a = b \<or> (a,b) \<in> r \<or> (b,a) \<in> r"
-    using 1 2 TOTAL total_on_def[of _ r] by auto
+      using 1 2 TOTAL total_on_def[of _ r] by auto
     moreover
     {assume "a = b" with 1 2 have ?thesis by auto
     }
     moreover
     {assume "(a,b) \<in> r"
-     with underS_incr[of r] TRANS ANTISYM 1 2
-     have "A \<le> B" by auto
-     hence ?thesis by auto
+      with underS_incr[of r] TRANS ANTISYM 1 2
+      have "A \<le> B" by auto
+      hence ?thesis by auto
     }
     moreover
-     {assume "(b,a) \<in> r"
-     with underS_incr[of r] TRANS ANTISYM 1 2
-     have "B \<le> A" by auto
-     hence ?thesis by auto
+    {assume "(b,a) \<in> r"
+      with underS_incr[of r] TRANS ANTISYM 1 2
+      have "B \<le> A" by auto
+      hence ?thesis by auto
     }
     ultimately show ?thesis by blast
   qed
 qed
 
 lemma ofilter_AboveS_Field:
-assumes "ofilter A"
-shows "A \<union> (AboveS A) = Field r"
+  assumes "ofilter A"
+  shows "A \<union> (AboveS A) = Field r"
 proof
   show "A \<union> (AboveS A) \<le> Field r"
-  using assms ofilter_def AboveS_Field[of r] by auto
+    using assms ofilter_def AboveS_Field[of r] by auto
 next
   {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
-   {fix y assume ***: "y \<in> A"
-    with ** have 1: "y \<noteq> x" by auto
-    {assume "(y,x) \<notin> r"
-     moreover
-     have "y \<in> Field r" using assms ofilter_def *** by auto
-     ultimately have "(x,y) \<in> r"
-     using 1 * TOTAL total_on_def[of _ r] by auto
-     with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
-     with ** have False by contradiction
+    {fix y assume ***: "y \<in> A"
+      with ** have 1: "y \<noteq> x" by auto
+      {assume "(y,x) \<notin> r"
+        moreover
+        have "y \<in> Field r" using assms ofilter_def *** by auto
+        ultimately have "(x,y) \<in> r"
+          using 1 * TOTAL total_on_def[of _ r] by auto
+        with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
+        with ** have False by contradiction
+      }
+      hence "(y,x) \<in> r" by blast
+      with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
     }
-    hence "(y,x) \<in> r" by blast
-    with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
-   }
-   with * have "x \<in> AboveS A" unfolding AboveS_def by auto
+    with * have "x \<in> AboveS A" unfolding AboveS_def by auto
   }
   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"
-shows "b \<in> A"
+  assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
+    REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
+  shows "b \<in> A"
 proof-
   have *: "suc A \<in> Field r \<and> b \<in> Field r"
-  using WELL REL well_order_on_domain[of "Field r"] by auto
+    using WELL REL well_order_on_domain[of "Field r"] by auto
   {assume **: "b \<notin> A"
-   hence "b \<in> AboveS A"
-   using OF * ofilter_AboveS_Field by auto
-   hence "(suc A, b) \<in> r"
-   using suc_least_AboveS by auto
-   hence False using REL DIFF ANTISYM *
-   by (auto simp add: antisym_def)
+    hence "b \<in> AboveS A"
+      using OF * ofilter_AboveS_Field by auto
+    hence "(suc A, b) \<in> r"
+      using suc_least_AboveS by auto
+    hence False using REL DIFF ANTISYM *
+      by (auto simp add: antisym_def)
   }
   thus ?thesis by blast
 qed
diff -r ec4c38e156c7 -r f881fd264929 src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jan 13 16:44:00 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jan 13 22:47:40 2023 +0000
@@ -182,7 +182,7 @@
 
 subsection \<open>The maxim among a finite set of ordinals\<close>
 
-text \<open>The correct phrasing would be ``a maxim of \<dots>", as \<open>\<le>o\<close> is only a preorder.\<close>
+text \<open>The correct phrasing would be ``a maxim of ...", as \<open>\<le>o\<close> is only a preorder.\<close>
 
 definition isOmax :: "'a rel set \<Rightarrow> 'a rel \<Rightarrow> bool"
   where
@@ -211,23 +211,19 @@
     next
       case False
       then obtain p where p: "isOmax R p" using IH by auto
-      hence 1: "Well_order p" using **** unfolding isOmax_def by simp
-      {assume Case21: "r \<le>o p"
-        hence "isOmax ?R' p" using p unfolding isOmax_def by simp
-        hence ?thesis by auto
-      }
-      moreover
-      {assume Case22: "p \<le>o r"
-        { fix r' assume "r' \<in> ?R'"
-          then have "r' \<le>o r"
-            by (metis "***" Case22 insert_iff isOmax_def ordLeq_transitive p ordLeq_reflexive)
-        }
-        hence "isOmax ?R' r" unfolding isOmax_def by simp
-        hence ?thesis by auto
-      }
-      moreover have "r \<le>o p \<or> p \<le>o r"
-        using 1 *** ordLeq_total by auto
-      ultimately show ?thesis by blast
+      hence  "Well_order p" using **** unfolding isOmax_def by simp
+      then consider  "r \<le>o p" | "p \<le>o r"
+        using *** ordLeq_total by auto
+      then show ?thesis 
+      proof cases
+        case 1
+        then show ?thesis
+         using p unfolding isOmax_def by auto
+      next
+        case 2
+        then show ?thesis
+          by (metis "***" insert_iff isOmax_def ordLeq_reflexive ordLeq_transitive p)
+      qed
     qed
   qed
   thus ?thesis using assms by auto