src/HOL/BNF_Constructions_on_Wellorders.thy

 header {* Constructions on Wellorders as Needed by Bounded Natural Functors *}
 
 theory BNF_Constructions_on_Wellorders
 imports BNF_Wellorder_Embedding
 begin
-
 
 text {* In this section, we study basic constructions on well-orders, such as restriction to
 a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,
 and bounded square.  We also define between well-orders
 the relations @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"}),
 @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and
 @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).  We study the
 connections between these relations, order filters, and the aforementioned constructions.
-A main result of this section is that @{text "<o"} is well-founded.  *}
-
-
-subsection {* Restriction to a set  *}
-
+A main result of this section is that @{text "<o"} is well-founded. *}
+
+
+subsection {* Restriction to a set *}
 
 abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel"
 where "Restr r A \<equiv> r Int (A \<times> A)"
-
 
 lemma Restr_subset:
 "A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"
 by blast
 
-
 lemma Restr_Field: "Restr r (Field r) = r"
 unfolding Field_def by auto
 
-
 lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
 unfolding refl_on_def Field_def by auto
-
 
 lemma antisym_Restr:
 "antisym r \<Longrightarrow> antisym(Restr r A)"
 unfolding antisym_def Field_def by auto
 
-
 lemma Total_Restr:
 "Total r \<Longrightarrow> Total(Restr r A)"
 unfolding total_on_def Field_def by auto
 
-
 lemma trans_Restr:
 "trans r \<Longrightarrow> trans(Restr r A)"
 unfolding trans_def Field_def by blast
 
-
 lemma Preorder_Restr:
 "Preorder r \<Longrightarrow> Preorder(Restr r A)"
 unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)
 
-
 lemma Partial_order_Restr:
 "Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
 unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)
 
-
 lemma Linear_order_Restr:
 "Linear_order r \<Longrightarrow> Linear_order(Restr r A)"
 unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)
-
 
 lemma Well_order_Restr:
 assumes "Well_order r"
 shows "Well_order(Restr r A)"
 proof-

   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
 
-
 lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
 by (auto simp add: Field_def)
-
 
 lemma Refl_Field_Restr:
 "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
 unfolding refl_on_def Field_def by blast
 
-
 lemma Refl_Field_Restr2:
 "\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
 by (auto simp add: Refl_Field_Restr)
-
 
 lemma well_order_on_Restr:
 assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
 shows "well_order_on A (Restr r A)"
 using assms
 using Well_order_Restr[of r A] Refl_Field_Restr2[of r A]
      order_on_defs[of "Field r" r] by auto
 
 
-subsection {* Order filters versus restrictions and embeddings  *}
-
+subsection {* Order filters versus restrictions and embeddings *}
 
 lemma Field_Restr_ofilter:
 "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
 by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2)
-
 
 lemma ofilter_Restr_under:
 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
 shows "under (Restr r A) a = under r a"
 using assms wo_rel_def

   fix b assume *: "a \<in> A" and "(b,a) \<in> r"
   hence "b \<in> under r a \<and> a \<in> Field r"
   unfolding under_def using Field_def by fastforce
   thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
 qed
-
 
 lemma ofilter_embed:
 assumes "Well_order r"
 shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"
 proof

    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)"
 proof-
   let ?rB = "Restr r B"

     fix a b assume "a \<in> A" and "(b,a) \<in> r"
     thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def)
   qed
 qed
 
-
 lemma ofilter_Restr_subset:
 assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B"
 shows "wo_rel.ofilter (Restr r B) A"
 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)"

     }
     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>
        ((A = B) = (iso (Restr r A) (Restr r B) id))"

   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
 qed
 
-
 lemma ofilter_subset_embedS:
 assumes WELL: "Well_order r" and
         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
 shows "(A < B) = embedS (Restr r A) (Restr r B) id"
 using assms by (simp add: ofilter_subset_embedS_iso)
-
 
 lemma embed_implies_iso_Restr:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r' r f"
 shows "iso r' (Restr r (f ` (Field r'))) f"

 qed
 
 
 subsection {* The strict inclusion on proper ofilters is well-founded *}
 
-
 definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel"
 where
 "ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and>
                          wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}"
-
 
 lemma wf_ofilterIncl:
 assumes WELL: "Well_order r"
 shows "wf(ofilterIncl r)"
 proof-

   qed
   ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf)
 qed
 
 
-
 subsection {* Ordering the well-orders by existence of embeddings *}
-
 
 text {* We define three relations between well-orders:
 \begin{itemize}
 \item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"});
 \item @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"});

 The prefix "ord" and the index "o" in these names stand for "ordinal-like".
 These relations shall be proved to be inter-connected in a similar fashion as the trio
 @{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set.
 *}
 
-
 definition ordLeq :: "('a rel * 'a' rel) set"
 where
 "ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}"
 
-
 abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50)
 where "r <=o r' \<equiv> (r,r') \<in> ordLeq"
 
-
 abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50)
 where "r \<le>o r' \<equiv> r <=o r'"
-
 
 definition ordLess :: "('a rel * 'a' rel) set"
 where
 "ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"
 
 abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
 where "r <o r' \<equiv> (r,r') \<in> ordLess"
 
-
 definition ordIso :: "('a rel * 'a' rel) set"
 where
 "ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"
 
 abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
 where "r =o r' \<equiv> (r,r') \<in> ordIso"
-
 
 lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def
 
 lemma ordLeq_Well_order_simp:
 assumes "r \<le>o r'"
 shows "Well_order r \<and> Well_order r'"
 using assms unfolding ordLeq_def by simp
 
-
 text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
 on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
 restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,
-to @{text "'a rel rel"}.  *}
-
+to @{text "'a rel rel"}. *}
 
 lemma ordLeq_reflexive:
 "Well_order r \<Longrightarrow> r \<le>o r"
 unfolding ordLeq_def using id_embed[of r] by blast
-
 
 lemma ordLeq_transitive[trans]:
 assumes *: "r \<le>o r'" and **: "r' \<le>o r''"
 shows "r \<le>o r''"
 proof-

   hence "embed r r'' (f' o 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
 
-
 lemma ordLeq_total:
 "\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r"
 unfolding ordLeq_def using wellorders_totally_ordered by blast
 
-
 lemma ordIso_reflexive:
 "Well_order r \<Longrightarrow> r =o r"
 unfolding ordIso_def using id_iso[of r] by blast
-
 
 lemma ordIso_transitive[trans]:
 assumes *: "r =o r'" and **: "r' =o r''"
 shows "r =o r''"
 proof-

   hence "iso r r'' (f' o f)"
   using comp_iso[of r r' f r'' f'] by auto
   thus "r =o r''" unfolding ordIso_def using 1 by auto
 qed
 
-
 lemma ordIso_symmetric:
 assumes *: "r =o r'"
 shows "r' =o r"
 proof-
   obtain f where 1: "Well_order r \<and> Well_order r'" and

   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)
   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''"
 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 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
 
-
 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
 
-
 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
 
-
 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
 
-
 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
-
 
 lemma ordLess_not_embed:
 assumes "r <o r'"
 shows "\<not>(\<exists>f'. embed r' r f')"
 proof-

    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)"
 proof-

   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'))"
 proof
   assume *: "r <o r'"

   }
   ultimately show "(r,r') \<in> ordLess"
   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
 
-
 lemma ordLeq_iff_ordLess_or_ordIso:
 "r \<le>o r' = (r <o r' \<or> r =o r')"
 unfolding ordRels_def embedS_defs iso_defs by blast
-
 
 lemma ordIso_iff_ordLeq:
 "(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"
 proof
   assume "r =o r'"

   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
-
 
 lemma ordLess_or_ordLeq:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "r <o r' \<or> r' \<le>o r"
 proof-

    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 assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
-
 
 lemma not_ordLeq_iff_ordLess:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "(\<not> r' \<le>o r) = (r <o r')"
 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
 
-
 lemma not_ordLess_iff_ordLeq:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
 shows "(\<not> r' <o r) = (r \<le>o r')"
 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
 
-
 lemma ordLess_transitive[trans]:
 "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
 using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
 
-
 corollary ordLess_trans: "trans ordLess"
 unfolding trans_def using ordLess_transitive by blast
 
-
 lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric
-
 
 lemma ordIso_imp_ordLeq:
 "r =o r' \<Longrightarrow> r \<le>o r'"
 using ordIso_iff_ordLeq by blast
 
-
 lemma ordLess_imp_ordLeq:
 "r <o r' \<Longrightarrow> r \<le>o r'"
 using ordLeq_iff_ordLess_or_ordIso by blast
-
 
 lemma ofilter_subset_ordLeq:
 assumes WELL: "Well_order r" and
         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
 shows "(A \<le> B) = (Restr r A \<le>o Restr r B)"

   }
   thus "A \<le> B" using OFA OFB WELL
   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)"
 proof-

   also have "\<dots> = (Restr r A <o Restr r B)"
   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)
 
-
 corollary underS_Restr_ordLess:
 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)
   thus ?thesis using assms
   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"

   (*  *)
   with 5 6 show ?thesis
   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))"
 proof(auto)
   fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"

   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)"
 proof
   assume *: "r' <o r"
   hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto

 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)"
 proof
   assume *: "r' \<le>o r"
   moreover

 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')"
 proof(auto)
   assume *: "r \<le>o r'"

    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'"
 proof-

    unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
    hence False using finite_imageD finite_subset FIN INF by metis
   }
   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'"

     thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto
   qed
   ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis
 qed
 
-
 subsection{* @{text "<o"} is well-founded *}
-
 
 text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded
 on the restricted type @{text "'a rel rel"}.  We prove this by first showing that, for any set
 of well-orders all embedded in a fixed well-order, the function mapping each well-order
 in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus
 {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded. *}
 
-
 definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"
 where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)"
-
 
 lemma ord_to_filter_compat:
 "compat (ordLess Int (ordLess^-1``{r0} \<times> ordLess^-1``{r0}))
         (ofilterIncl r0)
         (ord_to_filter r0)"

   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)
 qed
-
 
 theorem wf_ordLess: "wf ordLess"
 proof-
   {fix r0 :: "('a \<times> 'a) set"
    (* need to annotate here!*)

     equals0I[of R] by blast
   with not_ordLeq_iff_ordLess WELL show ?thesis by blast
 qed
 
 
-
-subsection {* Copy via direct images  *}
-
+subsection {* Copy via direct images *}
 
 text{* The direct image operator is the dual of the inverse image operator @{text "inv_image"}
 from @{text "Relation.thy"}.  It is useful for transporting a well-order between
 different types. *}
 
-
 definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"
 where
 "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
 
-
 lemma dir_image_Field:
 "Field(dir_image r f) \<le> f ` (Field r)"
 unfolding dir_image_def Field_def by auto
 
-
 lemma dir_image_minus_Id:
 "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
 unfolding inj_on_def Field_def dir_image_def by auto
-
 
 lemma Refl_dir_image:
 assumes "Refl r"
 shows "Refl(dir_image r f)"
 proof-

    unfolding dir_image_def by auto
   }
   thus ?thesis
   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)"
 proof(unfold trans_def, auto)

   hence "(a,c): 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
 qed
 
-
 lemma Preorder_dir_image:
 "\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)"
 by (simp add: preorder_on_def Refl_dir_image trans_dir_image)
-
 
 lemma antisym_dir_image:
 assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
 shows "antisym(dir_image r f)"
 proof(unfold antisym_def, auto)

   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)
-
 
 lemma Total_dir_image:
 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)

   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
 qed
 
-
 lemma Linear_order_dir_image:
 "\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)"
 by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image)
-
 
 lemma wf_dir_image:
 assumes WF: "wf r" and INJ: "inj_on f (Field r)"
 shows "wf(dir_image r f)"
 proof(unfold wf_eq_minimal2, intro allI impI, elim conjE)

   qed
   thus "\<exists>a'\<in>A'. \<forall>b'\<in>A'. (b', a') \<notin> dir_image r f"
   using A_def 1 by blast
 qed
 
-
 lemma Well_order_dir_image:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
 using assms unfolding well_order_on_def
 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_Field2:
 "Refl r \<Longrightarrow> Field(dir_image r f) = f ` (Field r)"
 unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast
-
 
 lemma dir_image_bij_betw:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
 unfolding bij_betw_def
 by (simp add: dir_image_Field2 order_on_defs)
 
-
 lemma dir_image_compat:
 "compat r (dir_image r f) f"
 unfolding compat_def dir_image_def by auto
 
-
 lemma dir_image_iso:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> iso r (dir_image r f) f"
 using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast
 
-
 lemma dir_image_ordIso:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> r =o dir_image r f"
 unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast
-
 
 lemma Well_order_iso_copy:
 assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'"
 shows "\<exists>r'. well_order_on A' r' \<and> r =o r'"
 proof-

    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
 
 
-
-subsection {* Bounded square  *}
-
+subsection {* Bounded square *}
 
 text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic
 order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the
 following criteria (in this order):
 \begin{itemize}

 at proving that the square of an infinite set has the same cardinal
 as that set. The essential property required there (and which is ensured by this
 construction) is that any proper order filter of the product order is included in a rectangle, i.e.,
 in a product of proper filters on the original relation (assumed to be a well-order). *}
 
-
 definition bsqr :: "'a rel => ('a * 'a)rel"
 where
 "bsqr r = {((a1,a2),(b1,b2)).
            {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>
             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
            )}"
-
 
 lemma Field_bsqr:
 "Field (bsqr r) = Field r \<times> Field r"
 proof
   show "Field (bsqr r) \<le> Field r \<times> Field r"

     hence "((a1,a2),(a1,a2)) \<in> bsqr r" unfolding bsqr_def by blast
     thus "(a1,a2) \<in> Field (bsqr r)" unfolding Field_def by auto
   qed
 qed
 
-
 lemma bsqr_Refl: "Refl(bsqr r)"
 by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
-
 
 lemma bsqr_Trans:
 assumes "Well_order r"
 shows "trans (bsqr r)"
 proof(unfold trans_def, auto)

     }
     ultimately show ?thesis using 0 1 by auto
   qed
 qed
 
-
 lemma bsqr_antisym:
 assumes "Well_order r"
 shows "antisym (bsqr r)"
 proof(unfold antisym_def, clarify)
   (* Preliminary facts *)

      ultimately have ?thesis using 0 2 by auto
     }
     ultimately show ?thesis using 0 1 by blast
   qed
 qed
-
 
 lemma bsqr_Total:
 assumes "Well_order r"
 shows "Total(bsqr r)"
 proof-

    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
-
 
 lemma bsqr_Well_order:
 assumes "Well_order r"
 shows "Well_order(bsqr r)"
 using assms

   }
   (*  *)
   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"
 proof-
   have "{(a1,a2),(b1,b2)} \<le> Field(bsqr r)"

   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
   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)"