# Theory Constructions_on_Wellorders

Up to index of Isabelle/HOL/Free-Groups

theory Constructions_on_Wellorders
imports Constructions_on_Wellorders_Base Wellorder_Embedding
`(*  Title:      HOL/Cardinals/Constructions_on_Wellorders.thy    Author:     Andrei Popescu, TU Muenchen    Copyright   2012Constructions on wellorders.*)header {* Constructions on Wellorders *}theory Constructions_on_Wellordersimports Constructions_on_Wellorders_Base Wellorder_Embeddingbegindeclare  ordLeq_Well_order_simp[simp]  ordLess_Well_order_simp[simp]  ordIso_Well_order_simp[simp]  not_ordLeq_iff_ordLess[simp]  not_ordLess_iff_ordLeq[simp]subsection {* Restriction to a set  *}lemma Restr_incr2:"r <= r' ==> Restr r A <= Restr r' A"by blastlemma Restr_incr:"[|r ≤ r'; A ≤ A'|] ==> Restr r A ≤ Restr r' A'"by blastlemma Restr_Int:"Restr (Restr r A) B = Restr r (A Int B)"by blastlemma Restr_iff: "(a,b) : Restr r A = (a : A ∧ b : A ∧ (a,b) : r)"by (auto simp add: Field_def)lemma Restr_subset1: "Restr r A ≤ r"by autolemma Restr_subset2: "Restr r A ≤ A × A"by autolemma wf_Restr:"wf r ==> wf(Restr r A)"using wf_subset Restr_subset by blastlemma Restr_incr1:"A ≤ B ==> Restr r A ≤ Restr r B"by blastsubsection {* Order filters versus restrictions and embeddings  *}lemma ofilter_Restr:assumes WELL: "Well_order r" and        OFA: "ofilter r A" and OFB: "ofilter r B" and SUB: "A ≤ B"shows "ofilter (Restr r B) A"proof-  let ?rB = "Restr r B"  have Well: "wo_rel r" unfolding wo_rel_def using WELL .  hence Refl: "Refl r" by (auto simp add: wo_rel.REFL)  hence Field: "Field ?rB = Field r Int B"  using Refl_Field_Restr by blast  have WellB: "wo_rel ?rB ∧ Well_order ?rB" using WELL  by (auto simp add: Well_order_Restr wo_rel_def)  (* Main proof *)  show ?thesis  proof(auto simp add: WellB wo_rel.ofilter_def)    fix a assume "a ∈ A"    hence "a ∈ Field r ∧ a ∈ B" using assms Well    by (auto simp add: wo_rel.ofilter_def)    with Field show "a ∈ Field(Restr r B)" by auto  next    fix a b assume *: "a ∈ A"  and "b ∈ under (Restr r B) a"    hence "b ∈ under r a"    using WELL OFB SUB ofilter_Restr_under[of r B a] by auto    thus "b ∈ A" using * Well OFA by(auto simp add: wo_rel.ofilter_def)  qedqedlemma ofilter_subset_iso:assumes WELL: "Well_order r" and        OFA: "ofilter r A" and OFB: "ofilter r B"shows "(A = B) = iso (Restr r A) (Restr r B) id"using assmsby (auto simp add: ofilter_subset_embedS_iso)subsection {* Ordering the  well-orders by existence of embeddings *}corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq"using ordLeq_reflexive unfolding ordLeq_def refl_on_defby blastcorollary ordLeq_trans: "trans ordLeq"using trans_def[of ordLeq] ordLeq_transitive by blastcorollary ordLeq_preorder_on: "preorder_on {r. Well_order r} ordLeq"by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans)corollary ordIso_refl_on: "refl_on {r. Well_order r} ordIso"using ordIso_reflexive unfolding refl_on_def ordIso_defby blastcorollary ordIso_trans: "trans ordIso"using trans_def[of ordIso] ordIso_transitive by blastcorollary ordIso_sym: "sym ordIso"by (auto simp add: sym_def ordIso_symmetric)corollary ordIso_equiv: "equiv {r. Well_order r} ordIso"by (auto simp add:  equiv_def ordIso_sym ordIso_refl_on ordIso_trans)lemma ordLess_irrefl: "irrefl ordLess"by(unfold irrefl_def, auto simp add: ordLess_irreflexive)lemma ordLess_or_ordIso:assumes WELL: "Well_order r" and WELL': "Well_order r'"shows "r <o r' ∨ r' <o r ∨ r =o r'"unfolding ordLess_def ordIso_defusing assms embedS_or_iso[of r r'] by autocorollary ordLeq_ordLess_Un_ordIso:"ordLeq = ordLess ∪ ordIso"by (auto simp add: ordLeq_iff_ordLess_or_ordIso)lemma not_ordLeq_ordLess:"r ≤o r' ==> ¬ r' <o r"using not_ordLess_ordLeq by blastlemma ordIso_or_ordLess:assumes WELL: "Well_order r" and WELL': "Well_order r'"shows "r =o r' ∨ r <o r' ∨ r' <o r"using assms ordLess_or_ordLeq ordLeq_iff_ordLess_or_ordIso by blastlemmas ord_trans = ordIso_transitive ordLeq_transitive ordLess_transitive                   ordIso_ordLeq_trans ordLeq_ordIso_trans                   ordIso_ordLess_trans ordLess_ordIso_trans                   ordLess_ordLeq_trans ordLeq_ordLess_translemma ofilter_ordLeq:assumes "Well_order r" and "ofilter r A"shows "Restr r A ≤o r"proof-  have "A ≤ Field r" using assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)  thus ?thesis using assms  by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter      wo_rel_def Restr_Field)qedcorollary under_Restr_ordLeq:"Well_order r ==> Restr r (under r a) ≤o r"by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def)subsection {* Copy via direct images  *}lemma Id_dir_image: "dir_image Id f ≤ Id"unfolding dir_image_def by autolemma Un_dir_image:"dir_image (r1 ∪ r2) f = (dir_image r1 f) ∪ (dir_image r2 f)"unfolding dir_image_def by autolemma Int_dir_image:assumes "inj_on f (Field r1 ∪ Field r2)"shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)"proof  show "dir_image (r1 Int r2) f ≤ (dir_image r1 f) Int (dir_image r2 f)"  using assms unfolding dir_image_def inj_on_def by autonext  show "(dir_image r1 f) Int (dir_image r2 f) ≤ dir_image (r1 Int r2) f"  proof(clarify)    fix a' b'    assume "(a',b') ∈ dir_image r1 f" "(a',b') ∈ dir_image r2 f"    then obtain a1 b1 a2 b2    where 1: "a' = f a1 ∧ b' = f b1 ∧ a' = f a2 ∧ b' = f b2" and          2: "(a1,b1) ∈ r1 ∧ (a2,b2) ∈ r2" and          3: "{a1,b1} ≤ Field r1 ∧ {a2,b2} ≤ Field r2"    unfolding dir_image_def Field_def by blast    hence "a1 = a2 ∧ b1 = b2" using assms unfolding inj_on_def by auto    hence "a' = f a1 ∧ b' = f b1 ∧ (a1,b1) ∈ r1 Int r2 ∧ (a2,b2) ∈ r1 Int r2"    using 1 2 by auto    thus "(a',b') ∈ dir_image (r1 ∩ r2) f"    unfolding dir_image_def by blast  qedqedsubsection {* Ordinal-like sum of two (disjoint) well-orders *}text{* This is roughly obtained by ``concatenating" the two well-orders -- thus, all elementsof the first will be smaller than all elements of the second.  This constructiononly makes sense if the fields of the two well-order relations are disjoint. *}definition Osum :: "'a rel => 'a rel => 'a rel"  (infix "Osum" 60)where"r Osum r' = r ∪ r' ∪ {(a,a'). a ∈ Field r ∧ a' ∈ Field r'}"abbreviation Osum2 :: "'a rel => 'a rel => 'a rel" (infix "∪o" 60)where "r ∪o r' ≡ r Osum r'"lemma Field_Osum: "Field(r Osum r') = Field r ∪ Field r'"unfolding Osum_def Field_def by blastlemma Osum_Refl:assumes FLD: "Field r Int Field r' = {}" and        REFL: "Refl r" and REFL': "Refl r'"shows "Refl (r Osum r')"using assms  (* Need first unfold Field_Osum, only then Osum_def *)unfolding refl_on_def  Field_Osum unfolding Osum_def by blastlemma Osum_trans:assumes FLD: "Field r Int Field r' = {}" and        TRANS: "trans r" and TRANS': "trans r'"shows "trans (r Osum r')"proof(unfold trans_def, auto)  fix x y z assume *: "(x, y) ∈ r ∪o r'" and **: "(y, z) ∈ r ∪o r'"  show  "(x, z) ∈ r ∪o r'"  proof-    {assume Case1: "(x,y) ∈ r"     hence 1: "x ∈ Field r ∧ y ∈ Field r" unfolding Field_def by auto     have ?thesis     proof-       {assume Case11: "(y,z) ∈ r"        hence "(x,z) ∈ r" using Case1 TRANS trans_def[of r] by blast        hence ?thesis unfolding Osum_def by auto       }       moreover       {assume Case12: "(y,z) ∈ r'"        hence "y ∈ Field r'" unfolding Field_def by auto        hence False using FLD 1 by auto       }       moreover       {assume Case13: "z ∈ Field r'"        hence ?thesis using 1 unfolding Osum_def by auto       }       ultimately show ?thesis using ** unfolding Osum_def by blast     qed    }    moreover    {assume Case2: "(x,y) ∈ r'"     hence 2: "x ∈ Field r' ∧ y ∈ Field r'" unfolding Field_def by auto     have ?thesis     proof-       {assume Case21: "(y,z) ∈ r"        hence "y ∈ Field r" unfolding Field_def by auto        hence False using FLD 2 by auto       }       moreover       {assume Case22: "(y,z) ∈ r'"        hence "(x,z) ∈ r'" using Case2 TRANS' trans_def[of r'] by blast        hence ?thesis unfolding Osum_def by auto       }       moreover       {assume Case23: "y ∈ Field r"        hence False using FLD 2 by auto       }       ultimately show ?thesis using ** unfolding Osum_def by blast     qed    }    moreover    {assume Case3: "x ∈ Field r ∧ y ∈ Field r'"     have ?thesis     proof-       {assume Case31: "(y,z) ∈ r"        hence "y ∈ Field r" unfolding Field_def by auto        hence False using FLD Case3 by auto       }       moreover       {assume Case32: "(y,z) ∈ r'"        hence "z ∈ Field r'" unfolding Field_def by blast        hence ?thesis unfolding Osum_def using Case3 by auto       }       moreover       {assume Case33: "y ∈ Field r"        hence False using FLD Case3 by auto       }       ultimately show ?thesis using ** unfolding Osum_def by blast     qed    }    ultimately show ?thesis using * unfolding Osum_def by blast  qedqedlemma Osum_Preorder:"[|Field r Int Field r' = {}; Preorder r; Preorder r'|] ==> Preorder (r Osum r')"unfolding preorder_on_def using Osum_Refl Osum_trans by blastlemma Osum_antisym:assumes FLD: "Field r Int Field r' = {}" and        AN: "antisym r" and AN': "antisym r'"shows "antisym (r Osum r')"proof(unfold antisym_def, auto)  fix x y assume *: "(x, y) ∈ r ∪o r'" and **: "(y, x) ∈ r ∪o r'"  show  "x = y"  proof-    {assume Case1: "(x,y) ∈ r"     hence 1: "x ∈ Field r ∧ y ∈ Field r" unfolding Field_def by auto     have ?thesis     proof-       have "(y,x) ∈ r ==> ?thesis"       using Case1 AN antisym_def[of r] by blast       moreover       {assume "(y,x) ∈ r'"        hence "y ∈ Field r'" unfolding Field_def by auto        hence False using FLD 1 by auto       }       moreover       have "x ∈ Field r' ==> False" using FLD 1 by auto       ultimately show ?thesis using ** unfolding Osum_def by blast     qed    }    moreover    {assume Case2: "(x,y) ∈ r'"     hence 2: "x ∈ Field r' ∧ y ∈ Field r'" unfolding Field_def by auto     have ?thesis     proof-       {assume "(y,x) ∈ r"        hence "y ∈ Field r" unfolding Field_def by auto        hence False using FLD 2 by auto       }       moreover       have "(y,x) ∈ r' ==> ?thesis"       using Case2 AN' antisym_def[of r'] by blast       moreover       {assume "y ∈ Field r"        hence False using FLD 2 by auto       }       ultimately show ?thesis using ** unfolding Osum_def by blast     qed    }    moreover    {assume Case3: "x ∈ Field r ∧ y ∈ Field r'"     have ?thesis     proof-       {assume "(y,x) ∈ r"        hence "y ∈ Field r" unfolding Field_def by auto        hence False using FLD Case3 by auto       }       moreover       {assume Case32: "(y,x) ∈ r'"        hence "x ∈ Field r'" unfolding Field_def by blast        hence False using FLD Case3 by auto       }       moreover       have "¬ y ∈ Field r" using FLD Case3 by auto       ultimately show ?thesis using ** unfolding Osum_def by blast     qed    }    ultimately show ?thesis using * unfolding Osum_def by blast  qedqedlemma Osum_Partial_order:"[|Field r Int Field r' = {}; Partial_order r; Partial_order r'|] ==> Partial_order (r Osum r')"unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blastlemma Osum_Total:assumes FLD: "Field r Int Field r' = {}" and        TOT: "Total r" and TOT': "Total r'"shows "Total (r Osum r')"using assmsunfolding total_on_def  Field_Osum unfolding Osum_def by blastlemma Osum_Linear_order:"[|Field r Int Field r' = {}; Linear_order r; Linear_order r'|] ==> Linear_order (r Osum r')"unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blastlemma Osum_wf:assumes FLD: "Field r Int Field r' = {}" and        WF: "wf r" and WF': "wf r'"shows "wf (r Osum r')"unfolding wf_eq_minimal2 unfolding Field_Osumproof(intro allI impI, elim conjE)  fix A assume *: "A ⊆ Field r ∪ Field r'" and **: "A ≠ {}"  obtain B where B_def: "B = A Int Field r" by blast  show "∃a∈A. ∀a'∈A. (a', a) ∉ r ∪o r'"  proof(cases "B = {}")    assume Case1: "B ≠ {}"    hence "B ≠ {} ∧ B ≤ Field r" using B_def by auto    then obtain a where 1: "a ∈ B" and 2: "∀a1 ∈ B. (a1,a) ∉ r"    using WF  unfolding wf_eq_minimal2 by blast    hence 3: "a ∈ Field r ∧ a ∉ Field r'" using B_def FLD by auto    (*  *)    have "∀a1 ∈ A. (a1,a) ∉ r Osum r'"    proof(intro ballI)      fix a1 assume **: "a1 ∈ A"      {assume Case11: "a1 ∈ Field r"       hence "(a1,a) ∉ r" using B_def ** 2 by auto       moreover       have "(a1,a) ∉ r'" using 3 by (auto simp add: Field_def)       ultimately have "(a1,a) ∉ r Osum r'"       using 3 unfolding Osum_def by auto      }      moreover      {assume Case12: "a1 ∉ Field r"       hence "(a1,a) ∉ r" unfolding Field_def by auto       moreover       have "(a1,a) ∉ r'" using 3 unfolding Field_def by auto       ultimately have "(a1,a) ∉ r Osum r'"       using 3 unfolding Osum_def by auto      }      ultimately show "(a1,a) ∉ r Osum r'" by blast    qed    thus ?thesis using 1 B_def by auto  next    assume Case2: "B = {}"    hence 1: "A ≠ {} ∧ A ≤ Field r'" using * ** B_def by auto    then obtain a' where 2: "a' ∈ A" and 3: "∀a1' ∈ A. (a1',a') ∉ r'"    using WF' unfolding wf_eq_minimal2 by blast    hence 4: "a' ∈ Field r' ∧ a' ∉ Field r" using 1 FLD by blast    (*  *)    have "∀a1' ∈ A. (a1',a') ∉ r Osum r'"    proof(unfold Osum_def, auto simp add: 3)      fix a1' assume "(a1', a') ∈ r"      thus False using 4 unfolding Field_def by blast    next      fix a1' assume "a1' ∈ A" and "a1' ∈ Field r"      thus False using Case2 B_def by auto    qed    thus ?thesis using 2 by blast  qedqedlemma Osum_minus_Id:assumes TOT: "Total r" and TOT': "Total r'" and        NID: "¬ (r ≤ Id)" and NID': "¬ (r' ≤ Id)"shows "(r Osum r') - Id ≤ (r - Id) Osum (r' - Id)"proof-  {fix a a' assume *: "(a,a') ∈ (r Osum r')" and **: "a ≠ a'"   have "(a,a') ∈ (r - Id) Osum (r' - Id)"   proof-     {assume "(a,a') ∈ r ∨ (a,a') ∈ r'"      with ** have ?thesis unfolding Osum_def by auto     }     moreover     {assume "a ∈ Field r ∧ a' ∈ Field r'"      hence "a ∈ Field(r - Id) ∧ a' ∈ Field (r' - Id)"      using assms rel.Total_Id_Field by blast      hence ?thesis unfolding Osum_def by auto     }     ultimately show ?thesis using * unfolding Osum_def by blast   qed  }  thus ?thesis by(auto simp add: Osum_def)qedlemma wf_Int_Times:assumes "A Int B = {}"shows "wf(A × B)"proof(unfold wf_def, auto)  fix P x  assume *: "∀x. (∀y. y ∈ A ∧ x ∈ B --> P y) --> P x"  moreover have "∀y ∈ A. P y" using assms * by blast  ultimately show "P x" using * by (case_tac "x ∈ B", auto)qedlemma Osum_minus_Id1:assumes "r ≤ Id"shows "(r Osum r') - Id ≤ (r' - Id) ∪ (Field r × Field r')"proof-  let ?Left = "(r Osum r') - Id"  let ?Right = "(r' - Id) ∪ (Field r × Field r')"  {fix a::'a and b assume *: "(a,b) ∉ Id"   {assume "(a,b) ∈ r"    with * have False using assms by auto   }   moreover   {assume "(a,b) ∈ r'"    with * have "(a,b) ∈ r' - Id" by auto   }   ultimately   have "(a,b) ∈ ?Left ==> (a,b) ∈ ?Right"   unfolding Osum_def by auto  }  thus ?thesis by autoqedlemma Osum_minus_Id2:assumes "r' ≤ Id"shows "(r Osum r') - Id ≤ (r - Id) ∪ (Field r × Field r')"proof-  let ?Left = "(r Osum r') - Id"  let ?Right = "(r - Id) ∪ (Field r × Field r')"  {fix a::'a and b assume *: "(a,b) ∉ Id"   {assume "(a,b) ∈ r'"    with * have False using assms by auto   }   moreover   {assume "(a,b) ∈ r"    with * have "(a,b) ∈ r - Id" by auto   }   ultimately   have "(a,b) ∈ ?Left ==> (a,b) ∈ ?Right"   unfolding Osum_def by auto  }  thus ?thesis by autoqedlemma Osum_wf_Id:assumes TOT: "Total r" and TOT': "Total r'" and        FLD: "Field r Int Field r' = {}" and        WF: "wf(r - Id)" and WF': "wf(r' - Id)"shows "wf ((r Osum r') - Id)"proof(cases "r ≤ Id ∨ r' ≤ Id")  assume Case1: "¬(r ≤ Id ∨ r' ≤ Id)"  have "Field(r - Id) Int Field(r' - Id) = {}"  using FLD mono_Field[of "r - Id" r]  mono_Field[of "r' - Id" r']            Diff_subset[of r Id] Diff_subset[of r' Id] by blast  thus ?thesis  using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"]        wf_subset[of "(r - Id) ∪o (r' - Id)" "(r Osum r') - Id"] by autonext  have 1: "wf(Field r × Field r')"  using FLD by (auto simp add: wf_Int_Times)  assume Case2: "r ≤ Id ∨ r' ≤ Id"  moreover  {assume Case21: "r ≤ Id"   hence "(r Osum r') - Id ≤ (r' - Id) ∪ (Field r × Field r')"   using Osum_minus_Id1[of r r'] by simp   moreover   {have "Domain(Field r × Field r') Int Range(r' - Id) = {}"    using FLD unfolding Field_def by blast    hence "wf((r' - Id) ∪ (Field r × Field r'))"    using 1 WF' wf_Un[of "Field r × Field r'" "r' - Id"]    by (auto simp add: Un_commute)   }   ultimately have ?thesis by (auto simp add: wf_subset)  }  moreover  {assume Case22: "r' ≤ Id"   hence "(r Osum r') - Id ≤ (r - Id) ∪ (Field r × Field r')"   using Osum_minus_Id2[of r' r] by simp   moreover   {have "Range(Field r × Field r') Int Domain(r - Id) = {}"    using FLD unfolding Field_def by blast    hence "wf((r - Id) ∪ (Field r × Field r'))"    using 1 WF wf_Un[of "r - Id" "Field r × Field r'"]    by (auto simp add: Un_commute)   }   ultimately have ?thesis by (auto simp add: wf_subset)  }  ultimately show ?thesis by blastqedlemma Osum_Well_order:assumes FLD: "Field r Int Field r' = {}" and        WELL: "Well_order r" and WELL': "Well_order r'"shows "Well_order (r Osum r')"proof-  have "Total r ∧ Total r'" using WELL WELL'  by (auto simp add: order_on_defs)  thus ?thesis using assms unfolding well_order_on_def  using Osum_Linear_order Osum_wf_Id by blastqedlemma Osum_embed:assumes FLD: "Field r Int Field r' = {}" and        WELL: "Well_order r" and WELL': "Well_order r'"shows "embed r (r Osum r') id"proof-  have 1: "Well_order (r Osum r')"  using assms by (auto simp add: Osum_Well_order)  moreover  have "compat r (r Osum r') id"  unfolding compat_def Osum_def by auto  moreover  have "inj_on id (Field r)" by simp  moreover  have "ofilter (r Osum r') (Field r)"  using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def                               Field_Osum rel.under_def)    fix a b assume 2: "a ∈ Field r" and 3: "(b,a) ∈ r Osum r'"    moreover    {assume "(b,a) ∈ r'"     hence "a ∈ Field r'" using Field_def[of r'] by blast     hence False using 2 FLD by blast    }    moreover    {assume "a ∈ Field r'"     hence False using 2 FLD by blast    }    ultimately    show "b ∈ Field r" by (auto simp add: Osum_def Field_def)  qed  ultimately show ?thesis  using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)qedcorollary Osum_ordLeq:assumes FLD: "Field r Int Field r' = {}" and        WELL: "Well_order r" and WELL': "Well_order r'"shows "r ≤o r Osum r'"using assms Osum_embed Osum_Well_orderunfolding ordLeq_def by blastlemma Well_order_embed_copy:assumes WELL: "well_order_on A r" and        INJ: "inj_on f A" and SUB: "f ` A ≤ B"shows "∃r'. well_order_on B r' ∧ r ≤o r'"proof-  have "bij_betw f A (f ` A)"  using INJ inj_on_imp_bij_betw by blast  then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''"  using WELL  Well_order_iso_copy by blast  hence 2: "Well_order r'' ∧ Field r'' = (f ` A)"  using rel.well_order_on_Well_order by blast  (*  *)  let ?C = "B - (f ` A)"  obtain r''' where "well_order_on ?C r'''"  using well_order_on by blast  hence 3: "Well_order r''' ∧ Field r''' = ?C"  using rel.well_order_on_Well_order by blast  (*  *)  let ?r' = "r'' Osum r'''"  have "Field r'' Int Field r''' = {}"  using 2 3 by auto  hence "r'' ≤o ?r'" using Osum_ordLeq[of r'' r'''] 2 3 by blast  hence 4: "r ≤o ?r'" using 1 ordIso_ordLeq_trans by blast  (*  *)  hence "Well_order ?r'" unfolding ordLeq_def by auto  moreover  have "Field ?r' = B" using 2 3 SUB by (auto simp add: Field_Osum)  ultimately show ?thesis using 4 by blastqedsubsection {* The maxim among a finite set of ordinals  *}text {* The correct phrasing would be ``a maxim of ...", as @{text "≤o"} is only a preorder. *}definition isOmax :: "'a rel set => 'a rel => bool"where"isOmax  R r == r ∈ R ∧ (ALL r' : R. r' ≤o r)"definition omax :: "'a rel set => 'a rel"where"omax R == SOME r. isOmax R r"lemma exists_isOmax:assumes "finite R" and "R ≠ {}" and "∀ r ∈ R. Well_order r"shows "∃ r. isOmax R r"proof-  have "finite R ==> R ≠ {} --> (∀ r ∈ R. Well_order r) --> (∃ r. isOmax R r)"  apply(erule finite_induct) apply(simp add: isOmax_def)  proof(clarsimp)    fix r :: "('a × 'a) set" and R assume *: "finite R" and **: "r ∉ R"    and ***: "Well_order r" and ****: "∀r∈R. Well_order r"    and IH: "R ≠ {} --> (∃p. isOmax R p)"    let ?R' = "insert r R"    show "∃p'. (isOmax ?R' p')"    proof(cases "R = {}")      assume Case1: "R = {}"      thus ?thesis unfolding isOmax_def using ***      by (simp add: ordLeq_reflexive)    next      assume Case2: "R ≠ {}"      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 ≤o p"       hence "isOmax ?R' p" using p unfolding isOmax_def by simp       hence ?thesis by auto      }      moreover      {assume Case22: "p ≤o r"       {fix r' assume "r' ∈ ?R'"        moreover        {assume "r' ∈ R"         hence "r' ≤o p" using p unfolding isOmax_def by simp         hence "r' ≤o r" using Case22 by(rule ordLeq_transitive)        }        moreover have "r ≤o r" using *** by(rule ordLeq_reflexive)        ultimately have "r' ≤o r" by auto       }       hence "isOmax ?R' r" unfolding isOmax_def by simp       hence ?thesis by auto      }      moreover have "r ≤o p ∨ p ≤o r"      using 1 *** ordLeq_total by auto      ultimately show ?thesis by blast    qed  qed  thus ?thesis using assms by autoqedlemma omax_isOmax:assumes "finite R" and "R ≠ {}" and "∀ r ∈ R. Well_order r"shows "isOmax R (omax R)"unfolding omax_def using assmsby(simp add: exists_isOmax someI_ex)lemma omax_in:assumes "finite R" and "R ≠ {}" and "∀ r ∈ R. Well_order r"shows "omax R ∈ R"using assms omax_isOmax unfolding isOmax_def by blastlemma Well_order_omax:assumes "finite R" and "R ≠ {}" and "∀r∈R. Well_order r"shows "Well_order (omax R)"using assms apply - apply(drule omax_in) by autolemma omax_maxim:assumes "finite R" and "∀ r ∈ R. Well_order r" and "r ∈ R"shows "r ≤o omax R"using assms omax_isOmax unfolding isOmax_def by blastlemma omax_ordLeq:assumes "finite R" and "R ≠ {}" and *: "∀ r ∈ R. r ≤o p"shows "omax R ≤o p"proof-  have "∀ r ∈ R. Well_order r" using * unfolding ordLeq_def by simp  thus ?thesis using assms omax_in by autoqedlemma omax_ordLess:assumes "finite R" and "R ≠ {}" and *: "∀ r ∈ R. r <o p"shows "omax R <o p"proof-  have "∀ r ∈ R. Well_order r" using * unfolding ordLess_def by simp  thus ?thesis using assms omax_in by autoqedlemma omax_ordLeq_elim:assumes "finite R" and "∀ r ∈ R. Well_order r"and "omax R ≤o p" and "r ∈ R"shows "r ≤o p"using assms omax_maxim[of R r] apply simpusing ordLeq_transitive by blastlemma omax_ordLess_elim:assumes "finite R" and "∀ r ∈ R. Well_order r"and "omax R <o p" and "r ∈ R"shows "r <o p"using assms omax_maxim[of R r] apply simpusing ordLeq_ordLess_trans by blastlemma ordLeq_omax:assumes "finite R" and "∀ r ∈ R. Well_order r"and "r ∈ R" and "p ≤o r"shows "p ≤o omax R"using assms omax_maxim[of R r] apply simpusing ordLeq_transitive by blastlemma ordLess_omax:assumes "finite R" and "∀ r ∈ R. Well_order r"and "r ∈ R" and "p <o r"shows "p <o omax R"using assms omax_maxim[of R r] apply simpusing ordLess_ordLeq_trans by blastlemma omax_ordLeq_mono:assumes P: "finite P" and R: "finite R"and NE_P: "P ≠ {}" and Well_R: "∀ r ∈ R. Well_order r"and LEQ: "∀ p ∈ P. ∃ r ∈ R. p ≤o r"shows "omax P ≤o omax R"proof-  let ?mp = "omax P"  let ?mr = "omax R"  {fix p assume "p : P"   then obtain r where r: "r : R" and "p ≤o r"   using LEQ by blast   moreover have "r <=o ?mr"   using r R Well_R omax_maxim by blast   ultimately have "p <=o ?mr"   using ordLeq_transitive by blast  }  thus "?mp <=o ?mr"  using NE_P P using omax_ordLeq by blastqedlemma omax_ordLess_mono:assumes P: "finite P" and R: "finite R"and NE_P: "P ≠ {}" and Well_R: "∀ r ∈ R. Well_order r"and LEQ: "∀ p ∈ P. ∃ r ∈ R. p <o r"shows "omax P <o omax R"proof-  let ?mp = "omax P"  let ?mr = "omax R"  {fix p assume "p : P"   then obtain r where r: "r : R" and "p <o r"   using LEQ by blast   moreover have "r <=o ?mr"   using r R Well_R omax_maxim by blast   ultimately have "p <o ?mr"   using ordLess_ordLeq_trans by blast  }  thus "?mp <o ?mr"  using NE_P P omax_ordLess by blastqedend`