# Theory Wellorder_Embedding

Up to index of Isabelle/HOL/Free-Groups

theory Wellorder_Embedding
imports Wellorder_Embedding_Base Fun_More Wellorder_Relation
`(*  Title:      HOL/Cardinals/Wellorder_Embedding.thy    Author:     Andrei Popescu, TU Muenchen    Copyright   2012Well-order embeddings.*)header {* Well-Order Embeddings *}theory Wellorder_Embeddingimports Wellorder_Embedding_Base Fun_More Wellorder_Relationbeginsubsection {* Auxiliaries *}lemma UNION_bij_betw_ofilter:assumes WELL: "Well_order r" and        OF: "!! i. i ∈ I ==> ofilter r (A i)" and       BIJ: "!! i. i ∈ I ==> bij_betw f (A i) (A' i)"shows "bij_betw f (\<Union> i ∈ I. A i) (\<Union> i ∈ I. A' i)"proof-  have "wo_rel r" using WELL by (simp add: wo_rel_def)  hence "!! i j. [|i ∈ I; j ∈ I|] ==> A i ≤ A j ∨ A j ≤ A i"  using wo_rel.ofilter_linord[of r] OF by blast  with WELL BIJ show ?thesis  by (auto simp add: bij_betw_UNION_chain)qedsubsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatiblefunctions *}lemma embed_halfcong:assumes EQ: "!! a. a ∈ Field r ==> f a = g a" and        EMB: "embed r r' f"shows "embed r r' g"proof(unfold embed_def, auto)  fix a assume *: "a ∈ Field r"  hence "bij_betw f (under r a) (under r' (f a))"  using EMB unfolding embed_def by simp  moreover  {have "under r a ≤ Field r"   by (auto simp add: rel.under_Field)   hence "!! b. b ∈ under r a ==> f b = g b"   using EQ by blast  }  moreover have "f a = g a" using * EQ by auto  ultimately show "bij_betw g (under r a) (under r' (g a))"  using bij_betw_cong[of "under r a" f g "under r' (f a)"] by autoqedlemma embed_cong[fundef_cong]:assumes "!! a. a ∈ Field r ==> f a = g a"shows "embed r r' f = embed r r' g"using assms embed_halfcong[of r f g r']            embed_halfcong[of r g f r'] by autolemma embedS_cong[fundef_cong]:assumes "!! a. a ∈ Field r ==> f a = g a"shows "embedS r r' f = embedS r r' g"unfolding embedS_def using assmsembed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blastlemma iso_cong[fundef_cong]:assumes "!! a. a ∈ Field r ==> f a = g a"shows "iso r r' f = iso r r' g"unfolding iso_def using assmsembed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blastlemma id_compat: "compat r r id"by(auto simp add: id_def compat_def)lemma comp_compat:"[|compat r r' f; compat r' r'' f'|] ==> compat r r'' (f' o f)"by(auto simp add: comp_def compat_def)corollary one_set_greater:"(∃f::'a => 'a'. f ` A ≤ A' ∧ inj_on f A) ∨ (∃g::'a' => 'a. g ` A' ≤ A ∧ inj_on g A')"proof-  obtain r where "well_order_on A r" by (fastforce simp add: well_order_on)  hence 1: "A = Field r ∧ Well_order r"  using rel.well_order_on_Well_order by auto  obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on)  hence 2: "A' = Field r' ∧ Well_order r'"  using rel.well_order_on_Well_order by auto  hence "(∃f. embed r r' f) ∨ (∃g. embed r' r g)"  using 1 2 by (auto simp add: wellorders_totally_ordered)  moreover  {fix f assume "embed r r' f"   hence "f`A ≤ A' ∧ inj_on f A"   using 1 2 by (auto simp add: embed_Field embed_inj_on)  }  moreover  {fix g assume "embed r' r g"   hence "g`A' ≤ A ∧ inj_on g A'"   using 1 2 by (auto simp add: embed_Field embed_inj_on)  }  ultimately show ?thesis by blastqedcorollary one_type_greater:"(∃f::'a => 'a'. inj f) ∨ (∃g::'a' => 'a. inj g)"using one_set_greater[of UNIV UNIV] by autosubsection {* Uniqueness of embeddings  *}lemma comp_embedS:assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"        and  EMB: "embedS r r' f" and EMB': "embedS r' r'' f'"shows "embedS r r'' (f' o f)"proof-  have "embed r' r'' f'" using EMB' unfolding embedS_def by simp  thus ?thesis using assms by (auto simp add: embedS_comp_embed)qedlemma iso_iff4:assumes WELL: "Well_order r"  and WELL': "Well_order r'"shows "iso r r' f = (embed r r' f ∧ embed r' r (inv_into (Field r) f))"using assms embed_bothWays_isoby(unfold iso_def, auto simp add: inv_into_Field_embed_bij_betw)lemma embed_embedS_iso:"embed r r' f = (embedS r r' f ∨ iso r r' f)"unfolding embedS_def iso_def by blastlemma not_embedS_iso:"¬ (embedS r r' f ∧ iso r r' f)"unfolding embedS_def iso_def by blastlemma embed_embedS_iff_not_iso:assumes "embed r r' f"shows "embedS r r' f = (¬ iso r r' f)"using assms unfolding embedS_def iso_def by blastlemma iso_inv_into:assumes WELL: "Well_order r" and ISO: "iso r r' f"shows "iso r' r (inv_into (Field r) f)"using assms unfolding iso_defusing bij_betw_inv_into inv_into_Field_embed_bij_betw by blastlemma embedS_or_iso:assumes WELL: "Well_order r" and WELL': "Well_order r'"shows "(∃g. embedS r r' g) ∨ (∃h. embedS r' r h) ∨ (∃f. iso r r' f)"proof-  {fix f assume *: "embed r r' f"   {assume "bij_betw f (Field r) (Field r')"    hence ?thesis using * by (auto simp add: iso_def)   }   moreover   {assume "¬ bij_betw f (Field r) (Field r')"    hence ?thesis using * by (auto simp add: embedS_def)   }   ultimately have ?thesis by auto  }  moreover  {fix f assume *: "embed r' r f"   {assume "bij_betw f (Field r') (Field r)"    hence "iso r' r f" using * by (auto simp add: iso_def)    hence "iso r r' (inv_into (Field r') f)"    using WELL' by (auto simp add: iso_inv_into)    hence ?thesis by blast   }   moreover   {assume "¬ bij_betw f (Field r') (Field r)"    hence ?thesis using * by (auto simp add: embedS_def)   }   ultimately have ?thesis by auto  }  ultimately show ?thesis using WELL WELL'  wellorders_totally_ordered[of r r'] by blastqedend`