# HG changeset patch # User blanchet # Date 1409582079 -7200 # Node ID b7cab82f488e9696e94bfb98cd50b9d9cdef49fa # Parent 3831312eb476b47b2d42809a1b36883d4690ffdc renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions' diff -r 3831312eb476 -r b7cab82f488e src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Sep 01 16:34:38 2014 +0200 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Sep 01 16:34:39 2014 +0200 @@ -8,7 +8,7 @@ header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *} theory BNF_Cardinal_Order_Relation -imports Zorn BNF_Constructions_on_Wellorders +imports Zorn BNF_Wellorder_Constructions begin text{* In this section, we define cardinal-order relations to be minim well-orders diff -r 3831312eb476 -r b7cab82f488e src/HOL/BNF_Constructions_on_Wellorders.thy --- a/src/HOL/BNF_Constructions_on_Wellorders.thy Mon Sep 01 16:34:38 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1656 +0,0 @@ -(* Title: HOL/BNF_Constructions_on_Wellorders.thy - Author: Andrei Popescu, TU Muenchen - Copyright 2012 - -Constructions on wellorders as needed by bounded natural functors. -*) - -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 "\o"}), -@{text "ordLess"}, of being strictly embedded (abbreviated @{text " 'a set \ 'a rel" -where "Restr r A \ r Int (A \ A)" - -lemma Restr_subset: -"A \ B \ 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 \ Refl(Restr r A)" -unfolding refl_on_def Field_def by auto - -lemma antisym_Restr: -"antisym r \ antisym(Restr r A)" -unfolding antisym_def Field_def by auto - -lemma Total_Restr: -"Total r \ Total(Restr r A)" -unfolding total_on_def Field_def by auto - -lemma trans_Restr: -"trans r \ trans(Restr r A)" -unfolding trans_def Field_def by blast - -lemma Preorder_Restr: -"Preorder r \ Preorder(Restr r A)" -unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr) - -lemma Partial_order_Restr: -"Partial_order r \ Partial_order(Restr r A)" -unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr) - -lemma Linear_order_Restr: -"Linear_order r \ 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- - have "Restr r A - Id \ r - Id" using Restr_subset by blast - hence "wf(Restr r A - Id)" using assms - using well_order_on_def wf_subset by blast - thus ?thesis using assms unfolding well_order_on_def - by (simp add: Linear_order_Restr) -qed - -lemma Field_Restr_subset: "Field(Restr r A) \ A" -by (auto simp add: Field_def) - -lemma Refl_Field_Restr: -"Refl r \ Field(Restr r A) = (Field r) Int A" -unfolding refl_on_def Field_def by blast - -lemma Refl_Field_Restr2: -"\Refl r; A \ Field r\ \ 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 \ 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 *} - -lemma Field_Restr_ofilter: -"\Well_order r; wo_rel.ofilter r A\ \ 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 \ A" -shows "under (Restr r A) a = under r a" -using assms wo_rel_def -proof(auto simp add: wo_rel.ofilter_def under_def) - fix b assume *: "a \ A" and "(b,a) \ r" - hence "b \ under r a \ a \ Field r" - unfolding under_def using Field_def by fastforce - thus "b \ 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 \ Field r \ embed (Restr r A) r id)" -proof - assume *: "wo_rel.ofilter r A" - show "A \ Field r \ embed (Restr r A) r id" - proof(unfold embed_def, auto) - fix a assume "a \ A" thus "a \ Field r" using assms * - by (auto simp add: wo_rel_def wo_rel.ofilter_def) - next - fix a assume "a \ Field (Restr r A)" - thus "bij_betw id (under (Restr r A) a) (under r a)" using assms * - by (simp add: ofilter_Restr_under Field_Restr_ofilter) - qed -next - assume *: "A \ Field r \ embed (Restr r A) r id" - hence "Field(Restr r A) \ Field r" - using assms embed_Field[of "Restr r A" r id] id_def - Well_order_Restr[of r] by auto - {fix a assume "a \ A" - hence "a \ Field(Restr r A)" using * assms - by (simp add: order_on_defs Refl_Field_Restr2) - hence "bij_betw id (under (Restr r A) a) (under r a)" - using * unfolding embed_def by auto - hence "under r a \ under (Restr r A) a" - unfolding bij_betw_def by auto - also have "\ \ Field(Restr r A)" by (simp add: under_Field) - also have "\ \ A" by (simp add: Field_Restr_subset) - finally have "under r a \ 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" - have Well: "wo_rel r" unfolding wo_rel_def using WELL . - hence Refl: "Refl r" by (simp add: wo_rel.REFL) - hence Field: "Field ?rB = Field r Int B" - using Refl_Field_Restr by blast - have WellB: "wo_rel ?rB \ Well_order ?rB" using WELL - by (simp add: Well_order_Restr wo_rel_def) - (* Main proof *) - show ?thesis using WellB assms - proof(auto simp add: wo_rel.ofilter_def under_def) - fix a assume "a \ A" and *: "a \ B" - hence "a \ Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def) - with * show "a \ Field ?rB" using Field by auto - next - fix a b assume "a \ A" and "(b,a) \ r" - thus "b \ 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 \ 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 \ B) = (embed (Restr r A) (Restr r B) id)" -proof- - let ?rA = "Restr r A" let ?rB = "Restr r B" - have Well: "wo_rel r" unfolding wo_rel_def using WELL . - hence Refl: "Refl r" by (simp add: wo_rel.REFL) - hence FieldA: "Field ?rA = Field r Int A" - using Refl_Field_Restr by blast - have FieldB: "Field ?rB = Field r Int B" - using Refl Refl_Field_Restr by blast - have WellA: "wo_rel ?rA \ Well_order ?rA" using WELL - by (simp add: Well_order_Restr wo_rel_def) - have WellB: "wo_rel ?rB \ Well_order ?rB" using WELL - by (simp add: Well_order_Restr wo_rel_def) - (* Main proof *) - show ?thesis - proof - assume *: "A \ B" - hence "wo_rel.ofilter (Restr r B) A" using assms - by (simp add: ofilter_Restr_subset) - hence "embed (Restr ?rB A) (Restr r B) id" - using WellB ofilter_embed[of "?rB" A] by auto - thus "embed (Restr r A) (Restr r B) id" - using * by (simp add: Restr_subset) - next - assume *: "embed (Restr r A) (Restr r B) id" - {fix a assume **: "a \ A" - hence "a \ Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def) - with ** FieldA have "a \ Field ?rA" by auto - hence "a \ Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto - hence "a \ B" using FieldB by auto - } - thus "A \ 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)) \ - ((A = B) = (iso (Restr r A) (Restr r B) id))" -proof- - let ?rA = "Restr r A" let ?rB = "Restr r B" - have Well: "wo_rel r" unfolding wo_rel_def using WELL . - hence Refl: "Refl r" by (simp add: wo_rel.REFL) - hence "Field ?rA = Field r Int A" - using Refl_Field_Restr by blast - hence FieldA: "Field ?rA = A" using OFA Well - by (auto simp add: wo_rel.ofilter_def) - have "Field ?rB = Field r Int B" - using Refl Refl_Field_Restr by blast - hence FieldB: "Field ?rB = B" using OFB Well - by (auto simp add: wo_rel.ofilter_def) - (* Main proof *) - 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" -proof- - let ?A' = "Field r'" - let ?r'' = "Restr r (f ` ?A')" - have 0: "Well_order ?r''" using WELL Well_order_Restr by blast - have 1: "wo_rel.ofilter r (f ` ?A')" using assms embed_Field_ofilter by blast - hence "Field ?r'' = f ` (Field r')" using WELL Field_Restr_ofilter by blast - hence "bij_betw f ?A' (Field ?r'')" - using EMB embed_inj_on WELL' unfolding bij_betw_def by blast - moreover - {have "\a b. (a,b) \ r' \ a \ Field r' \ b \ Field r'" - unfolding Field_def by auto - hence "compat r' ?r'' f" - using assms embed_iff_compat_inj_on_ofilter - unfolding compat_def by blast - } - ultimately show ?thesis using WELL' 0 iso_iff3 by blast -qed - - -subsection {* The strict inclusion on proper ofilters is well-founded *} - -definition ofilterIncl :: "'a rel \ 'a set rel" -where -"ofilterIncl r \ {(A,B). wo_rel.ofilter r A \ A \ Field r \ - wo_rel.ofilter r B \ B \ Field r \ A < B}" - -lemma wf_ofilterIncl: -assumes WELL: "Well_order r" -shows "wf(ofilterIncl r)" -proof- - have Well: "wo_rel r" using WELL by (simp add: wo_rel_def) - hence Lo: "Linear_order r" by (simp add: wo_rel.LIN) - let ?h = "(\ A. wo_rel.suc r A)" - let ?rS = "r - Id" - have "wf ?rS" using WELL by (simp add: order_on_defs) - moreover - have "compat (ofilterIncl r) ?rS ?h" - proof(unfold compat_def ofilterIncl_def, - intro allI impI, simp, elim conjE) - fix A B - assume *: "wo_rel.ofilter r A" "A \ Field r" and - **: "wo_rel.ofilter r B" "B \ Field r" and ***: "A < B" - then obtain a and b where 0: "a \ Field r \ b \ Field r" and - 1: "A = underS r a \ B = underS r b" - using Well by (auto simp add: wo_rel.ofilter_underS_Field) - hence "a \ b" using *** by auto - moreover - have "(a,b) \ r" using 0 1 Lo *** - by (auto simp add: underS_incl_iff) - moreover - have "a = wo_rel.suc r A \ b = wo_rel.suc r B" - using Well 0 1 by (simp add: wo_rel.suc_underS) - ultimately - show "(wo_rel.suc r A, wo_rel.suc r B) \ r \ wo_rel.suc r A \ wo_rel.suc r B" - by simp - 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 "\o"}); -\item @{text "ordLess"}, of being strictly embedded (abbreviated @{text ""}, @{text "<"}, @{text "="} associated to a total order on a set. -*} - -definition ordLeq :: "('a rel * 'a' rel) set" -where -"ordLeq = {(r,r'). Well_order r \ Well_order r' \ (\f. embed r r' f)}" - -abbreviation ordLeq2 :: "'a rel \ 'a' rel \ bool" (infix "<=o" 50) -where "r <=o r' \ (r,r') \ ordLeq" - -abbreviation ordLeq3 :: "'a rel \ 'a' rel \ bool" (infix "\o" 50) -where "r \o r' \ r <=o r'" - -definition ordLess :: "('a rel * 'a' rel) set" -where -"ordLess = {(r,r'). Well_order r \ Well_order r' \ (\f. embedS r r' f)}" - -abbreviation ordLess2 :: "'a rel \ 'a' rel \ bool" (infix " (r,r') \ ordLess" - -definition ordIso :: "('a rel * 'a' rel) set" -where -"ordIso = {(r,r'). Well_order r \ Well_order r' \ (\f. iso r r' f)}" - -abbreviation ordIso2 :: "'a rel \ 'a' rel \ bool" (infix "=o" 50) -where "r =o r' \ (r,r') \ ordIso" - -lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def - -lemma ordLeq_Well_order_simp: -assumes "r \o r'" -shows "Well_order r \ Well_order r'" -using assms unfolding ordLeq_def by simp - -text{* Notice that the relations @{text "\o"}, @{text " r \o r" -unfolding ordLeq_def using id_embed[of r] by blast - -lemma ordLeq_transitive[trans]: -assumes *: "r \o r'" and **: "r' \o r''" -shows "r \o r''" -proof- - obtain f and f' - where 1: "Well_order r \ Well_order r' \ Well_order r''" and - "embed r r' f" and "embed r' r'' f'" - using * ** unfolding ordLeq_def by blast - hence "embed r r'' (f' o f)" - using comp_embed[of r r' f r'' f'] by auto - thus "r \o r''" unfolding ordLeq_def using 1 by auto -qed - -lemma ordLeq_total: -"\Well_order r; Well_order r'\ \ r \o r' \ r' \o r" -unfolding ordLeq_def using wellorders_totally_ordered by blast - -lemma ordIso_reflexive: -"Well_order r \ r =o r" -unfolding ordIso_def using id_iso[of r] by blast - -lemma ordIso_transitive[trans]: -assumes *: "r =o r'" and **: "r' =o r''" -shows "r =o r''" -proof- - obtain f and f' - where 1: "Well_order r \ Well_order r' \ Well_order r''" and - "iso r r' f" and 3: "iso r' r'' f'" - using * ** unfolding ordIso_def by auto - hence "iso r r'' (f' 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 \ Well_order r'" and - 2: "embed r r' f \ bij_betw f (Field r) (Field r')" - using * by (auto simp add: ordIso_def iso_def) - let ?f' = "inv_into (Field r) f" - have "embed r' r ?f' \ 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 \o r'" and " r' 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''" -shows "r 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 \o r'" and " r' =o r''" -shows "r \o r''" -proof- - have "Well_order r \ 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' \o r''" -shows "r \o r''" -proof- - have "Well_order r \ 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 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' 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 (\f'. embed r' r f')" -proof- - obtain f where 1: "Well_order r \ Well_order r'" and 2: "embed r r' f" and - 3: " \ bij_betw f (Field r) (Field r')" - using assms unfolding ordLess_def by (auto simp add: embedS_def) - {fix f' assume *: "embed r' r f'" - hence "bij_betw f (Field r) (Field r')" using 1 2 - by (simp add: embed_bothWays_Field_bij_betw) - with 3 have False by contradiction - } - thus ?thesis by blast -qed - -lemma ordLess_Field: -assumes OL: "r1 (f`(Field r1) = Field r2)" -proof- - let ?A1 = "Field r1" let ?A2 = "Field r2" - obtain g where - 0: "Well_order r1 \ Well_order r2" and - 1: "embed r1 r2 g \ \(bij_betw g ?A1 ?A2)" - using OL unfolding ordLess_def by (auto simp add: embedS_def) - hence "\a \ ?A1. f a = g a" - using 0 EMB embed_unique[of r1] by auto - hence "\(bij_betw f ?A1 ?A2)" - 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 Well_order r' \ \(\f'. embed r' r f'))" -proof - assume *: "r (\f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp - with * show "Well_order r \ Well_order r' \ \ (\f'. embed r' r f')" - unfolding ordLess_def by auto -next - assume *: "Well_order r \ Well_order r' \ \ (\f'. embed r' r f')" - then obtain f where 1: "embed r r' f" - using wellorders_totally_ordered[of r r'] by blast - moreover - {assume "bij_betw f (Field r) (Field r')" - with * 1 have "embed r' r (inv_into (Field r) f) " - using inv_into_Field_embed_bij_betw[of r r' f] by auto - with * have False by blast - } - ultimately show "(r,r') \ ordLess" - unfolding ordLess_def using * by (fastforce simp add: embedS_def) -qed - -lemma ordLess_irreflexive: "\ r \(\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 \o r' = (r r =o r')" -unfolding ordRels_def embedS_defs iso_defs by blast - -lemma ordIso_iff_ordLeq: -"(r =o r') = (r \o r' \ r' \o r)" -proof - assume "r =o r'" - then obtain f where 1: "Well_order r \ Well_order r' \ - embed r r' f \ bij_betw f (Field r) (Field r')" - unfolding ordIso_def iso_defs by auto - hence "embed r r' f \ embed r' r (inv_into (Field r) f)" - by (simp add: inv_into_Field_embed_bij_betw) - thus "r \o r' \ r' \o r" - unfolding ordLeq_def using 1 by auto -next - assume "r \o r' \ r' \o r" - then obtain f and g where 1: "Well_order r \ Well_order r' \ - embed r r' f \ embed r' r g" - 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 \ r' \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 r' \o r" -proof- - have "r \o r' \ r' \o r" - using assms by (simp add: ordLeq_total) - moreover - {assume "\ r r \o r'" - hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast - hence "r' \o r" using ordIso_symmetric ordIso_iff_ordLeq by blast - } - ultimately show ?thesis by blast -qed - -lemma not_ordLess_ordIso: -"r \ 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 "(\ r' \o r) = (r r' o r')" -using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast - -lemma ordLess_transitive[trans]: -"\r \ r r \o r'" -using ordIso_iff_ordLeq by blast - -lemma ordLess_imp_ordLeq: -"r r \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 \ B) = (Restr r A \o Restr r B)" -proof - assume "A \ B" - thus "Restr r A \o Restr r B" - unfolding ordLeq_def using assms - Well_order_Restr Well_order_Restr ofilter_subset_embed by blast -next - assume *: "Restr r A \o Restr r B" - then obtain f where "embed (Restr r A) (Restr r B) f" - unfolding ordLeq_def by blast - {assume "B < A" - hence "Restr r B 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 Well_order ?rB" - using WELL Well_order_Restr by blast - have "(A < B) = (\ B \ A)" using assms - wo_rel_def wo_rel.ofilter_linord[of r A B] by blast - also have "\ = (\ Restr r B \o Restr r A)" - using assms ofilter_subset_ordLeq by blast - also have "\ = (Restr r A Well_order r; wo_rel.ofilter r A\ \ (A < Field r) = (Restr r A {}" -shows "Restr r (underS r a) (ofilterIncl r3)" -proof- - have OL13: "r1 Well_order r2 \ Well_order r3" and - 1: "embed r1 r2 f12 \ \(bij_betw f12 ?A1 ?A2)" and - 2: "embed r2 r3 g23 \ \(bij_betw g23 ?A2 ?A3)" - using OL12 OL23 by (auto simp add: ordLess_def embedS_def) - hence "\a \ ?A2. f23 a = g23 a" - using EMB23 embed_unique[of r2 r3] by blast - hence 3: "\(bij_betw f23 ?A2 ?A3)" - using 2 bij_betw_cong[of ?A2 f23 g23] by blast - (* *) - have 4: "wo_rel.ofilter r2 (f12 ` ?A1) \ f12 ` ?A1 \ ?A2" - using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field) - have 5: "wo_rel.ofilter r3 (f23 ` ?A2) \ f23 ` ?A2 \ ?A3" - using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field) - have 6: "wo_rel.ofilter r3 (f13 ` ?A1) \ f13 ` ?A1 \ ?A3" - using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field) - (* *) - have "f12 ` ?A1 < ?A2" - using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def) - moreover have "inj_on f23 ?A2" - using EMB23 0 by (simp add: wo_rel_def embed_inj_on) - ultimately - have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset) - moreover - {have "embed r1 r3 (f23 o f12)" - using 1 EMB23 0 by (auto simp add: comp_embed) - hence "\a \ ?A1. f23(f12 a) = f13 a" - using EMB13 0 embed_unique[of r1 r3 "f23 o f12" f13] by auto - hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force - } - ultimately - have "f13 ` ?A1 < f23 ` ?A2" by simp - (* *) - with 5 6 show ?thesis - unfolding ofilterIncl_def by auto -qed - -lemma ordLess_iff_ordIso_Restr: -assumes WELL: "Well_order r" and WELL': "Well_order r'" -shows "(r' a \ Field r. r' =o Restr r (underS r a))" -proof(auto) - fix a assume *: "a \ Field r" and **: "r' =o Restr r (underS r a)" - hence "Restr r (underS r a) Well_order r'" and - 2: "embed r' r f \ f ` (Field r') \ Field r" - unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast - hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast - then obtain a where 3: "a \ Field r" and 4: "underS r a = f ` (Field r')" - using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def) - have "iso r' (Restr r (f ` (Field r'))) f" - using embed_implies_iso_Restr 2 assms by blast - moreover have "Well_order (Restr r (f ` (Field r')))" - using WELL Well_order_Restr by blast - ultimately have "r' =o Restr r (f ` (Field r'))" - using WELL' unfolding ordIso_def by auto - hence "r' =o Restr r (underS r a)" using 4 by auto - thus "\a \ Field r. r' =o Restr r (underS r a)" using 3 by auto -qed - -lemma internalize_ordLess: -"(r' p. Field p < Field r \ r' =o p \ p Well_order r'" unfolding ordLess_def by auto - with * obtain a where 1: "a \ Field r" and 2: "r' =o Restr r (underS r a)" - using ordLess_iff_ordIso_Restr by blast - let ?p = "Restr r (underS r a)" - have "wo_rel.ofilter r (underS r a)" using 0 - by (simp add: wo_rel_def wo_rel.underS_ofilter) - hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast - hence "Field ?p < Field r" using underS_Field2 1 by fast - moreover have "?p p. Field p < Field r \ r' =o p \ p p. Field p < Field r \ r' =o p \ p o r) = (\p. Field p \ Field r \ r' =o p \ p \o r)" -proof - assume *: "r' \o r" - moreover - {assume "r' r' =o p \ p p. Field p \ Field r \ r' =o p \ p \o r" - using ordLeq_iff_ordLess_or_ordIso by blast - } - moreover - have "r \o r" using * ordLeq_def ordLeq_reflexive by blast - ultimately show "\p. Field p \ Field r \ r' =o p \ p \o r" - using ordLeq_iff_ordLess_or_ordIso by blast -next - assume "\p. Field p \ Field r \ r' =o p \ p \o r" - thus "r' \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 \o r') = (\a \ Field r. Restr r (underS r a) o r'" - fix a assume "a \ Field r" - hence "Restr r (underS r a) a \ Field r. Restr r (underS r a) Field r \ r' =o Restr r (underS r a)" - using assms ordLess_iff_ordIso_Restr by blast - hence False using * not_ordLess_ordIso ordIso_symmetric by blast - } - thus "r \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: "\finite(Field r')" -shows "r o r" - then obtain h where "inj_on h (Field r') \ h ` (Field r') \ Field r" - unfolding ordLeq_def using assms embed_inj_on embed_Field by blast - hence False using finite_imageD finite_subset FIN INF by blast - } - thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast -qed - -lemma finite_well_order_on_ordIso: -assumes FIN: "finite A" and - WELL: "well_order_on A r" and WELL': "well_order_on A r'" -shows "r =o r'" -proof- - have 0: "Well_order r \ Well_order r' \ Field r = A \ Field r' = A" - using assms well_order_on_Well_order by blast - moreover - have "\r r'. well_order_on A r \ well_order_on A r' \ r \o r' - \ r =o r'" - proof(clarify) - fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'" - have 2: "Well_order r \ Well_order r' \ Field r = A \ Field r' = A" - using * ** well_order_on_Well_order by blast - assume "r \o r'" - then obtain f where 1: "embed r r' f" and - "inj_on f A \ f ` A \ A" - unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast - hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast - thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto - qed - ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast -qed - -subsection{* @{text " 'a rel \ 'a set" -where "ord_to_filter r0 r \ (SOME f. embed r r0 f) ` (Field r)" - -lemma ord_to_filter_compat: -"compat (ordLess Int (ordLess^-1``{r0} \ ordLess^-1``{r0})) - (ofilterIncl r0) - (ord_to_filter r0)" -proof(unfold compat_def ord_to_filter_def, clarify) - fix r1::"'a rel" and r2::"'a rel" - let ?A1 = "Field r1" let ?A2 ="Field r2" let ?A0 ="Field r0" - let ?phi10 = "\ f10. embed r1 r0 f10" let ?f10 = "SOME f. ?phi10 f" - let ?phi20 = "\ f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f" - assume *: "r1 f. ?phi10 f) \ (\f. ?phi20 f)" - by (auto simp add: ordLess_def embedS_def) - hence "?phi10 ?f10 \ ?phi20 ?f20" by (auto simp add: someI_ex) - thus "(?f10 ` ?A1, ?f20 ` ?A2) \ ofilterIncl r0" - using * ** by (simp add: embed_ordLess_ofilterIncl) -qed - -theorem wf_ordLess: "wf ordLess" -proof- - {fix r0 :: "('a \ 'a) set" - (* need to annotate here!*) - let ?ordLess = "ordLess::('d rel * 'd rel) set" - let ?R = "?ordLess Int (?ordLess^-1``{r0} \ ?ordLess^-1``{r0})" - {assume Case1: "Well_order r0" - hence "wf ?R" - using wf_ofilterIncl[of r0] - compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"] - ord_to_filter_compat[of r0] by auto - } - moreover - {assume Case2: "\ Well_order r0" - hence "?R = {}" unfolding ordLess_def by auto - hence "wf ?R" using wf_empty by simp - } - ultimately have "wf ?R" by blast - } - thus ?thesis by (simp add: trans_wf_iff ordLess_trans) -qed - -corollary exists_minim_Well_order: -assumes NE: "R \ {}" and WELL: "\r \ R. Well_order r" -shows "\r \ R. \r' \ R. r \o r'" -proof- - obtain r where "r \ R \ (\r' \ R. \ r' ('a \ 'a') \ 'a' rel" -where -"dir_image r f = {(f a, f b)| a b. (a,b) \ r}" - -lemma dir_image_Field: -"Field(dir_image r f) = f ` (Field r)" -unfolding dir_image_def Field_def Range_def Domain_def by fast - -lemma dir_image_minus_Id: -"inj_on f (Field r) \ (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- - {fix a' b' - assume "(a',b') \ dir_image r f" - then obtain a b where 1: "a' = f a \ b' = f b \ (a,b) \ r" - unfolding dir_image_def by blast - hence "a \ Field r \ b \ Field r" using Field_def by fastforce - hence "(a,a) \ r \ (b,b) \ r" using assms by (simp add: refl_on_def) - with 1 have "(a',a') \ dir_image r f \ (b',b') \ dir_image r f" - 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) - fix a' b' c' - assume "(a',b') \ dir_image r f" "(b',c') \ dir_image r f" - then obtain a b1 b2 c where 1: "a' = f a \ b' = f b1 \ b' = f b2 \ c' = f c" and - 2: "(a,b1) \ r \ (b2,c) \ r" - unfolding dir_image_def by blast - hence "b1 \ Field r \ b2 \ Field r" - unfolding Field_def by auto - hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto - hence "(a,c): r" using 2 TRANS unfolding trans_def by blast - thus "(a',c') \ dir_image r f" - unfolding dir_image_def using 1 by auto -qed - -lemma Preorder_dir_image: -"\Preorder r; inj_on f (Field r)\ \ 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) - fix a' b' - assume "(a',b') \ dir_image r f" "(b',a') \ dir_image r f" - then obtain a1 b1 a2 b2 where 1: "a' = f a1 \ a' = f a2 \ b' = f b1 \ b' = f b2" and - 2: "(a1,b1) \ r \ (b2,a2) \ r " and - 3: "{a1,a2,b1,b2} \ Field r" - unfolding dir_image_def Field_def by blast - hence "a1 = a2 \ 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: -"\Partial_order r; inj_on f (Field r)\ \ 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) - fix a' b' - assume "a' \ Field (dir_image r f)" "b' \ Field (dir_image r f)" - then obtain a and b where 1: "a \ Field r \ b \ Field r \ f a = a' \ f b = b'" - unfolding dir_image_Field[of r f] by blast - moreover assume "a' \ b'" - ultimately have "a \ b" using INJ unfolding inj_on_def by auto - hence "(a,b) \ r \ (b,a) \ r" using 1 TOT unfolding total_on_def by auto - thus "(a',b') \ dir_image r f \ (b',a') \ dir_image r f" - using 1 unfolding dir_image_def by auto -qed - -lemma Linear_order_dir_image: -"\Linear_order r; inj_on f (Field r)\ \ 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) - fix A'::"'b set" - assume SUB: "A' \ Field(dir_image r f)" and NE: "A' \ {}" - obtain A where A_def: "A = {a \ Field r. f a \ A'}" by blast - have "A \ {} \ A \ Field r" using A_def SUB NE by (auto simp: dir_image_Field) - then obtain a where 1: "a \ A \ (\b \ A. (b,a) \ r)" - using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast - have "\b' \ A'. (b',f a) \ dir_image r f" - proof(clarify) - fix b' assume *: "b' \ A'" and **: "(b',f a) \ dir_image r f" - obtain b1 a1 where 2: "b' = f b1 \ f a = f a1" and - 3: "(b1,a1) \ r \ {a1,b1} \ Field r" - using ** unfolding dir_image_def Field_def by blast - hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto - hence "b1 \ A \ (b1,a) \ r" using 2 3 A_def * by auto - with 1 show False by auto - qed - thus "\a'\A'. \b'\A'. (b', a') \ dir_image r f" - using A_def 1 by blast -qed - -lemma Well_order_dir_image: -"\Well_order r; inj_on f (Field r)\ \ 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_bij_betw: -"\inj_on f (Field r)\ \ bij_betw f (Field r) (Field (dir_image r f))" -unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs) - -lemma dir_image_compat: -"compat r (dir_image r f) f" -unfolding compat_def dir_image_def by auto - -lemma dir_image_iso: -"\Well_order r; inj_on f (Field r)\ \ 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: -"\Well_order r; inj_on f (Field r)\ \ 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 "\r'. well_order_on A' r' \ r =o r'" -proof- - let ?r' = "dir_image r f" - have 1: "A = Field r \ Well_order r" - using WELL well_order_on_Well_order by blast - hence 2: "iso r ?r' f" - using dir_image_iso using BIJ unfolding bij_betw_def by auto - hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast - hence "Field ?r' = A'" - using 1 BIJ unfolding bij_betw_def by auto - moreover have "Well_order ?r'" - using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast - ultimately show ?thesis unfolding ordIso_def using 1 2 by blast -qed - - -subsection {* Bounded square *} - -text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic -order @{text "bsqr r"} on @{text "(Field r) \ (Field r)"}, applying the -following criteria (in this order): -\begin{itemize} -\item compare the maximums; -\item compare the first components; -\item compare the second components. -\end{itemize} -% -The only application of this construction that we are aware of is -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} \ Field r \ - (a1 = b1 \ a2 = b2 \ - (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id \ - wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id \ - wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id - )}" - -lemma Field_bsqr: -"Field (bsqr r) = Field r \ Field r" -proof - show "Field (bsqr r) \ Field r \ Field r" - proof- - {fix a1 a2 assume "(a1,a2) \ Field (bsqr r)" - moreover - have "\ b1 b2. ((a1,a2),(b1,b2)) \ bsqr r \ ((b1,b2),(a1,a2)) \ bsqr r \ - a1 \ Field r \ a2 \ Field r" unfolding bsqr_def by auto - ultimately have "a1 \ Field r \ a2 \ Field r" unfolding Field_def by auto - } - thus ?thesis unfolding Field_def by force - qed -next - show "Field r \ Field r \ Field (bsqr r)" - proof(auto) - fix a1 a2 assume "a1 \ Field r" and "a2 \ Field r" - hence "((a1,a2),(a1,a2)) \ bsqr r" unfolding bsqr_def by blast - thus "(a1,a2) \ 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) - (* Preliminary facts *) - have Well: "wo_rel r" using assms wo_rel_def by auto - hence Trans: "trans r" using wo_rel.TRANS by auto - have Anti: "antisym r" using wo_rel.ANTISYM Well by auto - hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id) - (* Main proof *) - fix a1 a2 b1 b2 c1 c2 - assume *: "((a1,a2),(b1,b2)) \ bsqr r" and **: "((b1,b2),(c1,c2)) \ bsqr r" - hence 0: "{a1,a2,b1,b2,c1,c2} \ Field r" unfolding bsqr_def by auto - have 1: "a1 = b1 \ a2 = b2 \ (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id \ - wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id \ - wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id" - using * unfolding bsqr_def by auto - have 2: "b1 = c1 \ b2 = c2 \ (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \ r - Id \ - wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ (b1,c1) \ r - Id \ - wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ b1 = c1 \ (b2,c2) \ r - Id" - using ** unfolding bsqr_def by auto - show "((a1,a2),(c1,c2)) \ bsqr r" - proof- - {assume Case1: "a1 = b1 \ a2 = b2" - hence ?thesis using ** by simp - } - moreover - {assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id" - {assume Case21: "b1 = c1 \ b2 = c2" - hence ?thesis using * by simp - } - moreover - {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \ r - Id" - hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \ r - Id" - using Case2 TransS trans_def[of "r - Id"] by blast - hence ?thesis using 0 unfolding bsqr_def by auto - } - moreover - {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2" - hence ?thesis using Case2 0 unfolding bsqr_def by auto - } - ultimately have ?thesis using 0 2 by auto - } - moreover - {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id" - {assume Case31: "b1 = c1 \ b2 = c2" - hence ?thesis using * by simp - } - moreover - {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \ r - Id" - hence ?thesis using Case3 0 unfolding bsqr_def by auto - } - moreover - {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ (b1,c1) \ r - Id" - hence "(a1,c1) \ r - Id" - using Case3 TransS trans_def[of "r - Id"] by blast - hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto - } - moreover - {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ b1 = c1" - hence ?thesis using Case3 0 unfolding bsqr_def by auto - } - ultimately have ?thesis using 0 2 by auto - } - moreover - {assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id" - {assume Case41: "b1 = c1 \ b2 = c2" - hence ?thesis using * by simp - } - moreover - {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \ r - Id" - hence ?thesis using Case4 0 unfolding bsqr_def by force - } - moreover - {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ (b1,c1) \ r - Id" - hence ?thesis using Case4 0 unfolding bsqr_def by auto - } - moreover - {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ b1 = c1 \ (b2,c2) \ r - Id" - hence "(a2,c2) \ r - Id" - using Case4 TransS trans_def[of "r - Id"] by blast - hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto - } - ultimately have ?thesis using 0 2 by auto - } - ultimately show ?thesis using 0 1 by auto - qed -qed - -lemma bsqr_antisym: -assumes "Well_order r" -shows "antisym (bsqr r)" -proof(unfold antisym_def, clarify) - (* Preliminary facts *) - have Well: "wo_rel r" using assms wo_rel_def by auto - hence Trans: "trans r" using wo_rel.TRANS by auto - have Anti: "antisym r" using wo_rel.ANTISYM Well by auto - hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id) - hence IrrS: "\a b. \((a,b) \ r - Id \ (b,a) \ r - Id)" - using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast - (* Main proof *) - fix a1 a2 b1 b2 - assume *: "((a1,a2),(b1,b2)) \ bsqr r" and **: "((b1,b2),(a1,a2)) \ bsqr r" - hence 0: "{a1,a2,b1,b2} \ Field r" unfolding bsqr_def by auto - have 1: "a1 = b1 \ a2 = b2 \ (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id \ - wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id \ - wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id" - using * unfolding bsqr_def by auto - have 2: "b1 = a1 \ b2 = a2 \ (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \ r - Id \ - wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \ (b1,a1) \ r - Id \ - wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \ b1 = a1 \ (b2,a2) \ r - Id" - using ** unfolding bsqr_def by auto - show "a1 = b1 \ a2 = b2" - proof- - {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id" - {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \ r - Id" - hence False using Case1 IrrS by blast - } - moreover - {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2" - hence False using Case1 by auto - } - ultimately have ?thesis using 0 2 by auto - } - moreover - {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id" - {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \ r - Id" - hence False using Case2 by auto - } - moreover - {assume Case22: "(b1,a1) \ r - Id" - hence False using Case2 IrrS by blast - } - moreover - {assume Case23: "b1 = a1" - hence False using Case2 by auto - } - ultimately have ?thesis using 0 2 by auto - } - moreover - {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id" - moreover - {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \ r - Id" - hence False using Case3 by auto - } - moreover - {assume Case32: "(b1,a1) \ r - Id" - hence False using Case3 by auto - } - moreover - {assume Case33: "(b2,a2) \ r - Id" - hence False using Case3 IrrS by blast - } - ultimately have ?thesis using 0 2 by auto - } - ultimately show ?thesis using 0 1 by blast - qed -qed - -lemma bsqr_Total: -assumes "Well_order r" -shows "Total(bsqr r)" -proof- - (* Preliminary facts *) - have Well: "wo_rel r" using assms wo_rel_def by auto - hence Total: "\a \ Field r. \b \ Field r. (a,b) \ r \ (b,a) \ r" - using wo_rel.TOTALS by auto - (* Main proof *) - {fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \ Field(bsqr r)" - hence 0: "a1 \ Field r \ a2 \ Field r \ b1 \ Field r \ b2 \ Field r" - using Field_bsqr by blast - have "((a1,a2) = (b1,b2) \ ((a1,a2),(b1,b2)) \ bsqr r \ ((b1,b2),(a1,a2)) \ bsqr r)" - proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0) - (* Why didn't clarsimp simp add: Well 0 do the same job? *) - assume Case1: "(a1,a2) \ r" - hence 1: "wo_rel.max2 r a1 a2 = a2" - using Well 0 by (simp add: wo_rel.max2_equals2) - show ?thesis - proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0) - assume Case11: "(b1,b2) \ r" - hence 2: "wo_rel.max2 r b1 b2 = b2" - using Well 0 by (simp add: wo_rel.max2_equals2) - show ?thesis - proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) - assume Case111: "(a2,b2) \ r - Id \ (b2,a2) \ r - Id" - thus ?thesis using 0 1 2 unfolding bsqr_def by auto - next - assume Case112: "a2 = b2" - show ?thesis - proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) - assume Case1121: "(a1,b1) \ r - Id \ (b1,a1) \ r - Id" - thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto - next - assume Case1122: "a1 = b1" - thus ?thesis using Case112 by auto - qed - qed - next - assume Case12: "(b2,b1) \ r" - hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1) - show ?thesis - proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0) - assume Case121: "(a2,b1) \ r - Id \ (b1,a2) \ r - Id" - thus ?thesis using 0 1 3 unfolding bsqr_def by auto - next - assume Case122: "a2 = b1" - show ?thesis - proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) - assume Case1221: "(a1,b1) \ r - Id \ (b1,a1) \ r - Id" - thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto - next - assume Case1222: "a1 = b1" - show ?thesis - proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) - assume Case12221: "(a2,b2) \ r - Id \ (b2,a2) \ r - Id" - thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto - next - assume Case12222: "a2 = b2" - thus ?thesis using Case122 Case1222 by auto - qed - qed - qed - qed - next - assume Case2: "(a2,a1) \ r" - hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1) - show ?thesis - proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0) - assume Case21: "(b1,b2) \ r" - hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2) - show ?thesis - proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0) - assume Case211: "(a1,b2) \ r - Id \ (b2,a1) \ r - Id" - thus ?thesis using 0 1 2 unfolding bsqr_def by auto - next - assume Case212: "a1 = b2" - show ?thesis - proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) - assume Case2121: "(a1,b1) \ r - Id \ (b1,a1) \ r - Id" - thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto - next - assume Case2122: "a1 = b1" - show ?thesis - proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) - assume Case21221: "(a2,b2) \ r - Id \ (b2,a2) \ r - Id" - thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto - next - assume Case21222: "a2 = b2" - thus ?thesis using Case2122 Case212 by auto - qed - qed - qed - next - assume Case22: "(b2,b1) \ r" - hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1) - show ?thesis - proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) - assume Case221: "(a1,b1) \ r - Id \ (b1,a1) \ r - Id" - thus ?thesis using 0 1 3 unfolding bsqr_def by auto - next - assume Case222: "a1 = b1" - show ?thesis - proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) - assume Case2221: "(a2,b2) \ r - Id \ (b2,a2) \ r - Id" - thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto - next - assume Case2222: "a2 = b2" - thus ?thesis using Case222 by auto - qed - qed - qed - qed - } - thus ?thesis unfolding total_on_def by fast -qed - -lemma bsqr_Linear_order: -assumes "Well_order r" -shows "Linear_order(bsqr r)" -unfolding order_on_defs -using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast - -lemma bsqr_Well_order: -assumes "Well_order r" -shows "Well_order(bsqr r)" -using assms -proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI) - have 0: "\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a,a') \ r)" - using assms well_order_on_def Linear_order_Well_order_iff by blast - fix D assume *: "D \ Field (bsqr r)" and **: "D \ {}" - hence 1: "D \ Field r \ Field r" unfolding Field_bsqr by simp - (* *) - obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \ D}" by blast - have "M \ {}" using 1 M_def ** by auto - moreover - have "M \ Field r" unfolding M_def - using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce - ultimately obtain m where m_min: "m \ M \ (\a \ M. (m,a) \ r)" - using 0 by blast - (* *) - obtain A1 where A1_def: "A1 = {a1. \a2. (a1,a2) \ D \ wo_rel.max2 r a1 a2 = m}" by blast - have "A1 \ Field r" unfolding A1_def using 1 by auto - moreover have "A1 \ {}" unfolding A1_def using m_min unfolding M_def by blast - ultimately obtain a1 where a1_min: "a1 \ A1 \ (\a \ A1. (a1,a) \ r)" - using 0 by blast - (* *) - obtain A2 where A2_def: "A2 = {a2. (a1,a2) \ D \ wo_rel.max2 r a1 a2 = m}" by blast - have "A2 \ Field r" unfolding A2_def using 1 by auto - moreover have "A2 \ {}" unfolding A2_def - using m_min a1_min unfolding A1_def M_def by blast - ultimately obtain a2 where a2_min: "a2 \ A2 \ (\a \ A2. (a2,a) \ r)" - using 0 by blast - (* *) - have 2: "wo_rel.max2 r a1 a2 = m" - using a1_min a2_min unfolding A1_def A2_def by auto - have 3: "(a1,a2) \ D" using a2_min unfolding A2_def by auto - (* *) - moreover - {fix b1 b2 assume ***: "(b1,b2) \ D" - hence 4: "{a1,a2,b1,b2} \ Field r" using 1 3 by blast - have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r" - using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto - have "((a1,a2),(b1,b2)) \ bsqr r" - proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2") - assume Case1: "wo_rel.max2 r a1 a2 \ wo_rel.max2 r b1 b2" - thus ?thesis unfolding bsqr_def using 4 5 by auto - next - assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2" - hence "b1 \ A1" unfolding A1_def using 2 *** by auto - hence 6: "(a1,b1) \ r" using a1_min by auto - show ?thesis - proof(cases "a1 = b1") - assume Case21: "a1 \ b1" - thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto - next - assume Case22: "a1 = b1" - hence "b2 \ A2" unfolding A2_def using 2 *** Case2 by auto - hence 7: "(a2,b2) \ r" using a2_min by auto - thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto - qed - qed - } - (* *) - ultimately show "\d \ D. \d' \ D. (d,d') \ bsqr r" by fastforce -qed - -lemma bsqr_max2: -assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \ bsqr r" -shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r" -proof- - have "{(a1,a2),(b1,b2)} \ Field(bsqr r)" - using LEQ unfolding Field_def by auto - hence "{a1,a2,b1,b2} \ Field r" unfolding Field_bsqr by auto - hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \ Field 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) \ r \ 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 \ Field r" and - NE: "\ (\a. Field r = under r a)" -shows "\A. wo_rel.ofilter r A \ A < Field r \ D \ A \ A" -proof- - let ?r' = "bsqr r" - have Well: "wo_rel r" using WELL wo_rel_def by blast - hence Trans: "trans r" using wo_rel.TRANS by blast - have Well': "Well_order ?r' \ wo_rel ?r'" - using WELL bsqr_Well_order wo_rel_def by blast - (* *) - have "D < Field ?r'" unfolding Field_bsqr using SUB . - with OF obtain a1 and a2 where - "(a1,a2) \ Field ?r'" and 1: "D = underS ?r' (a1,a2)" - using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto - hence 2: "{a1,a2} \ Field r" unfolding Field_bsqr by auto - let ?m = "wo_rel.max2 r a1 a2" - have "D \ (under r ?m) \ (under r ?m)" - proof(unfold 1) - {fix b1 b2 - let ?n = "wo_rel.max2 r b1 b2" - assume "(b1,b2) \ underS ?r' (a1,a2)" - hence 3: "((b1,b2),(a1,a2)) \ ?r'" - unfolding underS_def by blast - hence "(?n,?m) \ r" using WELL by (simp add: bsqr_max2) - moreover - {have "(b1,b2) \ Field ?r'" using 3 unfolding Field_def by auto - hence "{b1,b2} \ Field r" unfolding Field_bsqr by auto - hence "(b1,?n) \ r \ (b2,?n) \ r" - using Well by (simp add: wo_rel.max2_greater) - } - ultimately have "(b1,?m) \ r \ (b2,?m) \ r" - using Trans trans_def[of r] by blast - hence "(b1,b2) \ (under r ?m) \ (under r ?m)" unfolding under_def by simp} - thus "underS ?r' (a1,a2) \ (under r ?m) \ (under r ?m)" by auto - qed - moreover have "wo_rel.ofilter r (under r ?m)" - using Well by (simp add: wo_rel.under_ofilter) - moreover have "under r ?m < Field r" - using NE under_Field[of r ?m] by blast - ultimately show ?thesis by blast -qed - -definition Func where -"Func A B = {f . (\ a \ A. f a \ B) \ (\ a. a \ A \ f a = undefined)}" - -lemma Func_empty: -"Func {} B = {\x. undefined}" -unfolding Func_def by auto - -lemma Func_elim: -assumes "g \ Func A B" and "a \ A" -shows "\ b. b \ B \ g a = b" -using assms unfolding Func_def by (cases "g a = undefined") auto - -definition curr where -"curr A f \ \ a. if a \ A then \b. f (a,b) else undefined" - -lemma curr_in: -assumes f: "f \ Func (A <*> B) C" -shows "curr A f \ Func A (Func B C)" -using assms unfolding curr_def Func_def by auto - -lemma curr_inj: -assumes "f1 \ Func (A <*> B) C" and "f2 \ Func (A <*> B) C" -shows "curr A f1 = curr A f2 \ f1 = f2" -proof safe - assume c: "curr A f1 = curr A f2" - show "f1 = f2" - proof (rule ext, clarify) - fix a b show "f1 (a, b) = f2 (a, b)" - proof (cases "(a,b) \ A <*> B") - case False - thus ?thesis using assms unfolding Func_def by auto - next - case True hence a: "a \ A" and b: "b \ B" by auto - thus ?thesis - using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp - qed - qed -qed - -lemma curr_surj: -assumes "g \ Func A (Func B C)" -shows "\ f \ Func (A <*> B) C. curr A f = g" -proof - let ?f = "\ ab. if fst ab \ A \ snd ab \ B then g (fst ab) (snd ab) else undefined" - show "curr A ?f = g" - proof (rule ext) - fix a show "curr A ?f a = g a" - proof (cases "a \ A") - case False - hence "g a = undefined" using assms unfolding Func_def by auto - thus ?thesis unfolding curr_def using False by simp - next - case True - obtain g1 where "g1 \ Func B C" and "g a = g1" - using assms using Func_elim[OF assms True] by blast - thus ?thesis using True unfolding Func_def curr_def by auto - qed - qed - show "?f \ Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto -qed - -lemma bij_betw_curr: -"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))" -unfolding bij_betw_def inj_on_def image_def -apply (intro impI conjI ballI) -apply (erule curr_inj[THEN iffD1], assumption+) -apply auto -apply (erule curr_in) -using curr_surj by blast - -definition Func_map where -"Func_map B2 f1 f2 g b2 \ if b2 \ B2 then f1 (g (f2 b2)) else undefined" - -lemma Func_map: -assumes g: "g \ Func A2 A1" and f1: "f1 ` A1 \ B1" and f2: "f2 ` B2 \ A2" -shows "Func_map B2 f1 f2 g \ Func B2 B1" -using assms unfolding Func_def Func_map_def mem_Collect_eq by auto - -lemma Func_non_emp: -assumes "B \ {}" -shows "Func A B \ {}" -proof- - obtain b where b: "b \ B" using assms by auto - hence "(\ a. if a \ A then b else undefined) \ Func A B" unfolding Func_def by auto - thus ?thesis by blast -qed - -lemma Func_is_emp: -"Func A B = {} \ A \ {} \ B = {}" (is "?L \ ?R") -proof - assume L: ?L - moreover {assume "A = {}" hence False using L Func_empty by auto} - moreover {assume "B \ {}" hence False using L Func_non_emp[of B A] by simp } - ultimately show ?R by blast -next - assume R: ?R - moreover - {fix f assume "f \ Func A B" - moreover obtain a where "a \ A" using R by blast - ultimately obtain b where "b \ B" unfolding Func_def by blast - with R have False by blast - } - thus ?L by blast -qed - -lemma Func_map_surj: -assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \ A2" -and B2A2: "B2 = {} \ A2 = {}" -shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1" -proof(cases "B2 = {}") - case True - thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def) -next - case False note B2 = False - show ?thesis - proof safe - fix h assume h: "h \ Func B2 B1" - def j1 \ "inv_into A1 f1" - have "\ a2 \ f2 ` B2. \ b2. b2 \ B2 \ f2 b2 = a2" by blast - then obtain k where k: "\ a2 \ f2 ` B2. k a2 \ B2 \ f2 (k a2) = a2" - by atomize_elim (rule bchoice) - {fix b2 assume b2: "b2 \ B2" - hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto - moreover have "k (f2 b2) \ B2" using b2 A2(2) k by auto - ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast - } note kk = this - obtain b22 where b22: "b22 \ B2" using B2 by auto - def j2 \ "\ a2. if a2 \ f2 ` B2 then k a2 else b22" - have j2A2: "j2 ` A2 \ B2" unfolding j2_def using k b22 by auto - have j2: "\ b2. b2 \ B2 \ j2 (f2 b2) = b2" - using kk unfolding j2_def by auto - def g \ "Func_map A2 j1 j2 h" - have "Func_map B2 f1 f2 g = h" - proof (rule ext) - fix b2 show "Func_map B2 f1 f2 g b2 = h b2" - proof(cases "b2 \ B2") - case True - show ?thesis - proof (cases "h b2 = undefined") - case True - hence b1: "h b2 \ f1 ` A1" using h `b2 \ B2` unfolding B1 Func_def by auto - show ?thesis using A2 f_inv_into_f[OF b1] - unfolding True g_def Func_map_def j1_def j2[OF `b2 \ B2`] by auto - qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def, - auto intro: f_inv_into_f) - qed(insert h, unfold Func_def Func_map_def, auto) - qed - moreover have "g \ Func A2 A1" unfolding g_def apply(rule Func_map[OF h]) - using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+ - ultimately show "h \ Func_map B2 f1 f2 ` Func A2 A1" - unfolding Func_map_def[abs_def] by auto - qed(insert B1 Func_map[OF _ _ A2(2)], auto) -qed - -end diff -r 3831312eb476 -r b7cab82f488e src/HOL/BNF_Wellorder_Constructions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF_Wellorder_Constructions.thy Mon Sep 01 16:34:39 2014 +0200 @@ -0,0 +1,1656 @@ +(* Title: HOL/BNF_Wellorder_Constructions.thy + Author: Andrei Popescu, TU Muenchen + Copyright 2012 + +Constructions on wellorders as needed by bounded natural functors. +*) + +header {* Constructions on Wellorders as Needed by Bounded Natural Functors *} + +theory BNF_Wellorder_Constructions +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 "\o"}), +@{text "ordLess"}, of being strictly embedded (abbreviated @{text " 'a set \ 'a rel" +where "Restr r A \ r Int (A \ A)" + +lemma Restr_subset: +"A \ B \ 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 \ Refl(Restr r A)" +unfolding refl_on_def Field_def by auto + +lemma antisym_Restr: +"antisym r \ antisym(Restr r A)" +unfolding antisym_def Field_def by auto + +lemma Total_Restr: +"Total r \ Total(Restr r A)" +unfolding total_on_def Field_def by auto + +lemma trans_Restr: +"trans r \ trans(Restr r A)" +unfolding trans_def Field_def by blast + +lemma Preorder_Restr: +"Preorder r \ Preorder(Restr r A)" +unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr) + +lemma Partial_order_Restr: +"Partial_order r \ Partial_order(Restr r A)" +unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr) + +lemma Linear_order_Restr: +"Linear_order r \ 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- + have "Restr r A - Id \ r - Id" using Restr_subset by blast + hence "wf(Restr r A - Id)" using assms + using well_order_on_def wf_subset by blast + thus ?thesis using assms unfolding well_order_on_def + by (simp add: Linear_order_Restr) +qed + +lemma Field_Restr_subset: "Field(Restr r A) \ A" +by (auto simp add: Field_def) + +lemma Refl_Field_Restr: +"Refl r \ Field(Restr r A) = (Field r) Int A" +unfolding refl_on_def Field_def by blast + +lemma Refl_Field_Restr2: +"\Refl r; A \ Field r\ \ 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 \ 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 *} + +lemma Field_Restr_ofilter: +"\Well_order r; wo_rel.ofilter r A\ \ 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 \ A" +shows "under (Restr r A) a = under r a" +using assms wo_rel_def +proof(auto simp add: wo_rel.ofilter_def under_def) + fix b assume *: "a \ A" and "(b,a) \ r" + hence "b \ under r a \ a \ Field r" + unfolding under_def using Field_def by fastforce + thus "b \ 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 \ Field r \ embed (Restr r A) r id)" +proof + assume *: "wo_rel.ofilter r A" + show "A \ Field r \ embed (Restr r A) r id" + proof(unfold embed_def, auto) + fix a assume "a \ A" thus "a \ Field r" using assms * + by (auto simp add: wo_rel_def wo_rel.ofilter_def) + next + fix a assume "a \ Field (Restr r A)" + thus "bij_betw id (under (Restr r A) a) (under r a)" using assms * + by (simp add: ofilter_Restr_under Field_Restr_ofilter) + qed +next + assume *: "A \ Field r \ embed (Restr r A) r id" + hence "Field(Restr r A) \ Field r" + using assms embed_Field[of "Restr r A" r id] id_def + Well_order_Restr[of r] by auto + {fix a assume "a \ A" + hence "a \ Field(Restr r A)" using * assms + by (simp add: order_on_defs Refl_Field_Restr2) + hence "bij_betw id (under (Restr r A) a) (under r a)" + using * unfolding embed_def by auto + hence "under r a \ under (Restr r A) a" + unfolding bij_betw_def by auto + also have "\ \ Field(Restr r A)" by (simp add: under_Field) + also have "\ \ A" by (simp add: Field_Restr_subset) + finally have "under r a \ 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" + have Well: "wo_rel r" unfolding wo_rel_def using WELL . + hence Refl: "Refl r" by (simp add: wo_rel.REFL) + hence Field: "Field ?rB = Field r Int B" + using Refl_Field_Restr by blast + have WellB: "wo_rel ?rB \ Well_order ?rB" using WELL + by (simp add: Well_order_Restr wo_rel_def) + (* Main proof *) + show ?thesis using WellB assms + proof(auto simp add: wo_rel.ofilter_def under_def) + fix a assume "a \ A" and *: "a \ B" + hence "a \ Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def) + with * show "a \ Field ?rB" using Field by auto + next + fix a b assume "a \ A" and "(b,a) \ r" + thus "b \ 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 \ 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 \ B) = (embed (Restr r A) (Restr r B) id)" +proof- + let ?rA = "Restr r A" let ?rB = "Restr r B" + have Well: "wo_rel r" unfolding wo_rel_def using WELL . + hence Refl: "Refl r" by (simp add: wo_rel.REFL) + hence FieldA: "Field ?rA = Field r Int A" + using Refl_Field_Restr by blast + have FieldB: "Field ?rB = Field r Int B" + using Refl Refl_Field_Restr by blast + have WellA: "wo_rel ?rA \ Well_order ?rA" using WELL + by (simp add: Well_order_Restr wo_rel_def) + have WellB: "wo_rel ?rB \ Well_order ?rB" using WELL + by (simp add: Well_order_Restr wo_rel_def) + (* Main proof *) + show ?thesis + proof + assume *: "A \ B" + hence "wo_rel.ofilter (Restr r B) A" using assms + by (simp add: ofilter_Restr_subset) + hence "embed (Restr ?rB A) (Restr r B) id" + using WellB ofilter_embed[of "?rB" A] by auto + thus "embed (Restr r A) (Restr r B) id" + using * by (simp add: Restr_subset) + next + assume *: "embed (Restr r A) (Restr r B) id" + {fix a assume **: "a \ A" + hence "a \ Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def) + with ** FieldA have "a \ Field ?rA" by auto + hence "a \ Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto + hence "a \ B" using FieldB by auto + } + thus "A \ 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)) \ + ((A = B) = (iso (Restr r A) (Restr r B) id))" +proof- + let ?rA = "Restr r A" let ?rB = "Restr r B" + have Well: "wo_rel r" unfolding wo_rel_def using WELL . + hence Refl: "Refl r" by (simp add: wo_rel.REFL) + hence "Field ?rA = Field r Int A" + using Refl_Field_Restr by blast + hence FieldA: "Field ?rA = A" using OFA Well + by (auto simp add: wo_rel.ofilter_def) + have "Field ?rB = Field r Int B" + using Refl Refl_Field_Restr by blast + hence FieldB: "Field ?rB = B" using OFB Well + by (auto simp add: wo_rel.ofilter_def) + (* Main proof *) + 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" +proof- + let ?A' = "Field r'" + let ?r'' = "Restr r (f ` ?A')" + have 0: "Well_order ?r''" using WELL Well_order_Restr by blast + have 1: "wo_rel.ofilter r (f ` ?A')" using assms embed_Field_ofilter by blast + hence "Field ?r'' = f ` (Field r')" using WELL Field_Restr_ofilter by blast + hence "bij_betw f ?A' (Field ?r'')" + using EMB embed_inj_on WELL' unfolding bij_betw_def by blast + moreover + {have "\a b. (a,b) \ r' \ a \ Field r' \ b \ Field r'" + unfolding Field_def by auto + hence "compat r' ?r'' f" + using assms embed_iff_compat_inj_on_ofilter + unfolding compat_def by blast + } + ultimately show ?thesis using WELL' 0 iso_iff3 by blast +qed + + +subsection {* The strict inclusion on proper ofilters is well-founded *} + +definition ofilterIncl :: "'a rel \ 'a set rel" +where +"ofilterIncl r \ {(A,B). wo_rel.ofilter r A \ A \ Field r \ + wo_rel.ofilter r B \ B \ Field r \ A < B}" + +lemma wf_ofilterIncl: +assumes WELL: "Well_order r" +shows "wf(ofilterIncl r)" +proof- + have Well: "wo_rel r" using WELL by (simp add: wo_rel_def) + hence Lo: "Linear_order r" by (simp add: wo_rel.LIN) + let ?h = "(\ A. wo_rel.suc r A)" + let ?rS = "r - Id" + have "wf ?rS" using WELL by (simp add: order_on_defs) + moreover + have "compat (ofilterIncl r) ?rS ?h" + proof(unfold compat_def ofilterIncl_def, + intro allI impI, simp, elim conjE) + fix A B + assume *: "wo_rel.ofilter r A" "A \ Field r" and + **: "wo_rel.ofilter r B" "B \ Field r" and ***: "A < B" + then obtain a and b where 0: "a \ Field r \ b \ Field r" and + 1: "A = underS r a \ B = underS r b" + using Well by (auto simp add: wo_rel.ofilter_underS_Field) + hence "a \ b" using *** by auto + moreover + have "(a,b) \ r" using 0 1 Lo *** + by (auto simp add: underS_incl_iff) + moreover + have "a = wo_rel.suc r A \ b = wo_rel.suc r B" + using Well 0 1 by (simp add: wo_rel.suc_underS) + ultimately + show "(wo_rel.suc r A, wo_rel.suc r B) \ r \ wo_rel.suc r A \ wo_rel.suc r B" + by simp + 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 "\o"}); +\item @{text "ordLess"}, of being strictly embedded (abbreviated @{text ""}, @{text "<"}, @{text "="} associated to a total order on a set. +*} + +definition ordLeq :: "('a rel * 'a' rel) set" +where +"ordLeq = {(r,r'). Well_order r \ Well_order r' \ (\f. embed r r' f)}" + +abbreviation ordLeq2 :: "'a rel \ 'a' rel \ bool" (infix "<=o" 50) +where "r <=o r' \ (r,r') \ ordLeq" + +abbreviation ordLeq3 :: "'a rel \ 'a' rel \ bool" (infix "\o" 50) +where "r \o r' \ r <=o r'" + +definition ordLess :: "('a rel * 'a' rel) set" +where +"ordLess = {(r,r'). Well_order r \ Well_order r' \ (\f. embedS r r' f)}" + +abbreviation ordLess2 :: "'a rel \ 'a' rel \ bool" (infix " (r,r') \ ordLess" + +definition ordIso :: "('a rel * 'a' rel) set" +where +"ordIso = {(r,r'). Well_order r \ Well_order r' \ (\f. iso r r' f)}" + +abbreviation ordIso2 :: "'a rel \ 'a' rel \ bool" (infix "=o" 50) +where "r =o r' \ (r,r') \ ordIso" + +lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def + +lemma ordLeq_Well_order_simp: +assumes "r \o r'" +shows "Well_order r \ Well_order r'" +using assms unfolding ordLeq_def by simp + +text{* Notice that the relations @{text "\o"}, @{text " r \o r" +unfolding ordLeq_def using id_embed[of r] by blast + +lemma ordLeq_transitive[trans]: +assumes *: "r \o r'" and **: "r' \o r''" +shows "r \o r''" +proof- + obtain f and f' + where 1: "Well_order r \ Well_order r' \ Well_order r''" and + "embed r r' f" and "embed r' r'' f'" + using * ** unfolding ordLeq_def by blast + hence "embed r r'' (f' o f)" + using comp_embed[of r r' f r'' f'] by auto + thus "r \o r''" unfolding ordLeq_def using 1 by auto +qed + +lemma ordLeq_total: +"\Well_order r; Well_order r'\ \ r \o r' \ r' \o r" +unfolding ordLeq_def using wellorders_totally_ordered by blast + +lemma ordIso_reflexive: +"Well_order r \ r =o r" +unfolding ordIso_def using id_iso[of r] by blast + +lemma ordIso_transitive[trans]: +assumes *: "r =o r'" and **: "r' =o r''" +shows "r =o r''" +proof- + obtain f and f' + where 1: "Well_order r \ Well_order r' \ Well_order r''" and + "iso r r' f" and 3: "iso r' r'' f'" + using * ** unfolding ordIso_def by auto + hence "iso r r'' (f' 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 \ Well_order r'" and + 2: "embed r r' f \ bij_betw f (Field r) (Field r')" + using * by (auto simp add: ordIso_def iso_def) + let ?f' = "inv_into (Field r) f" + have "embed r' r ?f' \ 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 \o r'" and " r' 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''" +shows "r 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 \o r'" and " r' =o r''" +shows "r \o r''" +proof- + have "Well_order r \ 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' \o r''" +shows "r \o r''" +proof- + have "Well_order r \ 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 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' 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 (\f'. embed r' r f')" +proof- + obtain f where 1: "Well_order r \ Well_order r'" and 2: "embed r r' f" and + 3: " \ bij_betw f (Field r) (Field r')" + using assms unfolding ordLess_def by (auto simp add: embedS_def) + {fix f' assume *: "embed r' r f'" + hence "bij_betw f (Field r) (Field r')" using 1 2 + by (simp add: embed_bothWays_Field_bij_betw) + with 3 have False by contradiction + } + thus ?thesis by blast +qed + +lemma ordLess_Field: +assumes OL: "r1 (f`(Field r1) = Field r2)" +proof- + let ?A1 = "Field r1" let ?A2 = "Field r2" + obtain g where + 0: "Well_order r1 \ Well_order r2" and + 1: "embed r1 r2 g \ \(bij_betw g ?A1 ?A2)" + using OL unfolding ordLess_def by (auto simp add: embedS_def) + hence "\a \ ?A1. f a = g a" + using 0 EMB embed_unique[of r1] by auto + hence "\(bij_betw f ?A1 ?A2)" + 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 Well_order r' \ \(\f'. embed r' r f'))" +proof + assume *: "r (\f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp + with * show "Well_order r \ Well_order r' \ \ (\f'. embed r' r f')" + unfolding ordLess_def by auto +next + assume *: "Well_order r \ Well_order r' \ \ (\f'. embed r' r f')" + then obtain f where 1: "embed r r' f" + using wellorders_totally_ordered[of r r'] by blast + moreover + {assume "bij_betw f (Field r) (Field r')" + with * 1 have "embed r' r (inv_into (Field r) f) " + using inv_into_Field_embed_bij_betw[of r r' f] by auto + with * have False by blast + } + ultimately show "(r,r') \ ordLess" + unfolding ordLess_def using * by (fastforce simp add: embedS_def) +qed + +lemma ordLess_irreflexive: "\ r \(\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 \o r' = (r r =o r')" +unfolding ordRels_def embedS_defs iso_defs by blast + +lemma ordIso_iff_ordLeq: +"(r =o r') = (r \o r' \ r' \o r)" +proof + assume "r =o r'" + then obtain f where 1: "Well_order r \ Well_order r' \ + embed r r' f \ bij_betw f (Field r) (Field r')" + unfolding ordIso_def iso_defs by auto + hence "embed r r' f \ embed r' r (inv_into (Field r) f)" + by (simp add: inv_into_Field_embed_bij_betw) + thus "r \o r' \ r' \o r" + unfolding ordLeq_def using 1 by auto +next + assume "r \o r' \ r' \o r" + then obtain f and g where 1: "Well_order r \ Well_order r' \ + embed r r' f \ embed r' r g" + 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 \ r' \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 r' \o r" +proof- + have "r \o r' \ r' \o r" + using assms by (simp add: ordLeq_total) + moreover + {assume "\ r r \o r'" + hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast + hence "r' \o r" using ordIso_symmetric ordIso_iff_ordLeq by blast + } + ultimately show ?thesis by blast +qed + +lemma not_ordLess_ordIso: +"r \ 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 "(\ r' \o r) = (r r' o r')" +using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast + +lemma ordLess_transitive[trans]: +"\r \ r r \o r'" +using ordIso_iff_ordLeq by blast + +lemma ordLess_imp_ordLeq: +"r r \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 \ B) = (Restr r A \o Restr r B)" +proof + assume "A \ B" + thus "Restr r A \o Restr r B" + unfolding ordLeq_def using assms + Well_order_Restr Well_order_Restr ofilter_subset_embed by blast +next + assume *: "Restr r A \o Restr r B" + then obtain f where "embed (Restr r A) (Restr r B) f" + unfolding ordLeq_def by blast + {assume "B < A" + hence "Restr r B 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 Well_order ?rB" + using WELL Well_order_Restr by blast + have "(A < B) = (\ B \ A)" using assms + wo_rel_def wo_rel.ofilter_linord[of r A B] by blast + also have "\ = (\ Restr r B \o Restr r A)" + using assms ofilter_subset_ordLeq by blast + also have "\ = (Restr r A Well_order r; wo_rel.ofilter r A\ \ (A < Field r) = (Restr r A {}" +shows "Restr r (underS r a) (ofilterIncl r3)" +proof- + have OL13: "r1 Well_order r2 \ Well_order r3" and + 1: "embed r1 r2 f12 \ \(bij_betw f12 ?A1 ?A2)" and + 2: "embed r2 r3 g23 \ \(bij_betw g23 ?A2 ?A3)" + using OL12 OL23 by (auto simp add: ordLess_def embedS_def) + hence "\a \ ?A2. f23 a = g23 a" + using EMB23 embed_unique[of r2 r3] by blast + hence 3: "\(bij_betw f23 ?A2 ?A3)" + using 2 bij_betw_cong[of ?A2 f23 g23] by blast + (* *) + have 4: "wo_rel.ofilter r2 (f12 ` ?A1) \ f12 ` ?A1 \ ?A2" + using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field) + have 5: "wo_rel.ofilter r3 (f23 ` ?A2) \ f23 ` ?A2 \ ?A3" + using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field) + have 6: "wo_rel.ofilter r3 (f13 ` ?A1) \ f13 ` ?A1 \ ?A3" + using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field) + (* *) + have "f12 ` ?A1 < ?A2" + using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def) + moreover have "inj_on f23 ?A2" + using EMB23 0 by (simp add: wo_rel_def embed_inj_on) + ultimately + have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset) + moreover + {have "embed r1 r3 (f23 o f12)" + using 1 EMB23 0 by (auto simp add: comp_embed) + hence "\a \ ?A1. f23(f12 a) = f13 a" + using EMB13 0 embed_unique[of r1 r3 "f23 o f12" f13] by auto + hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force + } + ultimately + have "f13 ` ?A1 < f23 ` ?A2" by simp + (* *) + with 5 6 show ?thesis + unfolding ofilterIncl_def by auto +qed + +lemma ordLess_iff_ordIso_Restr: +assumes WELL: "Well_order r" and WELL': "Well_order r'" +shows "(r' a \ Field r. r' =o Restr r (underS r a))" +proof(auto) + fix a assume *: "a \ Field r" and **: "r' =o Restr r (underS r a)" + hence "Restr r (underS r a) Well_order r'" and + 2: "embed r' r f \ f ` (Field r') \ Field r" + unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast + hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast + then obtain a where 3: "a \ Field r" and 4: "underS r a = f ` (Field r')" + using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def) + have "iso r' (Restr r (f ` (Field r'))) f" + using embed_implies_iso_Restr 2 assms by blast + moreover have "Well_order (Restr r (f ` (Field r')))" + using WELL Well_order_Restr by blast + ultimately have "r' =o Restr r (f ` (Field r'))" + using WELL' unfolding ordIso_def by auto + hence "r' =o Restr r (underS r a)" using 4 by auto + thus "\a \ Field r. r' =o Restr r (underS r a)" using 3 by auto +qed + +lemma internalize_ordLess: +"(r' p. Field p < Field r \ r' =o p \ p Well_order r'" unfolding ordLess_def by auto + with * obtain a where 1: "a \ Field r" and 2: "r' =o Restr r (underS r a)" + using ordLess_iff_ordIso_Restr by blast + let ?p = "Restr r (underS r a)" + have "wo_rel.ofilter r (underS r a)" using 0 + by (simp add: wo_rel_def wo_rel.underS_ofilter) + hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast + hence "Field ?p < Field r" using underS_Field2 1 by fast + moreover have "?p p. Field p < Field r \ r' =o p \ p p. Field p < Field r \ r' =o p \ p o r) = (\p. Field p \ Field r \ r' =o p \ p \o r)" +proof + assume *: "r' \o r" + moreover + {assume "r' r' =o p \ p p. Field p \ Field r \ r' =o p \ p \o r" + using ordLeq_iff_ordLess_or_ordIso by blast + } + moreover + have "r \o r" using * ordLeq_def ordLeq_reflexive by blast + ultimately show "\p. Field p \ Field r \ r' =o p \ p \o r" + using ordLeq_iff_ordLess_or_ordIso by blast +next + assume "\p. Field p \ Field r \ r' =o p \ p \o r" + thus "r' \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 \o r') = (\a \ Field r. Restr r (underS r a) o r'" + fix a assume "a \ Field r" + hence "Restr r (underS r a) a \ Field r. Restr r (underS r a) Field r \ r' =o Restr r (underS r a)" + using assms ordLess_iff_ordIso_Restr by blast + hence False using * not_ordLess_ordIso ordIso_symmetric by blast + } + thus "r \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: "\finite(Field r')" +shows "r o r" + then obtain h where "inj_on h (Field r') \ h ` (Field r') \ Field r" + unfolding ordLeq_def using assms embed_inj_on embed_Field by blast + hence False using finite_imageD finite_subset FIN INF by blast + } + thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast +qed + +lemma finite_well_order_on_ordIso: +assumes FIN: "finite A" and + WELL: "well_order_on A r" and WELL': "well_order_on A r'" +shows "r =o r'" +proof- + have 0: "Well_order r \ Well_order r' \ Field r = A \ Field r' = A" + using assms well_order_on_Well_order by blast + moreover + have "\r r'. well_order_on A r \ well_order_on A r' \ r \o r' + \ r =o r'" + proof(clarify) + fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'" + have 2: "Well_order r \ Well_order r' \ Field r = A \ Field r' = A" + using * ** well_order_on_Well_order by blast + assume "r \o r'" + then obtain f where 1: "embed r r' f" and + "inj_on f A \ f ` A \ A" + unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast + hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast + thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto + qed + ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast +qed + +subsection{* @{text " 'a rel \ 'a set" +where "ord_to_filter r0 r \ (SOME f. embed r r0 f) ` (Field r)" + +lemma ord_to_filter_compat: +"compat (ordLess Int (ordLess^-1``{r0} \ ordLess^-1``{r0})) + (ofilterIncl r0) + (ord_to_filter r0)" +proof(unfold compat_def ord_to_filter_def, clarify) + fix r1::"'a rel" and r2::"'a rel" + let ?A1 = "Field r1" let ?A2 ="Field r2" let ?A0 ="Field r0" + let ?phi10 = "\ f10. embed r1 r0 f10" let ?f10 = "SOME f. ?phi10 f" + let ?phi20 = "\ f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f" + assume *: "r1 f. ?phi10 f) \ (\f. ?phi20 f)" + by (auto simp add: ordLess_def embedS_def) + hence "?phi10 ?f10 \ ?phi20 ?f20" by (auto simp add: someI_ex) + thus "(?f10 ` ?A1, ?f20 ` ?A2) \ ofilterIncl r0" + using * ** by (simp add: embed_ordLess_ofilterIncl) +qed + +theorem wf_ordLess: "wf ordLess" +proof- + {fix r0 :: "('a \ 'a) set" + (* need to annotate here!*) + let ?ordLess = "ordLess::('d rel * 'd rel) set" + let ?R = "?ordLess Int (?ordLess^-1``{r0} \ ?ordLess^-1``{r0})" + {assume Case1: "Well_order r0" + hence "wf ?R" + using wf_ofilterIncl[of r0] + compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"] + ord_to_filter_compat[of r0] by auto + } + moreover + {assume Case2: "\ Well_order r0" + hence "?R = {}" unfolding ordLess_def by auto + hence "wf ?R" using wf_empty by simp + } + ultimately have "wf ?R" by blast + } + thus ?thesis by (simp add: trans_wf_iff ordLess_trans) +qed + +corollary exists_minim_Well_order: +assumes NE: "R \ {}" and WELL: "\r \ R. Well_order r" +shows "\r \ R. \r' \ R. r \o r'" +proof- + obtain r where "r \ R \ (\r' \ R. \ r' ('a \ 'a') \ 'a' rel" +where +"dir_image r f = {(f a, f b)| a b. (a,b) \ r}" + +lemma dir_image_Field: +"Field(dir_image r f) = f ` (Field r)" +unfolding dir_image_def Field_def Range_def Domain_def by fast + +lemma dir_image_minus_Id: +"inj_on f (Field r) \ (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- + {fix a' b' + assume "(a',b') \ dir_image r f" + then obtain a b where 1: "a' = f a \ b' = f b \ (a,b) \ r" + unfolding dir_image_def by blast + hence "a \ Field r \ b \ Field r" using Field_def by fastforce + hence "(a,a) \ r \ (b,b) \ r" using assms by (simp add: refl_on_def) + with 1 have "(a',a') \ dir_image r f \ (b',b') \ dir_image r f" + 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) + fix a' b' c' + assume "(a',b') \ dir_image r f" "(b',c') \ dir_image r f" + then obtain a b1 b2 c where 1: "a' = f a \ b' = f b1 \ b' = f b2 \ c' = f c" and + 2: "(a,b1) \ r \ (b2,c) \ r" + unfolding dir_image_def by blast + hence "b1 \ Field r \ b2 \ Field r" + unfolding Field_def by auto + hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto + hence "(a,c): r" using 2 TRANS unfolding trans_def by blast + thus "(a',c') \ dir_image r f" + unfolding dir_image_def using 1 by auto +qed + +lemma Preorder_dir_image: +"\Preorder r; inj_on f (Field r)\ \ 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) + fix a' b' + assume "(a',b') \ dir_image r f" "(b',a') \ dir_image r f" + then obtain a1 b1 a2 b2 where 1: "a' = f a1 \ a' = f a2 \ b' = f b1 \ b' = f b2" and + 2: "(a1,b1) \ r \ (b2,a2) \ r " and + 3: "{a1,a2,b1,b2} \ Field r" + unfolding dir_image_def Field_def by blast + hence "a1 = a2 \ 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: +"\Partial_order r; inj_on f (Field r)\ \ 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) + fix a' b' + assume "a' \ Field (dir_image r f)" "b' \ Field (dir_image r f)" + then obtain a and b where 1: "a \ Field r \ b \ Field r \ f a = a' \ f b = b'" + unfolding dir_image_Field[of r f] by blast + moreover assume "a' \ b'" + ultimately have "a \ b" using INJ unfolding inj_on_def by auto + hence "(a,b) \ r \ (b,a) \ r" using 1 TOT unfolding total_on_def by auto + thus "(a',b') \ dir_image r f \ (b',a') \ dir_image r f" + using 1 unfolding dir_image_def by auto +qed + +lemma Linear_order_dir_image: +"\Linear_order r; inj_on f (Field r)\ \ 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) + fix A'::"'b set" + assume SUB: "A' \ Field(dir_image r f)" and NE: "A' \ {}" + obtain A where A_def: "A = {a \ Field r. f a \ A'}" by blast + have "A \ {} \ A \ Field r" using A_def SUB NE by (auto simp: dir_image_Field) + then obtain a where 1: "a \ A \ (\b \ A. (b,a) \ r)" + using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast + have "\b' \ A'. (b',f a) \ dir_image r f" + proof(clarify) + fix b' assume *: "b' \ A'" and **: "(b',f a) \ dir_image r f" + obtain b1 a1 where 2: "b' = f b1 \ f a = f a1" and + 3: "(b1,a1) \ r \ {a1,b1} \ Field r" + using ** unfolding dir_image_def Field_def by blast + hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto + hence "b1 \ A \ (b1,a) \ r" using 2 3 A_def * by auto + with 1 show False by auto + qed + thus "\a'\A'. \b'\A'. (b', a') \ dir_image r f" + using A_def 1 by blast +qed + +lemma Well_order_dir_image: +"\Well_order r; inj_on f (Field r)\ \ 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_bij_betw: +"\inj_on f (Field r)\ \ bij_betw f (Field r) (Field (dir_image r f))" +unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs) + +lemma dir_image_compat: +"compat r (dir_image r f) f" +unfolding compat_def dir_image_def by auto + +lemma dir_image_iso: +"\Well_order r; inj_on f (Field r)\ \ 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: +"\Well_order r; inj_on f (Field r)\ \ 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 "\r'. well_order_on A' r' \ r =o r'" +proof- + let ?r' = "dir_image r f" + have 1: "A = Field r \ Well_order r" + using WELL well_order_on_Well_order by blast + hence 2: "iso r ?r' f" + using dir_image_iso using BIJ unfolding bij_betw_def by auto + hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast + hence "Field ?r' = A'" + using 1 BIJ unfolding bij_betw_def by auto + moreover have "Well_order ?r'" + using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast + ultimately show ?thesis unfolding ordIso_def using 1 2 by blast +qed + + +subsection {* Bounded square *} + +text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic +order @{text "bsqr r"} on @{text "(Field r) \ (Field r)"}, applying the +following criteria (in this order): +\begin{itemize} +\item compare the maximums; +\item compare the first components; +\item compare the second components. +\end{itemize} +% +The only application of this construction that we are aware of is +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} \ Field r \ + (a1 = b1 \ a2 = b2 \ + (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id \ + wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id \ + wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id + )}" + +lemma Field_bsqr: +"Field (bsqr r) = Field r \ Field r" +proof + show "Field (bsqr r) \ Field r \ Field r" + proof- + {fix a1 a2 assume "(a1,a2) \ Field (bsqr r)" + moreover + have "\ b1 b2. ((a1,a2),(b1,b2)) \ bsqr r \ ((b1,b2),(a1,a2)) \ bsqr r \ + a1 \ Field r \ a2 \ Field r" unfolding bsqr_def by auto + ultimately have "a1 \ Field r \ a2 \ Field r" unfolding Field_def by auto + } + thus ?thesis unfolding Field_def by force + qed +next + show "Field r \ Field r \ Field (bsqr r)" + proof(auto) + fix a1 a2 assume "a1 \ Field r" and "a2 \ Field r" + hence "((a1,a2),(a1,a2)) \ bsqr r" unfolding bsqr_def by blast + thus "(a1,a2) \ 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) + (* Preliminary facts *) + have Well: "wo_rel r" using assms wo_rel_def by auto + hence Trans: "trans r" using wo_rel.TRANS by auto + have Anti: "antisym r" using wo_rel.ANTISYM Well by auto + hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id) + (* Main proof *) + fix a1 a2 b1 b2 c1 c2 + assume *: "((a1,a2),(b1,b2)) \ bsqr r" and **: "((b1,b2),(c1,c2)) \ bsqr r" + hence 0: "{a1,a2,b1,b2,c1,c2} \ Field r" unfolding bsqr_def by auto + have 1: "a1 = b1 \ a2 = b2 \ (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id \ + wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id \ + wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id" + using * unfolding bsqr_def by auto + have 2: "b1 = c1 \ b2 = c2 \ (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \ r - Id \ + wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ (b1,c1) \ r - Id \ + wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ b1 = c1 \ (b2,c2) \ r - Id" + using ** unfolding bsqr_def by auto + show "((a1,a2),(c1,c2)) \ bsqr r" + proof- + {assume Case1: "a1 = b1 \ a2 = b2" + hence ?thesis using ** by simp + } + moreover + {assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id" + {assume Case21: "b1 = c1 \ b2 = c2" + hence ?thesis using * by simp + } + moreover + {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \ r - Id" + hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \ r - Id" + using Case2 TransS trans_def[of "r - Id"] by blast + hence ?thesis using 0 unfolding bsqr_def by auto + } + moreover + {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2" + hence ?thesis using Case2 0 unfolding bsqr_def by auto + } + ultimately have ?thesis using 0 2 by auto + } + moreover + {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id" + {assume Case31: "b1 = c1 \ b2 = c2" + hence ?thesis using * by simp + } + moreover + {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \ r - Id" + hence ?thesis using Case3 0 unfolding bsqr_def by auto + } + moreover + {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ (b1,c1) \ r - Id" + hence "(a1,c1) \ r - Id" + using Case3 TransS trans_def[of "r - Id"] by blast + hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto + } + moreover + {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ b1 = c1" + hence ?thesis using Case3 0 unfolding bsqr_def by auto + } + ultimately have ?thesis using 0 2 by auto + } + moreover + {assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id" + {assume Case41: "b1 = c1 \ b2 = c2" + hence ?thesis using * by simp + } + moreover + {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \ r - Id" + hence ?thesis using Case4 0 unfolding bsqr_def by force + } + moreover + {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ (b1,c1) \ r - Id" + hence ?thesis using Case4 0 unfolding bsqr_def by auto + } + moreover + {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \ b1 = c1 \ (b2,c2) \ r - Id" + hence "(a2,c2) \ r - Id" + using Case4 TransS trans_def[of "r - Id"] by blast + hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto + } + ultimately have ?thesis using 0 2 by auto + } + ultimately show ?thesis using 0 1 by auto + qed +qed + +lemma bsqr_antisym: +assumes "Well_order r" +shows "antisym (bsqr r)" +proof(unfold antisym_def, clarify) + (* Preliminary facts *) + have Well: "wo_rel r" using assms wo_rel_def by auto + hence Trans: "trans r" using wo_rel.TRANS by auto + have Anti: "antisym r" using wo_rel.ANTISYM Well by auto + hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id) + hence IrrS: "\a b. \((a,b) \ r - Id \ (b,a) \ r - Id)" + using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast + (* Main proof *) + fix a1 a2 b1 b2 + assume *: "((a1,a2),(b1,b2)) \ bsqr r" and **: "((b1,b2),(a1,a2)) \ bsqr r" + hence 0: "{a1,a2,b1,b2} \ Field r" unfolding bsqr_def by auto + have 1: "a1 = b1 \ a2 = b2 \ (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id \ + wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id \ + wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id" + using * unfolding bsqr_def by auto + have 2: "b1 = a1 \ b2 = a2 \ (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \ r - Id \ + wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \ (b1,a1) \ r - Id \ + wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \ b1 = a1 \ (b2,a2) \ r - Id" + using ** unfolding bsqr_def by auto + show "a1 = b1 \ a2 = b2" + proof- + {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r - Id" + {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \ r - Id" + hence False using Case1 IrrS by blast + } + moreover + {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2" + hence False using Case1 by auto + } + ultimately have ?thesis using 0 2 by auto + } + moreover + {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ (a1,b1) \ r - Id" + {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \ r - Id" + hence False using Case2 by auto + } + moreover + {assume Case22: "(b1,a1) \ r - Id" + hence False using Case2 IrrS by blast + } + moreover + {assume Case23: "b1 = a1" + hence False using Case2 by auto + } + ultimately have ?thesis using 0 2 by auto + } + moreover + {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \ a1 = b1 \ (a2,b2) \ r - Id" + moreover + {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \ r - Id" + hence False using Case3 by auto + } + moreover + {assume Case32: "(b1,a1) \ r - Id" + hence False using Case3 by auto + } + moreover + {assume Case33: "(b2,a2) \ r - Id" + hence False using Case3 IrrS by blast + } + ultimately have ?thesis using 0 2 by auto + } + ultimately show ?thesis using 0 1 by blast + qed +qed + +lemma bsqr_Total: +assumes "Well_order r" +shows "Total(bsqr r)" +proof- + (* Preliminary facts *) + have Well: "wo_rel r" using assms wo_rel_def by auto + hence Total: "\a \ Field r. \b \ Field r. (a,b) \ r \ (b,a) \ r" + using wo_rel.TOTALS by auto + (* Main proof *) + {fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \ Field(bsqr r)" + hence 0: "a1 \ Field r \ a2 \ Field r \ b1 \ Field r \ b2 \ Field r" + using Field_bsqr by blast + have "((a1,a2) = (b1,b2) \ ((a1,a2),(b1,b2)) \ bsqr r \ ((b1,b2),(a1,a2)) \ bsqr r)" + proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0) + (* Why didn't clarsimp simp add: Well 0 do the same job? *) + assume Case1: "(a1,a2) \ r" + hence 1: "wo_rel.max2 r a1 a2 = a2" + using Well 0 by (simp add: wo_rel.max2_equals2) + show ?thesis + proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0) + assume Case11: "(b1,b2) \ r" + hence 2: "wo_rel.max2 r b1 b2 = b2" + using Well 0 by (simp add: wo_rel.max2_equals2) + show ?thesis + proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) + assume Case111: "(a2,b2) \ r - Id \ (b2,a2) \ r - Id" + thus ?thesis using 0 1 2 unfolding bsqr_def by auto + next + assume Case112: "a2 = b2" + show ?thesis + proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) + assume Case1121: "(a1,b1) \ r - Id \ (b1,a1) \ r - Id" + thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto + next + assume Case1122: "a1 = b1" + thus ?thesis using Case112 by auto + qed + qed + next + assume Case12: "(b2,b1) \ r" + hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1) + show ?thesis + proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0) + assume Case121: "(a2,b1) \ r - Id \ (b1,a2) \ r - Id" + thus ?thesis using 0 1 3 unfolding bsqr_def by auto + next + assume Case122: "a2 = b1" + show ?thesis + proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) + assume Case1221: "(a1,b1) \ r - Id \ (b1,a1) \ r - Id" + thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto + next + assume Case1222: "a1 = b1" + show ?thesis + proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) + assume Case12221: "(a2,b2) \ r - Id \ (b2,a2) \ r - Id" + thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto + next + assume Case12222: "a2 = b2" + thus ?thesis using Case122 Case1222 by auto + qed + qed + qed + qed + next + assume Case2: "(a2,a1) \ r" + hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1) + show ?thesis + proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0) + assume Case21: "(b1,b2) \ r" + hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2) + show ?thesis + proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0) + assume Case211: "(a1,b2) \ r - Id \ (b2,a1) \ r - Id" + thus ?thesis using 0 1 2 unfolding bsqr_def by auto + next + assume Case212: "a1 = b2" + show ?thesis + proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) + assume Case2121: "(a1,b1) \ r - Id \ (b1,a1) \ r - Id" + thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto + next + assume Case2122: "a1 = b1" + show ?thesis + proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) + assume Case21221: "(a2,b2) \ r - Id \ (b2,a2) \ r - Id" + thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto + next + assume Case21222: "a2 = b2" + thus ?thesis using Case2122 Case212 by auto + qed + qed + qed + next + assume Case22: "(b2,b1) \ r" + hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1) + show ?thesis + proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) + assume Case221: "(a1,b1) \ r - Id \ (b1,a1) \ r - Id" + thus ?thesis using 0 1 3 unfolding bsqr_def by auto + next + assume Case222: "a1 = b1" + show ?thesis + proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) + assume Case2221: "(a2,b2) \ r - Id \ (b2,a2) \ r - Id" + thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto + next + assume Case2222: "a2 = b2" + thus ?thesis using Case222 by auto + qed + qed + qed + qed + } + thus ?thesis unfolding total_on_def by fast +qed + +lemma bsqr_Linear_order: +assumes "Well_order r" +shows "Linear_order(bsqr r)" +unfolding order_on_defs +using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast + +lemma bsqr_Well_order: +assumes "Well_order r" +shows "Well_order(bsqr r)" +using assms +proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI) + have 0: "\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a,a') \ r)" + using assms well_order_on_def Linear_order_Well_order_iff by blast + fix D assume *: "D \ Field (bsqr r)" and **: "D \ {}" + hence 1: "D \ Field r \ Field r" unfolding Field_bsqr by simp + (* *) + obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \ D}" by blast + have "M \ {}" using 1 M_def ** by auto + moreover + have "M \ Field r" unfolding M_def + using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce + ultimately obtain m where m_min: "m \ M \ (\a \ M. (m,a) \ r)" + using 0 by blast + (* *) + obtain A1 where A1_def: "A1 = {a1. \a2. (a1,a2) \ D \ wo_rel.max2 r a1 a2 = m}" by blast + have "A1 \ Field r" unfolding A1_def using 1 by auto + moreover have "A1 \ {}" unfolding A1_def using m_min unfolding M_def by blast + ultimately obtain a1 where a1_min: "a1 \ A1 \ (\a \ A1. (a1,a) \ r)" + using 0 by blast + (* *) + obtain A2 where A2_def: "A2 = {a2. (a1,a2) \ D \ wo_rel.max2 r a1 a2 = m}" by blast + have "A2 \ Field r" unfolding A2_def using 1 by auto + moreover have "A2 \ {}" unfolding A2_def + using m_min a1_min unfolding A1_def M_def by blast + ultimately obtain a2 where a2_min: "a2 \ A2 \ (\a \ A2. (a2,a) \ r)" + using 0 by blast + (* *) + have 2: "wo_rel.max2 r a1 a2 = m" + using a1_min a2_min unfolding A1_def A2_def by auto + have 3: "(a1,a2) \ D" using a2_min unfolding A2_def by auto + (* *) + moreover + {fix b1 b2 assume ***: "(b1,b2) \ D" + hence 4: "{a1,a2,b1,b2} \ Field r" using 1 3 by blast + have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r" + using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto + have "((a1,a2),(b1,b2)) \ bsqr r" + proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2") + assume Case1: "wo_rel.max2 r a1 a2 \ wo_rel.max2 r b1 b2" + thus ?thesis unfolding bsqr_def using 4 5 by auto + next + assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2" + hence "b1 \ A1" unfolding A1_def using 2 *** by auto + hence 6: "(a1,b1) \ r" using a1_min by auto + show ?thesis + proof(cases "a1 = b1") + assume Case21: "a1 \ b1" + thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto + next + assume Case22: "a1 = b1" + hence "b2 \ A2" unfolding A2_def using 2 *** Case2 by auto + hence 7: "(a2,b2) \ r" using a2_min by auto + thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto + qed + qed + } + (* *) + ultimately show "\d \ D. \d' \ D. (d,d') \ bsqr r" by fastforce +qed + +lemma bsqr_max2: +assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \ bsqr r" +shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \ r" +proof- + have "{(a1,a2),(b1,b2)} \ Field(bsqr r)" + using LEQ unfolding Field_def by auto + hence "{a1,a2,b1,b2} \ Field r" unfolding Field_bsqr by auto + hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \ Field 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) \ r \ 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 \ Field r" and + NE: "\ (\a. Field r = under r a)" +shows "\A. wo_rel.ofilter r A \ A < Field r \ D \ A \ A" +proof- + let ?r' = "bsqr r" + have Well: "wo_rel r" using WELL wo_rel_def by blast + hence Trans: "trans r" using wo_rel.TRANS by blast + have Well': "Well_order ?r' \ wo_rel ?r'" + using WELL bsqr_Well_order wo_rel_def by blast + (* *) + have "D < Field ?r'" unfolding Field_bsqr using SUB . + with OF obtain a1 and a2 where + "(a1,a2) \ Field ?r'" and 1: "D = underS ?r' (a1,a2)" + using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto + hence 2: "{a1,a2} \ Field r" unfolding Field_bsqr by auto + let ?m = "wo_rel.max2 r a1 a2" + have "D \ (under r ?m) \ (under r ?m)" + proof(unfold 1) + {fix b1 b2 + let ?n = "wo_rel.max2 r b1 b2" + assume "(b1,b2) \ underS ?r' (a1,a2)" + hence 3: "((b1,b2),(a1,a2)) \ ?r'" + unfolding underS_def by blast + hence "(?n,?m) \ r" using WELL by (simp add: bsqr_max2) + moreover + {have "(b1,b2) \ Field ?r'" using 3 unfolding Field_def by auto + hence "{b1,b2} \ Field r" unfolding Field_bsqr by auto + hence "(b1,?n) \ r \ (b2,?n) \ r" + using Well by (simp add: wo_rel.max2_greater) + } + ultimately have "(b1,?m) \ r \ (b2,?m) \ r" + using Trans trans_def[of r] by blast + hence "(b1,b2) \ (under r ?m) \ (under r ?m)" unfolding under_def by simp} + thus "underS ?r' (a1,a2) \ (under r ?m) \ (under r ?m)" by auto + qed + moreover have "wo_rel.ofilter r (under r ?m)" + using Well by (simp add: wo_rel.under_ofilter) + moreover have "under r ?m < Field r" + using NE under_Field[of r ?m] by blast + ultimately show ?thesis by blast +qed + +definition Func where +"Func A B = {f . (\ a \ A. f a \ B) \ (\ a. a \ A \ f a = undefined)}" + +lemma Func_empty: +"Func {} B = {\x. undefined}" +unfolding Func_def by auto + +lemma Func_elim: +assumes "g \ Func A B" and "a \ A" +shows "\ b. b \ B \ g a = b" +using assms unfolding Func_def by (cases "g a = undefined") auto + +definition curr where +"curr A f \ \ a. if a \ A then \b. f (a,b) else undefined" + +lemma curr_in: +assumes f: "f \ Func (A <*> B) C" +shows "curr A f \ Func A (Func B C)" +using assms unfolding curr_def Func_def by auto + +lemma curr_inj: +assumes "f1 \ Func (A <*> B) C" and "f2 \ Func (A <*> B) C" +shows "curr A f1 = curr A f2 \ f1 = f2" +proof safe + assume c: "curr A f1 = curr A f2" + show "f1 = f2" + proof (rule ext, clarify) + fix a b show "f1 (a, b) = f2 (a, b)" + proof (cases "(a,b) \ A <*> B") + case False + thus ?thesis using assms unfolding Func_def by auto + next + case True hence a: "a \ A" and b: "b \ B" by auto + thus ?thesis + using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp + qed + qed +qed + +lemma curr_surj: +assumes "g \ Func A (Func B C)" +shows "\ f \ Func (A <*> B) C. curr A f = g" +proof + let ?f = "\ ab. if fst ab \ A \ snd ab \ B then g (fst ab) (snd ab) else undefined" + show "curr A ?f = g" + proof (rule ext) + fix a show "curr A ?f a = g a" + proof (cases "a \ A") + case False + hence "g a = undefined" using assms unfolding Func_def by auto + thus ?thesis unfolding curr_def using False by simp + next + case True + obtain g1 where "g1 \ Func B C" and "g a = g1" + using assms using Func_elim[OF assms True] by blast + thus ?thesis using True unfolding Func_def curr_def by auto + qed + qed + show "?f \ Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto +qed + +lemma bij_betw_curr: +"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))" +unfolding bij_betw_def inj_on_def image_def +apply (intro impI conjI ballI) +apply (erule curr_inj[THEN iffD1], assumption+) +apply auto +apply (erule curr_in) +using curr_surj by blast + +definition Func_map where +"Func_map B2 f1 f2 g b2 \ if b2 \ B2 then f1 (g (f2 b2)) else undefined" + +lemma Func_map: +assumes g: "g \ Func A2 A1" and f1: "f1 ` A1 \ B1" and f2: "f2 ` B2 \ A2" +shows "Func_map B2 f1 f2 g \ Func B2 B1" +using assms unfolding Func_def Func_map_def mem_Collect_eq by auto + +lemma Func_non_emp: +assumes "B \ {}" +shows "Func A B \ {}" +proof- + obtain b where b: "b \ B" using assms by auto + hence "(\ a. if a \ A then b else undefined) \ Func A B" unfolding Func_def by auto + thus ?thesis by blast +qed + +lemma Func_is_emp: +"Func A B = {} \ A \ {} \ B = {}" (is "?L \ ?R") +proof + assume L: ?L + moreover {assume "A = {}" hence False using L Func_empty by auto} + moreover {assume "B \ {}" hence False using L Func_non_emp[of B A] by simp } + ultimately show ?R by blast +next + assume R: ?R + moreover + {fix f assume "f \ Func A B" + moreover obtain a where "a \ A" using R by blast + ultimately obtain b where "b \ B" unfolding Func_def by blast + with R have False by blast + } + thus ?L by blast +qed + +lemma Func_map_surj: +assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \ A2" +and B2A2: "B2 = {} \ A2 = {}" +shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1" +proof(cases "B2 = {}") + case True + thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def) +next + case False note B2 = False + show ?thesis + proof safe + fix h assume h: "h \ Func B2 B1" + def j1 \ "inv_into A1 f1" + have "\ a2 \ f2 ` B2. \ b2. b2 \ B2 \ f2 b2 = a2" by blast + then obtain k where k: "\ a2 \ f2 ` B2. k a2 \ B2 \ f2 (k a2) = a2" + by atomize_elim (rule bchoice) + {fix b2 assume b2: "b2 \ B2" + hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto + moreover have "k (f2 b2) \ B2" using b2 A2(2) k by auto + ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast + } note kk = this + obtain b22 where b22: "b22 \ B2" using B2 by auto + def j2 \ "\ a2. if a2 \ f2 ` B2 then k a2 else b22" + have j2A2: "j2 ` A2 \ B2" unfolding j2_def using k b22 by auto + have j2: "\ b2. b2 \ B2 \ j2 (f2 b2) = b2" + using kk unfolding j2_def by auto + def g \ "Func_map A2 j1 j2 h" + have "Func_map B2 f1 f2 g = h" + proof (rule ext) + fix b2 show "Func_map B2 f1 f2 g b2 = h b2" + proof(cases "b2 \ B2") + case True + show ?thesis + proof (cases "h b2 = undefined") + case True + hence b1: "h b2 \ f1 ` A1" using h `b2 \ B2` unfolding B1 Func_def by auto + show ?thesis using A2 f_inv_into_f[OF b1] + unfolding True g_def Func_map_def j1_def j2[OF `b2 \ B2`] by auto + qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def, + auto intro: f_inv_into_f) + qed(insert h, unfold Func_def Func_map_def, auto) + qed + moreover have "g \ Func A2 A1" unfolding g_def apply(rule Func_map[OF h]) + using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+ + ultimately show "h \ Func_map B2 f1 f2 ` Func A2 A1" + unfolding Func_map_def[abs_def] by auto + qed(insert B1 Func_map[OF _ _ A2(2)], auto) +qed + +end diff -r 3831312eb476 -r b7cab82f488e src/HOL/Cardinals/Cardinal_Arithmetic.thy --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Sep 01 16:34:38 2014 +0200 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Sep 01 16:34:39 2014 +0200 @@ -219,7 +219,7 @@ lemma czero_cexp: "Cnotzero r \ czero ^c r =o czero" by (drule Cnotzero_imp_not_empty) (simp add: cexp_def czero_def card_of_empty_ordIso) -lemma Func_singleton: +lemma Func_singleton: fixes x :: 'b and A :: "'a set" shows "|Func A {x}| =o |{x}|" proof (rule ordIso_symmetric) diff -r 3831312eb476 -r b7cab82f488e src/HOL/Cardinals/Cardinal_Order_Relation.thy --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Sep 01 16:34:38 2014 +0200 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Sep 01 16:34:39 2014 +0200 @@ -8,7 +8,7 @@ header {* Cardinal-Order Relations *} theory Cardinal_Order_Relation -imports BNF_Cardinal_Order_Relation Constructions_on_Wellorders +imports BNF_Cardinal_Order_Relation Wellorder_Constructions begin declare diff -r 3831312eb476 -r b7cab82f488e src/HOL/Cardinals/Constructions_on_Wellorders.thy --- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Mon Sep 01 16:34:38 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1077 +0,0 @@ -(* Title: HOL/Cardinals/Constructions_on_Wellorders.thy - Author: Andrei Popescu, TU Muenchen - Copyright 2012 - -Constructions on wellorders. -*) - -header {* Constructions on Wellorders *} - -theory Constructions_on_Wellorders -imports - BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union - "../Library/Cardinal_Notations" -begin - -declare - ordLeq_Well_order_simp[simp] - not_ordLeq_iff_ordLess[simp] - not_ordLess_iff_ordLeq[simp] - Func_empty[simp] - Func_is_emp[simp] - -lemma Func_emp2[simp]: "A \ {} \ Func A {} = {}" by auto - - -subsection {* Restriction to a set *} - -lemma Restr_incr2: -"r <= r' \ Restr r A <= Restr r' A" -by blast - -lemma Restr_incr: -"\r \ r'; A \ A'\ \ Restr r A \ Restr r' A'" -by blast - -lemma Restr_Int: -"Restr (Restr r A) B = Restr r (A Int B)" -by blast - -lemma 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 auto - -lemma Restr_subset2: "Restr r A \ A \ A" -by auto - -lemma wf_Restr: -"wf r \ wf(Restr r A)" -using Restr_subset by (elim wf_subset) simp - -lemma Restr_incr1: -"A \ B \ Restr r A \ Restr r B" -by blast - - -subsection {* 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) - qed -qed - -lemma 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 assms -by (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_def -by blast - -corollary ordLeq_trans: "trans ordLeq" -using trans_def[of ordLeq] ordLeq_transitive by blast - -corollary 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_def -by blast - -corollary ordIso_trans: "trans ordIso" -using trans_def[of ordIso] ordIso_transitive by blast - -corollary 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_Well_order_simp[simp]: -assumes "r Well_order r'" -using assms unfolding ordLess_def by simp - -lemma ordIso_Well_order_simp[simp]: -assumes "r =o r'" -shows "Well_order r \ Well_order r'" -using assms unfolding ordIso_def by simp - -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 r' r =o r'" -unfolding ordLess_def ordIso_def -using assms embedS_or_iso[of r r'] by auto - -corollary ordLeq_ordLess_Un_ordIso: -"ordLeq = ordLess \ ordIso" -by (auto simp add: ordLeq_iff_ordLess_or_ordIso) - -lemma not_ordLeq_ordLess: -"r \o r' \ \ r' r r' 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) -qed - -corollary 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 auto - -lemma Un_dir_image: -"dir_image (r1 \ r2) f = (dir_image r1 f) \ (dir_image r2 f)" -unfolding dir_image_def by auto - -lemma 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 auto -next - 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 - qed -qed - -(* More facts on ordinal sum: *) - -lemma 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 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) -qed - -corollary 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_order -unfolding ordLeq_def by blast - -lemma 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 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 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 blast -qed - - -subsection {* 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 auto -qed - -lemma omax_isOmax: -assumes "finite R" and "R \ {}" and "\ r \ R. Well_order r" -shows "isOmax R (omax R)" -unfolding omax_def using assms -by(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 blast - -lemma 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 auto - -lemma 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 blast - -lemma 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 auto -qed - -lemma omax_ordLess: -assumes "finite R" and "R \ {}" and *: "\ r \ R. r r \ R. Well_order r" using * unfolding ordLess_def by simp - thus ?thesis using assms omax_in by auto -qed - -lemma 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 simp -using ordLeq_transitive by blast - -lemma omax_ordLess_elim: -assumes "finite R" and "\ r \ R. Well_order r" -and "omax R R" -shows "r 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 simp -using ordLeq_transitive by blast - -lemma ordLess_omax: -assumes "finite R" and "\ r \ R. Well_order r" -and "r \ R" and "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 blast -qed - -lemma 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 Field r" -shows "g ` underS r a = underS s (g a)" -using embed_underS[OF assms] unfolding bij_betw_def by auto - -lemma bij_betw_insert: -assumes "b \ A" and "f b \ A'" and "bij_betw f A A'" -shows "bij_betw f (insert b A) (insert (f b) A')" -using notIn_Un_bij_betw[OF assms] by auto - -context wo_rel -begin - -lemma underS_induct: - assumes "\a. (\ a1. a1 \ underS a \ P a1) \ P a" - shows "P a" - by (induct rule: well_order_induct) (rule assms, simp add: underS_def) - -lemma suc_underS: -assumes B: "B \ Field r" and A: "AboveS B \ {}" and b: "b \ B" -shows "b \ underS (suc B)" -using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto - -lemma underS_supr: -assumes bA: "b \ underS (supr A)" and A: "A \ Field r" -shows "\ a \ A. b \ underS a" -proof(rule ccontr, auto) - have bb: "b \ Field r" using bA unfolding underS_def Field_def by auto - assume "\a\A. b \ underS a" - hence 0: "\a \ A. (a,b) \ r" using A bA unfolding underS_def - by simp (metis REFL in_mono max2_def max2_greater refl_on_domain) - have "(supr A, b) \ r" apply(rule supr_least[OF A bb]) using 0 by auto - thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) -qed - -lemma underS_suc: -assumes bA: "b \ underS (suc A)" and A: "A \ Field r" -shows "\ a \ A. b \ under a" -proof(rule ccontr, auto) - have bb: "b \ Field r" using bA unfolding underS_def Field_def by auto - assume "\a\A. b \ under a" - hence 0: "\a \ A. a \ underS b" using A bA unfolding underS_def - by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp) - have "(suc A, b) \ r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto - thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) -qed - -lemma (in wo_rel) in_underS_supr: -assumes j: "j \ underS i" and i: "i \ A" and A: "A \ Field r" and AA: "Above A \ {}" -shows "j \ underS (supr A)" -proof- - have "(i,supr A) \ r" using supr_greater[OF A AA i] . - thus ?thesis using j unfolding underS_def - by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD) -qed - -lemma inj_on_Field: -assumes A: "A \ Field r" and f: "\ a b. \a \ A; b \ A; a \ underS b\ \ f a \ f b" -shows "inj_on f A" -unfolding inj_on_def proof safe - fix a b assume a: "a \ A" and b: "b \ A" and fab: "f a = f b" - {assume "a \ underS b" - hence False using f[OF a b] fab by auto - } - moreover - {assume "b \ underS a" - hence False using f[OF b a] fab by auto - } - ultimately show "a = b" using TOTALS A a b unfolding underS_def by auto -qed - -lemma in_notinI: -assumes "(j,i) \ r \ j = i" and "i \ Field r" and "j \ Field r" -shows "(i,j) \ r" by (metis assms max2_def max2_greater_among) - -lemma ofilter_init_seg_of: -assumes "ofilter F" -shows "Restr r F initial_segment_of r" -using assms unfolding ofilter_def init_seg_of_def under_def by auto - -lemma underS_init_seg_of_Collect: -assumes "\j1 j2. \j2 \ underS i; (j1, j2) \ r\ \ R j1 initial_segment_of R j2" -shows "{R j |j. j \ underS i} \ Chains init_seg_of" -unfolding Chains_def proof safe - fix j ja assume jS: "j \ underS i" and jaS: "ja \ underS i" - and init: "(R ja, R j) \ init_seg_of" - hence jja: "{j,ja} \ Field r" and j: "j \ Field r" and ja: "ja \ Field r" - and jjai: "(j,i) \ r" "(ja,i) \ r" - and i: "i \ {j,ja}" unfolding Field_def underS_def by auto - have jj: "(j,j) \ r" and jaja: "(ja,ja) \ r" using j ja by (metis in_notinI)+ - show "R j initial_segment_of R ja" - using jja init jjai i - by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: underS_def) -qed - -lemma (in wo_rel) Field_init_seg_of_Collect: -assumes "\j1 j2. \j2 \ Field r; (j1, j2) \ r\ \ R j1 initial_segment_of R j2" -shows "{R j |j. j \ Field r} \ Chains init_seg_of" -unfolding Chains_def proof safe - fix j ja assume jS: "j \ Field r" and jaS: "ja \ Field r" - and init: "(R ja, R j) \ init_seg_of" - hence jja: "{j,ja} \ Field r" and j: "j \ Field r" and ja: "ja \ Field r" - unfolding Field_def underS_def by auto - have jj: "(j,j) \ r" and jaja: "(ja,ja) \ r" using j ja by (metis in_notinI)+ - show "R j initial_segment_of R ja" - using jja init - by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: Field_def) -qed - -subsubsection {* Successor and limit elements of an ordinal *} - -definition "succ i \ suc {i}" - -definition "isSucc i \ \ j. aboveS j \ {} \ i = succ j" - -definition "zero = minim (Field r)" - -definition "isLim i \ \ isSucc i" - -lemma zero_smallest[simp]: -assumes "j \ Field r" shows "(zero, j) \ r" -unfolding zero_def -by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS) - -lemma zero_in_Field: assumes "Field r \ {}" shows "zero \ Field r" -using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def) - -lemma leq_zero_imp[simp]: -"(x, zero) \ r \ x = zero" -by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest) - -lemma leq_zero[simp]: -assumes "Field r \ {}" shows "(x, zero) \ r \ x = zero" -using zero_in_Field[OF assms] in_notinI[of x zero] by auto - -lemma under_zero[simp]: -assumes "Field r \ {}" shows "under zero = {zero}" -using assms unfolding under_def by auto - -lemma underS_zero[simp,intro]: "underS zero = {}" -unfolding underS_def by auto - -lemma isSucc_succ: "aboveS i \ {} \ isSucc (succ i)" -unfolding isSucc_def succ_def by auto - -lemma succ_in_diff: -assumes "aboveS i \ {}" shows "(i,succ i) \ r \ succ i \ i" -using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto - -lemmas succ_in[simp] = succ_in_diff[THEN conjunct1] -lemmas succ_diff[simp] = succ_in_diff[THEN conjunct2] - -lemma succ_in_Field[simp]: -assumes "aboveS i \ {}" shows "succ i \ Field r" -using succ_in[OF assms] unfolding Field_def by auto - -lemma succ_not_in: -assumes "aboveS i \ {}" shows "(succ i, i) \ r" -proof - assume 1: "(succ i, i) \ r" - hence "succ i \ Field r \ i \ Field r" unfolding Field_def by auto - hence "(i, succ i) \ r \ succ i \ i" using assms by auto - thus False using 1 by (metis ANTISYM antisymD) -qed - -lemma not_isSucc_zero: "\ isSucc zero" -proof - assume "isSucc zero" - moreover - then obtain i where "aboveS i \ {}" and 1: "minim (Field r) = succ i" - unfolding isSucc_def zero_def by auto - hence "succ i \ Field r" by auto - ultimately show False by (metis REFL isSucc_def minim_least refl_on_domain - subset_refl succ_in succ_not_in zero_def) -qed - -lemma isLim_zero[simp]: "isLim zero" - by (metis isLim_def not_isSucc_zero) - -lemma succ_smallest: -assumes "(i,j) \ r" and "i \ j" -shows "(succ i, j) \ r" -unfolding succ_def apply(rule suc_least) -using assms unfolding Field_def by auto - -lemma isLim_supr: -assumes f: "i \ Field r" and l: "isLim i" -shows "i = supr (underS i)" -proof(rule equals_supr) - fix j assume j: "j \ Field r" and 1: "\ j'. j' \ underS i \ (j',j) \ r" - show "(i,j) \ r" proof(intro in_notinI[OF _ f j], safe) - assume ji: "(j,i) \ r" "j \ i" - hence a: "aboveS j \ {}" unfolding aboveS_def by auto - hence "i \ succ j" using l unfolding isLim_def isSucc_def by auto - moreover have "(succ j, i) \ r" using succ_smallest[OF ji] by auto - ultimately have "succ j \ underS i" unfolding underS_def by auto - hence "(succ j, j) \ r" using 1 by auto - thus False using succ_not_in[OF a] by simp - qed -qed(insert f, unfold underS_def Field_def, auto) - -definition "pred i \ SOME j. j \ Field r \ aboveS j \ {} \ succ j = i" - -lemma pred_Field_succ: -assumes "isSucc i" shows "pred i \ Field r \ aboveS (pred i) \ {} \ succ (pred i) = i" -proof- - obtain j where a: "aboveS j \ {}" and i: "i = succ j" using assms unfolding isSucc_def by auto - have 1: "j \ Field r" "j \ i" unfolding Field_def i - using succ_diff[OF a] a unfolding aboveS_def by auto - show ?thesis unfolding pred_def apply(rule someI_ex) using 1 i a by auto -qed - -lemmas pred_Field[simp] = pred_Field_succ[THEN conjunct1] -lemmas aboveS_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct1] -lemmas succ_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct2] - -lemma isSucc_pred_in: -assumes "isSucc i" shows "(pred i, i) \ r" -proof- - def j \ "pred i" - have i: "i = succ j" using assms unfolding j_def by simp - have a: "aboveS j \ {}" unfolding j_def using assms by auto - show ?thesis unfolding j_def[symmetric] unfolding i using succ_in[OF a] . -qed - -lemma isSucc_pred_diff: -assumes "isSucc i" shows "pred i \ i" -by (metis aboveS_pred assms succ_diff succ_pred) - -(* todo: pred maximal, pred injective? *) - -lemma succ_inj[simp]: -assumes "aboveS i \ {}" and "aboveS j \ {}" -shows "succ i = succ j \ i = j" -proof safe - assume s: "succ i = succ j" - {assume "i \ j" and "(i,j) \ r" - hence "(succ i, j) \ r" using assms by (metis succ_smallest) - hence False using s assms by (metis succ_not_in) - } - moreover - {assume "i \ j" and "(j,i) \ r" - hence "(succ j, i) \ r" using assms by (metis succ_smallest) - hence False using s assms by (metis succ_not_in) - } - ultimately show "i = j" by (metis TOTALS WELL assms(1) assms(2) succ_in_diff well_order_on_domain) -qed - -lemma pred_succ[simp]: -assumes "aboveS j \ {}" shows "pred (succ j) = j" -unfolding pred_def apply(rule some_equality) -using assms apply(force simp: Field_def aboveS_def) -by (metis assms succ_inj) - -lemma less_succ[simp]: -assumes "aboveS i \ {}" -shows "(j, succ i) \ r \ (j,i) \ r \ j = succ i" -apply safe - apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff) - apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD) - apply (metis assms in_notinI succ_in_Field) -done - -lemma underS_succ[simp]: -assumes "aboveS i \ {}" -shows "underS (succ i) = under i" -unfolding underS_def under_def by (auto simp: assms succ_not_in) - -lemma succ_mono: -assumes "aboveS j \ {}" and "(i,j) \ r" -shows "(succ i, succ j) \ r" -by (metis (full_types) assms less_succ succ_smallest) - -lemma under_succ[simp]: -assumes "aboveS i \ {}" -shows "under (succ i) = insert (succ i) (under i)" -using less_succ[OF assms] unfolding under_def by auto - -definition mergeSL :: "('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ ('a \ 'b) \ 'a \ 'b" -where -"mergeSL S L f i \ - if isSucc i then S (pred i) (f (pred i)) - else L f i" - - -subsubsection {* Well-order recursion with (zero), succesor, and limit *} - -definition worecSL :: "('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" -where "worecSL S L \ worec (mergeSL S L)" - -definition "adm_woL L \ \f g i. isLim i \ (\j\underS i. f j = g j) \ L f i = L g i" - -lemma mergeSL: -assumes "adm_woL L" shows "adm_wo (mergeSL S L)" -unfolding adm_wo_def proof safe - fix f g :: "'a => 'b" and i :: 'a - assume 1: "\j\underS i. f j = g j" - show "mergeSL S L f i = mergeSL S L g i" - proof(cases "isSucc i") - case True - hence "pred i \ underS i" unfolding underS_def using isSucc_pred_in isSucc_pred_diff by auto - thus ?thesis using True 1 unfolding mergeSL_def by auto - next - case False hence "isLim i" unfolding isLim_def by auto - thus ?thesis using assms False 1 unfolding mergeSL_def adm_woL_def by auto - qed -qed - -lemma worec_fixpoint1: "adm_wo H \ worec H i = H (worec H) i" -by (metis worec_fixpoint) - -lemma worecSL_isSucc: -assumes a: "adm_woL L" and i: "isSucc i" -shows "worecSL S L i = S (pred i) (worecSL S L (pred i))" -proof- - let ?H = "mergeSL S L" - have "worecSL S L i = ?H (worec ?H) i" - unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] . - also have "... = S (pred i) (worecSL S L (pred i))" - unfolding worecSL_def mergeSL_def using i by simp - finally show ?thesis . -qed - -lemma worecSL_succ: -assumes a: "adm_woL L" and i: "aboveS j \ {}" -shows "worecSL S L (succ j) = S j (worecSL S L j)" -proof- - def i \ "succ j" - have i: "isSucc i" by (metis i i_def isSucc_succ) - have ij: "j = pred i" unfolding i_def using assms by simp - have 0: "succ (pred i) = i" using i by simp - show ?thesis unfolding ij using worecSL_isSucc[OF a i] unfolding 0 . -qed - -lemma worecSL_isLim: -assumes a: "adm_woL L" and i: "isLim i" -shows "worecSL S L i = L (worecSL S L) i" -proof- - let ?H = "mergeSL S L" - have "worecSL S L i = ?H (worec ?H) i" - unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] . - also have "... = L (worecSL S L) i" - using i unfolding worecSL_def mergeSL_def isLim_def by simp - finally show ?thesis . -qed - -definition worecZSL :: "'b \ ('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" -where "worecZSL Z S L \ worecSL S (\ f a. if a = zero then Z else L f a)" - -lemma worecZSL_zero: -assumes a: "adm_woL L" -shows "worecZSL Z S L zero = Z" -proof- - let ?L = "\ f a. if a = zero then Z else L f a" - have "worecZSL Z S L zero = ?L (worecZSL Z S L) zero" - unfolding worecZSL_def apply(rule worecSL_isLim) - using assms unfolding adm_woL_def by auto - also have "... = Z" by simp - finally show ?thesis . -qed - -lemma worecZSL_succ: -assumes a: "adm_woL L" and i: "aboveS j \ {}" -shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)" -unfolding worecZSL_def apply(rule worecSL_succ) -using assms unfolding adm_woL_def by auto - -lemma worecZSL_isLim: -assumes a: "adm_woL L" and "isLim i" and "i \ zero" -shows "worecZSL Z S L i = L (worecZSL Z S L) i" -proof- - let ?L = "\ f a. if a = zero then Z else L f a" - have "worecZSL Z S L i = ?L (worecZSL Z S L) i" - unfolding worecZSL_def apply(rule worecSL_isLim) - using assms unfolding adm_woL_def by auto - also have "... = L (worecZSL Z S L) i" using assms by simp - finally show ?thesis . -qed - - -subsubsection {* Well-order succ-lim induction *} - -lemma ord_cases: -obtains j where "i = succ j" and "aboveS j \ {}" | "isLim i" -by (metis isLim_def isSucc_def) - -lemma well_order_inductSL[case_names Suc Lim]: -assumes SUCC: "\i. \aboveS i \ {}; P i\ \ P (succ i)" and -LIM: "\i. \isLim i; \j. j \ underS i \ P j\ \ P i" -shows "P i" -proof(induction rule: well_order_induct) - fix i assume 0: "\j. j \ i \ (j, i) \ r \ P j" - show "P i" proof(cases i rule: ord_cases) - fix j assume i: "i = succ j" and j: "aboveS j \ {}" - hence "j \ i \ (j, i) \ r" by (metis succ_diff succ_in) - hence 1: "P j" using 0 by simp - show "P i" unfolding i apply(rule SUCC) using 1 j by auto - qed(insert 0 LIM, unfold underS_def, auto) -qed - -lemma well_order_inductZSL[case_names Zero Suc Lim]: -assumes ZERO: "P zero" -and SUCC: "\i. \aboveS i \ {}; P i\ \ P (succ i)" and -LIM: "\i. \isLim i; i \ zero; \j. j \ underS i \ P j\ \ P i" -shows "P i" -apply(induction rule: well_order_inductSL) using assms by auto - -(* Succesor and limit ordinals *) -definition "isSuccOrd \ \ j \ Field r. \ i \ Field r. (i,j) \ r" -definition "isLimOrd \ \ isSuccOrd" - -lemma isLimOrd_succ: -assumes isLimOrd and "i \ Field r" -shows "succ i \ Field r" -using assms unfolding isLimOrd_def isSuccOrd_def -by (metis REFL in_notinI refl_on_domain succ_smallest) - -lemma isLimOrd_aboveS: -assumes l: isLimOrd and i: "i \ Field r" -shows "aboveS i \ {}" -proof- - obtain j where "j \ Field r" and "(j,i) \ r" - using assms unfolding isLimOrd_def isSuccOrd_def by auto - hence "(i,j) \ r \ j \ i" by (metis i max2_def max2_greater) - thus ?thesis unfolding aboveS_def by auto -qed - -lemma succ_aboveS_isLimOrd: -assumes "\ i \ Field r. aboveS i \ {} \ succ i \ Field r" -shows isLimOrd -unfolding isLimOrd_def isSuccOrd_def proof safe - fix j assume j: "j \ Field r" "\i\Field r. (i, j) \ r" - hence "(succ j, j) \ r" using assms by auto - moreover have "aboveS j \ {}" using assms j unfolding aboveS_def by auto - ultimately show False by (metis succ_not_in) -qed - -lemma isLim_iff: -assumes l: "isLim i" and j: "j \ underS i" -shows "\ k. k \ underS i \ j \ underS k" -proof- - have a: "aboveS j \ {}" using j unfolding underS_def aboveS_def by auto - show ?thesis apply(rule exI[of _ "succ j"]) apply safe - using assms a unfolding underS_def isLim_def - apply (metis (lifting, full_types) isSucc_def mem_Collect_eq succ_smallest) - by (metis (lifting, full_types) a mem_Collect_eq succ_diff succ_in) -qed - -end (* context wo_rel *) - -abbreviation "zero \ wo_rel.zero" -abbreviation "succ \ wo_rel.succ" -abbreviation "pred \ wo_rel.pred" -abbreviation "isSucc \ wo_rel.isSucc" -abbreviation "isLim \ wo_rel.isLim" -abbreviation "isLimOrd \ wo_rel.isLimOrd" -abbreviation "isSuccOrd \ wo_rel.isSuccOrd" -abbreviation "adm_woL \ wo_rel.adm_woL" -abbreviation "worecSL \ wo_rel.worecSL" -abbreviation "worecZSL \ wo_rel.worecZSL" - - -subsection {* Projections of wellorders *} - -definition "oproj r s f \ Field s \ f ` (Field r) \ compat r s f" - -lemma oproj_in: -assumes "oproj r s f" and "(a,a') \ r" -shows "(f a, f a') \ s" -using assms unfolding oproj_def compat_def by auto - -lemma oproj_Field: -assumes f: "oproj r s f" and a: "a \ Field r" -shows "f a \ Field s" -using oproj_in[OF f] a unfolding Field_def by auto - -lemma oproj_Field2: -assumes f: "oproj r s f" and a: "b \ Field s" -shows "\ a \ Field r. f a = b" -using assms unfolding oproj_def by auto - -lemma oproj_under: -assumes f: "oproj r s f" and a: "a \ under r a'" -shows "f a \ under s (f a')" -using oproj_in[OF f] a unfolding under_def by auto - -(* An ordinal is embedded in another whenever it is embedded as an order -(not necessarily as initial segment):*) -theorem embedI: -assumes r: "Well_order r" and s: "Well_order s" -and f: "\ a. a \ Field r \ f a \ Field s \ f ` underS r a \ underS s (f a)" -shows "\ g. embed r s g" -proof- - interpret r!: wo_rel r by unfold_locales (rule r) - interpret s!: wo_rel s by unfold_locales (rule s) - let ?G = "\ g a. suc s (g ` underS r a)" - def g \ "worec r ?G" - have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto - (* *) - {fix a assume "a \ Field r" - hence "bij_betw g (under r a) (under s (g a)) \ - g a \ under s (f a)" - proof(induction a rule: r.underS_induct) - case (1 a) - hence a: "a \ Field r" - and IH1a: "\ a1. a1 \ underS r a \ inj_on g (under r a1)" - and IH1b: "\ a1. a1 \ underS r a \ g ` under r a1 = under s (g a1)" - and IH2: "\ a1. a1 \ underS r a \ g a1 \ under s (f a1)" - unfolding underS_def Field_def bij_betw_def by auto - have fa: "f a \ Field s" using f[OF a] by auto - have g: "g a = suc s (g ` underS r a)" - using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp - have A0: "g ` underS r a \ Field s" - using IH1b by (metis IH2 image_subsetI in_mono under_Field) - {fix a1 assume a1: "a1 \ underS r a" - from IH2[OF this] have "g a1 \ under s (f a1)" . - moreover have "f a1 \ underS s (f a)" using f[OF a] a1 by auto - ultimately have "g a1 \ underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans) - } - hence "f a \ AboveS s (g ` underS r a)" unfolding AboveS_def - using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def) - hence A: "AboveS s (g ` underS r a) \ {}" by auto - have B: "\ a1. a1 \ underS r a \ g a1 \ underS s (g a)" - unfolding g apply(rule s.suc_underS[OF A0 A]) by auto - {fix a1 a2 assume a2: "a2 \ underS r a" and 1: "a1 \ underS r a2" - hence a12: "{a1,a2} \ under r a2" and "a1 \ a2" using r.REFL a - unfolding underS_def under_def refl_on_def Field_def by auto - hence "g a1 \ g a2" using IH1a[OF a2] unfolding inj_on_def by auto - hence "g a1 \ underS s (g a2)" using IH1b[OF a2] a12 - unfolding underS_def under_def by auto - } note C = this - have ga: "g a \ Field s" unfolding g using s.suc_inField[OF A0 A] . - have aa: "a \ under r a" - using a r.REFL unfolding under_def underS_def refl_on_def by auto - show ?case proof safe - show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe - show "inj_on g (under r a)" proof(rule r.inj_on_Field) - fix a1 a2 assume "a1 \ under r a" and a2: "a2 \ under r a" and a1: "a1 \ underS r a2" - hence a22: "a2 \ under r a2" and a12: "a1 \ under r a2" "a1 \ a2" - using a r.REFL unfolding under_def underS_def refl_on_def by auto - show "g a1 \ g a2" - proof(cases "a2 = a") - case False hence "a2 \ underS r a" - using a2 unfolding underS_def under_def by auto - from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto - qed(insert B a1, unfold underS_def, auto) - qed(unfold under_def Field_def, auto) - next - fix a1 assume a1: "a1 \ under r a" - show "g a1 \ under s (g a)" - proof(cases "a1 = a") - case True thus ?thesis - using ga s.REFL unfolding refl_on_def under_def by auto - next - case False - hence a1: "a1 \ underS r a" using a1 unfolding underS_def under_def by auto - thus ?thesis using B unfolding underS_def under_def by auto - qed - next - fix b1 assume b1: "b1 \ under s (g a)" - show "b1 \ g ` under r a" - proof(cases "b1 = g a") - case True thus ?thesis using aa by auto - next - case False - hence "b1 \ underS s (g a)" using b1 unfolding underS_def under_def by auto - from s.underS_suc[OF this[unfolded g] A0] - obtain a1 where a1: "a1 \ underS r a" and b1: "b1 \ under s (g a1)" by auto - obtain a2 where "a2 \ under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto - hence "a2 \ under r a" using a1 - by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans) - thus ?thesis using b1 by auto - qed - qed - next - have "(g a, f a) \ s" unfolding g proof(rule s.suc_least[OF A0]) - fix b1 assume "b1 \ g ` underS r a" - then obtain a1 where a1: "b1 = g a1" and a1: "a1 \ underS r a" by auto - hence "b1 \ underS s (f a)" - using a by (metis `\a1. a1 \ underS r a \ g a1 \ underS s (f a)`) - thus "f a \ b1 \ (b1, f a) \ s" unfolding underS_def by auto - qed(insert fa, auto) - thus "g a \ under s (f a)" unfolding under_def by auto - qed - qed - } - thus ?thesis unfolding embed_def by auto -qed - -corollary ordLeq_def2: - "r \o s \ Well_order r \ Well_order s \ - (\ f. \ a \ Field r. f a \ Field s \ f ` underS r a \ underS s (f a))" -using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s] -unfolding ordLeq_def by fast - -lemma iso_oproj: - assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f" - shows "oproj r s f" -using assms unfolding oproj_def -by (subst (asm) iso_iff3) (auto simp: bij_betw_def) - -theorem oproj_embed: -assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" -shows "\ g. embed s r g" -proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe) - fix b assume "b \ Field s" - thus "inv_into (Field r) f b \ Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into) -next - fix a b assume "b \ Field s" "a \ b" "(a, b) \ s" - "inv_into (Field r) f a = inv_into (Field r) f b" - with f show False by (auto dest!: inv_into_injective simp: Field_def oproj_def) -next - fix a b assume *: "b \ Field s" "a \ b" "(a, b) \ s" - { assume "(inv_into (Field r) f a, inv_into (Field r) f b) \ r" - moreover - from *(3) have "a \ Field s" unfolding Field_def by auto - with *(1,2) have - "inv_into (Field r) f a \ Field r" "inv_into (Field r) f b \ Field r" - "inv_into (Field r) f a \ inv_into (Field r) f b" - by (auto dest!: oproj_Field2[OF f] inv_into_injective intro!: inv_into_into) - ultimately have "(inv_into (Field r) f b, inv_into (Field r) f a) \ r" - using r by (auto simp: well_order_on_def linear_order_on_def total_on_def) - with f[unfolded oproj_def compat_def] *(1) `a \ Field s` - f_inv_into_f[of b f "Field r"] f_inv_into_f[of a f "Field r"] - have "(b, a) \ s" by (metis in_mono) - with *(2,3) s have False - by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def antisym_def) - } thus "(inv_into (Field r) f a, inv_into (Field r) f b) \ r" by blast -qed - -corollary oproj_ordLeq: -assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" -shows "s \o r" -using oproj_embed[OF assms] r s unfolding ordLeq_def by auto - -end diff -r 3831312eb476 -r b7cab82f488e src/HOL/Cardinals/Order_Union.thy --- a/src/HOL/Cardinals/Order_Union.thy Mon Sep 01 16:34:38 2014 +0200 +++ b/src/HOL/Cardinals/Order_Union.thy Mon Sep 01 16:34:39 2014 +0200 @@ -78,7 +78,7 @@ assumes FLD: "Field r Int Field r' = {}" and REFL: "Refl r" and REFL': "Refl r'" shows "Refl (r Osum r')" -using assms +using assms unfolding refl_on_def Field_Osum unfolding Osum_def by blast lemma Osum_trans: diff -r 3831312eb476 -r b7cab82f488e src/HOL/Cardinals/Ordinal_Arithmetic.thy --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Mon Sep 01 16:34:38 2014 +0200 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Mon Sep 01 16:34:39 2014 +0200 @@ -8,12 +8,12 @@ header {* Ordinal Arithmetic *} theory Ordinal_Arithmetic -imports Constructions_on_Wellorders +imports Wellorder_Constructions begin definition osum :: "'a rel \ 'b rel \ ('a + 'b) rel" (infixr "+o" 70) where - "r +o r' = map_prod Inl Inl ` r \ map_prod Inr Inr ` r' \ + "r +o r' = map_prod Inl Inl ` r \ map_prod Inr Inr ` r' \ {(Inl a, Inr a') | a a' . a \ Field r \ a' \ Field r'}" lemma Field_osum: "Field(r +o r') = Inl ` Field r \ Inr ` Field r'" @@ -175,7 +175,7 @@ lemma oprod_Refl:"\Refl r; Refl r'\ \ Refl (r *o r')" unfolding refl_on_def Field_oprod unfolding oprod_def by auto -lemma oprod_trans: +lemma oprod_trans: assumes "trans r" "trans r'" "antisym r" "antisym r'" shows "trans (r *o r')" proof(unfold trans_def, safe) @@ -309,7 +309,7 @@ from assms(3) have r': "Field r' \ {}" unfolding Field_def by auto have minim[simp]: "minim r' (Field r') \ Field r'" using wo_rel.minim_inField[unfolded wo_rel_def, OF WELL' _ r'] by auto - { fix b + { fix b assume "(b, minim r' (Field r')) \ r'" moreover hence "b \ Field r'" unfolding Field_def by auto hence "(minim r' (Field r'), b) \ r'" @@ -390,7 +390,7 @@ unfolding isMaxim_def using antisymD[OF ANTISYM, of x y] by auto lemma maxim_isMaxim: "\finite A; A \ {}; A \ Field r\ \ isMaxim A (maxim A)" -unfolding maxim_def +unfolding maxim_def proof (rule theI', rule ex_ex1I[OF _ isMaxim_unique, rotated], assumption+, induct A rule: finite_induct) case (insert x A) @@ -494,7 +494,7 @@ locale wo_rel2 = fixes r s - assumes rWELL: "Well_order r" + assumes rWELL: "Well_order r" and sWELL: "Well_order s" begin @@ -539,7 +539,7 @@ lemma max_fun_diff_max2: assumes ineq: "s.max_fun_diff f g = s.max_fun_diff g h \ - f (s.max_fun_diff f g) \ h (s.max_fun_diff g h)" and + f (s.max_fun_diff f g) \ h (s.max_fun_diff g h)" and fg: "f \ g" and gh: "g \ h" and fh: "f \ h" and f: "f \ FINFUNC" and g: "g \ FINFUNC" and h: "h \ FINFUNC" shows "s.max_fun_diff f h = s.max2 (s.max_fun_diff f g) (s.max_fun_diff g h)" @@ -708,7 +708,7 @@ by (auto intro: finite_subset[OF support_upd_subset]) lemma fun_upd_same_oexp: - assumes "(f, g) \ oexp" "f x = g x" "x \ Field s" "y \ Field r" + assumes "(f, g) \ oexp" "f x = g x" "x \ Field s" "y \ Field r" shows "(f(x := y), g(x := y)) \ oexp" proof - from assms(1) fun_upd_FINFUNC[OF _ assms(3,4)] have fg: "f(x := y) \ FINFUNC" "g(x := y) \ FINFUNC" @@ -829,7 +829,7 @@ thus ?thesis proof (cases "s.maxim (SUPP f) = z \ f z = x0") case True - with f have "f(z := r.zero) \ G" unfolding G_def by blast + with f have "f(z := r.zero) \ G" unfolding G_def by blast with g0(2) f0z have "(f0(z := r.zero), f(z := r.zero)) \ oexp" by auto hence "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \ oexp" by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp @@ -922,10 +922,10 @@ unfolding ozero_def by simp lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})" - unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def + unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def by (auto dest: well_order_on_domain) -lemma ozero_ordLeq: +lemma ozero_ordLeq: assumes "Well_order r" shows "ozero \o r" using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto @@ -959,7 +959,7 @@ with f have "bij_betw ?f (Field ?L) (Field ?R)" unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto moreover from f have "compat ?L ?R ?f" - unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def + unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def by (auto simp: map_prod_imageI) ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t) thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t) @@ -977,7 +977,7 @@ with f have "bij_betw ?f (Field ?L) (Field ?R)" unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto moreover from f have "compat ?L ?R ?f" - unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def + unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def by (auto simp: map_prod_imageI) ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t) thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t) @@ -1269,7 +1269,7 @@ lemma ozero_oexp: "\ (s =o ozero) \ ozero ^o s =o ozero" unfolding oexp_def[OF ozero_Well_order s] FinFunc_def by simp (metis Func_emp2 bot.extremum_uniqueI emptyE well_order_on_domain s subrelI) - + lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R") by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s]) @@ -1490,7 +1490,7 @@ thus ?thesis unfolding ordLeq_def2 by (fast intro: oexp_Well_order r s) qed -lemma FinFunc_osum: +lemma FinFunc_osum: "fg \ FinFunc r (s +o t) = (fg o Inl \ FinFunc r s \ fg o Inr \ FinFunc r t)" (is "?L = (?R1 \ ?R2)") proof safe @@ -1696,7 +1696,7 @@ unfolding inj_on_def FinFunc_def Func_def Field_oprod rs.Field_oexp rev_curr_def[abs_def] by (auto simp: fun_eq_iff) metis show "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t" by (rule rev_curr_FinFunc[OF Field]) - qed + qed moreover have "compat ?L ?R rev_curr" unfolding compat_def proof safe diff -r 3831312eb476 -r b7cab82f488e src/HOL/Cardinals/README.txt --- a/src/HOL/Cardinals/README.txt Mon Sep 01 16:34:38 2014 +0200 +++ b/src/HOL/Cardinals/README.txt Mon Sep 01 16:34:39 2014 +0200 @@ -35,7 +35,7 @@ and *strict embeddings* are defined to be embeddings that are, and respectively are not, bijections. --- Constructions_on_Wellorders: +-- Wellorder_Constructions: ----- 1) Defines direct images, restrictions, disjoint unions and bounded squares of well-orders. ----- 2) Defines the relations "ordLeq", "ordLess" and "ordIso" @@ -203,7 +203,7 @@ making impossible to debug theorem instantiations. - At lemma "embed_unique": If we add the attribute "rule format" at lemma, we get an error at qed. -Theory Constructions_on_Wellorders (and BNF_Constructions_on_Wellorders): +Theory Wellorder_Constructions (and BNF_Wellorder_Constructions): - Some of the lemmas in this section are about more general kinds of relations than well-orders, but it is not clear whether they are useful in such more general contexts. - Recall that "equiv" does not have the "equiv_on" and "Equiv" versions, diff -r 3831312eb476 -r b7cab82f488e src/HOL/Cardinals/Wellorder_Constructions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Mon Sep 01 16:34:39 2014 +0200 @@ -0,0 +1,1077 @@ +(* Title: HOL/Cardinals/Wellorder_Constructions.thy + Author: Andrei Popescu, TU Muenchen + Copyright 2012 + +Constructions on wellorders. +*) + +header {* Constructions on Wellorders *} + +theory Wellorder_Constructions +imports + BNF_Wellorder_Constructions Wellorder_Embedding Order_Union + "../Library/Cardinal_Notations" +begin + +declare + ordLeq_Well_order_simp[simp] + not_ordLeq_iff_ordLess[simp] + not_ordLess_iff_ordLeq[simp] + Func_empty[simp] + Func_is_emp[simp] + +lemma Func_emp2[simp]: "A \ {} \ Func A {} = {}" by auto + + +subsection {* Restriction to a set *} + +lemma Restr_incr2: +"r <= r' \ Restr r A <= Restr r' A" +by blast + +lemma Restr_incr: +"\r \ r'; A \ A'\ \ Restr r A \ Restr r' A'" +by blast + +lemma Restr_Int: +"Restr (Restr r A) B = Restr r (A Int B)" +by blast + +lemma 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 auto + +lemma Restr_subset2: "Restr r A \ A \ A" +by auto + +lemma wf_Restr: +"wf r \ wf(Restr r A)" +using Restr_subset by (elim wf_subset) simp + +lemma Restr_incr1: +"A \ B \ Restr r A \ Restr r B" +by blast + + +subsection {* 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) + qed +qed + +lemma 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 assms +by (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_def +by blast + +corollary ordLeq_trans: "trans ordLeq" +using trans_def[of ordLeq] ordLeq_transitive by blast + +corollary 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_def +by blast + +corollary ordIso_trans: "trans ordIso" +using trans_def[of ordIso] ordIso_transitive by blast + +corollary 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_Well_order_simp[simp]: +assumes "r Well_order r'" +using assms unfolding ordLess_def by simp + +lemma ordIso_Well_order_simp[simp]: +assumes "r =o r'" +shows "Well_order r \ Well_order r'" +using assms unfolding ordIso_def by simp + +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 r' r =o r'" +unfolding ordLess_def ordIso_def +using assms embedS_or_iso[of r r'] by auto + +corollary ordLeq_ordLess_Un_ordIso: +"ordLeq = ordLess \ ordIso" +by (auto simp add: ordLeq_iff_ordLess_or_ordIso) + +lemma not_ordLeq_ordLess: +"r \o r' \ \ r' r r' 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) +qed + +corollary 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 auto + +lemma Un_dir_image: +"dir_image (r1 \ r2) f = (dir_image r1 f) \ (dir_image r2 f)" +unfolding dir_image_def by auto + +lemma 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 auto +next + 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 + qed +qed + +(* More facts on ordinal sum: *) + +lemma 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 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) +qed + +corollary 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_order +unfolding ordLeq_def by blast + +lemma 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 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 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 blast +qed + + +subsection {* 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 auto +qed + +lemma omax_isOmax: +assumes "finite R" and "R \ {}" and "\ r \ R. Well_order r" +shows "isOmax R (omax R)" +unfolding omax_def using assms +by(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 blast + +lemma 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 auto + +lemma 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 blast + +lemma 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 auto +qed + +lemma omax_ordLess: +assumes "finite R" and "R \ {}" and *: "\ r \ R. r r \ R. Well_order r" using * unfolding ordLess_def by simp + thus ?thesis using assms omax_in by auto +qed + +lemma 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 simp +using ordLeq_transitive by blast + +lemma omax_ordLess_elim: +assumes "finite R" and "\ r \ R. Well_order r" +and "omax R R" +shows "r 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 simp +using ordLeq_transitive by blast + +lemma ordLess_omax: +assumes "finite R" and "\ r \ R. Well_order r" +and "r \ R" and "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 blast +qed + +lemma 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 Field r" +shows "g ` underS r a = underS s (g a)" +using embed_underS[OF assms] unfolding bij_betw_def by auto + +lemma bij_betw_insert: +assumes "b \ A" and "f b \ A'" and "bij_betw f A A'" +shows "bij_betw f (insert b A) (insert (f b) A')" +using notIn_Un_bij_betw[OF assms] by auto + +context wo_rel +begin + +lemma underS_induct: + assumes "\a. (\ a1. a1 \ underS a \ P a1) \ P a" + shows "P a" + by (induct rule: well_order_induct) (rule assms, simp add: underS_def) + +lemma suc_underS: +assumes B: "B \ Field r" and A: "AboveS B \ {}" and b: "b \ B" +shows "b \ underS (suc B)" +using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto + +lemma underS_supr: +assumes bA: "b \ underS (supr A)" and A: "A \ Field r" +shows "\ a \ A. b \ underS a" +proof(rule ccontr, auto) + have bb: "b \ Field r" using bA unfolding underS_def Field_def by auto + assume "\a\A. b \ underS a" + hence 0: "\a \ A. (a,b) \ r" using A bA unfolding underS_def + by simp (metis REFL in_mono max2_def max2_greater refl_on_domain) + have "(supr A, b) \ r" apply(rule supr_least[OF A bb]) using 0 by auto + thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) +qed + +lemma underS_suc: +assumes bA: "b \ underS (suc A)" and A: "A \ Field r" +shows "\ a \ A. b \ under a" +proof(rule ccontr, auto) + have bb: "b \ Field r" using bA unfolding underS_def Field_def by auto + assume "\a\A. b \ under a" + hence 0: "\a \ A. a \ underS b" using A bA unfolding underS_def + by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp) + have "(suc A, b) \ r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto + thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) +qed + +lemma (in wo_rel) in_underS_supr: +assumes j: "j \ underS i" and i: "i \ A" and A: "A \ Field r" and AA: "Above A \ {}" +shows "j \ underS (supr A)" +proof- + have "(i,supr A) \ r" using supr_greater[OF A AA i] . + thus ?thesis using j unfolding underS_def + by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD) +qed + +lemma inj_on_Field: +assumes A: "A \ Field r" and f: "\ a b. \a \ A; b \ A; a \ underS b\ \ f a \ f b" +shows "inj_on f A" +unfolding inj_on_def proof safe + fix a b assume a: "a \ A" and b: "b \ A" and fab: "f a = f b" + {assume "a \ underS b" + hence False using f[OF a b] fab by auto + } + moreover + {assume "b \ underS a" + hence False using f[OF b a] fab by auto + } + ultimately show "a = b" using TOTALS A a b unfolding underS_def by auto +qed + +lemma in_notinI: +assumes "(j,i) \ r \ j = i" and "i \ Field r" and "j \ Field r" +shows "(i,j) \ r" by (metis assms max2_def max2_greater_among) + +lemma ofilter_init_seg_of: +assumes "ofilter F" +shows "Restr r F initial_segment_of r" +using assms unfolding ofilter_def init_seg_of_def under_def by auto + +lemma underS_init_seg_of_Collect: +assumes "\j1 j2. \j2 \ underS i; (j1, j2) \ r\ \ R j1 initial_segment_of R j2" +shows "{R j |j. j \ underS i} \ Chains init_seg_of" +unfolding Chains_def proof safe + fix j ja assume jS: "j \ underS i" and jaS: "ja \ underS i" + and init: "(R ja, R j) \ init_seg_of" + hence jja: "{j,ja} \ Field r" and j: "j \ Field r" and ja: "ja \ Field r" + and jjai: "(j,i) \ r" "(ja,i) \ r" + and i: "i \ {j,ja}" unfolding Field_def underS_def by auto + have jj: "(j,j) \ r" and jaja: "(ja,ja) \ r" using j ja by (metis in_notinI)+ + show "R j initial_segment_of R ja" + using jja init jjai i + by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: underS_def) +qed + +lemma (in wo_rel) Field_init_seg_of_Collect: +assumes "\j1 j2. \j2 \ Field r; (j1, j2) \ r\ \ R j1 initial_segment_of R j2" +shows "{R j |j. j \ Field r} \ Chains init_seg_of" +unfolding Chains_def proof safe + fix j ja assume jS: "j \ Field r" and jaS: "ja \ Field r" + and init: "(R ja, R j) \ init_seg_of" + hence jja: "{j,ja} \ Field r" and j: "j \ Field r" and ja: "ja \ Field r" + unfolding Field_def underS_def by auto + have jj: "(j,j) \ r" and jaja: "(ja,ja) \ r" using j ja by (metis in_notinI)+ + show "R j initial_segment_of R ja" + using jja init + by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: Field_def) +qed + +subsubsection {* Successor and limit elements of an ordinal *} + +definition "succ i \ suc {i}" + +definition "isSucc i \ \ j. aboveS j \ {} \ i = succ j" + +definition "zero = minim (Field r)" + +definition "isLim i \ \ isSucc i" + +lemma zero_smallest[simp]: +assumes "j \ Field r" shows "(zero, j) \ r" +unfolding zero_def +by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS) + +lemma zero_in_Field: assumes "Field r \ {}" shows "zero \ Field r" +using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def) + +lemma leq_zero_imp[simp]: +"(x, zero) \ r \ x = zero" +by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest) + +lemma leq_zero[simp]: +assumes "Field r \ {}" shows "(x, zero) \ r \ x = zero" +using zero_in_Field[OF assms] in_notinI[of x zero] by auto + +lemma under_zero[simp]: +assumes "Field r \ {}" shows "under zero = {zero}" +using assms unfolding under_def by auto + +lemma underS_zero[simp,intro]: "underS zero = {}" +unfolding underS_def by auto + +lemma isSucc_succ: "aboveS i \ {} \ isSucc (succ i)" +unfolding isSucc_def succ_def by auto + +lemma succ_in_diff: +assumes "aboveS i \ {}" shows "(i,succ i) \ r \ succ i \ i" +using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto + +lemmas succ_in[simp] = succ_in_diff[THEN conjunct1] +lemmas succ_diff[simp] = succ_in_diff[THEN conjunct2] + +lemma succ_in_Field[simp]: +assumes "aboveS i \ {}" shows "succ i \ Field r" +using succ_in[OF assms] unfolding Field_def by auto + +lemma succ_not_in: +assumes "aboveS i \ {}" shows "(succ i, i) \ r" +proof + assume 1: "(succ i, i) \ r" + hence "succ i \ Field r \ i \ Field r" unfolding Field_def by auto + hence "(i, succ i) \ r \ succ i \ i" using assms by auto + thus False using 1 by (metis ANTISYM antisymD) +qed + +lemma not_isSucc_zero: "\ isSucc zero" +proof + assume "isSucc zero" + moreover + then obtain i where "aboveS i \ {}" and 1: "minim (Field r) = succ i" + unfolding isSucc_def zero_def by auto + hence "succ i \ Field r" by auto + ultimately show False by (metis REFL isSucc_def minim_least refl_on_domain + subset_refl succ_in succ_not_in zero_def) +qed + +lemma isLim_zero[simp]: "isLim zero" + by (metis isLim_def not_isSucc_zero) + +lemma succ_smallest: +assumes "(i,j) \ r" and "i \ j" +shows "(succ i, j) \ r" +unfolding succ_def apply(rule suc_least) +using assms unfolding Field_def by auto + +lemma isLim_supr: +assumes f: "i \ Field r" and l: "isLim i" +shows "i = supr (underS i)" +proof(rule equals_supr) + fix j assume j: "j \ Field r" and 1: "\ j'. j' \ underS i \ (j',j) \ r" + show "(i,j) \ r" proof(intro in_notinI[OF _ f j], safe) + assume ji: "(j,i) \ r" "j \ i" + hence a: "aboveS j \ {}" unfolding aboveS_def by auto + hence "i \ succ j" using l unfolding isLim_def isSucc_def by auto + moreover have "(succ j, i) \ r" using succ_smallest[OF ji] by auto + ultimately have "succ j \ underS i" unfolding underS_def by auto + hence "(succ j, j) \ r" using 1 by auto + thus False using succ_not_in[OF a] by simp + qed +qed(insert f, unfold underS_def Field_def, auto) + +definition "pred i \ SOME j. j \ Field r \ aboveS j \ {} \ succ j = i" + +lemma pred_Field_succ: +assumes "isSucc i" shows "pred i \ Field r \ aboveS (pred i) \ {} \ succ (pred i) = i" +proof- + obtain j where a: "aboveS j \ {}" and i: "i = succ j" using assms unfolding isSucc_def by auto + have 1: "j \ Field r" "j \ i" unfolding Field_def i + using succ_diff[OF a] a unfolding aboveS_def by auto + show ?thesis unfolding pred_def apply(rule someI_ex) using 1 i a by auto +qed + +lemmas pred_Field[simp] = pred_Field_succ[THEN conjunct1] +lemmas aboveS_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct1] +lemmas succ_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct2] + +lemma isSucc_pred_in: +assumes "isSucc i" shows "(pred i, i) \ r" +proof- + def j \ "pred i" + have i: "i = succ j" using assms unfolding j_def by simp + have a: "aboveS j \ {}" unfolding j_def using assms by auto + show ?thesis unfolding j_def[symmetric] unfolding i using succ_in[OF a] . +qed + +lemma isSucc_pred_diff: +assumes "isSucc i" shows "pred i \ i" +by (metis aboveS_pred assms succ_diff succ_pred) + +(* todo: pred maximal, pred injective? *) + +lemma succ_inj[simp]: +assumes "aboveS i \ {}" and "aboveS j \ {}" +shows "succ i = succ j \ i = j" +proof safe + assume s: "succ i = succ j" + {assume "i \ j" and "(i,j) \ r" + hence "(succ i, j) \ r" using assms by (metis succ_smallest) + hence False using s assms by (metis succ_not_in) + } + moreover + {assume "i \ j" and "(j,i) \ r" + hence "(succ j, i) \ r" using assms by (metis succ_smallest) + hence False using s assms by (metis succ_not_in) + } + ultimately show "i = j" by (metis TOTALS WELL assms(1) assms(2) succ_in_diff well_order_on_domain) +qed + +lemma pred_succ[simp]: +assumes "aboveS j \ {}" shows "pred (succ j) = j" +unfolding pred_def apply(rule some_equality) +using assms apply(force simp: Field_def aboveS_def) +by (metis assms succ_inj) + +lemma less_succ[simp]: +assumes "aboveS i \ {}" +shows "(j, succ i) \ r \ (j,i) \ r \ j = succ i" +apply safe + apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff) + apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD) + apply (metis assms in_notinI succ_in_Field) +done + +lemma underS_succ[simp]: +assumes "aboveS i \ {}" +shows "underS (succ i) = under i" +unfolding underS_def under_def by (auto simp: assms succ_not_in) + +lemma succ_mono: +assumes "aboveS j \ {}" and "(i,j) \ r" +shows "(succ i, succ j) \ r" +by (metis (full_types) assms less_succ succ_smallest) + +lemma under_succ[simp]: +assumes "aboveS i \ {}" +shows "under (succ i) = insert (succ i) (under i)" +using less_succ[OF assms] unfolding under_def by auto + +definition mergeSL :: "('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ ('a \ 'b) \ 'a \ 'b" +where +"mergeSL S L f i \ + if isSucc i then S (pred i) (f (pred i)) + else L f i" + + +subsubsection {* Well-order recursion with (zero), succesor, and limit *} + +definition worecSL :: "('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" +where "worecSL S L \ worec (mergeSL S L)" + +definition "adm_woL L \ \f g i. isLim i \ (\j\underS i. f j = g j) \ L f i = L g i" + +lemma mergeSL: +assumes "adm_woL L" shows "adm_wo (mergeSL S L)" +unfolding adm_wo_def proof safe + fix f g :: "'a => 'b" and i :: 'a + assume 1: "\j\underS i. f j = g j" + show "mergeSL S L f i = mergeSL S L g i" + proof(cases "isSucc i") + case True + hence "pred i \ underS i" unfolding underS_def using isSucc_pred_in isSucc_pred_diff by auto + thus ?thesis using True 1 unfolding mergeSL_def by auto + next + case False hence "isLim i" unfolding isLim_def by auto + thus ?thesis using assms False 1 unfolding mergeSL_def adm_woL_def by auto + qed +qed + +lemma worec_fixpoint1: "adm_wo H \ worec H i = H (worec H) i" +by (metis worec_fixpoint) + +lemma worecSL_isSucc: +assumes a: "adm_woL L" and i: "isSucc i" +shows "worecSL S L i = S (pred i) (worecSL S L (pred i))" +proof- + let ?H = "mergeSL S L" + have "worecSL S L i = ?H (worec ?H) i" + unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] . + also have "... = S (pred i) (worecSL S L (pred i))" + unfolding worecSL_def mergeSL_def using i by simp + finally show ?thesis . +qed + +lemma worecSL_succ: +assumes a: "adm_woL L" and i: "aboveS j \ {}" +shows "worecSL S L (succ j) = S j (worecSL S L j)" +proof- + def i \ "succ j" + have i: "isSucc i" by (metis i i_def isSucc_succ) + have ij: "j = pred i" unfolding i_def using assms by simp + have 0: "succ (pred i) = i" using i by simp + show ?thesis unfolding ij using worecSL_isSucc[OF a i] unfolding 0 . +qed + +lemma worecSL_isLim: +assumes a: "adm_woL L" and i: "isLim i" +shows "worecSL S L i = L (worecSL S L) i" +proof- + let ?H = "mergeSL S L" + have "worecSL S L i = ?H (worec ?H) i" + unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] . + also have "... = L (worecSL S L) i" + using i unfolding worecSL_def mergeSL_def isLim_def by simp + finally show ?thesis . +qed + +definition worecZSL :: "'b \ ('a \ 'b \ 'b) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" +where "worecZSL Z S L \ worecSL S (\ f a. if a = zero then Z else L f a)" + +lemma worecZSL_zero: +assumes a: "adm_woL L" +shows "worecZSL Z S L zero = Z" +proof- + let ?L = "\ f a. if a = zero then Z else L f a" + have "worecZSL Z S L zero = ?L (worecZSL Z S L) zero" + unfolding worecZSL_def apply(rule worecSL_isLim) + using assms unfolding adm_woL_def by auto + also have "... = Z" by simp + finally show ?thesis . +qed + +lemma worecZSL_succ: +assumes a: "adm_woL L" and i: "aboveS j \ {}" +shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)" +unfolding worecZSL_def apply(rule worecSL_succ) +using assms unfolding adm_woL_def by auto + +lemma worecZSL_isLim: +assumes a: "adm_woL L" and "isLim i" and "i \ zero" +shows "worecZSL Z S L i = L (worecZSL Z S L) i" +proof- + let ?L = "\ f a. if a = zero then Z else L f a" + have "worecZSL Z S L i = ?L (worecZSL Z S L) i" + unfolding worecZSL_def apply(rule worecSL_isLim) + using assms unfolding adm_woL_def by auto + also have "... = L (worecZSL Z S L) i" using assms by simp + finally show ?thesis . +qed + + +subsubsection {* Well-order succ-lim induction *} + +lemma ord_cases: +obtains j where "i = succ j" and "aboveS j \ {}" | "isLim i" +by (metis isLim_def isSucc_def) + +lemma well_order_inductSL[case_names Suc Lim]: +assumes SUCC: "\i. \aboveS i \ {}; P i\ \ P (succ i)" and +LIM: "\i. \isLim i; \j. j \ underS i \ P j\ \ P i" +shows "P i" +proof(induction rule: well_order_induct) + fix i assume 0: "\j. j \ i \ (j, i) \ r \ P j" + show "P i" proof(cases i rule: ord_cases) + fix j assume i: "i = succ j" and j: "aboveS j \ {}" + hence "j \ i \ (j, i) \ r" by (metis succ_diff succ_in) + hence 1: "P j" using 0 by simp + show "P i" unfolding i apply(rule SUCC) using 1 j by auto + qed(insert 0 LIM, unfold underS_def, auto) +qed + +lemma well_order_inductZSL[case_names Zero Suc Lim]: +assumes ZERO: "P zero" +and SUCC: "\i. \aboveS i \ {}; P i\ \ P (succ i)" and +LIM: "\i. \isLim i; i \ zero; \j. j \ underS i \ P j\ \ P i" +shows "P i" +apply(induction rule: well_order_inductSL) using assms by auto + +(* Succesor and limit ordinals *) +definition "isSuccOrd \ \ j \ Field r. \ i \ Field r. (i,j) \ r" +definition "isLimOrd \ \ isSuccOrd" + +lemma isLimOrd_succ: +assumes isLimOrd and "i \ Field r" +shows "succ i \ Field r" +using assms unfolding isLimOrd_def isSuccOrd_def +by (metis REFL in_notinI refl_on_domain succ_smallest) + +lemma isLimOrd_aboveS: +assumes l: isLimOrd and i: "i \ Field r" +shows "aboveS i \ {}" +proof- + obtain j where "j \ Field r" and "(j,i) \ r" + using assms unfolding isLimOrd_def isSuccOrd_def by auto + hence "(i,j) \ r \ j \ i" by (metis i max2_def max2_greater) + thus ?thesis unfolding aboveS_def by auto +qed + +lemma succ_aboveS_isLimOrd: +assumes "\ i \ Field r. aboveS i \ {} \ succ i \ Field r" +shows isLimOrd +unfolding isLimOrd_def isSuccOrd_def proof safe + fix j assume j: "j \ Field r" "\i\Field r. (i, j) \ r" + hence "(succ j, j) \ r" using assms by auto + moreover have "aboveS j \ {}" using assms j unfolding aboveS_def by auto + ultimately show False by (metis succ_not_in) +qed + +lemma isLim_iff: +assumes l: "isLim i" and j: "j \ underS i" +shows "\ k. k \ underS i \ j \ underS k" +proof- + have a: "aboveS j \ {}" using j unfolding underS_def aboveS_def by auto + show ?thesis apply(rule exI[of _ "succ j"]) apply safe + using assms a unfolding underS_def isLim_def + apply (metis (lifting, full_types) isSucc_def mem_Collect_eq succ_smallest) + by (metis (lifting, full_types) a mem_Collect_eq succ_diff succ_in) +qed + +end (* context wo_rel *) + +abbreviation "zero \ wo_rel.zero" +abbreviation "succ \ wo_rel.succ" +abbreviation "pred \ wo_rel.pred" +abbreviation "isSucc \ wo_rel.isSucc" +abbreviation "isLim \ wo_rel.isLim" +abbreviation "isLimOrd \ wo_rel.isLimOrd" +abbreviation "isSuccOrd \ wo_rel.isSuccOrd" +abbreviation "adm_woL \ wo_rel.adm_woL" +abbreviation "worecSL \ wo_rel.worecSL" +abbreviation "worecZSL \ wo_rel.worecZSL" + + +subsection {* Projections of wellorders *} + +definition "oproj r s f \ Field s \ f ` (Field r) \ compat r s f" + +lemma oproj_in: +assumes "oproj r s f" and "(a,a') \ r" +shows "(f a, f a') \ s" +using assms unfolding oproj_def compat_def by auto + +lemma oproj_Field: +assumes f: "oproj r s f" and a: "a \ Field r" +shows "f a \ Field s" +using oproj_in[OF f] a unfolding Field_def by auto + +lemma oproj_Field2: +assumes f: "oproj r s f" and a: "b \ Field s" +shows "\ a \ Field r. f a = b" +using assms unfolding oproj_def by auto + +lemma oproj_under: +assumes f: "oproj r s f" and a: "a \ under r a'" +shows "f a \ under s (f a')" +using oproj_in[OF f] a unfolding under_def by auto + +(* An ordinal is embedded in another whenever it is embedded as an order +(not necessarily as initial segment):*) +theorem embedI: +assumes r: "Well_order r" and s: "Well_order s" +and f: "\ a. a \ Field r \ f a \ Field s \ f ` underS r a \ underS s (f a)" +shows "\ g. embed r s g" +proof- + interpret r!: wo_rel r by unfold_locales (rule r) + interpret s!: wo_rel s by unfold_locales (rule s) + let ?G = "\ g a. suc s (g ` underS r a)" + def g \ "worec r ?G" + have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto + (* *) + {fix a assume "a \ Field r" + hence "bij_betw g (under r a) (under s (g a)) \ + g a \ under s (f a)" + proof(induction a rule: r.underS_induct) + case (1 a) + hence a: "a \ Field r" + and IH1a: "\ a1. a1 \ underS r a \ inj_on g (under r a1)" + and IH1b: "\ a1. a1 \ underS r a \ g ` under r a1 = under s (g a1)" + and IH2: "\ a1. a1 \ underS r a \ g a1 \ under s (f a1)" + unfolding underS_def Field_def bij_betw_def by auto + have fa: "f a \ Field s" using f[OF a] by auto + have g: "g a = suc s (g ` underS r a)" + using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp + have A0: "g ` underS r a \ Field s" + using IH1b by (metis IH2 image_subsetI in_mono under_Field) + {fix a1 assume a1: "a1 \ underS r a" + from IH2[OF this] have "g a1 \ under s (f a1)" . + moreover have "f a1 \ underS s (f a)" using f[OF a] a1 by auto + ultimately have "g a1 \ underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans) + } + hence "f a \ AboveS s (g ` underS r a)" unfolding AboveS_def + using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def) + hence A: "AboveS s (g ` underS r a) \ {}" by auto + have B: "\ a1. a1 \ underS r a \ g a1 \ underS s (g a)" + unfolding g apply(rule s.suc_underS[OF A0 A]) by auto + {fix a1 a2 assume a2: "a2 \ underS r a" and 1: "a1 \ underS r a2" + hence a12: "{a1,a2} \ under r a2" and "a1 \ a2" using r.REFL a + unfolding underS_def under_def refl_on_def Field_def by auto + hence "g a1 \ g a2" using IH1a[OF a2] unfolding inj_on_def by auto + hence "g a1 \ underS s (g a2)" using IH1b[OF a2] a12 + unfolding underS_def under_def by auto + } note C = this + have ga: "g a \ Field s" unfolding g using s.suc_inField[OF A0 A] . + have aa: "a \ under r a" + using a r.REFL unfolding under_def underS_def refl_on_def by auto + show ?case proof safe + show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe + show "inj_on g (under r a)" proof(rule r.inj_on_Field) + fix a1 a2 assume "a1 \ under r a" and a2: "a2 \ under r a" and a1: "a1 \ underS r a2" + hence a22: "a2 \ under r a2" and a12: "a1 \ under r a2" "a1 \ a2" + using a r.REFL unfolding under_def underS_def refl_on_def by auto + show "g a1 \ g a2" + proof(cases "a2 = a") + case False hence "a2 \ underS r a" + using a2 unfolding underS_def under_def by auto + from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto + qed(insert B a1, unfold underS_def, auto) + qed(unfold under_def Field_def, auto) + next + fix a1 assume a1: "a1 \ under r a" + show "g a1 \ under s (g a)" + proof(cases "a1 = a") + case True thus ?thesis + using ga s.REFL unfolding refl_on_def under_def by auto + next + case False + hence a1: "a1 \ underS r a" using a1 unfolding underS_def under_def by auto + thus ?thesis using B unfolding underS_def under_def by auto + qed + next + fix b1 assume b1: "b1 \ under s (g a)" + show "b1 \ g ` under r a" + proof(cases "b1 = g a") + case True thus ?thesis using aa by auto + next + case False + hence "b1 \ underS s (g a)" using b1 unfolding underS_def under_def by auto + from s.underS_suc[OF this[unfolded g] A0] + obtain a1 where a1: "a1 \ underS r a" and b1: "b1 \ under s (g a1)" by auto + obtain a2 where "a2 \ under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto + hence "a2 \ under r a" using a1 + by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans) + thus ?thesis using b1 by auto + qed + qed + next + have "(g a, f a) \ s" unfolding g proof(rule s.suc_least[OF A0]) + fix b1 assume "b1 \ g ` underS r a" + then obtain a1 where a1: "b1 = g a1" and a1: "a1 \ underS r a" by auto + hence "b1 \ underS s (f a)" + using a by (metis `\a1. a1 \ underS r a \ g a1 \ underS s (f a)`) + thus "f a \ b1 \ (b1, f a) \ s" unfolding underS_def by auto + qed(insert fa, auto) + thus "g a \ under s (f a)" unfolding under_def by auto + qed + qed + } + thus ?thesis unfolding embed_def by auto +qed + +corollary ordLeq_def2: + "r \o s \ Well_order r \ Well_order s \ + (\ f. \ a \ Field r. f a \ Field s \ f ` underS r a \ underS s (f a))" +using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s] +unfolding ordLeq_def by fast + +lemma iso_oproj: + assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f" + shows "oproj r s f" +using assms unfolding oproj_def +by (subst (asm) iso_iff3) (auto simp: bij_betw_def) + +theorem oproj_embed: +assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" +shows "\ g. embed s r g" +proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe) + fix b assume "b \ Field s" + thus "inv_into (Field r) f b \ Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into) +next + fix a b assume "b \ Field s" "a \ b" "(a, b) \ s" + "inv_into (Field r) f a = inv_into (Field r) f b" + with f show False by (auto dest!: inv_into_injective simp: Field_def oproj_def) +next + fix a b assume *: "b \ Field s" "a \ b" "(a, b) \ s" + { assume "(inv_into (Field r) f a, inv_into (Field r) f b) \ r" + moreover + from *(3) have "a \ Field s" unfolding Field_def by auto + with *(1,2) have + "inv_into (Field r) f a \ Field r" "inv_into (Field r) f b \ Field r" + "inv_into (Field r) f a \ inv_into (Field r) f b" + by (auto dest!: oproj_Field2[OF f] inv_into_injective intro!: inv_into_into) + ultimately have "(inv_into (Field r) f b, inv_into (Field r) f a) \ r" + using r by (auto simp: well_order_on_def linear_order_on_def total_on_def) + with f[unfolded oproj_def compat_def] *(1) `a \ Field s` + f_inv_into_f[of b f "Field r"] f_inv_into_f[of a f "Field r"] + have "(b, a) \ s" by (metis in_mono) + with *(2,3) s have False + by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def antisym_def) + } thus "(inv_into (Field r) f a, inv_into (Field r) f b) \ r" by blast +qed + +corollary oproj_ordLeq: +assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" +shows "s \o r" +using oproj_embed[OF assms] r s unfolding ordLeq_def by auto + +end