blanchet@55056: (* Title: HOL/BNF_Wellorder_Embedding.thy blanchet@48975: Author: Andrei Popescu, TU Muenchen blanchet@48975: Copyright 2012 blanchet@48975: blanchet@55059: Well-order embeddings as needed by bounded natural functors. blanchet@48975: *) blanchet@48975: blanchet@55059: header {* Well-Order Embeddings as Needed by Bounded Natural Functors *} blanchet@48975: blanchet@55056: theory BNF_Wellorder_Embedding traytel@55936: imports Hilbert_Choice BNF_Wellorder_Relation blanchet@48975: begin blanchet@48975: blanchet@48975: text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and blanchet@48975: prove their basic properties. The notion of embedding is considered from the point blanchet@48975: of view of the theory of ordinals, and therefore requires the source to be injected blanchet@48975: as an {\em initial segment} (i.e., {\em order filter}) of the target. A main result blanchet@48975: of this section is the existence of embeddings (in one direction or another) between blanchet@48975: any two well-orders, having as a consequence the fact that, given any two sets on blanchet@48975: any two types, one is smaller than (i.e., can be injected into) the other. *} blanchet@48975: blanchet@48975: blanchet@48975: subsection {* Auxiliaries *} blanchet@48975: blanchet@48975: lemma UNION_inj_on_ofilter: blanchet@48975: assumes WELL: "Well_order r" and blanchet@48975: OF: "\ i. i \ I \ wo_rel.ofilter r (A i)" and blanchet@48975: INJ: "\ i. i \ I \ inj_on f (A i)" blanchet@48975: shows "inj_on f (\ i \ I. A i)" blanchet@48975: proof- blanchet@48975: have "wo_rel r" using WELL by (simp add: wo_rel_def) blanchet@48975: hence "\ i j. \i \ I; j \ I\ \ A i <= A j \ A j <= A i" blanchet@48975: using wo_rel.ofilter_linord[of r] OF by blast blanchet@48975: with WELL INJ show ?thesis blanchet@48975: by (auto simp add: inj_on_UNION_chain) blanchet@48975: qed blanchet@48975: blanchet@48975: lemma under_underS_bij_betw: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: IN: "a \ Field r" and IN': "f a \ Field r'" and blanchet@55023: BIJ: "bij_betw f (underS r a) (underS r' (f a))" blanchet@55023: shows "bij_betw f (under r a) (under r' (f a))" blanchet@48975: proof- blanchet@55023: have "a \ underS r a \ f a \ underS r' (f a)" blanchet@55023: unfolding underS_def by auto blanchet@48975: moreover blanchet@48975: {have "Refl r \ Refl r'" using WELL WELL' blanchet@48975: by (auto simp add: order_on_defs) blanchet@55023: hence "under r a = underS r a \ {a} \ blanchet@55023: under r' (f a) = underS r' (f a) \ {f a}" blanchet@55023: using IN IN' by(auto simp add: Refl_under_underS) blanchet@48975: } blanchet@48975: ultimately show ?thesis blanchet@55023: using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto blanchet@48975: qed blanchet@48975: blanchet@48975: blanchet@48975: subsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatible blanchet@55101: functions *} blanchet@48975: blanchet@48975: text{* Standardly, a function is an embedding of a well-order in another if it injectively and blanchet@48975: order-compatibly maps the former into an order filter of the latter. blanchet@48975: Here we opt for a more succinct definition (operator @{text "embed"}), blanchet@48975: asking that, for any element in the source, the function should be a bijection blanchet@48975: between the set of strict lower bounds of that element blanchet@48975: and the set of strict lower bounds of its image. (Later we prove equivalence with blanchet@48975: the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.) blanchet@48975: A {\em strict embedding} (operator @{text "embedS"}) is a non-bijective embedding blanchet@55101: and an isomorphism (operator @{text "iso"}) is a bijective embedding. *} blanchet@48975: blanchet@48975: definition embed :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" blanchet@48975: where blanchet@55023: "embed r r' f \ \a \ Field r. bij_betw f (under r a) (under r' (f a))" blanchet@48975: blanchet@48975: lemmas embed_defs = embed_def embed_def[abs_def] blanchet@48975: blanchet@48975: text {* Strict embeddings: *} blanchet@48975: blanchet@48975: definition embedS :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" blanchet@48975: where blanchet@48975: "embedS r r' f \ embed r r' f \ \ bij_betw f (Field r) (Field r')" blanchet@48975: blanchet@48975: lemmas embedS_defs = embedS_def embedS_def[abs_def] blanchet@48975: blanchet@48975: definition iso :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" blanchet@48975: where blanchet@48975: "iso r r' f \ embed r r' f \ bij_betw f (Field r) (Field r')" blanchet@48975: blanchet@48975: lemmas iso_defs = iso_def iso_def[abs_def] blanchet@48975: blanchet@48975: definition compat :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" blanchet@48975: where blanchet@48975: "compat r r' f \ \a b. (a,b) \ r \ (f a, f b) \ r'" blanchet@48975: blanchet@48975: lemma compat_wf: blanchet@48975: assumes CMP: "compat r r' f" and WF: "wf r'" blanchet@48975: shows "wf r" blanchet@48975: proof- blanchet@48975: have "r \ inv_image r' f" blanchet@48975: unfolding inv_image_def using CMP blanchet@48975: by (auto simp add: compat_def) blanchet@48975: with WF show ?thesis blanchet@48975: using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma id_embed: "embed r r id" blanchet@48975: by(auto simp add: id_def embed_def bij_betw_def) blanchet@48975: blanchet@48975: lemma id_iso: "iso r r id" blanchet@48975: by(auto simp add: id_def embed_def iso_def bij_betw_def) blanchet@48975: blanchet@48975: lemma embed_in_Field: blanchet@48975: assumes WELL: "Well_order r" and blanchet@48975: EMB: "embed r r' f" and IN: "a \ Field r" blanchet@48975: shows "f a \ Field r'" blanchet@48975: proof- blanchet@48975: have Well: "wo_rel r" blanchet@48975: using WELL by (auto simp add: wo_rel_def) blanchet@48975: hence 1: "Refl r" blanchet@48975: by (auto simp add: wo_rel.REFL) blanchet@55023: hence "a \ under r a" using IN Refl_under_in by fastforce blanchet@55023: hence "f a \ under r' (f a)" blanchet@48975: using EMB IN by (auto simp add: embed_def bij_betw_def) blanchet@48975: thus ?thesis unfolding Field_def blanchet@55023: by (auto simp: under_def) blanchet@48975: qed blanchet@48975: blanchet@48975: lemma comp_embed: blanchet@48975: assumes WELL: "Well_order r" and blanchet@48975: EMB: "embed r r' f" and EMB': "embed r' r'' f'" blanchet@48975: shows "embed r r'' (f' o f)" blanchet@48975: proof(unfold embed_def, auto) blanchet@48975: fix a assume *: "a \ Field r" blanchet@55023: hence "bij_betw f (under r a) (under r' (f a))" blanchet@48975: using embed_def[of r] EMB by auto blanchet@48975: moreover blanchet@48975: {have "f a \ Field r'" blanchet@48975: using EMB WELL * by (auto simp add: embed_in_Field) blanchet@55023: hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))" blanchet@48975: using embed_def[of r'] EMB' by auto blanchet@48975: } blanchet@48975: ultimately blanchet@55023: show "bij_betw (f' \ f) (under r a) (under r'' (f'(f a)))" blanchet@48975: by(auto simp add: bij_betw_trans) blanchet@48975: qed blanchet@48975: blanchet@48975: lemma comp_iso: blanchet@48975: assumes WELL: "Well_order r" and blanchet@48975: EMB: "iso r r' f" and EMB': "iso r' r'' f'" blanchet@48975: shows "iso r r'' (f' o f)" blanchet@48975: using assms unfolding iso_def blanchet@48975: by (auto simp add: comp_embed bij_betw_trans) blanchet@48975: blanchet@55101: text{* That @{text "embedS"} is also preserved by function composition shall be proved only later. *} blanchet@48975: blanchet@48975: lemma embed_Field: blanchet@48975: "\Well_order r; embed r r' f\ \ f`(Field r) \ Field r'" blanchet@48975: by (auto simp add: embed_in_Field) blanchet@48975: blanchet@48975: lemma embed_preserves_ofilter: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMB: "embed r r' f" and OF: "wo_rel.ofilter r A" blanchet@48975: shows "wo_rel.ofilter r' (f`A)" blanchet@48975: proof- blanchet@48975: (* Preliminary facts *) blanchet@48975: from WELL have Well: "wo_rel r" unfolding wo_rel_def . blanchet@48975: from WELL' have Well': "wo_rel r'" unfolding wo_rel_def . blanchet@48975: from OF have 0: "A \ Field r" by(auto simp add: Well wo_rel.ofilter_def) blanchet@48975: (* Main proof *) blanchet@48975: show ?thesis using Well' WELL EMB 0 embed_Field[of r r' f] blanchet@48975: proof(unfold wo_rel.ofilter_def, auto simp add: image_def) blanchet@48975: fix a b' blanchet@55023: assume *: "a \ A" and **: "b' \ under r' (f a)" blanchet@48975: hence "a \ Field r" using 0 by auto blanchet@55023: hence "bij_betw f (under r a) (under r' (f a))" blanchet@48975: using * EMB by (auto simp add: embed_def) blanchet@55023: hence "f`(under r a) = under r' (f a)" blanchet@48975: by (simp add: bij_betw_def) blanchet@55023: with ** image_def[of f "under r a"] obtain b where blanchet@55023: 1: "b \ under r a \ b' = f b" by blast blanchet@48975: hence "b \ A" using Well * OF blanchet@48975: by (auto simp add: wo_rel.ofilter_def) blanchet@48975: with 1 show "\b \ A. b' = f b" by blast blanchet@48975: qed blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_Field_ofilter: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMB: "embed r r' f" blanchet@48975: shows "wo_rel.ofilter r' (f`(Field r))" blanchet@48975: proof- blanchet@48975: have "wo_rel.ofilter r (Field r)" blanchet@48975: using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter) blanchet@48975: with WELL WELL' EMB blanchet@48975: show ?thesis by (auto simp add: embed_preserves_ofilter) blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_compat: blanchet@48975: assumes EMB: "embed r r' f" blanchet@48975: shows "compat r r' f" blanchet@48975: proof(unfold compat_def, clarify) blanchet@48975: fix a b blanchet@48975: assume *: "(a,b) \ r" blanchet@48975: hence 1: "b \ Field r" using Field_def[of r] by blast blanchet@55023: have "a \ under r b" blanchet@55023: using * under_def[of r] by simp blanchet@55023: hence "f a \ under r' (f b)" blanchet@48975: using EMB embed_def[of r r' f] blanchet@55023: bij_betw_def[of f "under r b" "under r' (f b)"] blanchet@55023: image_def[of f "under r b"] 1 by auto blanchet@48975: thus "(f a, f b) \ r'" blanchet@55023: by (auto simp add: under_def) blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_inj_on: blanchet@48975: assumes WELL: "Well_order r" and EMB: "embed r r' f" blanchet@48975: shows "inj_on f (Field r)" blanchet@48975: proof(unfold inj_on_def, clarify) blanchet@48975: (* Preliminary facts *) blanchet@48975: from WELL have Well: "wo_rel r" unfolding wo_rel_def . blanchet@48975: with wo_rel.TOTAL[of r] blanchet@48975: have Total: "Total r" by simp blanchet@48975: from Well wo_rel.REFL[of r] blanchet@48975: have Refl: "Refl r" by simp blanchet@48975: (* Main proof *) blanchet@48975: fix a b blanchet@48975: assume *: "a \ Field r" and **: "b \ Field r" and blanchet@48975: ***: "f a = f b" blanchet@48975: hence 1: "a \ Field r \ b \ Field r" blanchet@48975: unfolding Field_def by auto blanchet@48975: {assume "(a,b) \ r" blanchet@55023: hence "a \ under r b \ b \ under r b" blanchet@55023: using Refl by(auto simp add: under_def refl_on_def) blanchet@48975: hence "a = b" blanchet@48975: using EMB 1 *** blanchet@48975: by (auto simp add: embed_def bij_betw_def inj_on_def) blanchet@48975: } blanchet@48975: moreover blanchet@48975: {assume "(b,a) \ r" blanchet@55023: hence "a \ under r a \ b \ under r a" blanchet@55023: using Refl by(auto simp add: under_def refl_on_def) blanchet@48975: hence "a = b" blanchet@48975: using EMB 1 *** blanchet@48975: by (auto simp add: embed_def bij_betw_def inj_on_def) blanchet@48975: } blanchet@48975: ultimately blanchet@48975: show "a = b" using Total 1 blanchet@48975: by (auto simp add: total_on_def) blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_underS: wenzelm@49753: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMB: "embed r r' f" and IN: "a \ Field r" blanchet@55023: shows "bij_betw f (underS r a) (underS r' (f a))" blanchet@48975: proof- blanchet@55023: have "bij_betw f (under r a) (under r' (f a))" blanchet@48975: using assms by (auto simp add: embed_def) blanchet@48975: moreover blanchet@48975: {have "f a \ Field r'" using assms embed_Field[of r r' f] by auto blanchet@55023: hence "under r a = underS r a \ {a} \ blanchet@55023: under r' (f a) = underS r' (f a) \ {f a}" blanchet@55023: using assms by (auto simp add: order_on_defs Refl_under_underS) blanchet@48975: } blanchet@48975: moreover blanchet@55023: {have "a \ underS r a \ f a \ underS r' (f a)" blanchet@55023: unfolding underS_def by blast blanchet@48975: } blanchet@48975: ultimately show ?thesis blanchet@48975: by (auto simp add: notIn_Un_bij_betw3) blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_iff_compat_inj_on_ofilter: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" blanchet@48975: shows "embed r r' f = (compat r r' f \ inj_on f (Field r) \ wo_rel.ofilter r' (f`(Field r)))" blanchet@48975: using assms blanchet@48975: proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter, blanchet@48975: unfold embed_def, auto) (* get rid of one implication *) blanchet@48975: fix a blanchet@48975: assume *: "inj_on f (Field r)" and blanchet@48975: **: "compat r r' f" and blanchet@48975: ***: "wo_rel.ofilter r' (f`(Field r))" and blanchet@48975: ****: "a \ Field r" blanchet@48975: (* Preliminary facts *) blanchet@48975: have Well: "wo_rel r" blanchet@48975: using WELL wo_rel_def[of r] by simp blanchet@48975: hence Refl: "Refl r" blanchet@48975: using wo_rel.REFL[of r] by simp blanchet@48975: have Total: "Total r" blanchet@48975: using Well wo_rel.TOTAL[of r] by simp blanchet@48975: have Well': "wo_rel r'" blanchet@48975: using WELL' wo_rel_def[of r'] by simp blanchet@48975: hence Antisym': "antisym r'" blanchet@48975: using wo_rel.ANTISYM[of r'] by simp blanchet@48975: have "(a,a) \ r" blanchet@48975: using **** Well wo_rel.REFL[of r] blanchet@48975: refl_on_def[of _ r] by auto blanchet@48975: hence "(f a, f a) \ r'" blanchet@48975: using ** by(auto simp add: compat_def) blanchet@48975: hence 0: "f a \ Field r'" blanchet@48975: unfolding Field_def by auto blanchet@48975: have "f a \ f`(Field r)" blanchet@48975: using **** by auto blanchet@55023: hence 2: "under r' (f a) \ f`(Field r)" blanchet@48975: using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce blanchet@48975: (* Main proof *) blanchet@55023: show "bij_betw f (under r a) (under r' (f a))" blanchet@48975: proof(unfold bij_betw_def, auto) traytel@55811: show "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field]) blanchet@48975: next blanchet@55023: fix b assume "b \ under r a" blanchet@55023: thus "f b \ under r' (f a)" blanchet@55023: unfolding under_def using ** blanchet@48975: by (auto simp add: compat_def) blanchet@48975: next blanchet@55023: fix b' assume *****: "b' \ under r' (f a)" blanchet@48975: hence "b' \ f`(Field r)" blanchet@48975: using 2 by auto blanchet@48975: with Field_def[of r] obtain b where blanchet@48975: 3: "b \ Field r" and 4: "b' = f b" by auto blanchet@48975: have "(b,a): r" blanchet@48975: proof- blanchet@48975: {assume "(a,b) \ r" blanchet@48975: with ** 4 have "(f a, b'): r'" blanchet@48975: by (auto simp add: compat_def) blanchet@48975: with ***** Antisym' have "f a = b'" blanchet@55023: by(auto simp add: under_def antisym_def) blanchet@48975: with 3 **** 4 * have "a = b" blanchet@48975: by(auto simp add: inj_on_def) blanchet@48975: } blanchet@48975: moreover blanchet@48975: {assume "a = b" blanchet@48975: hence "(b,a) \ r" using Refl **** 3 blanchet@48975: by (auto simp add: refl_on_def) blanchet@48975: } blanchet@48975: ultimately blanchet@48975: show ?thesis using Total **** 3 by (fastforce simp add: total_on_def) blanchet@48975: qed blanchet@55023: with 4 show "b' \ f`(under r a)" blanchet@55023: unfolding under_def by auto blanchet@48975: qed blanchet@48975: qed blanchet@48975: blanchet@48975: lemma inv_into_ofilter_embed: blanchet@48975: assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and blanchet@55023: BIJ: "\b \ A. bij_betw f (under r b) (under r' (f b))" and blanchet@48975: IMAGE: "f ` A = Field r'" blanchet@48975: shows "embed r' r (inv_into A f)" blanchet@48975: proof- blanchet@48975: (* Preliminary facts *) blanchet@48975: have Well: "wo_rel r" blanchet@48975: using WELL wo_rel_def[of r] by simp blanchet@48975: have Refl: "Refl r" blanchet@48975: using Well wo_rel.REFL[of r] by simp blanchet@48975: have Total: "Total r" blanchet@48975: using Well wo_rel.TOTAL[of r] by simp blanchet@48975: (* Main proof *) blanchet@48975: have 1: "bij_betw f A (Field r')" blanchet@48975: proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE) blanchet@48975: fix b1 b2 blanchet@48975: assume *: "b1 \ A" and **: "b2 \ A" and blanchet@48975: ***: "f b1 = f b2" blanchet@48975: have 11: "b1 \ Field r \ b2 \ Field r" blanchet@48975: using * ** Well OF by (auto simp add: wo_rel.ofilter_def) blanchet@48975: moreover blanchet@48975: {assume "(b1,b2) \ r" blanchet@55023: hence "b1 \ under r b2 \ b2 \ under r b2" blanchet@55023: unfolding under_def using 11 Refl blanchet@48975: by (auto simp add: refl_on_def) blanchet@48975: hence "b1 = b2" using BIJ * ** *** blanchet@54482: by (simp add: bij_betw_def inj_on_def) blanchet@48975: } blanchet@48975: moreover blanchet@48975: {assume "(b2,b1) \ r" blanchet@55023: hence "b1 \ under r b1 \ b2 \ under r b1" blanchet@55023: unfolding under_def using 11 Refl blanchet@48975: by (auto simp add: refl_on_def) blanchet@48975: hence "b1 = b2" using BIJ * ** *** blanchet@54482: by (simp add: bij_betw_def inj_on_def) blanchet@48975: } blanchet@48975: ultimately blanchet@48975: show "b1 = b2" blanchet@48975: using Total by (auto simp add: total_on_def) blanchet@48975: qed blanchet@48975: (* *) blanchet@48975: let ?f' = "(inv_into A f)" blanchet@48975: (* *) blanchet@55023: have 2: "\b \ A. bij_betw ?f' (under r' (f b)) (under r b)" blanchet@48975: proof(clarify) blanchet@48975: fix b assume *: "b \ A" blanchet@55023: hence "under r b \ A" blanchet@48975: using Well OF by(auto simp add: wo_rel.ofilter_def) blanchet@48975: moreover blanchet@55023: have "f ` (under r b) = under r' (f b)" blanchet@48975: using * BIJ by (auto simp add: bij_betw_def) blanchet@48975: ultimately blanchet@55023: show "bij_betw ?f' (under r' (f b)) (under r b)" blanchet@48975: using 1 by (auto simp add: bij_betw_inv_into_subset) blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: have 3: "\b' \ Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))" blanchet@48975: proof(clarify) blanchet@48975: fix b' assume *: "b' \ Field r'" blanchet@48975: have "b' = f (?f' b')" using * 1 blanchet@48975: by (auto simp add: bij_betw_inv_into_right) blanchet@48975: moreover blanchet@48975: {obtain b where 31: "b \ A" and "f b = b'" using IMAGE * by force blanchet@48975: hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left) blanchet@48975: with 31 have "?f' b' \ A" by auto blanchet@48975: } blanchet@48975: ultimately blanchet@55023: show "bij_betw ?f' (under r' b') (under r (?f' b'))" blanchet@48975: using 2 by auto blanchet@48975: qed blanchet@48975: (* *) blanchet@48975: thus ?thesis unfolding embed_def . blanchet@48975: qed blanchet@48975: blanchet@48975: lemma inv_into_underS_embed: blanchet@48975: assumes WELL: "Well_order r" and blanchet@55023: BIJ: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and blanchet@48975: IN: "a \ Field r" and blanchet@55023: IMAGE: "f ` (underS r a) = Field r'" blanchet@55023: shows "embed r' r (inv_into (underS r a) f)" blanchet@48975: using assms blanchet@48975: by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed) blanchet@48975: blanchet@48975: lemma inv_into_Field_embed: blanchet@48975: assumes WELL: "Well_order r" and EMB: "embed r r' f" and blanchet@48975: IMAGE: "Field r' \ f ` (Field r)" blanchet@48975: shows "embed r' r (inv_into (Field r) f)" blanchet@48975: proof- blanchet@55023: have "(\b \ Field r. bij_betw f (under r b) (under r' (f b)))" blanchet@48975: using EMB by (auto simp add: embed_def) blanchet@48975: moreover blanchet@48975: have "f ` (Field r) \ Field r'" blanchet@48975: using EMB WELL by (auto simp add: embed_Field) blanchet@48975: ultimately blanchet@48975: show ?thesis using assms blanchet@48975: by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed) blanchet@48975: qed blanchet@48975: blanchet@48975: lemma inv_into_Field_embed_bij_betw: blanchet@48975: assumes WELL: "Well_order r" and blanchet@48975: EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')" blanchet@48975: shows "embed r' r (inv_into (Field r) f)" blanchet@48975: proof- blanchet@48975: have "Field r' \ f ` (Field r)" blanchet@48975: using BIJ by (auto simp add: bij_betw_def) blanchet@48975: thus ?thesis using assms blanchet@48975: by(auto simp add: inv_into_Field_embed) blanchet@48975: qed blanchet@48975: blanchet@48975: blanchet@48975: subsection {* Given any two well-orders, one can be embedded in the other *} blanchet@48975: blanchet@48975: text{* Here is an overview of the proof of of this fact, stated in theorem blanchet@48975: @{text "wellorders_totally_ordered"}: blanchet@48975: blanchet@48975: Fix the well-orders @{text "r::'a rel"} and @{text "r'::'a' rel"}. blanchet@48975: Attempt to define an embedding @{text "f::'a \ 'a'"} from @{text "r"} to @{text "r'"} in the blanchet@48975: natural way by well-order recursion ("hoping" that @{text "Field r"} turns out to be smaller blanchet@48975: than @{text "Field r'"}), but also record, at the recursive step, in a function blanchet@48975: @{text "g::'a \ bool"}, the extra information of whether @{text "Field r'"} blanchet@48975: gets exhausted or not. blanchet@48975: blanchet@48975: If @{text "Field r'"} does not get exhausted, then @{text "Field r"} is indeed smaller blanchet@48975: and @{text "f"} is the desired embedding from @{text "r"} to @{text "r'"} blanchet@48975: (lemma @{text "wellorders_totally_ordered_aux"}). blanchet@48975: blanchet@48975: Otherwise, it means that @{text "Field r'"} is the smaller one, and the inverse of blanchet@48975: (the "good" segment of) @{text "f"} is the desired embedding from @{text "r'"} to @{text "r"} blanchet@48975: (lemma @{text "wellorders_totally_ordered_aux2"}). blanchet@48975: *} blanchet@48975: blanchet@48975: lemma wellorders_totally_ordered_aux: blanchet@48975: fixes r ::"'a rel" and r'::"'a' rel" and blanchet@48975: f :: "'a \ 'a'" and a::'a blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \ Field r" and blanchet@55023: IH: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and blanchet@55023: NOT: "f ` (underS r a) \ Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))" blanchet@55023: shows "bij_betw f (under r a) (under r' (f a))" blanchet@48975: proof- blanchet@48975: (* Preliminary facts *) blanchet@48975: have Well: "wo_rel r" using WELL unfolding wo_rel_def . blanchet@48975: hence Refl: "Refl r" using wo_rel.REFL[of r] by auto blanchet@48975: have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto blanchet@48975: have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . blanchet@55023: have OF: "wo_rel.ofilter r (underS r a)" blanchet@48975: by (auto simp add: Well wo_rel.underS_ofilter) blanchet@55023: hence UN: "underS r a = (\ b \ underS r a. under r b)" blanchet@55023: using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast blanchet@55023: (* Gather facts about elements of underS r a *) blanchet@55023: {fix b assume *: "b \ underS r a" blanchet@55023: hence t0: "(b,a) \ r \ b \ a" unfolding underS_def by auto blanchet@48975: have t1: "b \ Field r" blanchet@55023: using * underS_Field[of r a] by auto blanchet@55023: have t2: "f`(under r b) = under r' (f b)" blanchet@48975: using IH * by (auto simp add: bij_betw_def) blanchet@55023: hence t3: "wo_rel.ofilter r' (f`(under r b))" blanchet@48975: using Well' by (auto simp add: wo_rel.under_ofilter) blanchet@55023: have "f`(under r b) \ Field r'" blanchet@55023: using t2 by (auto simp add: under_Field) blanchet@48975: moreover blanchet@55023: have "b \ under r b" blanchet@55023: using t1 by(auto simp add: Refl Refl_under_in) blanchet@48975: ultimately blanchet@48975: have t4: "f b \ Field r'" by auto blanchet@55023: have "f`(under r b) = under r' (f b) \ blanchet@55023: wo_rel.ofilter r' (f`(under r b)) \ blanchet@48975: f b \ Field r'" blanchet@48975: using t2 t3 t4 by auto blanchet@48975: } blanchet@48975: hence bFact: blanchet@55023: "\b \ underS r a. f`(under r b) = under r' (f b) \ blanchet@55023: wo_rel.ofilter r' (f`(under r b)) \ blanchet@48975: f b \ Field r'" by blast blanchet@48975: (* *) blanchet@55023: have subField: "f`(underS r a) \ Field r'" blanchet@48975: using bFact by blast blanchet@48975: (* *) blanchet@55023: have OF': "wo_rel.ofilter r' (f`(underS r a))" blanchet@48975: proof- blanchet@55023: have "f`(underS r a) = f`(\ b \ underS r a. under r b)" blanchet@48975: using UN by auto blanchet@55023: also have "\ = (\ b \ underS r a. f`(under r b))" by blast blanchet@55023: also have "\ = (\ b \ underS r a. (under r' (f b)))" blanchet@48975: using bFact by auto blanchet@48975: finally blanchet@55023: have "f`(underS r a) = (\ b \ underS r a. (under r' (f b)))" . blanchet@48975: thus ?thesis blanchet@48975: using Well' bFact blanchet@55023: wo_rel.ofilter_UNION[of r' "underS r a" "\ b. under r' (f b)"] by fastforce blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: have "f`(underS r a) \ AboveS r' (f`(underS r a)) = Field r'" blanchet@48975: using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field) blanchet@55023: hence NE: "AboveS r' (f`(underS r a)) \ {}" blanchet@48975: using subField NOT by blast blanchet@48975: (* Main proof *) blanchet@55023: have INCL1: "f`(underS r a) \ underS r' (f a) " blanchet@48975: proof(auto) blanchet@55023: fix b assume *: "b \ underS r a" blanchet@48975: have "f b \ f a \ (f b, f a) \ r'" blanchet@48975: using subField Well' SUC NE * blanchet@55023: wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force blanchet@55023: thus "f b \ underS r' (f a)" blanchet@55023: unfolding underS_def by simp blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: have INCL2: "underS r' (f a) \ f`(underS r a)" blanchet@48975: proof blanchet@55023: fix b' assume "b' \ underS r' (f a)" blanchet@48975: hence "b' \ f a \ (b', f a) \ r'" blanchet@55023: unfolding underS_def by simp blanchet@55023: thus "b' \ f`(underS r a)" blanchet@48975: using Well' SUC NE OF' blanchet@55023: wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: have INJ: "inj_on f (underS r a)" blanchet@48975: proof- blanchet@55023: have "\b \ underS r a. inj_on f (under r b)" blanchet@48975: using IH by (auto simp add: bij_betw_def) blanchet@48975: moreover blanchet@55023: have "\b. wo_rel.ofilter r (under r b)" blanchet@48975: using Well by (auto simp add: wo_rel.under_ofilter) blanchet@48975: ultimately show ?thesis blanchet@48975: using WELL bFact UN blanchet@55023: UNION_inj_on_ofilter[of r "underS r a" "\b. under r b" f] blanchet@48975: by auto blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: have BIJ: "bij_betw f (underS r a) (underS r' (f a))" blanchet@48975: unfolding bij_betw_def blanchet@48975: using INJ INCL1 INCL2 by auto blanchet@48975: (* *) blanchet@48975: have "f a \ Field r'" blanchet@48975: using Well' subField NE SUC blanchet@48975: by (auto simp add: wo_rel.suc_inField) blanchet@48975: thus ?thesis blanchet@48975: using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma wellorders_totally_ordered_aux2: blanchet@48975: fixes r ::"'a rel" and r'::"'a' rel" and blanchet@48975: f :: "'a \ 'a'" and g :: "'a \ bool" and a::'a blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: MAIN1: blanchet@55023: "\ a. (False \ g`(underS r a) \ f`(underS r a) \ Field r' blanchet@55023: \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) blanchet@48975: \ blanchet@55023: (\(False \ (g`(underS r a)) \ f`(underS r a) \ Field r') blanchet@48975: \ g a = False)" and blanchet@55023: MAIN2: "\ a. a \ Field r \ False \ g`(under r a) \ blanchet@55023: bij_betw f (under r a) (under r' (f a))" and blanchet@55023: Case: "a \ Field r \ False \ g`(under r a)" blanchet@48975: shows "\f'. embed r' r f'" blanchet@48975: proof- blanchet@48975: have Well: "wo_rel r" using WELL unfolding wo_rel_def . blanchet@48975: hence Refl: "Refl r" using wo_rel.REFL[of r] by auto blanchet@48975: have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto blanchet@48975: have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto blanchet@48975: have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . blanchet@48975: (* *) blanchet@55023: have 0: "under r a = underS r a \ {a}" blanchet@55023: using Refl Case by(auto simp add: Refl_under_underS) blanchet@48975: (* *) blanchet@48975: have 1: "g a = False" blanchet@48975: proof- blanchet@48975: {assume "g a \ False" blanchet@55023: with 0 Case have "False \ g`(underS r a)" by blast blanchet@48975: with MAIN1 have "g a = False" by blast} blanchet@48975: thus ?thesis by blast blanchet@48975: qed blanchet@48975: let ?A = "{a \ Field r. g a = False}" blanchet@48975: let ?a = "(wo_rel.minim r ?A)" blanchet@48975: (* *) blanchet@48975: have 2: "?A \ {} \ ?A \ Field r" using Case 1 by blast blanchet@48975: (* *) blanchet@55023: have 3: "False \ g`(underS r ?a)" blanchet@48975: proof blanchet@55023: assume "False \ g`(underS r ?a)" blanchet@55023: then obtain b where "b \ underS r ?a" and 31: "g b = False" by auto blanchet@48975: hence 32: "(b,?a) \ r \ b \ ?a" blanchet@55023: by (auto simp add: underS_def) blanchet@48975: hence "b \ Field r" unfolding Field_def by auto blanchet@48975: with 31 have "b \ ?A" by auto blanchet@48975: hence "(?a,b) \ r" using wo_rel.minim_least 2 Well by fastforce blanchet@48975: (* again: why worked without type annotations? *) blanchet@48975: with 32 Antisym show False blanchet@48975: by (auto simp add: antisym_def) blanchet@48975: qed blanchet@48975: have temp: "?a \ ?A" blanchet@48975: using Well 2 wo_rel.minim_in[of r ?A] by auto blanchet@48975: hence 4: "?a \ Field r" by auto blanchet@48975: (* *) blanchet@48975: have 5: "g ?a = False" using temp by blast blanchet@48975: (* *) blanchet@55023: have 6: "f`(underS r ?a) = Field r'" blanchet@48975: using MAIN1[of ?a] 3 5 by blast blanchet@48975: (* *) blanchet@55023: have 7: "\b \ underS r ?a. bij_betw f (under r b) (under r' (f b))" blanchet@48975: proof blanchet@55023: fix b assume as: "b \ underS r ?a" blanchet@48975: moreover blanchet@55023: have "wo_rel.ofilter r (underS r ?a)" blanchet@48975: using Well by (auto simp add: wo_rel.underS_ofilter) blanchet@48975: ultimately blanchet@55023: have "False \ g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+ blanchet@48975: moreover have "b \ Field r" blanchet@55023: unfolding Field_def using as by (auto simp add: underS_def) blanchet@48975: ultimately blanchet@55023: show "bij_betw f (under r b) (under r' (f b))" blanchet@48975: using MAIN2 by auto blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: have "embed r' r (inv_into (underS r ?a) f)" blanchet@48975: using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto blanchet@48975: thus ?thesis blanchet@48975: unfolding embed_def by blast blanchet@48975: qed blanchet@48975: blanchet@48975: theorem wellorders_totally_ordered: blanchet@48975: fixes r ::"'a rel" and r'::"'a' rel" blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" blanchet@48975: shows "(\f. embed r r' f) \ (\f'. embed r' r f')" blanchet@48975: proof- blanchet@48975: (* Preliminary facts *) blanchet@48975: have Well: "wo_rel r" using WELL unfolding wo_rel_def . blanchet@48975: hence Refl: "Refl r" using wo_rel.REFL[of r] by auto blanchet@48975: have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto blanchet@48975: have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . blanchet@48975: (* Main proof *) blanchet@48975: obtain H where H_def: "H = blanchet@55023: (\h a. if False \ (snd o h)`(underS r a) \ (fst o h)`(underS r a) \ Field r' blanchet@55023: then (wo_rel.suc r' ((fst o h)`(underS r a)), True) blanchet@48975: else (undefined, False))" by blast blanchet@48975: have Adm: "wo_rel.adm_wo r H" blanchet@48975: using Well blanchet@48975: proof(unfold wo_rel.adm_wo_def, clarify) blanchet@48975: fix h1::"'a \ 'a' * bool" and h2::"'a \ 'a' * bool" and x blanchet@55023: assume "\y\underS r x. h1 y = h2 y" blanchet@55023: hence "\y\underS r x. (fst o h1) y = (fst o h2) y \ blanchet@48975: (snd o h1) y = (snd o h2) y" by auto blanchet@55023: hence "(fst o h1)`(underS r x) = (fst o h2)`(underS r x) \ blanchet@55023: (snd o h1)`(underS r x) = (snd o h2)`(underS r x)" wenzelm@49922: by (auto simp add: image_def) wenzelm@49922: thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball) blanchet@48975: qed blanchet@48975: (* More constant definitions: *) blanchet@48975: obtain h::"'a \ 'a' * bool" and f::"'a \ 'a'" and g::"'a \ bool" blanchet@48975: where h_def: "h = wo_rel.worec r H" and blanchet@48975: f_def: "f = fst o h" and g_def: "g = snd o h" by blast blanchet@48975: obtain test where test_def: blanchet@55023: "test = (\ a. False \ (g`(underS r a)) \ f`(underS r a) \ Field r')" by blast blanchet@48975: (* *) blanchet@48975: have *: "\ a. h a = H h a" blanchet@48975: using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def) blanchet@48975: have Main1: blanchet@55023: "\ a. (test a \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ blanchet@48975: (\(test a) \ g a = False)" blanchet@48975: proof- (* How can I prove this withou fixing a? *) blanchet@55023: fix a show "(test a \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ blanchet@48975: (\(test a) \ g a = False)" blanchet@48975: using *[of a] test_def f_def g_def H_def by auto blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: let ?phi = "\ a. a \ Field r \ False \ g`(under r a) \ blanchet@55023: bij_betw f (under r a) (under r' (f a))" blanchet@48975: have Main2: "\ a. ?phi a" blanchet@48975: proof- blanchet@48975: fix a show "?phi a" blanchet@48975: proof(rule wo_rel.well_order_induct[of r ?phi], blanchet@48975: simp only: Well, clarify) blanchet@48975: fix a blanchet@48975: assume IH: "\b. b \ a \ (b,a) \ r \ ?phi b" and blanchet@48975: *: "a \ Field r" and blanchet@55023: **: "False \ g`(under r a)" blanchet@55023: have 1: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" blanchet@48975: proof(clarify) blanchet@55023: fix b assume ***: "b \ underS r a" blanchet@55023: hence 0: "(b,a) \ r \ b \ a" unfolding underS_def by auto blanchet@48975: moreover have "b \ Field r" blanchet@55023: using *** underS_Field[of r a] by auto blanchet@55023: moreover have "False \ g`(under r b)" blanchet@55023: using 0 ** Trans under_incr[of r b a] by auto blanchet@55023: ultimately show "bij_betw f (under r b) (under r' (f b))" blanchet@48975: using IH by auto blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: have 21: "False \ g`(underS r a)" blanchet@55023: using ** underS_subset_under[of r a] by auto blanchet@55023: have 22: "g`(under r a) \ {True}" using ** by auto blanchet@55023: moreover have 23: "a \ under r a" blanchet@55023: using Refl * by (auto simp add: Refl_under_in) blanchet@48975: ultimately have 24: "g a = True" by blast blanchet@55023: have 2: "f`(underS r a) \ Field r'" blanchet@48975: proof blanchet@55023: assume "f`(underS r a) = Field r'" blanchet@48975: hence "g a = False" using Main1 test_def by blast blanchet@48975: with 24 show False using ** by blast blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: have 3: "f a = wo_rel.suc r' (f`(underS r a))" blanchet@48975: using 21 2 Main1 test_def by blast blanchet@48975: (* *) blanchet@55023: show "bij_betw f (under r a) (under r' (f a))" blanchet@48975: using WELL WELL' 1 2 3 * blanchet@48975: wellorders_totally_ordered_aux[of r r' a f] by auto blanchet@48975: qed blanchet@48975: qed blanchet@48975: (* *) blanchet@55023: let ?chi = "(\ a. a \ Field r \ False \ g`(under r a))" blanchet@48975: show ?thesis blanchet@48975: proof(cases "\a. ?chi a") blanchet@48975: assume "\ (\a. ?chi a)" blanchet@55023: hence "\a \ Field r. bij_betw f (under r a) (under r' (f a))" blanchet@48975: using Main2 by blast blanchet@48975: thus ?thesis unfolding embed_def by blast blanchet@48975: next blanchet@48975: assume "\a. ?chi a" blanchet@48975: then obtain a where "?chi a" by blast blanchet@48975: hence "\f'. embed r' r f'" blanchet@48975: using wellorders_totally_ordered_aux2[of r r' g f a] blanchet@54482: WELL WELL' Main1 Main2 test_def by fast blanchet@48975: thus ?thesis by blast blanchet@48975: qed blanchet@48975: qed blanchet@48975: blanchet@48975: blanchet@55101: subsection {* Uniqueness of embeddings *} blanchet@48975: blanchet@48975: text{* Here we show a fact complementary to the one from the previous subsection -- namely, blanchet@48975: that between any two well-orders there is {\em at most} one embedding, and is the one blanchet@48975: definable by the expected well-order recursive equation. As a consequence, any two blanchet@48975: embeddings of opposite directions are mutually inverse. *} blanchet@48975: blanchet@48975: lemma embed_determined: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMB: "embed r r' f" and IN: "a \ Field r" blanchet@55023: shows "f a = wo_rel.suc r' (f`(underS r a))" blanchet@48975: proof- blanchet@55023: have "bij_betw f (underS r a) (underS r' (f a))" blanchet@48975: using assms by (auto simp add: embed_underS) blanchet@55023: hence "f`(underS r a) = underS r' (f a)" blanchet@48975: by (auto simp add: bij_betw_def) blanchet@48975: moreover blanchet@48975: {have "f a \ Field r'" using IN blanchet@48975: using EMB WELL embed_Field[of r r' f] by auto blanchet@55023: hence "f a = wo_rel.suc r' (underS r' (f a))" blanchet@48975: using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS) blanchet@48975: } blanchet@48975: ultimately show ?thesis by simp blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_unique: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMBf: "embed r r' f" and EMBg: "embed r r' g" blanchet@48975: shows "a \ Field r \ f a = g a" blanchet@48975: proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def) blanchet@48975: fix a blanchet@48975: assume IH: "\b. b \ a \ (b,a): r \ b \ Field r \ f b = g b" and blanchet@48975: *: "a \ Field r" blanchet@55023: hence "\b \ underS r a. f b = g b" blanchet@55023: unfolding underS_def by (auto simp add: Field_def) blanchet@55023: hence "f`(underS r a) = g`(underS r a)" by force blanchet@48975: thus "f a = g a" blanchet@48975: using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_bothWays_inverse: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMB: "embed r r' f" and EMB': "embed r' r f'" blanchet@48975: shows "(\a \ Field r. f'(f a) = a) \ (\a' \ Field r'. f(f' a') = a')" blanchet@48975: proof- blanchet@48975: have "embed r r (f' o f)" using assms blanchet@48975: by(auto simp add: comp_embed) blanchet@48975: moreover have "embed r r id" using assms blanchet@48975: by (auto simp add: id_embed) blanchet@48975: ultimately have "\a \ Field r. f'(f a) = a" blanchet@48975: using assms embed_unique[of r r "f' o f" id] id_def by auto blanchet@48975: moreover blanchet@48975: {have "embed r' r' (f o f')" using assms blanchet@48975: by(auto simp add: comp_embed) blanchet@48975: moreover have "embed r' r' id" using assms blanchet@48975: by (auto simp add: id_embed) blanchet@48975: ultimately have "\a' \ Field r'. f(f' a') = a'" blanchet@48975: using assms embed_unique[of r' r' "f o f'" id] id_def by auto blanchet@48975: } blanchet@48975: ultimately show ?thesis by blast blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_bothWays_bij_betw: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMB: "embed r r' f" and EMB': "embed r' r g" blanchet@48975: shows "bij_betw f (Field r) (Field r')" blanchet@48975: proof- blanchet@48975: let ?A = "Field r" let ?A' = "Field r'" blanchet@48975: have "embed r r (g o f) \ embed r' r' (f o g)" blanchet@48975: using assms by (auto simp add: comp_embed) blanchet@48975: hence 1: "(\a \ ?A. g(f a) = a) \ (\a' \ ?A'. f(g a') = a')" blanchet@48975: using WELL id_embed[of r] embed_unique[of r r "g o f" id] blanchet@48975: WELL' id_embed[of r'] embed_unique[of r' r' "f o g" id] blanchet@48975: id_def by auto blanchet@48975: have 2: "(\a \ ?A. f a \ ?A') \ (\a' \ ?A'. g a' \ ?A)" blanchet@48975: using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast blanchet@48975: (* *) blanchet@48975: show ?thesis blanchet@48975: proof(unfold bij_betw_def inj_on_def, auto simp add: 2) blanchet@48975: fix a b assume *: "a \ ?A" "b \ ?A" and **: "f a = f b" blanchet@48975: have "a = g(f a) \ b = g(f b)" using * 1 by auto blanchet@48975: with ** show "a = b" by auto blanchet@48975: next blanchet@48975: fix a' assume *: "a' \ ?A'" blanchet@48975: hence "g a' \ ?A \ f(g a') = a'" using 1 2 by auto blanchet@48975: thus "a' \ f ` ?A" by force blanchet@48975: qed blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_bothWays_iso: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMB: "embed r r' f" and EMB': "embed r' r g" blanchet@48975: shows "iso r r' f" blanchet@48975: unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw) blanchet@48975: blanchet@48975: blanchet@55101: subsection {* More properties of embeddings, strict embeddings and isomorphisms *} blanchet@48975: blanchet@48975: lemma embed_bothWays_Field_bij_betw: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and blanchet@48975: EMB: "embed r r' f" and EMB': "embed r' r f'" blanchet@48975: shows "bij_betw f (Field r) (Field r')" blanchet@48975: proof- blanchet@48975: have "(\a \ Field r. f'(f a) = a) \ (\a' \ Field r'. f(f' a') = a')" blanchet@48975: using assms by (auto simp add: embed_bothWays_inverse) blanchet@48975: moreover blanchet@48975: have "f`(Field r) \ Field r' \ f' ` (Field r') \ Field r" blanchet@48975: using assms by (auto simp add: embed_Field) blanchet@48975: ultimately blanchet@48975: show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embedS_comp_embed: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" blanchet@48975: and EMB: "embedS r r' f" and EMB': "embed r' r'' f'" blanchet@48975: shows "embedS r r'' (f' o f)" blanchet@48975: proof- blanchet@48975: let ?g = "(f' o f)" let ?h = "inv_into (Field r) ?g" blanchet@48975: have 1: "embed r r' f \ \ (bij_betw f (Field r) (Field r'))" blanchet@48975: using EMB by (auto simp add: embedS_def) blanchet@48975: hence 2: "embed r r'' ?g" blanchet@48975: using WELL EMB' comp_embed[of r r' f r'' f'] by auto blanchet@48975: moreover blanchet@48975: {assume "bij_betw ?g (Field r) (Field r'')" blanchet@48975: hence "embed r'' r ?h" using 2 WELL blanchet@48975: by (auto simp add: inv_into_Field_embed_bij_betw) blanchet@48975: hence "embed r' r (?h o f')" using WELL' EMB' blanchet@48975: by (auto simp add: comp_embed) blanchet@48975: hence "bij_betw f (Field r) (Field r')" using WELL WELL' 1 blanchet@48975: by (auto simp add: embed_bothWays_Field_bij_betw) blanchet@48975: with 1 have False by blast blanchet@48975: } blanchet@48975: ultimately show ?thesis unfolding embedS_def by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_comp_embedS: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" blanchet@48975: and EMB: "embed r r' f" and EMB': "embedS r' r'' f'" blanchet@48975: shows "embedS r r'' (f' o f)" blanchet@48975: proof- blanchet@48975: let ?g = "(f' o f)" let ?h = "inv_into (Field r) ?g" blanchet@48975: have 1: "embed r' r'' f' \ \ (bij_betw f' (Field r') (Field r''))" blanchet@48975: using EMB' by (auto simp add: embedS_def) blanchet@48975: hence 2: "embed r r'' ?g" blanchet@48975: using WELL EMB comp_embed[of r r' f r'' f'] by auto blanchet@48975: moreover blanchet@48975: {assume "bij_betw ?g (Field r) (Field r'')" blanchet@48975: hence "embed r'' r ?h" using 2 WELL blanchet@48975: by (auto simp add: inv_into_Field_embed_bij_betw) blanchet@48975: hence "embed r'' r' (f o ?h)" using WELL'' EMB blanchet@48975: by (auto simp add: comp_embed) blanchet@48975: hence "bij_betw f' (Field r') (Field r'')" using WELL' WELL'' 1 blanchet@48975: by (auto simp add: embed_bothWays_Field_bij_betw) blanchet@48975: with 1 have False by blast blanchet@48975: } blanchet@48975: ultimately show ?thesis unfolding embedS_def by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embed_comp_iso: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" blanchet@48975: and EMB: "embed r r' f" and EMB': "iso r' r'' f'" blanchet@48975: shows "embed r r'' (f' o f)" blanchet@48975: using assms unfolding iso_def blanchet@48975: by (auto simp add: comp_embed) blanchet@48975: blanchet@48975: lemma iso_comp_embed: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" blanchet@48975: and EMB: "iso r r' f" and EMB': "embed r' r'' f'" blanchet@48975: shows "embed r r'' (f' o f)" blanchet@48975: using assms unfolding iso_def blanchet@48975: by (auto simp add: comp_embed) blanchet@48975: blanchet@48975: lemma embedS_comp_iso: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" blanchet@48975: and EMB: "embedS r r' f" and EMB': "iso r' r'' f'" blanchet@48975: shows "embedS r r'' (f' o f)" blanchet@48975: using assms unfolding iso_def blanchet@48975: by (auto simp add: embedS_comp_embed) blanchet@48975: blanchet@48975: lemma iso_comp_embedS: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" blanchet@48975: and EMB: "iso r r' f" and EMB': "embedS r' r'' f'" blanchet@48975: shows "embedS r r'' (f' o f)" blanchet@48975: using assms unfolding iso_def using embed_comp_embedS blanchet@48975: by (auto simp add: embed_comp_embedS) blanchet@48975: blanchet@48975: lemma embedS_Field: blanchet@48975: assumes WELL: "Well_order r" and EMB: "embedS r r' f" blanchet@48975: shows "f ` (Field r) < Field r'" blanchet@48975: proof- blanchet@48975: have "f`(Field r) \ Field r'" using assms blanchet@48975: by (auto simp add: embed_Field embedS_def) blanchet@48975: moreover blanchet@48975: {have "inj_on f (Field r)" using assms blanchet@48975: by (auto simp add: embedS_def embed_inj_on) blanchet@48975: hence "f`(Field r) \ Field r'" using EMB blanchet@48975: by (auto simp add: embedS_def bij_betw_def) blanchet@48975: } blanchet@48975: ultimately show ?thesis by blast blanchet@48975: qed blanchet@48975: blanchet@48975: lemma embedS_iff: blanchet@48975: assumes WELL: "Well_order r" and ISO: "embed r r' f" blanchet@48975: shows "embedS r r' f = (f ` (Field r) < Field r')" blanchet@48975: proof blanchet@48975: assume "embedS r r' f" blanchet@48975: thus "f ` Field r \ Field r'" blanchet@48975: using WELL by (auto simp add: embedS_Field) blanchet@48975: next blanchet@48975: assume "f ` Field r \ Field r'" blanchet@48975: hence "\ bij_betw f (Field r) (Field r')" blanchet@48975: unfolding bij_betw_def by blast blanchet@48975: thus "embedS r r' f" unfolding embedS_def blanchet@48975: using ISO by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma iso_Field: blanchet@48975: "iso r r' f \ f ` (Field r) = Field r'" blanchet@48975: using assms by (auto simp add: iso_def bij_betw_def) blanchet@48975: blanchet@48975: lemma iso_iff: blanchet@48975: assumes "Well_order r" blanchet@48975: shows "iso r r' f = (embed r r' f \ f ` (Field r) = Field r')" blanchet@48975: proof blanchet@48975: assume "iso r r' f" blanchet@48975: thus "embed r r' f \ f ` (Field r) = Field r'" blanchet@48975: by (auto simp add: iso_Field iso_def) blanchet@48975: next blanchet@48975: assume *: "embed r r' f \ f ` Field r = Field r'" blanchet@48975: hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on) blanchet@48975: with * have "bij_betw f (Field r) (Field r')" blanchet@48975: unfolding bij_betw_def by simp blanchet@48975: with * show "iso r r' f" unfolding iso_def by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma iso_iff2: blanchet@48975: assumes "Well_order r" blanchet@48975: shows "iso r r' f = (bij_betw f (Field r) (Field r') \ blanchet@48975: (\a \ Field r. \b \ Field r. blanchet@48975: (((a,b) \ r) = ((f a, f b) \ r'))))" blanchet@48975: using assms blanchet@48975: proof(auto simp add: iso_def) blanchet@48975: fix a b blanchet@48975: assume "embed r r' f" blanchet@48975: hence "compat r r' f" using embed_compat[of r] by auto blanchet@48975: moreover assume "(a,b) \ r" blanchet@48975: ultimately show "(f a, f b) \ r'" using compat_def[of r] by auto blanchet@48975: next blanchet@48975: let ?f' = "inv_into (Field r) f" blanchet@48975: assume "embed r r' f" and 1: "bij_betw f (Field r) (Field r')" blanchet@48975: hence "embed r' r ?f'" using assms blanchet@48975: by (auto simp add: inv_into_Field_embed_bij_betw) blanchet@48975: hence 2: "compat r' r ?f'" using embed_compat[of r'] by auto blanchet@48975: fix a b assume *: "a \ Field r" "b \ Field r" and **: "(f a,f b) \ r'" blanchet@48975: hence "?f'(f a) = a \ ?f'(f b) = b" using 1 blanchet@48975: by (auto simp add: bij_betw_inv_into_left) blanchet@48975: thus "(a,b) \ r" using ** 2 compat_def[of r' r ?f'] by fastforce blanchet@48975: next blanchet@48975: assume *: "bij_betw f (Field r) (Field r')" and blanchet@48975: **: "\a\Field r. \b\Field r. ((a, b) \ r) = ((f a, f b) \ r')" blanchet@55023: have 1: "\ a. under r a \ Field r \ under r' (f a) \ Field r'" blanchet@55023: by (auto simp add: under_Field) blanchet@48975: have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def) blanchet@48975: {fix a assume ***: "a \ Field r" blanchet@55023: have "bij_betw f (under r a) (under r' (f a))" blanchet@48975: proof(unfold bij_betw_def, auto) traytel@55811: show "inj_on f (under r a)" using 1 2 subset_inj_on by blast blanchet@48975: next blanchet@55023: fix b assume "b \ under r a" blanchet@48975: hence "a \ Field r \ b \ Field r \ (b,a) \ r" blanchet@55023: unfolding under_def by (auto simp add: Field_def Range_def Domain_def) blanchet@55023: with 1 ** show "f b \ under r' (f a)" blanchet@55023: unfolding under_def by auto blanchet@48975: next blanchet@55023: fix b' assume "b' \ under r' (f a)" blanchet@55023: hence 3: "(b',f a) \ r'" unfolding under_def by simp blanchet@48975: hence "b' \ Field r'" unfolding Field_def by auto blanchet@48975: with * obtain b where "b \ Field r \ f b = b'" blanchet@48975: unfolding bij_betw_def by force blanchet@48975: with 3 ** *** blanchet@55023: show "b' \ f ` (under r a)" unfolding under_def by blast blanchet@48975: qed blanchet@48975: } blanchet@48975: thus "embed r r' f" unfolding embed_def using * by auto blanchet@48975: qed blanchet@48975: blanchet@48975: lemma iso_iff3: blanchet@48975: assumes WELL: "Well_order r" and WELL': "Well_order r'" blanchet@48975: shows "iso r r' f = (bij_betw f (Field r) (Field r') \ compat r r' f)" blanchet@48975: proof blanchet@48975: assume "iso r r' f" blanchet@48975: thus "bij_betw f (Field r) (Field r') \ compat r r' f" blanchet@48975: unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def) blanchet@48975: next blanchet@48975: have Well: "wo_rel r \ wo_rel r'" using WELL WELL' blanchet@48975: by (auto simp add: wo_rel_def) blanchet@48975: assume *: "bij_betw f (Field r) (Field r') \ compat r r' f" blanchet@48975: thus "iso r r' f" blanchet@48975: unfolding "compat_def" using assms blanchet@48975: proof(auto simp add: iso_iff2) blanchet@48975: fix a b assume **: "a \ Field r" "b \ Field r" and blanchet@48975: ***: "(f a, f b) \ r'" blanchet@48975: {assume "(b,a) \ r \ b = a" blanchet@48975: hence "(b,a): r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast blanchet@48975: hence "(f b, f a) \ r'" using * unfolding compat_def by auto blanchet@48975: hence "f a = f b" blanchet@48975: using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast blanchet@48975: hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto blanchet@48975: hence "(a,b) \ r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast blanchet@48975: } blanchet@48975: thus "(a,b) \ r" blanchet@48975: using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast blanchet@48975: qed blanchet@48975: qed blanchet@48975: blanchet@48975: end