# HG changeset patch # User paulson # Date 1673650060 0 # Node ID f881fd264929b1c0dfcf54b6460f678ab3691d0f # Parent ec4c38e156c703c0920b1dc1c145221e9887c6bb More cleaning up proofs, plus a TeX fix diff -r ec4c38e156c7 -r f881fd264929 src/HOL/BNF_Wellorder_Constructions.thy --- a/src/HOL/BNF_Wellorder_Constructions.thy Fri Jan 13 16:44:00 2023 +0000 +++ b/src/HOL/BNF_Wellorder_Constructions.thy Fri Jan 13 22:47:40 2023 +0000 @@ -8,7 +8,7 @@ section \Constructions on Wellorders as Needed by Bounded Natural Functors\ theory BNF_Wellorder_Constructions -imports BNF_Wellorder_Embedding + imports BNF_Wellorder_Embedding begin text \In this section, we study basic constructions on well-orders, such as restriction to @@ -70,13 +70,8 @@ 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 + using assms + by (auto simp: well_order_on_def Linear_order_Restr elim: wf_subset) lemma Field_Restr_subset: "Field(Restr r A) \ A" by (auto simp add: Field_def) @@ -92,7 +87,7 @@ 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 assms using Well_order_Restr[of r A] Refl_Field_Restr2[of r A] order_on_defs[of "Field r" r] by auto @@ -100,12 +95,12 @@ 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) + "\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" + 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" unfolding wo_rel.ofilter_def under_def proof show "{b. (b, a) \ Restr r A} \ {b. (b, a) \ r}" @@ -125,51 +120,51 @@ qed lemma ofilter_embed: -assumes "Well_order r" -shows "wo_rel.ofilter r A = (A \ Field r \ embed (Restr r A) r id)" + 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" - unfolding embed_def + unfolding embed_def proof safe fix a assume "a \ A" thus "a \ Field r" using assms * - by (auto simp add: wo_rel_def wo_rel.ofilter_def) + 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 (id a))" using assms * - by (simp add: ofilter_Restr_under Field_Restr_ofilter) + 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 + 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" . + 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)" + 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 + 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 *) + by (simp add: Well_order_Restr wo_rel_def) + (* Main proof *) show ?thesis using WellB assms unfolding wo_rel.ofilter_def under_def ofilter_def proof safe @@ -183,84 +178,84 @@ 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" + 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)" + 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 + using Refl_Field_Restr by blast have FieldB: "Field ?rB = Field r Int B" - using Refl Refl_Field_Restr by blast + 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) + 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 *) + 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) + by (simp add: ofilter_Restr_subset) hence "embed (Restr ?rB A) (Restr r B) id" - using WellB ofilter_embed[of "?rB" A] by auto + using WellB ofilter_embed[of "?rB" A] by auto thus "embed (Restr r A) (Restr r B) id" - using * by (simp add: Restr_subset) + 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 + 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)) \ + 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 + using Refl_Field_Restr by blast hence FieldA: "Field ?rA = A" using OFA Well - by (auto simp add: wo_rel.ofilter_def) + by (auto simp add: wo_rel.ofilter_def) have "Field ?rB = Field r Int B" - using Refl Refl_Field_Restr by blast + 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 *) + 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 + 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) + 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" + 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')" @@ -268,13 +263,13 @@ 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 + 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 + 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 @@ -283,13 +278,13 @@ 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 \ + 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)" + 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) @@ -299,23 +294,23 @@ moreover have "compat (ofilterIncl r) ?rS ?h" proof(unfold compat_def ofilterIncl_def, - intro allI impI, simp, elim conjE) + 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" + **: "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) + 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) + 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) + 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 + by simp qed ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf) qed @@ -336,35 +331,35 @@ \ definition ordLeq :: "('a rel * 'a' rel) set" -where -"ordLeq = {(r,r'). Well_order r \ Well_order r' \ (\f. embed r r' f)}" + 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" + where "r <=o r' \ (r,r') \ ordLeq" abbreviation ordLeq3 :: "'a rel \ 'a' rel \ bool" (infix "\o" 50) -where "r \o r' \ r <=o r'" + 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)}" + 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" + where "r (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)}" + 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" + 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 + assumes "r \o r'" + shows "Well_order r \ Well_order r'" + using assms unfolding ordLeq_def by simp text\Notice that the relations \\o\, \, \=o\ connect well-orders on potentially {\em distinct} types. However, some of the lemmas below, including the next one, @@ -372,360 +367,313 @@ to \'a rel rel\.\ lemma ordLeq_reflexive: -"Well_order r \ r \o r" -unfolding ordLeq_def using id_embed[of r] by blast + "Well_order r \ 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' \ f)" - using comp_embed[of r r' f r'' f'] by auto - thus "r \o r''" unfolding ordLeq_def using 1 by auto -qed + assumes "r \o r'" and "r' \o r''" + shows "r \o r''" + using assms by (auto simp: ordLeq_def intro: comp_embed) lemma ordLeq_total: -"\Well_order r; Well_order r'\ \ r \o r' \ r' \o r" -unfolding ordLeq_def using wellorders_totally_ordered by blast + "\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 + "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' \ f)" - using comp_iso[of r r' f r'' f'] by auto - thus "r =o r''" unfolding ordIso_def using 1 by auto -qed + assumes *: "r =o r'" and **: "r' =o r''" + shows "r =o r''" + using assms by (auto simp: ordIso_def intro: comp_iso) lemma ordIso_symmetric: -assumes *: "r =o r'" -shows "r' =o r" + 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) + 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) + 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' o r'" and " r' Well_order r''" - using assms unfolding ordLeq_def ordLess_def by auto + using assms unfolding ordLeq_def ordLess_def by auto thus ?thesis using assms unfolding ordLeq_def ordLess_def - using embed_comp_embedS by blast + 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 + assumes "r o r''" + shows "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 + assumes "r \o r'" and " r' =o r''" + shows "r \o r''" + using embed_comp_iso assms by (force simp: ordLeq_def ordIso_def) 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 + assumes "r =o r'" and " r' \o r''" + shows "r \o r''" + using iso_comp_embed assms by (force simp: ordLeq_def ordIso_def) 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 + assumes "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 + assumes "r =o r'" and " r' (\f'. embed r' r f')" + 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) + 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 + 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)" + 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) + 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 + using 0 EMB embed_unique[of r1] by auto hence "\(bij_betw f ?A1 ?A2)" - using 1 bij_betw_cong[of ?A1] by blast + 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'))" + "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 + 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 + 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 + 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) + 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 + using id_embed[of r] by (auto simp: ordLess_iff) lemma ordLeq_iff_ordLess_or_ordIso: -"r \o r' = (r r =o r')" -unfolding ordRels_def embedS_defs iso_defs by blast + "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)" + "(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 + 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) + by (simp add: inv_into_Field_embed_bij_betw) thus "r \o r' \ r' \o r" - unfolding ordLeq_def using 1 by auto + 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 + 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 + "r \ r' \o r" + using ordLess_ordLeq_trans ordLess_irreflexive by blast lemma not_ordLeq_ordLess: -"r \o r' \ \ r' o r' \ \ r' r' \o r" + 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) + 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 + 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 ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast + "r \ r =o r'" + using 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) = (r r' o r')" -using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast + assumes WELL: "Well_order r" and WELL': "Well_order r'" + shows "(\ r' o r')" + using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast lemma ordLess_transitive[trans]: -"\r \ r r \ r r \o r'" -using ordIso_iff_ordLeq by blast + "r =o 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 + "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)" + 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 + 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 + 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 + 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 + 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 + 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 + 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 Well_order r; wo_rel.ofilter r A\ \ (A < Field r) = (Restr r A {}" -shows "Restr r (underS r a) {}" + shows "Restr r (underS r a) (ofilterIncl r3)" + assumes + OL12: "r1 (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) + 0: "Well_order 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 + 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 - (* *) + 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) + 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) + 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) - (* *) + 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) + 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) + using EMB23 0 by (simp add: wo_rel_def embed_inj_on) ultimately have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: image_strict_mono) moreover {have "embed r1 r3 (f23 \ 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 \ f12" f13] by auto - hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force + 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 \ 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 + 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))" + assumes WELL: "Well_order r" and WELL': "Well_order r'" + shows "(r' a \ Field r. r' =o Restr r (underS r a))" proof safe 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 + 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) + 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 + 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 + using WELL Well_order_Restr by blast ultimately have "r' =o Restr r (f ` (Field r'))" - using WELL' unfolding ordIso_def by auto + 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 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 + 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) + 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 p. Field p < Field r \ r' =o p \ p o r) = (\p. Field p \ Field r \ r' =o p \ p \o r)" + "(r' \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 - } + have "r' \p. Field p \ Field r \ r' =o p \ p \o r" + using ordLeq_iff_ordLess_or_ordIso internalize_ordLess[of r' r] 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 + 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') = (\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 + then obtain a where "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 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 + 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'" + 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 + 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 + 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 + "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 @@ -854,10 +797,10 @@ {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.\ definition ord_to_filter :: "'a rel \ 'a rel \ 'a set" -where "ord_to_filter r0 r \ (SOME f. embed r r0 f) ` (Field r)" + where "ord_to_filter r0 r \ (SOME f. embed r r0 f) ` (Field r)" lemma ord_to_filter_compat: -"compat (ordLess Int (ordLess\``{r0} \ ordLess\``{r0})) + "compat (ordLess Int (ordLess\``{r0} \ ordLess\``{r0})) (ofilterIncl r0) (ord_to_filter r0)" proof(unfold compat_def ord_to_filter_def, clarify) @@ -867,41 +810,41 @@ 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) + 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) + 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\``{r0} \ ?ordLess\``{r0})" - {assume Case1: "Well_order r0" - hence "wf ?R" - using wf_ofilterIncl[of r0] + (* need to annotate here!*) + let ?ordLess = "ordLess::('d rel * 'd rel) set" + let ?R = "?ordLess Int (?ordLess\``{r0} \ ?ordLess\``{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 + } + 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'" + 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' definition dir_image :: "'a rel \ ('a \ 'a') \ 'a' rel" -where -"dir_image r f = {(f a, f b)| a b. (a,b) \ r}" + 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 + "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 + "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)" + 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 + 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) + 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)" -unfolding trans_def + assumes TRANS: "trans r" and INJ: "inj_on f (Field r)" + shows "trans(dir_image r f)" + unfolding trans_def proof safe 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 + 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 + 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 + 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) + "\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)" -unfolding antisym_def + assumes AN: "antisym r" and INJ: "inj_on f (Field r)" + shows "antisym(dir_image r f)" + unfolding antisym_def proof safe 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 + 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) + "\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)" + 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)" @@ -995,76 +938,76 @@ 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 + 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) + "\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)" + 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 + 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 + 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 + 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)" -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 + "\Well_order r; inj_on f (Field r)\ \ Well_order (dir_image r f)" + 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) + "\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 + "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 + "\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 + "\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'" + 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 + 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 @@ -1086,8 +1029,8 @@ 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)). + 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 \ @@ -1096,15 +1039,15 @@ )}" lemma Field_bsqr: -"Field (bsqr r) = Field r \ Field r" + "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 \ + 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 + ultimately have "a1 \ Field r \ a2 \ Field r" unfolding Field_def by auto } thus ?thesis unfolding Field_def by force qed @@ -1118,101 +1061,101 @@ qed lemma bsqr_Refl: "Refl(bsqr r)" -by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def) + by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def) lemma bsqr_Trans: -assumes "Well_order r" -shows "trans (bsqr r)" -unfolding trans_def + assumes "Well_order r" + shows "trans (bsqr r)" + unfolding trans_def proof safe (* 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 *) + (* 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 + 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 + 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 + 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 + {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 + {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 + {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)" + 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 @@ -1220,334 +1163,293 @@ 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 *) + 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 \ + hence "{a1,a2,b1,b2} \ Field r" unfolding bsqr_def by auto + moreover + have "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 \ + using * unfolding bsqr_def by auto + moreover + have "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 + using ** unfolding bsqr_def by auto + ultimately show "a1 = b1 \ a2 = b2" + using IrrS by auto qed lemma bsqr_Total: -assumes "Well_order r" -shows "Total(bsqr r)" + 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 *) + 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 + 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 + 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 + 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 + 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 + 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 - (* *) + 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 - (* *) + 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 + 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 - (* *) + 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 + 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 + 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" + 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 + 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 + 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 + 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" + 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 - (* *) + 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 + "(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 + 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) + 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 + 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)}" + "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 + "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 + 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" + "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 + 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" + 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" @@ -1559,14 +1461,14 @@ 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 + 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" + 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" @@ -1579,7 +1481,7 @@ next case True obtain g1 where "g1 \ Func B C" and "g a = g1" - using assms using Func_elim[OF assms True] by blast + using assms using Func_elim[OF assms True] by blast thus ?thesis using True unfolding Func_def curr_def by auto qed qed @@ -1587,24 +1489,21 @@ 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+, safe) - using curr_surj curr_in apply blast+ - done + "bij_betw (curr A) (Func (A \ B) C) (Func A (Func B C))" + unfolding bij_betw_def inj_on_def + using curr_surj curr_in curr_inj by blast definition Func_map where -"Func_map B2 f1 f2 g b2 \ if b2 \ B2 then f1 (g (f2 b2)) else undefined" + "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 + 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 \ {}" + 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 @@ -1612,27 +1511,21 @@ qed lemma Func_is_emp: -"Func A B = {} \ A \ {} \ B = {}" (is "?L \ ?R") + "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 + assume ?L + then show ?R + using Func_empty Func_non_emp[of B A] 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 + assume ?R + then show ?L + using Func_empty Func_non_emp[of B A] by (auto simp: Func_def) 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" + 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) @@ -1646,15 +1539,15 @@ 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 + 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 define j2 where [abs_def]: "j2 a2 = (if a2 \ f2 ` B2 then k a2 else b22)" for a2 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 + using kk unfolding j2_def by auto define g where "g = Func_map A2 j1 j2 h" have "Func_map B2 f1 f2 g = h" proof (rule ext) @@ -1668,13 +1561,13 @@ 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) + 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)+ + 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 + unfolding Func_map_def[abs_def] by auto qed(use B1 Func_map[OF _ _ A2(2)] in auto) qed diff -r ec4c38e156c7 -r f881fd264929 src/HOL/BNF_Wellorder_Embedding.thy --- a/src/HOL/BNF_Wellorder_Embedding.thy Fri Jan 13 16:44:00 2023 +0000 +++ b/src/HOL/BNF_Wellorder_Embedding.thy Fri Jan 13 22:47:40 2023 +0000 @@ -8,7 +8,7 @@ section \Well-Order Embeddings as Needed by Bounded Natural Functors\ theory BNF_Wellorder_Embedding -imports Hilbert_Choice BNF_Wellorder_Relation + imports Hilbert_Choice BNF_Wellorder_Relation begin text\In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and @@ -23,35 +23,35 @@ subsection \Auxiliaries\ lemma UNION_inj_on_ofilter: -assumes WELL: "Well_order r" and - OF: "\ i. i \ I \ wo_rel.ofilter r (A i)" and - INJ: "\ i. i \ I \ inj_on f (A i)" -shows "inj_on f (\i \ I. A i)" + assumes WELL: "Well_order r" and + OF: "\ i. i \ I \ wo_rel.ofilter r (A i)" and + INJ: "\ i. i \ I \ inj_on f (A i)" + shows "inj_on f (\i \ I. A i)" proof- have "wo_rel r" using WELL by (simp add: wo_rel_def) hence "\ i j. \i \ I; j \ I\ \ A i <= A j \ A j <= A i" - using wo_rel.ofilter_linord[of r] OF by blast + using wo_rel.ofilter_linord[of r] OF by blast with WELL INJ show ?thesis - by (auto simp add: inj_on_UNION_chain) + by (auto simp add: inj_on_UNION_chain) qed lemma under_underS_bij_betw: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - IN: "a \ Field r" and IN': "f a \ Field r'" and - BIJ: "bij_betw f (underS r a) (underS r' (f a))" -shows "bij_betw f (under r a) (under r' (f a))" + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + IN: "a \ Field r" and IN': "f a \ Field r'" and + BIJ: "bij_betw f (underS r a) (underS r' (f a))" + shows "bij_betw f (under r a) (under r' (f a))" proof- have "a \ underS r a \ f a \ underS r' (f a)" - unfolding underS_def by auto + unfolding underS_def by auto moreover {have "Refl r \ Refl r'" using WELL WELL' - by (auto simp add: order_on_defs) - hence "under r a = underS r a \ {a} \ + by (auto simp add: order_on_defs) + hence "under r a = underS r a \ {a} \ under r' (f a) = underS r' (f a) \ {f a}" - using IN IN' by(auto simp add: Refl_under_underS) + using IN IN' by(auto simp add: Refl_under_underS) } ultimately show ?thesis - using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto + using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto qed @@ -69,28 +69,28 @@ and an isomorphism (operator \iso\) is a bijective embedding.\ definition embed :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" -where -"embed r r' f \ \a \ Field r. bij_betw f (under r a) (under r' (f a))" + where + "embed r r' f \ \a \ Field r. bij_betw f (under r a) (under r' (f a))" lemmas embed_defs = embed_def embed_def[abs_def] text \Strict embeddings:\ definition embedS :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" -where -"embedS r r' f \ embed r r' f \ \ bij_betw f (Field r) (Field r')" + where + "embedS r r' f \ embed r r' f \ \ bij_betw f (Field r) (Field r')" lemmas embedS_defs = embedS_def embedS_def[abs_def] definition iso :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" -where -"iso r r' f \ embed r r' f \ bij_betw f (Field r) (Field r')" + where + "iso r r' f \ embed r r' f \ bij_betw f (Field r) (Field r')" lemmas iso_defs = iso_def iso_def[abs_def] definition compat :: "'a rel \ 'a' rel \ ('a \ 'a') \ bool" -where -"compat r r' f \ \a b. (a,b) \ r \ (f a, f b) \ r'" + where + "compat r r' f \ \a b. (a,b) \ r \ (f a, f b) \ r'" lemma compat_wf: assumes CMP: "compat r r' f" and WF: "wf r'" @@ -168,46 +168,46 @@ by (auto simp add: embed_in_Field) lemma embed_preserves_ofilter: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - EMB: "embed r r' f" and OF: "wo_rel.ofilter r A" -shows "wo_rel.ofilter r' (f`A)" + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + EMB: "embed r r' f" and OF: "wo_rel.ofilter r A" + shows "wo_rel.ofilter r' (f`A)" proof- (* Preliminary facts *) from WELL have Well: "wo_rel r" unfolding wo_rel_def . from WELL' have Well': "wo_rel r'" unfolding wo_rel_def . from OF have 0: "A \ Field r" by(auto simp add: Well wo_rel.ofilter_def) - (* Main proof *) + (* Main proof *) show ?thesis using Well' WELL EMB 0 embed_Field[of r r' f] proof(unfold wo_rel.ofilter_def, auto simp add: image_def) fix a b' assume *: "a \ A" and **: "b' \ under r' (f a)" hence "a \ Field r" using 0 by auto hence "bij_betw f (under r a) (under r' (f a))" - using * EMB by (auto simp add: embed_def) + using * EMB by (auto simp add: embed_def) hence "f`(under r a) = under r' (f a)" - by (simp add: bij_betw_def) + by (simp add: bij_betw_def) with ** image_def[of f "under r a"] obtain b where - 1: "b \ under r a \ b' = f b" by blast + 1: "b \ under r a \ b' = f b" by blast hence "b \ A" using Well * OF - by (auto simp add: wo_rel.ofilter_def) + by (auto simp add: wo_rel.ofilter_def) with 1 show "\b \ A. b' = f b" by blast qed qed lemma embed_Field_ofilter: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - EMB: "embed r r' f" -shows "wo_rel.ofilter r' (f`(Field r))" + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + EMB: "embed r r' f" + shows "wo_rel.ofilter r' (f`(Field r))" proof- have "wo_rel.ofilter r (Field r)" - using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter) + using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter) with WELL WELL' EMB show ?thesis by (auto simp add: embed_preserves_ofilter) qed lemma embed_inj_on: -assumes WELL: "Well_order r" and EMB: "embed r r' f" -shows "inj_on f (Field r)" + assumes WELL: "Well_order r" and EMB: "embed r r' f" + shows "inj_on f (Field r)" proof(unfold inj_on_def, clarify) (* Preliminary facts *) from WELL have Well: "wo_rel r" unfolding wo_rel_def . @@ -215,30 +215,30 @@ have Total: "Total r" by simp from Well wo_rel.REFL[of r] have Refl: "Refl r" by simp - (* Main proof *) + (* Main proof *) fix a b assume *: "a \ Field r" and **: "b \ Field r" and - ***: "f a = f b" + ***: "f a = f b" hence 1: "a \ Field r \ b \ Field r" - unfolding Field_def by auto + unfolding Field_def by auto {assume "(a,b) \ r" - hence "a \ under r b \ b \ under r b" - using Refl by(auto simp add: under_def refl_on_def) - hence "a = b" - using EMB 1 *** - by (auto simp add: embed_def bij_betw_def inj_on_def) + hence "a \ under r b \ b \ under r b" + using Refl by(auto simp add: under_def refl_on_def) + hence "a = b" + using EMB 1 *** + by (auto simp add: embed_def bij_betw_def inj_on_def) } moreover {assume "(b,a) \ r" - hence "a \ under r a \ b \ under r a" - using Refl by(auto simp add: under_def refl_on_def) - hence "a = b" - using EMB 1 *** - by (auto simp add: embed_def bij_betw_def inj_on_def) + hence "a \ under r a \ b \ under r a" + using Refl by(auto simp add: under_def refl_on_def) + hence "a = b" + using EMB 1 *** + by (auto simp add: embed_def bij_betw_def inj_on_def) } ultimately show "a = b" using Total 1 - by (auto simp add: total_on_def) + by (auto simp add: total_on_def) qed lemma embed_underS: @@ -265,173 +265,173 @@ qed lemma embed_iff_compat_inj_on_ofilter: -assumes WELL: "Well_order r" and WELL': "Well_order r'" -shows "embed r r' f = (compat r r' f \ inj_on f (Field r) \ wo_rel.ofilter r' (f`(Field r)))" -using assms + assumes WELL: "Well_order r" and WELL': "Well_order r'" + shows "embed r r' f = (compat r r' f \ inj_on f (Field r) \ wo_rel.ofilter r' (f`(Field r)))" + using assms proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter, - unfold embed_def, auto) (* get rid of one implication *) + unfold embed_def, auto) (* get rid of one implication *) fix a assume *: "inj_on f (Field r)" and - **: "compat r r' f" and - ***: "wo_rel.ofilter r' (f`(Field r))" and - ****: "a \ Field r" - (* Preliminary facts *) + **: "compat r r' f" and + ***: "wo_rel.ofilter r' (f`(Field r))" and + ****: "a \ Field r" + (* Preliminary facts *) have Well: "wo_rel r" - using WELL wo_rel_def[of r] by simp + using WELL wo_rel_def[of r] by simp hence Refl: "Refl r" - using wo_rel.REFL[of r] by simp + using wo_rel.REFL[of r] by simp have Total: "Total r" - using Well wo_rel.TOTAL[of r] by simp + using Well wo_rel.TOTAL[of r] by simp have Well': "wo_rel r'" - using WELL' wo_rel_def[of r'] by simp + using WELL' wo_rel_def[of r'] by simp hence Antisym': "antisym r'" - using wo_rel.ANTISYM[of r'] by simp + using wo_rel.ANTISYM[of r'] by simp have "(a,a) \ r" - using **** Well wo_rel.REFL[of r] - refl_on_def[of _ r] by auto + using **** Well wo_rel.REFL[of r] + refl_on_def[of _ r] by auto hence "(f a, f a) \ r'" - using ** by(auto simp add: compat_def) + using ** by(auto simp add: compat_def) hence 0: "f a \ Field r'" - unfolding Field_def by auto + unfolding Field_def by auto have "f a \ f`(Field r)" - using **** by auto + using **** by auto hence 2: "under r' (f a) \ f`(Field r)" - using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce - (* Main proof *) + using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce + (* Main proof *) show "bij_betw f (under r a) (under r' (f a))" proof(unfold bij_betw_def, auto) show "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field]) next fix b assume "b \ under r a" thus "f b \ under r' (f a)" - unfolding under_def using ** - by (auto simp add: compat_def) + unfolding under_def using ** + by (auto simp add: compat_def) next fix b' assume *****: "b' \ under r' (f a)" hence "b' \ f`(Field r)" - using 2 by auto + using 2 by auto with Field_def[of r] obtain b where - 3: "b \ Field r" and 4: "b' = f b" by auto + 3: "b \ Field r" and 4: "b' = f b" by auto have "(b,a) \ r" proof- {assume "(a,b) \ r" - with ** 4 have "(f a, b') \ r'" - by (auto simp add: compat_def) - with ***** Antisym' have "f a = b'" - by(auto simp add: under_def antisym_def) - with 3 **** 4 * have "a = b" - by(auto simp add: inj_on_def) + with ** 4 have "(f a, b') \ r'" + by (auto simp add: compat_def) + with ***** Antisym' have "f a = b'" + by(auto simp add: under_def antisym_def) + with 3 **** 4 * have "a = b" + by(auto simp add: inj_on_def) } moreover {assume "a = b" - hence "(b,a) \ r" using Refl **** 3 - by (auto simp add: refl_on_def) + hence "(b,a) \ r" using Refl **** 3 + by (auto simp add: refl_on_def) } ultimately show ?thesis using Total **** 3 by (fastforce simp add: total_on_def) qed with 4 show "b' \ f`(under r a)" - unfolding under_def by auto + unfolding under_def by auto qed qed lemma inv_into_ofilter_embed: -assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and - BIJ: "\b \ A. bij_betw f (under r b) (under r' (f b))" and - IMAGE: "f ` A = Field r'" -shows "embed r' r (inv_into A f)" + assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and + BIJ: "\b \ A. bij_betw f (under r b) (under r' (f b))" and + IMAGE: "f ` A = Field r'" + shows "embed r' r (inv_into A f)" proof- (* Preliminary facts *) have Well: "wo_rel r" - using WELL wo_rel_def[of r] by simp + using WELL wo_rel_def[of r] by simp have Refl: "Refl r" - using Well wo_rel.REFL[of r] by simp + using Well wo_rel.REFL[of r] by simp have Total: "Total r" - using Well wo_rel.TOTAL[of r] by simp - (* Main proof *) + using Well wo_rel.TOTAL[of r] by simp + (* Main proof *) have 1: "bij_betw f A (Field r')" proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE) fix b1 b2 assume *: "b1 \ A" and **: "b2 \ A" and - ***: "f b1 = f b2" + ***: "f b1 = f b2" have 11: "b1 \ Field r \ b2 \ Field r" - using * ** Well OF by (auto simp add: wo_rel.ofilter_def) + using * ** Well OF by (auto simp add: wo_rel.ofilter_def) moreover {assume "(b1,b2) \ r" - hence "b1 \ under r b2 \ b2 \ under r b2" - unfolding under_def using 11 Refl - by (auto simp add: refl_on_def) - hence "b1 = b2" using BIJ * ** *** - by (simp add: bij_betw_def inj_on_def) + hence "b1 \ under r b2 \ b2 \ under r b2" + unfolding under_def using 11 Refl + by (auto simp add: refl_on_def) + hence "b1 = b2" using BIJ * ** *** + by (simp add: bij_betw_def inj_on_def) } moreover - {assume "(b2,b1) \ r" - hence "b1 \ under r b1 \ b2 \ under r b1" - unfolding under_def using 11 Refl - by (auto simp add: refl_on_def) - hence "b1 = b2" using BIJ * ** *** - by (simp add: bij_betw_def inj_on_def) + {assume "(b2,b1) \ r" + hence "b1 \ under r b1 \ b2 \ under r b1" + unfolding under_def using 11 Refl + by (auto simp add: refl_on_def) + hence "b1 = b2" using BIJ * ** *** + by (simp add: bij_betw_def inj_on_def) } ultimately show "b1 = b2" - using Total by (auto simp add: total_on_def) + using Total by (auto simp add: total_on_def) qed - (* *) + (* *) let ?f' = "(inv_into A f)" - (* *) + (* *) have 2: "\b \ A. bij_betw ?f' (under r' (f b)) (under r b)" proof(clarify) fix b assume *: "b \ A" hence "under r b \ A" - using Well OF by(auto simp add: wo_rel.ofilter_def) + using Well OF by(auto simp add: wo_rel.ofilter_def) moreover have "f ` (under r b) = under r' (f b)" - using * BIJ by (auto simp add: bij_betw_def) + using * BIJ by (auto simp add: bij_betw_def) ultimately show "bij_betw ?f' (under r' (f b)) (under r b)" - using 1 by (auto simp add: bij_betw_inv_into_subset) + using 1 by (auto simp add: bij_betw_inv_into_subset) qed - (* *) + (* *) have 3: "\b' \ Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))" proof(clarify) fix b' assume *: "b' \ Field r'" have "b' = f (?f' b')" using * 1 - by (auto simp add: bij_betw_inv_into_right) + by (auto simp add: bij_betw_inv_into_right) moreover {obtain b where 31: "b \ A" and "f b = b'" using IMAGE * by force - hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left) - with 31 have "?f' b' \ A" by auto + hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left) + with 31 have "?f' b' \ A" by auto } ultimately show "bij_betw ?f' (under r' b') (under r (?f' b'))" - using 2 by auto + using 2 by auto qed - (* *) + (* *) thus ?thesis unfolding embed_def . qed lemma inv_into_underS_embed: -assumes WELL: "Well_order r" and - BIJ: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and - IN: "a \ Field r" and - IMAGE: "f ` (underS r a) = Field r'" -shows "embed r' r (inv_into (underS r a) f)" -using assms -by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed) + assumes WELL: "Well_order r" and + BIJ: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and + IN: "a \ Field r" and + IMAGE: "f ` (underS r a) = Field r'" + shows "embed r' r (inv_into (underS r a) f)" + using assms + by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed) lemma inv_into_Field_embed: -assumes WELL: "Well_order r" and EMB: "embed r r' f" and - IMAGE: "Field r' \ f ` (Field r)" -shows "embed r' r (inv_into (Field r) f)" + assumes WELL: "Well_order r" and EMB: "embed r r' f" and + IMAGE: "Field r' \ f ` (Field r)" + shows "embed r' r (inv_into (Field r) f)" proof- have "(\b \ Field r. bij_betw f (under r b) (under r' (f b)))" - using EMB by (auto simp add: embed_def) + using EMB by (auto simp add: embed_def) moreover have "f ` (Field r) \ Field r'" - using EMB WELL by (auto simp add: embed_Field) + using EMB WELL by (auto simp add: embed_Field) ultimately show ?thesis using assms - by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed) + by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed) qed lemma inv_into_Field_embed_bij_betw: @@ -487,12 +487,12 @@ \ lemma wellorders_totally_ordered_aux: -fixes r ::"'a rel" and r'::"'a' rel" and - f :: "'a \ 'a'" and a::'a -assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \ Field r" and - IH: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and - NOT: "f ` (underS r a) \ Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))" -shows "bij_betw f (under r a) (under r' (f a))" + fixes r ::"'a rel" and r'::"'a' rel" and + f :: "'a \ 'a'" and a::'a + assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \ Field r" and + IH: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" and + NOT: "f ` (underS r a) \ Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))" + shows "bij_betw f (under r a) (under r' (f a))" proof- (* Preliminary facts *) have Well: "wo_rel r" using WELL unfolding wo_rel_def . @@ -500,197 +500,197 @@ have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . have OF: "wo_rel.ofilter r (underS r a)" - by (auto simp add: Well wo_rel.underS_ofilter) + by (auto simp add: Well wo_rel.underS_ofilter) hence UN: "underS r a = (\b \ underS r a. under r b)" - using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast - (* Gather facts about elements of underS r a *) + using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast + (* Gather facts about elements of underS r a *) {fix b assume *: "b \ underS r a" - hence t0: "(b,a) \ r \ b \ a" unfolding underS_def by auto - have t1: "b \ Field r" - using * underS_Field[of r a] by auto - have t2: "f`(under r b) = under r' (f b)" - using IH * by (auto simp add: bij_betw_def) - hence t3: "wo_rel.ofilter r' (f`(under r b))" - using Well' by (auto simp add: wo_rel.under_ofilter) - have "f`(under r b) \ Field r'" - using t2 by (auto simp add: under_Field) - moreover - have "b \ under r b" - using t1 by(auto simp add: Refl Refl_under_in) - ultimately - have t4: "f b \ Field r'" by auto - have "f`(under r b) = under r' (f b) \ + hence t0: "(b,a) \ r \ b \ a" unfolding underS_def by auto + have t1: "b \ Field r" + using * underS_Field[of r a] by auto + have t2: "f`(under r b) = under r' (f b)" + using IH * by (auto simp add: bij_betw_def) + hence t3: "wo_rel.ofilter r' (f`(under r b))" + using Well' by (auto simp add: wo_rel.under_ofilter) + have "f`(under r b) \ Field r'" + using t2 by (auto simp add: under_Field) + moreover + have "b \ under r b" + using t1 by(auto simp add: Refl Refl_under_in) + ultimately + have t4: "f b \ Field r'" by auto + have "f`(under r b) = under r' (f b) \ wo_rel.ofilter r' (f`(under r b)) \ f b \ Field r'" - using t2 t3 t4 by auto + using t2 t3 t4 by auto } hence bFact: - "\b \ underS r a. f`(under r b) = under r' (f b) \ + "\b \ underS r a. f`(under r b) = under r' (f b) \ wo_rel.ofilter r' (f`(under r b)) \ f b \ Field r'" by blast - (* *) + (* *) have subField: "f`(underS r a) \ Field r'" - using bFact by blast - (* *) + using bFact by blast + (* *) have OF': "wo_rel.ofilter r' (f`(underS r a))" proof- have "f`(underS r a) = f`(\b \ underS r a. under r b)" - using UN by auto + using UN by auto also have "\ = (\b \ underS r a. f`(under r b))" by blast also have "\ = (\b \ underS r a. (under r' (f b)))" - using bFact by auto + using bFact by auto finally have "f`(underS r a) = (\b \ underS r a. (under r' (f b)))" . thus ?thesis - using Well' bFact - wo_rel.ofilter_UNION[of r' "underS r a" "\ b. under r' (f b)"] by fastforce + using Well' bFact + wo_rel.ofilter_UNION[of r' "underS r a" "\ b. under r' (f b)"] by fastforce qed - (* *) + (* *) have "f`(underS r a) \ AboveS r' (f`(underS r a)) = Field r'" - using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field) + using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field) hence NE: "AboveS r' (f`(underS r a)) \ {}" - using subField NOT by blast - (* Main proof *) + using subField NOT by blast + (* Main proof *) have INCL1: "f`(underS r a) \ underS r' (f a) " proof(auto) fix b assume *: "b \ underS r a" have "f b \ f a \ (f b, f a) \ r'" - using subField Well' SUC NE * - wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force + using subField Well' SUC NE * + wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force thus "f b \ underS r' (f a)" - unfolding underS_def by simp + unfolding underS_def by simp qed - (* *) + (* *) have INCL2: "underS r' (f a) \ f`(underS r a)" proof fix b' assume "b' \ underS r' (f a)" hence "b' \ f a \ (b', f a) \ r'" - unfolding underS_def by simp + unfolding underS_def by simp thus "b' \ f`(underS r a)" - using Well' SUC NE OF' - wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto + using Well' SUC NE OF' + wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto qed - (* *) + (* *) have INJ: "inj_on f (underS r a)" proof- have "\b \ underS r a. inj_on f (under r b)" - using IH by (auto simp add: bij_betw_def) + using IH by (auto simp add: bij_betw_def) moreover have "\b. wo_rel.ofilter r (under r b)" - using Well by (auto simp add: wo_rel.under_ofilter) + using Well by (auto simp add: wo_rel.under_ofilter) ultimately show ?thesis - using WELL bFact UN - UNION_inj_on_ofilter[of r "underS r a" "\b. under r b" f] - by auto + using WELL bFact UN + UNION_inj_on_ofilter[of r "underS r a" "\b. under r b" f] + by auto qed - (* *) + (* *) have BIJ: "bij_betw f (underS r a) (underS r' (f a))" - unfolding bij_betw_def - using INJ INCL1 INCL2 by auto - (* *) + unfolding bij_betw_def + using INJ INCL1 INCL2 by auto + (* *) have "f a \ Field r'" - using Well' subField NE SUC - by (auto simp add: wo_rel.suc_inField) + using Well' subField NE SUC + by (auto simp add: wo_rel.suc_inField) thus ?thesis - using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto + using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto qed lemma wellorders_totally_ordered_aux2: -fixes r ::"'a rel" and r'::"'a' rel" and - f :: "'a \ 'a'" and g :: "'a \ bool" and a::'a -assumes WELL: "Well_order r" and WELL': "Well_order r'" and -MAIN1: - "\ a. (False \ g`(underS r a) \ f`(underS r a) \ Field r' + fixes r ::"'a rel" and r'::"'a' rel" and + f :: "'a \ 'a'" and g :: "'a \ bool" and a::'a + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + MAIN1: + "\ a. (False \ g`(underS r a) \ f`(underS r a) \ Field r' \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ (\(False \ (g`(underS r a)) \ f`(underS r a) \ Field r') \ g a = False)" and -MAIN2: "\ a. a \ Field r \ False \ g`(under r a) \ + MAIN2: "\ a. a \ Field r \ False \ g`(under r a) \ bij_betw f (under r a) (under r' (f a))" and -Case: "a \ Field r \ False \ g`(under r a)" -shows "\f'. embed r' r f'" + Case: "a \ Field r \ False \ g`(under r a)" + shows "\f'. embed r' r f'" proof- have Well: "wo_rel r" using WELL unfolding wo_rel_def . hence Refl: "Refl r" using wo_rel.REFL[of r] by auto have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . - (* *) + (* *) have 0: "under r a = underS r a \ {a}" - using Refl Case by(auto simp add: Refl_under_underS) - (* *) + using Refl Case by(auto simp add: Refl_under_underS) + (* *) have 1: "g a = False" proof- {assume "g a \ False" - with 0 Case have "False \ g`(underS r a)" by blast - with MAIN1 have "g a = False" by blast} + with 0 Case have "False \ g`(underS r a)" by blast + with MAIN1 have "g a = False" by blast} thus ?thesis by blast qed let ?A = "{a \ Field r. g a = False}" let ?a = "(wo_rel.minim r ?A)" - (* *) + (* *) have 2: "?A \ {} \ ?A \ Field r" using Case 1 by blast - (* *) + (* *) have 3: "False \ g`(underS r ?a)" proof assume "False \ g`(underS r ?a)" then obtain b where "b \ underS r ?a" and 31: "g b = False" by auto hence 32: "(b,?a) \ r \ b \ ?a" - by (auto simp add: underS_def) + by (auto simp add: underS_def) hence "b \ Field r" unfolding Field_def by auto with 31 have "b \ ?A" by auto hence "(?a,b) \ r" using wo_rel.minim_least 2 Well by fastforce - (* again: why worked without type annotations? *) + (* again: why worked without type annotations? *) with 32 Antisym show False - by (auto simp add: antisym_def) + by (auto simp add: antisym_def) qed have temp: "?a \ ?A" - using Well 2 wo_rel.minim_in[of r ?A] by auto + using Well 2 wo_rel.minim_in[of r ?A] by auto hence 4: "?a \ Field r" by auto - (* *) + (* *) have 5: "g ?a = False" using temp by blast - (* *) + (* *) have 6: "f`(underS r ?a) = Field r'" - using MAIN1[of ?a] 3 5 by blast - (* *) + using MAIN1[of ?a] 3 5 by blast + (* *) have 7: "\b \ underS r ?a. bij_betw f (under r b) (under r' (f b))" proof fix b assume as: "b \ underS r ?a" moreover have "wo_rel.ofilter r (underS r ?a)" - using Well by (auto simp add: wo_rel.underS_ofilter) + using Well by (auto simp add: wo_rel.underS_ofilter) ultimately have "False \ g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+ moreover have "b \ Field r" - unfolding Field_def using as by (auto simp add: underS_def) + unfolding Field_def using as by (auto simp add: underS_def) ultimately show "bij_betw f (under r b) (under r' (f b))" - using MAIN2 by auto + using MAIN2 by auto qed - (* *) + (* *) have "embed r' r (inv_into (underS r ?a) f)" - using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto + using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto thus ?thesis - unfolding embed_def by blast + unfolding embed_def by blast qed theorem wellorders_totally_ordered: -fixes r ::"'a rel" and r'::"'a' rel" -assumes WELL: "Well_order r" and WELL': "Well_order r'" -shows "(\f. embed r r' f) \ (\f'. embed r' r f')" + fixes r ::"'a rel" and r'::"'a' rel" + assumes WELL: "Well_order r" and WELL': "Well_order r'" + shows "(\f. embed r r' f) \ (\f'. embed r' r f')" proof- (* Preliminary facts *) have Well: "wo_rel r" using WELL unfolding wo_rel_def . hence Refl: "Refl r" using wo_rel.REFL[of r] by auto have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . - (* Main proof *) + (* Main proof *) obtain H where H_def: "H = (\h a. if False \ (snd \ h)`(underS r a) \ (fst \ h)`(underS r a) \ Field r' then (wo_rel.suc r' ((fst \ h)`(underS r a)), True) else (undefined, False))" by blast have Adm: "wo_rel.adm_wo r H" - using Well + using Well proof(unfold wo_rel.adm_wo_def, clarify) fix h1::"'a \ 'a' * bool" and h2::"'a \ 'a' * bool" and x assume "\y\underS r x. h1 y = h2 y" @@ -701,52 +701,52 @@ by (auto simp add: image_def) thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball) qed - (* More constant definitions: *) + (* More constant definitions: *) obtain h::"'a \ 'a' * bool" and f::"'a \ 'a'" and g::"'a \ bool" - where h_def: "h = wo_rel.worec r H" and - f_def: "f = fst \ h" and g_def: "g = snd \ h" by blast + where h_def: "h = wo_rel.worec r H" and + f_def: "f = fst \ h" and g_def: "g = snd \ h" by blast obtain test where test_def: - "test = (\ a. False \ (g`(underS r a)) \ f`(underS r a) \ Field r')" by blast - (* *) + "test = (\ a. False \ (g`(underS r a)) \ f`(underS r a) \ Field r')" by blast + (* *) have *: "\ a. h a = H h a" - using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def) + using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def) have Main1: - "\ a. (test a \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ + "\ a. (test a \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ (\(test a) \ g a = False)" proof- (* How can I prove this withou fixing a? *) fix a show "(test a \ f a = wo_rel.suc r' (f`(underS r a)) \ g a = True) \ (\(test a) \ g a = False)" - using *[of a] test_def f_def g_def H_def by auto + using *[of a] test_def f_def g_def H_def by auto qed - (* *) + (* *) let ?phi = "\ a. a \ Field r \ False \ g`(under r a) \ bij_betw f (under r a) (under r' (f a))" have Main2: "\ a. ?phi a" proof- fix a show "?phi a" proof(rule wo_rel.well_order_induct[of r ?phi], - simp only: Well, clarify) + simp only: Well, clarify) fix a assume IH: "\b. b \ a \ (b,a) \ r \ ?phi b" and - *: "a \ Field r" and - **: "False \ g`(under r a)" + *: "a \ Field r" and + **: "False \ g`(under r a)" have 1: "\b \ underS r a. bij_betw f (under r b) (under r' (f b))" proof(clarify) fix b assume ***: "b \ underS r a" hence 0: "(b,a) \ r \ b \ a" unfolding underS_def by auto moreover have "b \ Field r" - using *** underS_Field[of r a] by auto + using *** underS_Field[of r a] by auto moreover have "False \ g`(under r b)" - using 0 ** Trans under_incr[of r b a] by auto + using 0 ** Trans under_incr[of r b a] by auto ultimately show "bij_betw f (under r b) (under r' (f b))" - using IH by auto + using IH by auto qed - (* *) + (* *) have 21: "False \ g`(underS r a)" - using ** underS_subset_under[of r a] by auto + using ** underS_subset_under[of r a] by auto have 22: "g`(under r a) \ {True}" using ** by auto moreover have 23: "a \ under r a" - using Refl * by (auto simp add: Refl_under_in) + using Refl * by (auto simp add: Refl_under_in) ultimately have 24: "g a = True" by blast have 2: "f`(underS r a) \ Field r'" proof @@ -754,29 +754,29 @@ hence "g a = False" using Main1 test_def by blast with 24 show False using ** by blast qed - (* *) + (* *) have 3: "f a = wo_rel.suc r' (f`(underS r a))" - using 21 2 Main1 test_def by blast - (* *) + using 21 2 Main1 test_def by blast + (* *) show "bij_betw f (under r a) (under r' (f a))" - using WELL WELL' 1 2 3 * - wellorders_totally_ordered_aux[of r r' a f] by auto + using WELL WELL' 1 2 3 * + wellorders_totally_ordered_aux[of r r' a f] by auto qed qed - (* *) + (* *) let ?chi = "(\ a. a \ Field r \ False \ g`(under r a))" show ?thesis proof(cases "\a. ?chi a") assume "\ (\a. ?chi a)" hence "\a \ Field r. bij_betw f (under r a) (under r' (f a))" - using Main2 by blast + using Main2 by blast thus ?thesis unfolding embed_def by blast next assume "\a. ?chi a" then obtain a where "?chi a" by blast hence "\f'. embed r' r f'" - using wellorders_totally_ordered_aux2[of r r' g f a] - WELL WELL' Main1 Main2 test_def by fast + using wellorders_totally_ordered_aux2[of r r' g f a] + WELL WELL' Main1 Main2 test_def by fast thus ?thesis by blast qed qed @@ -790,75 +790,75 @@ embeddings of opposite directions are mutually inverse.\ lemma embed_determined: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - EMB: "embed r r' f" and IN: "a \ Field r" -shows "f a = wo_rel.suc r' (f`(underS r a))" + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + EMB: "embed r r' f" and IN: "a \ Field r" + shows "f a = wo_rel.suc r' (f`(underS r a))" proof- have "bij_betw f (underS r a) (underS r' (f a))" - using assms by (auto simp add: embed_underS) + using assms by (auto simp add: embed_underS) hence "f`(underS r a) = underS r' (f a)" - by (auto simp add: bij_betw_def) + by (auto simp add: bij_betw_def) moreover {have "f a \ Field r'" using IN - using EMB WELL embed_Field[of r r' f] by auto - hence "f a = wo_rel.suc r' (underS r' (f a))" - using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS) + using EMB WELL embed_Field[of r r' f] by auto + hence "f a = wo_rel.suc r' (underS r' (f a))" + using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS) } ultimately show ?thesis by simp qed lemma embed_unique: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - EMBf: "embed r r' f" and EMBg: "embed r r' g" -shows "a \ Field r \ f a = g a" + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + EMBf: "embed r r' f" and EMBg: "embed r r' g" + shows "a \ Field r \ f a = g a" proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def) fix a assume IH: "\b. b \ a \ (b,a) \ r \ b \ Field r \ f b = g b" and - *: "a \ Field r" + *: "a \ Field r" hence "\b \ underS r a. f b = g b" - unfolding underS_def by (auto simp add: Field_def) + unfolding underS_def by (auto simp add: Field_def) hence "f`(underS r a) = g`(underS r a)" by force thus "f a = g a" - using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto + using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto qed lemma embed_bothWays_inverse: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - EMB: "embed r r' f" and EMB': "embed r' r f'" -shows "(\a \ Field r. f'(f a) = a) \ (\a' \ Field r'. f(f' a') = a')" + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + EMB: "embed r r' f" and EMB': "embed r' r f'" + shows "(\a \ Field r. f'(f a) = a) \ (\a' \ Field r'. f(f' a') = a')" proof- have "embed r r (f' \ f)" using assms - by(auto simp add: comp_embed) + by(auto simp add: comp_embed) moreover have "embed r r id" using assms - by (auto simp add: id_embed) + by (auto simp add: id_embed) ultimately have "\a \ Field r. f'(f a) = a" - using assms embed_unique[of r r "f' \ f" id] id_def by auto + using assms embed_unique[of r r "f' \ f" id] id_def by auto moreover {have "embed r' r' (f \ f')" using assms - by(auto simp add: comp_embed) - moreover have "embed r' r' id" using assms - by (auto simp add: id_embed) - ultimately have "\a' \ Field r'. f(f' a') = a'" - using assms embed_unique[of r' r' "f \ f'" id] id_def by auto + by(auto simp add: comp_embed) + moreover have "embed r' r' id" using assms + by (auto simp add: id_embed) + ultimately have "\a' \ Field r'. f(f' a') = a'" + using assms embed_unique[of r' r' "f \ f'" id] id_def by auto } ultimately show ?thesis by blast qed lemma embed_bothWays_bij_betw: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - EMB: "embed r r' f" and EMB': "embed r' r g" -shows "bij_betw f (Field r) (Field r')" + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + EMB: "embed r r' f" and EMB': "embed r' r g" + shows "bij_betw f (Field r) (Field r')" proof- let ?A = "Field r" let ?A' = "Field r'" have "embed r r (g \ f) \ embed r' r' (f \ g)" - using assms by (auto simp add: comp_embed) + using assms by (auto simp add: comp_embed) hence 1: "(\a \ ?A. g(f a) = a) \ (\a' \ ?A'. f(g a') = a')" - using WELL id_embed[of r] embed_unique[of r r "g \ f" id] - WELL' id_embed[of r'] embed_unique[of r' r' "f \ g" id] - id_def by auto + using WELL id_embed[of r] embed_unique[of r r "g \ f" id] + WELL' id_embed[of r'] embed_unique[of r' r' "f \ g" id] + id_def by auto have 2: "(\a \ ?A. f a \ ?A') \ (\a' \ ?A'. g a' \ ?A)" - using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast - (* *) + using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast + (* *) show ?thesis proof(unfold bij_betw_def inj_on_def, auto simp add: 2) fix a b assume *: "a \ ?A" "b \ ?A" and **: "f a = f b" @@ -872,24 +872,24 @@ qed lemma embed_bothWays_iso: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - EMB: "embed r r' f" and EMB': "embed r' r g" -shows "iso r r' f" -unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw) + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + EMB: "embed r r' f" and EMB': "embed r' r g" + shows "iso r r' f" + unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw) subsection \More properties of embeddings, strict embeddings and isomorphisms\ lemma embed_bothWays_Field_bij_betw: -assumes WELL: "Well_order r" and WELL': "Well_order r'" and - EMB: "embed r r' f" and EMB': "embed r' r f'" -shows "bij_betw f (Field r) (Field r')" + assumes WELL: "Well_order r" and WELL': "Well_order r'" and + EMB: "embed r r' f" and EMB': "embed r' r f'" + shows "bij_betw f (Field r) (Field r')" proof- have "(\a \ Field r. f'(f a) = a) \ (\a' \ Field r'. f(f' a') = a')" - using assms by (auto simp add: embed_bothWays_inverse) + using assms by (auto simp add: embed_bothWays_inverse) moreover have "f`(Field r) \ Field r' \ f' ` (Field r') \ Field r" - using assms by (auto simp add: embed_Field) + using assms by (auto simp add: embed_Field) ultimately show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto qed @@ -928,7 +928,7 @@ hence 2: "embed r r'' ?g" using WELL EMB comp_embed[of r r' f r'' f'] by auto moreover have \
: "f' ` Field r' \ Field r''" - by (simp add: "1" embed_Field) + by (simp add: "1" embed_Field) {assume \
: "bij_betw ?g (Field r) (Field r'')" hence "embed r'' r ?h" using 2 WELL by (auto simp add: inv_into_Field_embed_bij_betw) @@ -974,57 +974,57 @@ using assms unfolding iso_def by (auto simp add: embed_comp_embedS) lemma embedS_Field: -assumes WELL: "Well_order r" and EMB: "embedS r r' f" -shows "f ` (Field r) < Field r'" + assumes WELL: "Well_order r" and EMB: "embedS r r' f" + shows "f ` (Field r) < Field r'" proof- have "f`(Field r) \ Field r'" using assms - by (auto simp add: embed_Field embedS_def) + by (auto simp add: embed_Field embedS_def) moreover {have "inj_on f (Field r)" using assms - by (auto simp add: embedS_def embed_inj_on) - hence "f`(Field r) \ Field r'" using EMB - by (auto simp add: embedS_def bij_betw_def) + by (auto simp add: embedS_def embed_inj_on) + hence "f`(Field r) \ Field r'" using EMB + by (auto simp add: embedS_def bij_betw_def) } ultimately show ?thesis by blast qed lemma embedS_iff: -assumes WELL: "Well_order r" and ISO: "embed r r' f" -shows "embedS r r' f = (f ` (Field r) < Field r')" + assumes WELL: "Well_order r" and ISO: "embed r r' f" + shows "embedS r r' f = (f ` (Field r) < Field r')" proof assume "embedS r r' f" thus "f ` Field r \ Field r'" - using WELL by (auto simp add: embedS_Field) + using WELL by (auto simp add: embedS_Field) next assume "f ` Field r \ Field r'" hence "\ bij_betw f (Field r) (Field r')" - unfolding bij_betw_def by blast + unfolding bij_betw_def by blast thus "embedS r r' f" unfolding embedS_def - using ISO by auto + using ISO by auto qed lemma iso_Field: "iso r r' f \ f ` (Field r) = Field r'" by (auto simp add: iso_def bij_betw_def) lemma iso_iff: -assumes "Well_order r" -shows "iso r r' f = (embed r r' f \ f ` (Field r) = Field r')" + assumes "Well_order r" + shows "iso r r' f = (embed r r' f \ f ` (Field r) = Field r')" proof assume "iso r r' f" thus "embed r r' f \ f ` (Field r) = Field r'" - by (auto simp add: iso_Field iso_def) + by (auto simp add: iso_Field iso_def) next assume *: "embed r r' f \ f ` Field r = Field r'" hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on) with * have "bij_betw f (Field r) (Field r')" - unfolding bij_betw_def by simp + unfolding bij_betw_def by simp with * show "iso r r' f" unfolding iso_def by auto qed lemma iso_iff2: "iso r r' f \ bij_betw f (Field r) (Field r') \ (\a \ Field r. \b \ Field r. (a, b) \ r \ (f a, f b) \ r')" - (is "?lhs = ?rhs") + (is "?lhs = ?rhs") proof assume L: ?lhs then have "bij_betw f (Field r) (Field r')" and emb: "embed r r' f" @@ -1047,31 +1047,31 @@ qed lemma iso_iff3: -assumes WELL: "Well_order r" and WELL': "Well_order r'" -shows "iso r r' f = (bij_betw f (Field r) (Field r') \ compat r r' f)" + assumes WELL: "Well_order r" and WELL': "Well_order r'" + shows "iso r r' f = (bij_betw f (Field r) (Field r') \ compat r r' f)" proof assume "iso r r' f" thus "bij_betw f (Field r) (Field r') \ compat r r' f" - unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def) + unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def) next have Well: "wo_rel r \ wo_rel r'" using WELL WELL' - by (auto simp add: wo_rel_def) + by (auto simp add: wo_rel_def) assume *: "bij_betw f (Field r) (Field r') \ compat r r' f" thus "iso r r' f" - unfolding "compat_def" using assms + unfolding "compat_def" using assms proof(auto simp add: iso_iff2) fix a b assume **: "a \ Field r" "b \ Field r" and - ***: "(f a, f b) \ r'" + ***: "(f a, f b) \ r'" {assume "(b,a) \ r \ b = a" - hence "(b,a) \ r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast - hence "(f b, f a) \ r'" using * unfolding compat_def by auto - hence "f a = f b" - using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast - hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto - hence "(a,b) \ r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast + hence "(b,a) \ r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast + hence "(f b, f a) \ r'" using * unfolding compat_def by auto + hence "f a = f b" + using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast + hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto + hence "(a,b) \ r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast } thus "(a,b) \ r" - using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast + using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast qed qed @@ -1098,12 +1098,7 @@ lemma iso_forward: assumes "(x,y) \ r" "iso r r' f" shows "(f x,f y) \ r'" -proof - - have "x \ Field r" "y \ Field r" - using assms by (auto simp: Field_def) - with assms show ?thesis unfolding iso_iff2 by blast -qed - + using assms by (auto simp: Field_def iso_iff2) lemma iso_trans: assumes "trans r" and iso: "iso r r' f" shows "trans r'" @@ -1112,7 +1107,7 @@ fix x y z assume xyz: "(x, y) \ r'" "(y, z) \ r'" then have *: "(inv_into (Field r) f x, inv_into (Field r) f y) \ r" - "(inv_into (Field r) f y, inv_into (Field r) f z) \ r" + "(inv_into (Field r) f y, inv_into (Field r) f z) \ r" using iso_backward [OF _ iso] by blast+ then have "inv_into (Field r) f x \ Field r" "inv_into (Field r) f y \ Field r" by (auto simp: Field_def) diff -r ec4c38e156c7 -r f881fd264929 src/HOL/BNF_Wellorder_Relation.thy --- a/src/HOL/BNF_Wellorder_Relation.thy Fri Jan 13 16:44:00 2023 +0000 +++ b/src/HOL/BNF_Wellorder_Relation.thy Fri Jan 13 22:47:40 2023 +0000 @@ -8,7 +8,7 @@ section \Well-Order Relations as Needed by Bounded Natural Functors\ theory BNF_Wellorder_Relation -imports Order_Relation + imports Order_Relation begin text\In this section, we develop basic concepts and results pertaining @@ -41,35 +41,35 @@ subsection \Auxiliaries\ lemma REFL: "Refl r" -using WELL order_on_defs[of _ r] by auto + using WELL order_on_defs[of _ r] by auto lemma TRANS: "trans r" -using WELL order_on_defs[of _ r] by auto + using WELL order_on_defs[of _ r] by auto lemma ANTISYM: "antisym r" -using WELL order_on_defs[of _ r] by auto + using WELL order_on_defs[of _ r] by auto lemma TOTAL: "Total r" -using WELL order_on_defs[of _ r] by auto + using WELL order_on_defs[of _ r] by auto lemma TOTALS: "\a \ Field r. \b \ Field r. (a,b) \ r \ (b,a) \ r" -using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force + using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force lemma LIN: "Linear_order r" -using WELL well_order_on_def[of _ r] by auto + using WELL well_order_on_def[of _ r] by auto lemma WF: "wf (r - Id)" -using WELL well_order_on_def[of _ r] by auto + using WELL well_order_on_def[of _ r] by auto lemma cases_Total: -"\ phi a b. \{a,b} <= Field r; ((a,b) \ r \ phi a b); ((b,a) \ r \ phi a b)\ + "\ phi a b. \{a,b} <= Field r; ((a,b) \ r \ phi a b); ((b,a) \ r \ phi a b)\ \ phi a b" -using TOTALS by auto + using TOTALS by auto lemma cases_Total3: -"\ phi a b. \{a,b} \ Field r; ((a,b) \ r - Id \ (b,a) \ r - Id \ phi a b); + "\ phi a b. \{a,b} \ Field r; ((a,b) \ r - Id \ (b,a) \ r - Id \ phi a b); (a = b \ phi a b)\ \ phi a b" -using TOTALS by auto + using TOTALS by auto subsection \Well-founded induction and recursion adapted to non-strict well-order relations\ @@ -81,34 +81,34 @@ having to take out the diagonal each time in order to switch to a well-founded relation.\ lemma well_order_induct: -assumes IND: "\x. \y. y \ x \ (y, x) \ r \ P y \ P x" -shows "P a" + assumes IND: "\x. \y. y \ x \ (y, x) \ r \ P y \ P x" + shows "P a" proof- have "\x. \y. (y, x) \ r - Id \ P y \ P x" - using IND by blast + using IND by blast thus "P a" using WF wf_induct[of "r - Id" P a] by blast qed definition -worec :: "(('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" -where -"worec F \ wfrec (r - Id) F" + worec :: "(('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" + where + "worec F \ wfrec (r - Id) F" definition -adm_wo :: "(('a \ 'b) \ 'a \ 'b) \ bool" -where -"adm_wo H \ \f g x. (\y \ underS x. f y = g y) \ H f x = H g x" + adm_wo :: "(('a \ 'b) \ 'a \ 'b) \ bool" + where + "adm_wo H \ \f g x. (\y \ underS x. f y = g y) \ H f x = H g x" lemma worec_fixpoint: -assumes ADM: "adm_wo H" -shows "worec H = H (worec H)" + assumes ADM: "adm_wo H" + shows "worec H = H (worec H)" proof- let ?rS = "r - Id" have "adm_wf (r - Id) H" - unfolding adm_wf_def - using ADM adm_wo_def[of H] underS_def[of r] by auto + unfolding adm_wf_def + using ADM adm_wo_def[of H] underS_def[of r] by auto hence "wfrec ?rS H = H (wfrec ?rS H)" - using WF wfrec_fixpoint[of ?rS H] by simp + using WF wfrec_fixpoint[of ?rS H] by simp thus ?thesis unfolding worec_def . qed @@ -127,97 +127,83 @@ Order filters for well-orders are also known as ``initial segments".\ definition max2 :: "'a \ 'a \ 'a" -where "max2 a b \ if (a,b) \ r then b else a" + where "max2 a b \ if (a,b) \ r then b else a" definition isMinim :: "'a set \ 'a \ bool" -where "isMinim A b \ b \ A \ (\a \ A. (b,a) \ r)" + where "isMinim A b \ b \ A \ (\a \ A. (b,a) \ r)" definition minim :: "'a set \ 'a" -where "minim A \ THE b. isMinim A b" + where "minim A \ THE b. isMinim A b" definition supr :: "'a set \ 'a" -where "supr A \ minim (Above A)" + where "supr A \ minim (Above A)" definition suc :: "'a set \ 'a" -where "suc A \ minim (AboveS A)" + where "suc A \ minim (AboveS A)" subsubsection \Properties of max2\ lemma max2_greater_among: -assumes "a \ Field r" and "b \ Field r" -shows "(a, max2 a b) \ r \ (b, max2 a b) \ r \ max2 a b \ {a,b}" + assumes "a \ Field r" and "b \ Field r" + shows "(a, max2 a b) \ r \ (b, max2 a b) \ r \ max2 a b \ {a,b}" proof- {assume "(a,b) \ r" - hence ?thesis using max2_def assms REFL refl_on_def - by (auto simp add: refl_on_def) + hence ?thesis using max2_def assms REFL refl_on_def + by (auto simp add: refl_on_def) } moreover {assume "a = b" - hence "(a,b) \ r" using REFL assms - by (auto simp add: refl_on_def) + hence "(a,b) \ r" using REFL assms + by (auto simp add: refl_on_def) } moreover {assume *: "a \ b \ (b,a) \ r" - hence "(a,b) \ r" using ANTISYM - by (auto simp add: antisym_def) - hence ?thesis using * max2_def assms REFL refl_on_def - by (auto simp add: refl_on_def) + hence "(a,b) \ r" using ANTISYM + by (auto simp add: antisym_def) + hence ?thesis using * max2_def assms REFL refl_on_def + by (auto simp add: refl_on_def) } ultimately show ?thesis using assms TOTAL - total_on_def[of "Field r" r] by blast + total_on_def[of "Field r" r] by blast qed lemma max2_greater: -assumes "a \ Field r" and "b \ Field r" -shows "(a, max2 a b) \ r \ (b, max2 a b) \ r" -using assms by (auto simp add: max2_greater_among) + assumes "a \ Field r" and "b \ Field r" + shows "(a, max2 a b) \ r \ (b, max2 a b) \ r" + using assms by (auto simp add: max2_greater_among) lemma max2_among: -assumes "a \ Field r" and "b \ Field r" -shows "max2 a b \ {a, b}" -using assms max2_greater_among[of a b] by simp + assumes "a \ Field r" and "b \ Field r" + shows "max2 a b \ {a, b}" + using assms max2_greater_among[of a b] by simp lemma max2_equals1: -assumes "a \ Field r" and "b \ Field r" -shows "(max2 a b = a) = ((b,a) \ r)" -using assms ANTISYM unfolding antisym_def using TOTALS -by(auto simp add: max2_def max2_among) + assumes "a \ Field r" and "b \ Field r" + shows "(max2 a b = a) = ((b,a) \ r)" + using assms ANTISYM unfolding antisym_def using TOTALS + by(auto simp add: max2_def max2_among) lemma max2_equals2: -assumes "a \ Field r" and "b \ Field r" -shows "(max2 a b = b) = ((a,b) \ r)" -using assms ANTISYM unfolding antisym_def using TOTALS -unfolding max2_def by auto + assumes "a \ Field r" and "b \ Field r" + shows "(max2 a b = b) = ((a,b) \ r)" + using assms ANTISYM unfolding antisym_def using TOTALS + unfolding max2_def by auto lemma in_notinI: -assumes "(j,i) \ r \ j = i" and "i \ Field r" and "j \ Field r" -shows "(i,j) \ r" using assms max2_def max2_greater_among by fastforce + assumes "(j,i) \ r \ j = i" and "i \ Field r" and "j \ Field r" + shows "(i,j) \ r" using assms max2_def max2_greater_among by fastforce subsubsection \Existence and uniqueness for isMinim and well-definedness of minim\ lemma isMinim_unique: -assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'" -shows "a = a'" -proof- - {have "a \ B" - using MINIM isMinim_def by simp - hence "(a',a) \ r" - using MINIM' isMinim_def by simp - } - moreover - {have "a' \ B" - using MINIM' isMinim_def by simp - hence "(a,a') \ r" - using MINIM isMinim_def by simp - } - ultimately - show ?thesis using ANTISYM antisym_def[of r] by blast -qed + assumes "isMinim B a" "isMinim B a'" + shows "a = a'" + using assms ANTISYM antisym_def[of r] by (auto simp: isMinim_def) lemma Well_order_isMinim_exists: -assumes SUB: "B \ Field r" and NE: "B \ {}" -shows "\b. isMinim B b" + assumes SUB: "B \ Field r" and NE: "B \ {}" + shows "\b. isMinim B b" proof- from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where *: "b \ B \ (\b'. b' \ b \ (b',b) \ r \ b' \ B)" by auto @@ -232,52 +218,46 @@ moreover have "b' = b \ (b, b') \ r" using ** REFL by (auto simp add: refl_on_def) moreover have "b' \ b \ (b',b) \ r \ (b,b') \ r" - using ** TOTAL by (auto simp add: total_on_def) + using ** TOTAL by (auto simp add: total_on_def) ultimately show "(b,b') \ r" by blast qed qed - then have "isMinim B b" + then show ?thesis unfolding isMinim_def using * by auto - then show ?thesis - by auto qed lemma minim_isMinim: -assumes SUB: "B \ Field r" and NE: "B \ {}" -shows "isMinim B (minim B)" + assumes SUB: "B \ Field r" and NE: "B \ {}" + shows "isMinim B (minim B)" proof- let ?phi = "(\ b. isMinim B b)" from assms Well_order_isMinim_exists obtain b where *: "?phi b" by blast moreover have "\ b'. ?phi b' \ b' = b" - using isMinim_unique * by auto + using isMinim_unique * by auto ultimately show ?thesis - unfolding minim_def using theI[of ?phi b] by blast + unfolding minim_def using theI[of ?phi b] by blast qed subsubsection\Properties of minim\ lemma minim_in: -assumes "B \ Field r" and "B \ {}" -shows "minim B \ B" -proof- - from minim_isMinim[of B] assms - have "isMinim B (minim B)" by simp - thus ?thesis by (simp add: isMinim_def) -qed + assumes "B \ Field r" and "B \ {}" + shows "minim B \ B" + using assms minim_isMinim[of B] by (auto simp: isMinim_def) lemma minim_inField: -assumes "B \ Field r" and "B \ {}" -shows "minim B \ Field r" + assumes "B \ Field r" and "B \ {}" + shows "minim B \ Field r" proof- have "minim B \ B" using assms by (simp add: minim_in) thus ?thesis using assms by blast qed lemma minim_least: -assumes SUB: "B \ Field r" and IN: "b \ B" -shows "(minim B, b) \ r" + assumes SUB: "B \ Field r" and IN: "b \ B" + shows "(minim B, b) \ r" proof- from minim_isMinim[of B] assms have "isMinim B (minim B)" by auto @@ -285,137 +265,104 @@ qed lemma equals_minim: -assumes SUB: "B \ Field r" and IN: "a \ B" and - LEAST: "\ b. b \ B \ (a,b) \ r" -shows "a = minim B" + assumes SUB: "B \ Field r" and IN: "a \ B" and + LEAST: "\ b. b \ B \ (a,b) \ r" + shows "a = minim B" proof- from minim_isMinim[of B] assms have "isMinim B (minim B)" by auto moreover have "isMinim B a" using IN LEAST isMinim_def by auto ultimately show ?thesis - using isMinim_unique by auto + using isMinim_unique by auto qed subsubsection\Properties of successor\ lemma suc_AboveS: -assumes SUB: "B \ Field r" and ABOVES: "AboveS B \ {}" -shows "suc B \ AboveS B" + assumes SUB: "B \ Field r" and ABOVES: "AboveS B \ {}" + shows "suc B \ AboveS B" proof(unfold suc_def) have "AboveS B \ Field r" - using AboveS_Field[of r] by auto + using AboveS_Field[of r] by auto thus "minim (AboveS B) \ AboveS B" - using assms by (simp add: minim_in) + using assms by (simp add: minim_in) qed lemma suc_greater: -assumes SUB: "B \ Field r" and ABOVES: "AboveS B \ {}" and - IN: "b \ B" -shows "suc B \ b \ (b,suc B) \ r" -proof- - from assms suc_AboveS - have "suc B \ AboveS B" by simp - with IN AboveS_def[of r] show ?thesis by simp -qed + assumes SUB: "B \ Field r" and ABOVES: "AboveS B \ {}" and IN: "b \ B" + shows "suc B \ b \ (b,suc B) \ r" + using IN AboveS_def[of r] assms suc_AboveS by auto lemma suc_least_AboveS: -assumes ABOVES: "a \ AboveS B" -shows "(suc B,a) \ r" -proof(unfold suc_def) - have "AboveS B \ Field r" - using AboveS_Field[of r] by auto - thus "(minim (AboveS B),a) \ r" - using assms minim_least by simp -qed + assumes ABOVES: "a \ AboveS B" + shows "(suc B,a) \ r" + using assms minim_least AboveS_Field[of r] by (auto simp: suc_def) lemma suc_inField: -assumes "B \ Field r" and "AboveS B \ {}" -shows "suc B \ Field r" -proof- - have "suc B \ AboveS B" using suc_AboveS assms by simp - thus ?thesis - using assms AboveS_Field[of r] by auto -qed + assumes "B \ Field r" and "AboveS B \ {}" + shows "suc B \ Field r" + using suc_AboveS assms AboveS_Field[of r] by auto lemma equals_suc_AboveS: -assumes SUB: "B \ Field r" and ABV: "a \ AboveS B" and - MINIM: "\ a'. a' \ AboveS B \ (a,a') \ r" -shows "a = suc B" -proof(unfold suc_def) - have "AboveS B \ Field r" - using AboveS_Field[of r B] by auto - thus "a = minim (AboveS B)" - using assms equals_minim - by simp -qed + assumes "B \ Field r" and "a \ AboveS B" and "\ a'. a' \ AboveS B \ (a,a') \ r" + shows "a = suc B" + using assms equals_minim AboveS_Field[of r B] by (auto simp: suc_def) lemma suc_underS: -assumes IN: "a \ Field r" -shows "a = suc (underS a)" + assumes IN: "a \ Field r" + shows "a = suc (underS a)" proof- have "underS a \ Field r" - using underS_Field[of r] by auto + using underS_Field[of r] by auto moreover have "a \ AboveS (underS a)" - using in_AboveS_underS IN by fast + using in_AboveS_underS IN by fast moreover have "\a' \ AboveS (underS a). (a,a') \ r" proof(clarify) fix a' assume *: "a' \ AboveS (underS a)" hence **: "a' \ Field r" - using AboveS_Field by fast + using AboveS_Field by fast {assume "(a,a') \ r" - hence "a' = a \ (a',a) \ r" - using TOTAL IN ** by (auto simp add: total_on_def) - moreover - {assume "a' = a" - hence "(a,a') \ r" - using REFL IN ** by (auto simp add: refl_on_def) - } - moreover - {assume "a' \ a \ (a',a) \ r" - hence "a' \ underS a" - unfolding underS_def by simp - hence "a' \ AboveS (underS a)" - using AboveS_disjoint by fast - with * have False by simp - } - ultimately have "(a,a') \ r" by blast + hence "a' = a \ (a',a) \ r" + using TOTAL IN ** by (auto simp add: total_on_def) + moreover + {assume "a' = a" + hence "(a,a') \ r" + using REFL IN ** by (auto simp add: refl_on_def) + } + moreover + {assume "a' \ a \ (a',a) \ r" + hence "a' \ underS a" + unfolding underS_def by simp + hence "a' \ AboveS (underS a)" + using AboveS_disjoint by fast + with * have False by simp + } + ultimately have "(a,a') \ r" by blast } thus "(a, a') \ r" by blast qed ultimately show ?thesis - using equals_suc_AboveS by auto + using equals_suc_AboveS by auto qed subsubsection \Properties of order filters\ -lemma under_ofilter: -"ofilter (under a)" -proof - - have "\aa x. (aa, a) \ r \ (x, aa) \ r \ (x, a) \ r" - proof - - fix aa x - assume "(aa,a) \ r" "(x,aa) \ r" - then show "(x,a) \ r" - using TRANS trans_def[of r] by blast - qed - then show ?thesis unfolding ofilter_def under_def - by (auto simp add: Field_def) -qed +lemma under_ofilter: "ofilter (under a)" + using TRANS by (auto simp: ofilter_def under_def Field_iff trans_def) -lemma underS_ofilter: -"ofilter (underS a)" +lemma underS_ofilter: "ofilter (underS a)" unfolding ofilter_def underS_def under_def proof safe - fix aa assume "(a, aa) \ r" "(aa, a) \ r" and DIFF: "aa \ a" + fix b assume "(a, b) \ r" "(b, a) \ r" and DIFF: "b \ a" thus False - using ANTISYM antisym_def[of r] by blast + using ANTISYM antisym_def[of r] by blast next - fix aa x - assume "(aa,a) \ r" "aa \ a" "(x,aa) \ r" + fix b x + assume "(b,a) \ r" "b \ a" "(x,b) \ r" thus "(x,a) \ r" using TRANS trans_def[of r] by blast next @@ -427,15 +374,15 @@ qed lemma Field_ofilter: -"ofilter (Field r)" -by(unfold ofilter_def under_def, auto simp add: Field_def) + "ofilter (Field r)" + by(unfold ofilter_def under_def, auto simp add: Field_def) lemma ofilter_underS_Field: -"ofilter A = ((\a \ Field r. A = underS a) \ (A = Field r))" + "ofilter A = ((\a \ Field r. A = underS a) \ (A = Field r))" proof assume "(\a\Field r. A = underS a) \ A = Field r" thus "ofilter A" - by (auto simp: underS_ofilter Field_ofilter) + by (auto simp: underS_ofilter Field_ofilter) next assume *: "ofilter A" let ?One = "(\a\Field r. A = underS a)" @@ -451,7 +398,7 @@ have 3: "?a \ ?B" using minim_in[of ?B] 1 by blast hence 4: "?a \ A" by blast have 5: "A \ Field r" using * ofilter_def by auto - (* *) + (* *) moreover have "A = underS ?a" proof @@ -462,12 +409,12 @@ have 12: "x \ ?a" using 4 ** by auto have 13: "under x \ A" using * ofilter_def ** by auto {assume "(x,?a) \ r" - hence "(?a,x) \ r" - using TOTAL total_on_def[of "Field r" r] - 2 4 11 12 by auto - hence "?a \ under x" using under_def[of r] by auto - hence "?a \ A" using ** 13 by blast - with 4 have False by simp + hence "(?a,x) \ r" + using TOTAL total_on_def[of "Field r" r] + 2 4 11 12 by auto + hence "?a \ under x" using under_def[of r] by auto + hence "?a \ A" using ** 13 by blast + with 4 have False by simp } then have "(x,?a) \ r" by blast thus "x \ underS ?a" @@ -479,13 +426,13 @@ fix x assume **: "x \ underS ?a" hence 11: "x \ Field r" - using Field_def unfolding underS_def by fastforce - {assume "x \ A" + using Field_def unfolding underS_def by fastforce + {assume "x \ A" hence "x \ ?B" using 11 by auto hence "(?a,x) \ r" using 3 minim_least[of ?B x] by blast hence False - using ANTISYM antisym_def[of r] ** unfolding underS_def by auto - } + using ANTISYM antisym_def[of r] ** unfolding underS_def by auto + } thus "x \ A" by blast qed qed @@ -499,27 +446,27 @@ qed lemma ofilter_UNION: -"(\ i. i \ I \ ofilter(A i)) \ ofilter (\i \ I. A i)" -unfolding ofilter_def by blast + "(\ i. i \ I \ ofilter(A i)) \ ofilter (\i \ I. A i)" + unfolding ofilter_def by blast lemma ofilter_under_UNION: -assumes "ofilter A" -shows "A = (\a \ A. under a)" + assumes "ofilter A" + shows "A = (\a \ A. under a)" proof have "\a \ A. under a \ A" - using assms ofilter_def by auto + using assms ofilter_def by auto thus "(\a \ A. under a) \ A" by blast next have "\a \ A. a \ under a" - using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast + using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast thus "A \ (\a \ A. under a)" by blast qed subsubsection\Other properties\ lemma ofilter_linord: -assumes OF1: "ofilter A" and OF2: "ofilter B" -shows "A \ B \ B \ A" + assumes OF1: "ofilter A" and OF2: "ofilter B" + shows "A \ B \ B \ A" proof(cases "A = Field r") assume Case1: "A = Field r" hence "B \ A" using OF2 ofilter_def by auto @@ -527,7 +474,7 @@ next assume Case2: "A \ Field r" with ofilter_underS_Field OF1 obtain a where - 1: "a \ Field r \ A = underS a" by auto + 1: "a \ Field r \ A = underS a" by auto show ?thesis proof(cases "B = Field r") assume Case21: "B = Field r" @@ -536,68 +483,68 @@ next assume Case22: "B \ Field r" with ofilter_underS_Field OF2 obtain b where - 2: "b \ Field r \ B = underS b" by auto + 2: "b \ Field r \ B = underS b" by auto have "a = b \ (a,b) \ r \ (b,a) \ r" - using 1 2 TOTAL total_on_def[of _ r] by auto + using 1 2 TOTAL total_on_def[of _ r] by auto moreover {assume "a = b" with 1 2 have ?thesis by auto } moreover {assume "(a,b) \ r" - with underS_incr[of r] TRANS ANTISYM 1 2 - have "A \ B" by auto - hence ?thesis by auto + with underS_incr[of r] TRANS ANTISYM 1 2 + have "A \ B" by auto + hence ?thesis by auto } moreover - {assume "(b,a) \ r" - with underS_incr[of r] TRANS ANTISYM 1 2 - have "B \ A" by auto - hence ?thesis by auto + {assume "(b,a) \ r" + with underS_incr[of r] TRANS ANTISYM 1 2 + have "B \ A" by auto + hence ?thesis by auto } ultimately show ?thesis by blast qed qed lemma ofilter_AboveS_Field: -assumes "ofilter A" -shows "A \ (AboveS A) = Field r" + assumes "ofilter A" + shows "A \ (AboveS A) = Field r" proof show "A \ (AboveS A) \ Field r" - using assms ofilter_def AboveS_Field[of r] by auto + using assms ofilter_def AboveS_Field[of r] by auto next {fix x assume *: "x \ Field r" and **: "x \ A" - {fix y assume ***: "y \ A" - with ** have 1: "y \ x" by auto - {assume "(y,x) \ r" - moreover - have "y \ Field r" using assms ofilter_def *** by auto - ultimately have "(x,y) \ r" - using 1 * TOTAL total_on_def[of _ r] by auto - with *** assms ofilter_def under_def[of r] have "x \ A" by auto - with ** have False by contradiction + {fix y assume ***: "y \ A" + with ** have 1: "y \ x" by auto + {assume "(y,x) \ r" + moreover + have "y \ Field r" using assms ofilter_def *** by auto + ultimately have "(x,y) \ r" + using 1 * TOTAL total_on_def[of _ r] by auto + with *** assms ofilter_def under_def[of r] have "x \ A" by auto + with ** have False by contradiction + } + hence "(y,x) \ r" by blast + with 1 have "y \ x \ (y,x) \ r" by auto } - hence "(y,x) \ r" by blast - with 1 have "y \ x \ (y,x) \ r" by auto - } - with * have "x \ AboveS A" unfolding AboveS_def by auto + with * have "x \ AboveS A" unfolding AboveS_def by auto } thus "Field r \ A \ (AboveS A)" by blast qed lemma suc_ofilter_in: -assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \ {}" and - REL: "(b,suc A) \ r" and DIFF: "b \ suc A" -shows "b \ A" + assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \ {}" and + REL: "(b,suc A) \ r" and DIFF: "b \ suc A" + shows "b \ A" proof- have *: "suc A \ Field r \ b \ Field r" - using WELL REL well_order_on_domain[of "Field r"] by auto + using WELL REL well_order_on_domain[of "Field r"] by auto {assume **: "b \ A" - hence "b \ AboveS A" - using OF * ofilter_AboveS_Field by auto - hence "(suc A, b) \ r" - using suc_least_AboveS by auto - hence False using REL DIFF ANTISYM * - by (auto simp add: antisym_def) + hence "b \ AboveS A" + using OF * ofilter_AboveS_Field by auto + hence "(suc A, b) \ r" + using suc_least_AboveS by auto + hence False using REL DIFF ANTISYM * + by (auto simp add: antisym_def) } thus ?thesis by blast qed diff -r ec4c38e156c7 -r f881fd264929 src/HOL/Cardinals/Wellorder_Constructions.thy --- a/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jan 13 16:44:00 2023 +0000 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jan 13 22:47:40 2023 +0000 @@ -182,7 +182,7 @@ subsection \The maxim among a finite set of ordinals\ -text \The correct phrasing would be ``a maxim of \", as \\o\ is only a preorder.\ +text \The correct phrasing would be ``a maxim of ...", as \\o\ is only a preorder.\ definition isOmax :: "'a rel set \ 'a rel \ bool" where @@ -211,23 +211,19 @@ next case False 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'" - then have "r' \o r" - by (metis "***" Case22 insert_iff isOmax_def ordLeq_transitive p ordLeq_reflexive) - } - 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 + hence "Well_order p" using **** unfolding isOmax_def by simp + then consider "r \o p" | "p \o r" + using *** ordLeq_total by auto + then show ?thesis + proof cases + case 1 + then show ?thesis + using p unfolding isOmax_def by auto + next + case 2 + then show ?thesis + by (metis "***" insert_iff isOmax_def ordLeq_reflexive ordLeq_transitive p) + qed qed qed thus ?thesis using assms by auto