# HG changeset patch # User blanchet # Date 1384985646 -3600 # Node ID 483131676087620895373bcdd5b465c8747effb2 # Parent 7d23f8e501d4bcdab690a7f949023700a16d0c49 effectively reverted d25fc4c0ff62, to avoid quasi-cyclic dependencies with HOL-Cardinals and minimize BNF dependencies diff -r 7d23f8e501d4 -r 483131676087 src/HOL/Cardinals/Cardinals.thy --- a/src/HOL/Cardinals/Cardinals.thy Wed Nov 20 21:28:58 2013 +0100 +++ b/src/HOL/Cardinals/Cardinals.thy Wed Nov 20 23:14:06 2013 +0100 @@ -9,7 +9,7 @@ header {* Theory of Ordinals and Cardinals *} theory Cardinals -imports Cardinal_Order_Relation Cardinal_Arithmetic +imports Cardinal_Order_Relation Cardinal_Arithmetic Wellorder_Extension begin end diff -r 7d23f8e501d4 -r 483131676087 src/HOL/Cardinals/Constructions_on_Wellorders.thy --- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Wed Nov 20 21:28:58 2013 +0100 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Wed Nov 20 23:14:06 2013 +0100 @@ -8,7 +8,7 @@ header {* Constructions on Wellorders *} theory Constructions_on_Wellorders -imports Constructions_on_Wellorders_FP Wellorder_Embedding +imports Constructions_on_Wellorders_FP Wellorder_Embedding Order_Union begin declare diff -r 7d23f8e501d4 -r 483131676087 src/HOL/Cardinals/Order_Union.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Cardinals/Order_Union.thy Wed Nov 20 23:14:06 2013 +0100 @@ -0,0 +1,370 @@ +(* Title: HOL/Cardinals/Order_Union.thy + Author: Andrei Popescu, TU Muenchen + +The ordinal-like sum of two orders with disjoint fields +*) + +header {* Order Union *} + +theory Order_Union +imports Wellfounded_More_FP +begin + +definition Osum :: "'a rel \ 'a rel \ 'a rel" (infix "Osum" 60) where + "r Osum r' = r \ r' \ {(a, a'). a \ Field r \ a' \ Field r'}" + +notation Osum (infix "\o" 60) + +lemma Field_Osum: "Field (r \o r') = Field r \ Field r'" + unfolding Osum_def Field_def by blast + +lemma Osum_wf: +assumes FLD: "Field r Int Field r' = {}" and + WF: "wf r" and WF': "wf r'" +shows "wf (r Osum r')" +unfolding wf_eq_minimal2 unfolding Field_Osum +proof(intro allI impI, elim conjE) + fix A assume *: "A \ Field r \ Field r'" and **: "A \ {}" + obtain B where B_def: "B = A Int Field r" by blast + show "\a\A. \a'\A. (a', a) \ r \o r'" + proof(cases "B = {}") + assume Case1: "B \ {}" + hence "B \ {} \ B \ Field r" using B_def by auto + then obtain a where 1: "a \ B" and 2: "\a1 \ B. (a1,a) \ r" + using WF unfolding wf_eq_minimal2 by metis + hence 3: "a \ Field r \ a \ Field r'" using B_def FLD by auto + (* *) + have "\a1 \ A. (a1,a) \ r Osum r'" + proof(intro ballI) + fix a1 assume **: "a1 \ A" + {assume Case11: "a1 \ Field r" + hence "(a1,a) \ r" using B_def ** 2 by auto + moreover + have "(a1,a) \ r'" using 3 by (auto simp add: Field_def) + ultimately have "(a1,a) \ r Osum r'" + using 3 unfolding Osum_def by auto + } + moreover + {assume Case12: "a1 \ Field r" + hence "(a1,a) \ r" unfolding Field_def by auto + moreover + have "(a1,a) \ r'" using 3 unfolding Field_def by auto + ultimately have "(a1,a) \ r Osum r'" + using 3 unfolding Osum_def by auto + } + ultimately show "(a1,a) \ r Osum r'" by blast + qed + thus ?thesis using 1 B_def by auto + next + assume Case2: "B = {}" + hence 1: "A \ {} \ A \ Field r'" using * ** B_def by auto + then obtain a' where 2: "a' \ A" and 3: "\a1' \ A. (a1',a') \ r'" + using WF' unfolding wf_eq_minimal2 by metis + hence 4: "a' \ Field r' \ a' \ Field r" using 1 FLD by blast + (* *) + have "\a1' \ A. (a1',a') \ r Osum r'" + proof(unfold Osum_def, auto simp add: 3) + fix a1' assume "(a1', a') \ r" + thus False using 4 unfolding Field_def by blast + next + fix a1' assume "a1' \ A" and "a1' \ Field r" + thus False using Case2 B_def by auto + qed + thus ?thesis using 2 by blast + qed +qed + +lemma Osum_Refl: +assumes FLD: "Field r Int Field r' = {}" and + REFL: "Refl r" and REFL': "Refl r'" +shows "Refl (r Osum r')" +using assms +unfolding refl_on_def Field_Osum unfolding Osum_def by blast + +lemma Osum_trans: +assumes FLD: "Field r Int Field r' = {}" and + TRANS: "trans r" and TRANS': "trans r'" +shows "trans (r Osum r')" +proof(unfold trans_def, auto) + fix x y z assume *: "(x, y) \ r \o r'" and **: "(y, z) \ r \o r'" + show "(x, z) \ r \o r'" + proof- + {assume Case1: "(x,y) \ r" + hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto + have ?thesis + proof- + {assume Case11: "(y,z) \ r" + hence "(x,z) \ r" using Case1 TRANS trans_def[of r] by blast + hence ?thesis unfolding Osum_def by auto + } + moreover + {assume Case12: "(y,z) \ r'" + hence "y \ Field r'" unfolding Field_def by auto + hence False using FLD 1 by auto + } + moreover + {assume Case13: "z \ Field r'" + hence ?thesis using 1 unfolding Osum_def by auto + } + ultimately show ?thesis using ** unfolding Osum_def by blast + qed + } + moreover + {assume Case2: "(x,y) \ r'" + hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto + have ?thesis + proof- + {assume Case21: "(y,z) \ r" + hence "y \ Field r" unfolding Field_def by auto + hence False using FLD 2 by auto + } + moreover + {assume Case22: "(y,z) \ r'" + hence "(x,z) \ r'" using Case2 TRANS' trans_def[of r'] by blast + hence ?thesis unfolding Osum_def by auto + } + moreover + {assume Case23: "y \ Field r" + hence False using FLD 2 by auto + } + ultimately show ?thesis using ** unfolding Osum_def by blast + qed + } + moreover + {assume Case3: "x \ Field r \ y \ Field r'" + have ?thesis + proof- + {assume Case31: "(y,z) \ r" + hence "y \ Field r" unfolding Field_def by auto + hence False using FLD Case3 by auto + } + moreover + {assume Case32: "(y,z) \ r'" + hence "z \ Field r'" unfolding Field_def by blast + hence ?thesis unfolding Osum_def using Case3 by auto + } + moreover + {assume Case33: "y \ Field r" + hence False using FLD Case3 by auto + } + ultimately show ?thesis using ** unfolding Osum_def by blast + qed + } + ultimately show ?thesis using * unfolding Osum_def by blast + qed +qed + +lemma Osum_Preorder: +"\Field r Int Field r' = {}; Preorder r; Preorder r'\ \ Preorder (r Osum r')" +unfolding preorder_on_def using Osum_Refl Osum_trans by blast + +lemma Osum_antisym: +assumes FLD: "Field r Int Field r' = {}" and + AN: "antisym r" and AN': "antisym r'" +shows "antisym (r Osum r')" +proof(unfold antisym_def, auto) + fix x y assume *: "(x, y) \ r \o r'" and **: "(y, x) \ r \o r'" + show "x = y" + proof- + {assume Case1: "(x,y) \ r" + hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto + have ?thesis + proof- + have "(y,x) \ r \ ?thesis" + using Case1 AN antisym_def[of r] by blast + moreover + {assume "(y,x) \ r'" + hence "y \ Field r'" unfolding Field_def by auto + hence False using FLD 1 by auto + } + moreover + have "x \ Field r' \ False" using FLD 1 by auto + ultimately show ?thesis using ** unfolding Osum_def by blast + qed + } + moreover + {assume Case2: "(x,y) \ r'" + hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto + have ?thesis + proof- + {assume "(y,x) \ r" + hence "y \ Field r" unfolding Field_def by auto + hence False using FLD 2 by auto + } + moreover + have "(y,x) \ r' \ ?thesis" + using Case2 AN' antisym_def[of r'] by blast + moreover + {assume "y \ Field r" + hence False using FLD 2 by auto + } + ultimately show ?thesis using ** unfolding Osum_def by blast + qed + } + moreover + {assume Case3: "x \ Field r \ y \ Field r'" + have ?thesis + proof- + {assume "(y,x) \ r" + hence "y \ Field r" unfolding Field_def by auto + hence False using FLD Case3 by auto + } + moreover + {assume Case32: "(y,x) \ r'" + hence "x \ Field r'" unfolding Field_def by blast + hence False using FLD Case3 by auto + } + moreover + have "\ y \ Field r" using FLD Case3 by auto + ultimately show ?thesis using ** unfolding Osum_def by blast + qed + } + ultimately show ?thesis using * unfolding Osum_def by blast + qed +qed + +lemma Osum_Partial_order: +"\Field r Int Field r' = {}; Partial_order r; Partial_order r'\ \ + Partial_order (r Osum r')" +unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blast + +lemma Osum_Total: +assumes FLD: "Field r Int Field r' = {}" and + TOT: "Total r" and TOT': "Total r'" +shows "Total (r Osum r')" +using assms +unfolding total_on_def Field_Osum unfolding Osum_def by blast + +lemma Osum_Linear_order: +"\Field r Int Field r' = {}; Linear_order r; Linear_order r'\ \ + Linear_order (r Osum r')" +unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast + +lemma Osum_minus_Id1: +assumes "r \ Id" +shows "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" +proof- + let ?Left = "(r Osum r') - Id" + let ?Right = "(r' - Id) \ (Field r \ Field r')" + {fix a::'a and b assume *: "(a,b) \ Id" + {assume "(a,b) \ r" + with * have False using assms by auto + } + moreover + {assume "(a,b) \ r'" + with * have "(a,b) \ r' - Id" by auto + } + ultimately + have "(a,b) \ ?Left \ (a,b) \ ?Right" + unfolding Osum_def by auto + } + thus ?thesis by auto +qed + +lemma Osum_minus_Id2: +assumes "r' \ Id" +shows "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" +proof- + let ?Left = "(r Osum r') - Id" + let ?Right = "(r - Id) \ (Field r \ Field r')" + {fix a::'a and b assume *: "(a,b) \ Id" + {assume "(a,b) \ r'" + with * have False using assms by auto + } + moreover + {assume "(a,b) \ r" + with * have "(a,b) \ r - Id" by auto + } + ultimately + have "(a,b) \ ?Left \ (a,b) \ ?Right" + unfolding Osum_def by auto + } + thus ?thesis by auto +qed + +lemma Osum_minus_Id: +assumes TOT: "Total r" and TOT': "Total r'" and + NID: "\ (r \ Id)" and NID': "\ (r' \ Id)" +shows "(r Osum r') - Id \ (r - Id) Osum (r' - Id)" +proof- + {fix a a' assume *: "(a,a') \ (r Osum r')" and **: "a \ a'" + have "(a,a') \ (r - Id) Osum (r' - Id)" + proof- + {assume "(a,a') \ r \ (a,a') \ r'" + with ** have ?thesis unfolding Osum_def by auto + } + moreover + {assume "a \ Field r \ a' \ Field r'" + hence "a \ Field(r - Id) \ a' \ Field (r' - Id)" + using assms Total_Id_Field by blast + hence ?thesis unfolding Osum_def by auto + } + ultimately show ?thesis using * unfolding Osum_def by fast + qed + } + thus ?thesis by(auto simp add: Osum_def) +qed + +lemma wf_Int_Times: +assumes "A Int B = {}" +shows "wf(A \ B)" +unfolding wf_def using assms by blast + +lemma Osum_wf_Id: +assumes TOT: "Total r" and TOT': "Total r'" and + FLD: "Field r Int Field r' = {}" and + WF: "wf(r - Id)" and WF': "wf(r' - Id)" +shows "wf ((r Osum r') - Id)" +proof(cases "r \ Id \ r' \ Id") + assume Case1: "\(r \ Id \ r' \ Id)" + have "Field(r - Id) Int Field(r' - Id) = {}" + using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r'] + Diff_subset[of r Id] Diff_subset[of r' Id] by blast + thus ?thesis + using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"] + wf_subset[of "(r - Id) \o (r' - Id)" "(r Osum r') - Id"] by auto +next + have 1: "wf(Field r \ Field r')" + using FLD by (auto simp add: wf_Int_Times) + assume Case2: "r \ Id \ r' \ Id" + moreover + {assume Case21: "r \ Id" + hence "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" + using Osum_minus_Id1[of r r'] by simp + moreover + {have "Domain(Field r \ Field r') Int Range(r' - Id) = {}" + using FLD unfolding Field_def by blast + hence "wf((r' - Id) \ (Field r \ Field r'))" + using 1 WF' wf_Un[of "Field r \ Field r'" "r' - Id"] + by (auto simp add: Un_commute) + } + ultimately have ?thesis by (metis wf_subset) + } + moreover + {assume Case22: "r' \ Id" + hence "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" + using Osum_minus_Id2[of r' r] by simp + moreover + {have "Range(Field r \ Field r') Int Domain(r - Id) = {}" + using FLD unfolding Field_def by blast + hence "wf((r - Id) \ (Field r \ Field r'))" + using 1 WF wf_Un[of "r - Id" "Field r \ Field r'"] + by (auto simp add: Un_commute) + } + ultimately have ?thesis by (metis wf_subset) + } + ultimately show ?thesis by blast +qed + +lemma Osum_Well_order: +assumes FLD: "Field r Int Field r' = {}" and + WELL: "Well_order r" and WELL': "Well_order r'" +shows "Well_order (r Osum r')" +proof- + have "Total r \ Total r'" using WELL WELL' + by (auto simp add: order_on_defs) + thus ?thesis using assms unfolding well_order_on_def + using Osum_Linear_order Osum_wf_Id by blast +qed + +end diff -r 7d23f8e501d4 -r 483131676087 src/HOL/Cardinals/Wellorder_Extension.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy Wed Nov 20 23:14:06 2013 +0100 @@ -0,0 +1,213 @@ +(* Title: HOL/Cardinals/Wellorder_Extension.thy + Author: Christian Sternagel, JAIST +*) + +header {* Extending Well-founded Relations to Wellorders *} + +theory Wellorder_Extension +imports "~~/src/HOL/Library/Zorn" Order_Union +begin + +subsection {* Extending Well-founded Relations to Wellorders *} + +text {*A \emph{downset} (also lower set, decreasing set, initial segment, or +downward closed set) is closed w.r.t.\ smaller elements.*} +definition downset_on where + "downset_on A r = (\x y. (x, y) \ r \ y \ A \ x \ A)" + +(* +text {*Connection to order filters of the @{theory Cardinals} theory.*} +lemma (in wo_rel) ofilter_downset_on_conv: + "ofilter A \ downset_on A r \ A \ Field r" + by (auto simp: downset_on_def ofilter_def under_def) +*) + +lemma downset_onI: + "(\x y. (x, y) \ r \ y \ A \ x \ A) \ downset_on A r" + by (auto simp: downset_on_def) + +lemma downset_onD: + "downset_on A r \ (x, y) \ r \ y \ A \ x \ A" + unfolding downset_on_def by blast + +text {*Extensions of relations w.r.t.\ a given set.*} +definition extension_on where + "extension_on A r s = (\x\A. \y\A. (x, y) \ s \ (x, y) \ r)" + +lemma extension_onI: + "(\x y. \x \ A; y \ A; (x, y) \ s\ \ (x, y) \ r) \ extension_on A r s" + by (auto simp: extension_on_def) + +lemma extension_onD: + "extension_on A r s \ x \ A \ y \ A \ (x, y) \ s \ (x, y) \ r" + by (auto simp: extension_on_def) + +lemma downset_on_Union: + assumes "\r. r \ R \ downset_on (Field r) p" + shows "downset_on (Field (\R)) p" + using assms by (auto intro: downset_onI dest: downset_onD) + +lemma chain_subset_extension_on_Union: + assumes "chain\<^sub>\ R" and "\r. r \ R \ extension_on (Field r) r p" + shows "extension_on (Field (\R)) (\R) p" + using assms + by (simp add: chain_subset_def extension_on_def) + (metis (no_types) mono_Field set_mp) + +lemma downset_on_empty [simp]: "downset_on {} p" + by (auto simp: downset_on_def) + +lemma extension_on_empty [simp]: "extension_on {} p q" + by (auto simp: extension_on_def) + +text {*Every well-founded relation can be extended to a wellorder.*} +theorem well_order_extension: + assumes "wf p" + shows "\w. p \ w \ Well_order w" +proof - + let ?K = "{r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p}" + def I \ "init_seg_of \ ?K \ ?K" + have I_init: "I \ init_seg_of" by (simp add: I_def) + then have subch: "\R. R \ Chains I \ chain\<^sub>\ R" + by (auto simp: init_seg_of_def chain_subset_def Chains_def) + have Chains_wo: "\R r. R \ Chains I \ r \ R \ + Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p" + by (simp add: Chains_def I_def) blast + have FI: "Field I = ?K" by (auto simp: I_def init_seg_of_def Field_def) + then have 0: "Partial_order I" + by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def + trans_def I_def elim: trans_init_seg_of) + { fix R assume "R \ Chains I" + then have Ris: "R \ Chains init_seg_of" using mono_Chains [OF I_init] by blast + have subch: "chain\<^sub>\ R" using `R \ Chains I` I_init + by (auto simp: init_seg_of_def chain_subset_def Chains_def) + have "\r\R. Refl r" and "\r\R. trans r" and "\r\R. antisym r" and + "\r\R. Total r" and "\r\R. wf (r - Id)" and + "\r. r \ R \ downset_on (Field r) p" and + "\r. r \ R \ extension_on (Field r) r p" + using Chains_wo [OF `R \ Chains I`] by (simp_all add: order_on_defs) + have "Refl (\R)" using `\r\R. Refl r` unfolding refl_on_def by fastforce + moreover have "trans (\R)" + by (rule chain_subset_trans_Union [OF subch `\r\R. trans r`]) + moreover have "antisym (\R)" + by (rule chain_subset_antisym_Union [OF subch `\r\R. antisym r`]) + moreover have "Total (\R)" + by (rule chain_subset_Total_Union [OF subch `\r\R. Total r`]) + moreover have "wf ((\R) - Id)" + proof - + have "(\R) - Id = \{r - Id | r. r \ R}" by blast + with `\r\R. wf (r - Id)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] + show ?thesis by fastforce + qed + ultimately have "Well_order (\R)" by (simp add: order_on_defs) + moreover have "\r\R. r initial_segment_of \R" using Ris + by (simp add: Chains_init_seg_of_Union) + moreover have "downset_on (Field (\R)) p" + by (rule downset_on_Union [OF `\r. r \ R \ downset_on (Field r) p`]) + moreover have "extension_on (Field (\R)) (\R) p" + by (rule chain_subset_extension_on_Union [OF subch `\r. r \ R \ extension_on (Field r) r p`]) + ultimately have "\R \ ?K \ (\r\R. (r,\R) \ I)" + using mono_Chains [OF I_init] and `R \ Chains I` + by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) + } + then have 1: "\R\Chains I. \u\Field I. \r\R. (r, u) \ I" by (subst FI) blast + txt {*Zorn's Lemma yields a maximal wellorder m.*} + from Zorns_po_lemma [OF 0 1] obtain m :: "('a \ 'a) set" + where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and + max: "\r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p \ + (m, r) \ I \ r = m" + by (auto simp: FI) + have "Field p \ Field m" + proof (rule ccontr) + let ?Q = "Field p - Field m" + assume "\ (Field p \ Field m)" + with assms [unfolded wf_eq_minimal, THEN spec, of ?Q] + obtain x where "x \ Field p" and "x \ Field m" and + min: "\y. (y, x) \ p \ y \ ?Q" by blast + txt {*Add @{term x} as topmost element to @{term m}.*} + let ?s = "{(y, x) | y. y \ Field m}" + let ?m = "insert (x, x) m \ ?s" + have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def) + have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" + using `Well_order m` by (simp_all add: order_on_defs) + txt {*We show that the extension is a wellorder.*} + have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def) + moreover have "trans ?m" using `trans m` `x \ Field m` + unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast + moreover have "antisym ?m" using `antisym m` `x \ Field m` + unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast + moreover have "Total ?m" using `Total m` Fm by (auto simp: Relation.total_on_def) + moreover have "wf (?m - Id)" + proof - + have "wf ?s" using `x \ Field m` + by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis + thus ?thesis using `wf (m - Id)` `x \ Field m` + wf_subset [OF `wf ?s` Diff_subset] + by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) + qed + ultimately have "Well_order ?m" by (simp add: order_on_defs) + moreover have "extension_on (Field ?m) ?m p" + using `extension_on (Field m) m p` `downset_on (Field m) p` + by (subst Fm) (auto simp: extension_on_def dest: downset_onD) + moreover have "downset_on (Field ?m) p" + apply (subst Fm) + using `downset_on (Field m) p` and min + unfolding downset_on_def Field_def by blast + moreover have "(m, ?m) \ I" + using `Well_order m` and `Well_order ?m` and + `downset_on (Field m) p` and `downset_on (Field ?m) p` and + `extension_on (Field m) m p` and `extension_on (Field ?m) ?m p` and + `Refl m` and `x \ Field m` + by (auto simp: I_def init_seg_of_def refl_on_def) + ultimately + --{*This contradicts maximality of m:*} + show False using max and `x \ Field m` unfolding Field_def by blast + qed + have "p \ m" + using `Field p \ Field m` and `extension_on (Field m) m p` + unfolding Field_def extension_on_def by auto fast + with `Well_order m` show ?thesis by blast +qed + +text {*Every well-founded relation can be extended to a total wellorder.*} +corollary total_well_order_extension: + assumes "wf p" + shows "\w. p \ w \ Well_order w \ Field w = UNIV" +proof - + from well_order_extension [OF assms] obtain w + where "p \ w" and wo: "Well_order w" by blast + let ?A = "UNIV - Field w" + from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" .. + have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp + have *: "Field w \ Field w' = {}" by simp + let ?w = "w \o w'" + have "p \ ?w" using `p \ w` by (auto simp: Osum_def) + moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp + moreover have "Field ?w = UNIV" by (simp add: Field_Osum) + ultimately show ?thesis by blast +qed + +corollary well_order_on_extension: + assumes "wf p" and "Field p \ A" + shows "\w. p \ w \ well_order_on A w" +proof - + from total_well_order_extension [OF `wf p`] obtain r + where "p \ r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast + let ?r = "{(x, y). x \ A \ y \ A \ (x, y) \ r}" + from `p \ r` have "p \ ?r" using `Field p \ A` by (auto simp: Field_def) + have 1: "Field ?r = A" using wo univ + by (fastforce simp: Field_def order_on_defs refl_on_def) + have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" + using `Well_order r` by (simp_all add: order_on_defs) + have "refl_on A ?r" using `Refl r` by (auto simp: refl_on_def univ) + moreover have "trans ?r" using `trans r` + unfolding trans_def by blast + moreover have "antisym ?r" using `antisym r` + unfolding antisym_def by blast + moreover have "total_on A ?r" using `Total r` by (simp add: total_on_def univ) + moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf(r - Id)`]) blast + ultimately have "well_order_on A ?r" by (simp add: order_on_defs) + with `p \ ?r` show ?thesis by blast +qed + +end diff -r 7d23f8e501d4 -r 483131676087 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Nov 20 21:28:58 2013 +0100 +++ b/src/HOL/Library/Library.thy Wed Nov 20 23:14:06 2013 +0100 @@ -41,7 +41,6 @@ Numeral_Type OptionalSugar Option_ord - Order_Union Parallel Permutation Permutations @@ -66,7 +65,6 @@ Transitive_Closure_Table Wfrec While_Combinator - Zorn begin end (*>*) diff -r 7d23f8e501d4 -r 483131676087 src/HOL/Library/Order_Union.thy --- a/src/HOL/Library/Order_Union.thy Wed Nov 20 21:28:58 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,371 +0,0 @@ -(* Title: HOL/Library/Order_Union.thy - Author: Andrei Popescu, TU Muenchen - -The ordinal-like sum of two orders with disjoint fields -*) - -header {* Order Union *} - -theory Order_Union -imports "~~/src/HOL/Cardinals/Wellfounded_More_FP" -begin - -definition Osum :: "'a rel \ 'a rel \ 'a rel" (infix "Osum" 60) where - "r Osum r' = r \ r' \ {(a, a'). a \ Field r \ a' \ Field r'}" - -notation Osum (infix "\o" 60) - -lemma Field_Osum: "Field (r \o r') = Field r \ Field r'" - unfolding Osum_def Field_def by blast - -lemma Osum_wf: -assumes FLD: "Field r Int Field r' = {}" and - WF: "wf r" and WF': "wf r'" -shows "wf (r Osum r')" -unfolding wf_eq_minimal2 unfolding Field_Osum -proof(intro allI impI, elim conjE) - fix A assume *: "A \ Field r \ Field r'" and **: "A \ {}" - obtain B where B_def: "B = A Int Field r" by blast - show "\a\A. \a'\A. (a', a) \ r \o r'" - proof(cases "B = {}") - assume Case1: "B \ {}" - hence "B \ {} \ B \ Field r" using B_def by auto - then obtain a where 1: "a \ B" and 2: "\a1 \ B. (a1,a) \ r" - using WF unfolding wf_eq_minimal2 by metis - hence 3: "a \ Field r \ a \ Field r'" using B_def FLD by auto - (* *) - have "\a1 \ A. (a1,a) \ r Osum r'" - proof(intro ballI) - fix a1 assume **: "a1 \ A" - {assume Case11: "a1 \ Field r" - hence "(a1,a) \ r" using B_def ** 2 by auto - moreover - have "(a1,a) \ r'" using 3 by (auto simp add: Field_def) - ultimately have "(a1,a) \ r Osum r'" - using 3 unfolding Osum_def by auto - } - moreover - {assume Case12: "a1 \ Field r" - hence "(a1,a) \ r" unfolding Field_def by auto - moreover - have "(a1,a) \ r'" using 3 unfolding Field_def by auto - ultimately have "(a1,a) \ r Osum r'" - using 3 unfolding Osum_def by auto - } - ultimately show "(a1,a) \ r Osum r'" by blast - qed - thus ?thesis using 1 B_def by auto - next - assume Case2: "B = {}" - hence 1: "A \ {} \ A \ Field r'" using * ** B_def by auto - then obtain a' where 2: "a' \ A" and 3: "\a1' \ A. (a1',a') \ r'" - using WF' unfolding wf_eq_minimal2 by metis - hence 4: "a' \ Field r' \ a' \ Field r" using 1 FLD by blast - (* *) - have "\a1' \ A. (a1',a') \ r Osum r'" - proof(unfold Osum_def, auto simp add: 3) - fix a1' assume "(a1', a') \ r" - thus False using 4 unfolding Field_def by blast - next - fix a1' assume "a1' \ A" and "a1' \ Field r" - thus False using Case2 B_def by auto - qed - thus ?thesis using 2 by blast - qed -qed - -lemma Osum_Refl: -assumes FLD: "Field r Int Field r' = {}" and - REFL: "Refl r" and REFL': "Refl r'" -shows "Refl (r Osum r')" -using assms -unfolding refl_on_def Field_Osum unfolding Osum_def by blast - -lemma Osum_trans: -assumes FLD: "Field r Int Field r' = {}" and - TRANS: "trans r" and TRANS': "trans r'" -shows "trans (r Osum r')" -proof(unfold trans_def, auto) - fix x y z assume *: "(x, y) \ r \o r'" and **: "(y, z) \ r \o r'" - show "(x, z) \ r \o r'" - proof- - {assume Case1: "(x,y) \ r" - hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto - have ?thesis - proof- - {assume Case11: "(y,z) \ r" - hence "(x,z) \ r" using Case1 TRANS trans_def[of r] by blast - hence ?thesis unfolding Osum_def by auto - } - moreover - {assume Case12: "(y,z) \ r'" - hence "y \ Field r'" unfolding Field_def by auto - hence False using FLD 1 by auto - } - moreover - {assume Case13: "z \ Field r'" - hence ?thesis using 1 unfolding Osum_def by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case2: "(x,y) \ r'" - hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto - have ?thesis - proof- - {assume Case21: "(y,z) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD 2 by auto - } - moreover - {assume Case22: "(y,z) \ r'" - hence "(x,z) \ r'" using Case2 TRANS' trans_def[of r'] by blast - hence ?thesis unfolding Osum_def by auto - } - moreover - {assume Case23: "y \ Field r" - hence False using FLD 2 by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case3: "x \ Field r \ y \ Field r'" - have ?thesis - proof- - {assume Case31: "(y,z) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD Case3 by auto - } - moreover - {assume Case32: "(y,z) \ r'" - hence "z \ Field r'" unfolding Field_def by blast - hence ?thesis unfolding Osum_def using Case3 by auto - } - moreover - {assume Case33: "y \ Field r" - hence False using FLD Case3 by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - ultimately show ?thesis using * unfolding Osum_def by blast - qed -qed - -lemma Osum_Preorder: -"\Field r Int Field r' = {}; Preorder r; Preorder r'\ \ Preorder (r Osum r')" -unfolding preorder_on_def using Osum_Refl Osum_trans by blast - -lemma Osum_antisym: -assumes FLD: "Field r Int Field r' = {}" and - AN: "antisym r" and AN': "antisym r'" -shows "antisym (r Osum r')" -proof(unfold antisym_def, auto) - fix x y assume *: "(x, y) \ r \o r'" and **: "(y, x) \ r \o r'" - show "x = y" - proof- - {assume Case1: "(x,y) \ r" - hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto - have ?thesis - proof- - have "(y,x) \ r \ ?thesis" - using Case1 AN antisym_def[of r] by blast - moreover - {assume "(y,x) \ r'" - hence "y \ Field r'" unfolding Field_def by auto - hence False using FLD 1 by auto - } - moreover - have "x \ Field r' \ False" using FLD 1 by auto - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case2: "(x,y) \ r'" - hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto - have ?thesis - proof- - {assume "(y,x) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD 2 by auto - } - moreover - have "(y,x) \ r' \ ?thesis" - using Case2 AN' antisym_def[of r'] by blast - moreover - {assume "y \ Field r" - hence False using FLD 2 by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case3: "x \ Field r \ y \ Field r'" - have ?thesis - proof- - {assume "(y,x) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD Case3 by auto - } - moreover - {assume Case32: "(y,x) \ r'" - hence "x \ Field r'" unfolding Field_def by blast - hence False using FLD Case3 by auto - } - moreover - have "\ y \ Field r" using FLD Case3 by auto - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - ultimately show ?thesis using * unfolding Osum_def by blast - qed -qed - -lemma Osum_Partial_order: -"\Field r Int Field r' = {}; Partial_order r; Partial_order r'\ \ - Partial_order (r Osum r')" -unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blast - -lemma Osum_Total: -assumes FLD: "Field r Int Field r' = {}" and - TOT: "Total r" and TOT': "Total r'" -shows "Total (r Osum r')" -using assms -unfolding total_on_def Field_Osum unfolding Osum_def by blast - -lemma Osum_Linear_order: -"\Field r Int Field r' = {}; Linear_order r; Linear_order r'\ \ - Linear_order (r Osum r')" -unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast - -lemma Osum_minus_Id1: -assumes "r \ Id" -shows "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" -proof- - let ?Left = "(r Osum r') - Id" - let ?Right = "(r' - Id) \ (Field r \ Field r')" - {fix a::'a and b assume *: "(a,b) \ Id" - {assume "(a,b) \ r" - with * have False using assms by auto - } - moreover - {assume "(a,b) \ r'" - with * have "(a,b) \ r' - Id" by auto - } - ultimately - have "(a,b) \ ?Left \ (a,b) \ ?Right" - unfolding Osum_def by auto - } - thus ?thesis by auto -qed - -lemma Osum_minus_Id2: -assumes "r' \ Id" -shows "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" -proof- - let ?Left = "(r Osum r') - Id" - let ?Right = "(r - Id) \ (Field r \ Field r')" - {fix a::'a and b assume *: "(a,b) \ Id" - {assume "(a,b) \ r'" - with * have False using assms by auto - } - moreover - {assume "(a,b) \ r" - with * have "(a,b) \ r - Id" by auto - } - ultimately - have "(a,b) \ ?Left \ (a,b) \ ?Right" - unfolding Osum_def by auto - } - thus ?thesis by auto -qed - -lemma Osum_minus_Id: -assumes TOT: "Total r" and TOT': "Total r'" and - NID: "\ (r \ Id)" and NID': "\ (r' \ Id)" -shows "(r Osum r') - Id \ (r - Id) Osum (r' - Id)" -proof- - {fix a a' assume *: "(a,a') \ (r Osum r')" and **: "a \ a'" - have "(a,a') \ (r - Id) Osum (r' - Id)" - proof- - {assume "(a,a') \ r \ (a,a') \ r'" - with ** have ?thesis unfolding Osum_def by auto - } - moreover - {assume "a \ Field r \ a' \ Field r'" - hence "a \ Field(r - Id) \ a' \ Field (r' - Id)" - using assms Total_Id_Field by blast - hence ?thesis unfolding Osum_def by auto - } - ultimately show ?thesis using * unfolding Osum_def by fast - qed - } - thus ?thesis by(auto simp add: Osum_def) -qed - -lemma wf_Int_Times: -assumes "A Int B = {}" -shows "wf(A \ B)" -unfolding wf_def using assms by blast - -lemma Osum_wf_Id: -assumes TOT: "Total r" and TOT': "Total r'" and - FLD: "Field r Int Field r' = {}" and - WF: "wf(r - Id)" and WF': "wf(r' - Id)" -shows "wf ((r Osum r') - Id)" -proof(cases "r \ Id \ r' \ Id") - assume Case1: "\(r \ Id \ r' \ Id)" - have "Field(r - Id) Int Field(r' - Id) = {}" - using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r'] - Diff_subset[of r Id] Diff_subset[of r' Id] by blast - thus ?thesis - using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"] - wf_subset[of "(r - Id) \o (r' - Id)" "(r Osum r') - Id"] by auto -next - have 1: "wf(Field r \ Field r')" - using FLD by (auto simp add: wf_Int_Times) - assume Case2: "r \ Id \ r' \ Id" - moreover - {assume Case21: "r \ Id" - hence "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" - using Osum_minus_Id1[of r r'] by simp - moreover - {have "Domain(Field r \ Field r') Int Range(r' - Id) = {}" - using FLD unfolding Field_def by blast - hence "wf((r' - Id) \ (Field r \ Field r'))" - using 1 WF' wf_Un[of "Field r \ Field r'" "r' - Id"] - by (auto simp add: Un_commute) - } - ultimately have ?thesis by (metis wf_subset) - } - moreover - {assume Case22: "r' \ Id" - hence "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" - using Osum_minus_Id2[of r' r] by simp - moreover - {have "Range(Field r \ Field r') Int Domain(r - Id) = {}" - using FLD unfolding Field_def by blast - hence "wf((r - Id) \ (Field r \ Field r'))" - using 1 WF wf_Un[of "r - Id" "Field r \ Field r'"] - by (auto simp add: Un_commute) - } - ultimately have ?thesis by (metis wf_subset) - } - ultimately show ?thesis by blast -qed - -lemma Osum_Well_order: -assumes FLD: "Field r Int Field r' = {}" and - WELL: "Well_order r" and WELL': "Well_order r'" -shows "Well_order (r Osum r')" -proof- - have "Total r \ Total r'" using WELL WELL' - by (auto simp add: order_on_defs) - thus ?thesis using assms unfolding well_order_on_def - using Osum_Linear_order Osum_wf_Id by blast -qed - -end - diff -r 7d23f8e501d4 -r 483131676087 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Wed Nov 20 21:28:58 2013 +0100 +++ b/src/HOL/Library/Zorn.thy Wed Nov 20 23:14:06 2013 +0100 @@ -5,13 +5,12 @@ Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF). The well-ordering theorem. -The extension of any well-founded relation to a well-order. *) header {* Zorn's Lemma *} theory Zorn -imports Order_Union +imports Order_Relation begin subsection {* Zorn's Lemma for the Subset Relation *} @@ -710,207 +709,4 @@ with 1 show ?thesis by auto qed -subsection {* Extending Well-founded Relations to Well-Orders *} - -text {*A \emph{downset} (also lower set, decreasing set, initial segment, or -downward closed set) is closed w.r.t.\ smaller elements.*} -definition downset_on where - "downset_on A r = (\x y. (x, y) \ r \ y \ A \ x \ A)" - -(* -text {*Connection to order filters of the @{theory Cardinals} theory.*} -lemma (in wo_rel) ofilter_downset_on_conv: - "ofilter A \ downset_on A r \ A \ Field r" - by (auto simp: downset_on_def ofilter_def under_def) -*) - -lemma downset_onI: - "(\x y. (x, y) \ r \ y \ A \ x \ A) \ downset_on A r" - by (auto simp: downset_on_def) - -lemma downset_onD: - "downset_on A r \ (x, y) \ r \ y \ A \ x \ A" - unfolding downset_on_def by blast - -text {*Extensions of relations w.r.t.\ a given set.*} -definition extension_on where - "extension_on A r s = (\x\A. \y\A. (x, y) \ s \ (x, y) \ r)" - -lemma extension_onI: - "(\x y. \x \ A; y \ A; (x, y) \ s\ \ (x, y) \ r) \ extension_on A r s" - by (auto simp: extension_on_def) - -lemma extension_onD: - "extension_on A r s \ x \ A \ y \ A \ (x, y) \ s \ (x, y) \ r" - by (auto simp: extension_on_def) - -lemma downset_on_Union: - assumes "\r. r \ R \ downset_on (Field r) p" - shows "downset_on (Field (\R)) p" - using assms by (auto intro: downset_onI dest: downset_onD) - -lemma chain_subset_extension_on_Union: - assumes "chain\<^sub>\ R" and "\r. r \ R \ extension_on (Field r) r p" - shows "extension_on (Field (\R)) (\R) p" - using assms - by (simp add: chain_subset_def extension_on_def) - (metis (no_types) mono_Field set_mp) - -lemma downset_on_empty [simp]: "downset_on {} p" - by (auto simp: downset_on_def) - -lemma extension_on_empty [simp]: "extension_on {} p q" - by (auto simp: extension_on_def) - -text {*Every well-founded relation can be extended to a well-order.*} -theorem well_order_extension: - assumes "wf p" - shows "\w. p \ w \ Well_order w" -proof - - let ?K = "{r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p}" - def I \ "init_seg_of \ ?K \ ?K" - have I_init: "I \ init_seg_of" by (simp add: I_def) - then have subch: "\R. R \ Chains I \ chain\<^sub>\ R" - by (auto simp: init_seg_of_def chain_subset_def Chains_def) - have Chains_wo: "\R r. R \ Chains I \ r \ R \ - Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p" - by (simp add: Chains_def I_def) blast - have FI: "Field I = ?K" by (auto simp: I_def init_seg_of_def Field_def) - then have 0: "Partial_order I" - by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def - trans_def I_def elim: trans_init_seg_of) - { fix R assume "R \ Chains I" - then have Ris: "R \ Chains init_seg_of" using mono_Chains [OF I_init] by blast - have subch: "chain\<^sub>\ R" using `R \ Chains I` I_init - by (auto simp: init_seg_of_def chain_subset_def Chains_def) - have "\r\R. Refl r" and "\r\R. trans r" and "\r\R. antisym r" and - "\r\R. Total r" and "\r\R. wf (r - Id)" and - "\r. r \ R \ downset_on (Field r) p" and - "\r. r \ R \ extension_on (Field r) r p" - using Chains_wo [OF `R \ Chains I`] by (simp_all add: order_on_defs) - have "Refl (\R)" using `\r\R. Refl r` unfolding refl_on_def by fastforce - moreover have "trans (\R)" - by (rule chain_subset_trans_Union [OF subch `\r\R. trans r`]) - moreover have "antisym (\R)" - by (rule chain_subset_antisym_Union [OF subch `\r\R. antisym r`]) - moreover have "Total (\R)" - by (rule chain_subset_Total_Union [OF subch `\r\R. Total r`]) - moreover have "wf ((\R) - Id)" - proof - - have "(\R) - Id = \{r - Id | r. r \ R}" by blast - with `\r\R. wf (r - Id)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] - show ?thesis by fastforce - qed - ultimately have "Well_order (\R)" by (simp add: order_on_defs) - moreover have "\r\R. r initial_segment_of \R" using Ris - by (simp add: Chains_init_seg_of_Union) - moreover have "downset_on (Field (\R)) p" - by (rule downset_on_Union [OF `\r. r \ R \ downset_on (Field r) p`]) - moreover have "extension_on (Field (\R)) (\R) p" - by (rule chain_subset_extension_on_Union [OF subch `\r. r \ R \ extension_on (Field r) r p`]) - ultimately have "\R \ ?K \ (\r\R. (r,\R) \ I)" - using mono_Chains [OF I_init] and `R \ Chains I` - by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) - } - then have 1: "\R\Chains I. \u\Field I. \r\R. (r, u) \ I" by (subst FI) blast - txt {*Zorn's Lemma yields a maximal well-order m.*} - from Zorns_po_lemma [OF 0 1] obtain m :: "('a \ 'a) set" - where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and - max: "\r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p \ - (m, r) \ I \ r = m" - by (auto simp: FI) - have "Field p \ Field m" - proof (rule ccontr) - let ?Q = "Field p - Field m" - assume "\ (Field p \ Field m)" - with assms [unfolded wf_eq_minimal, THEN spec, of ?Q] - obtain x where "x \ Field p" and "x \ Field m" and - min: "\y. (y, x) \ p \ y \ ?Q" by blast - txt {*Add @{term x} as topmost element to @{term m}.*} - let ?s = "{(y, x) | y. y \ Field m}" - let ?m = "insert (x, x) m \ ?s" - have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def) - have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" - using `Well_order m` by (simp_all add: order_on_defs) - txt {*We show that the extension is a well-order.*} - have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def) - moreover have "trans ?m" using `trans m` `x \ Field m` - unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast - moreover have "antisym ?m" using `antisym m` `x \ Field m` - unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast - moreover have "Total ?m" using `Total m` Fm by (auto simp: Relation.total_on_def) - moreover have "wf (?m - Id)" - proof - - have "wf ?s" using `x \ Field m` - by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis - thus ?thesis using `wf (m - Id)` `x \ Field m` - wf_subset [OF `wf ?s` Diff_subset] - by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) - qed - ultimately have "Well_order ?m" by (simp add: order_on_defs) - moreover have "extension_on (Field ?m) ?m p" - using `extension_on (Field m) m p` `downset_on (Field m) p` - by (subst Fm) (auto simp: extension_on_def dest: downset_onD) - moreover have "downset_on (Field ?m) p" - apply (subst Fm) - using `downset_on (Field m) p` and min - unfolding downset_on_def Field_def by blast - moreover have "(m, ?m) \ I" - using `Well_order m` and `Well_order ?m` and - `downset_on (Field m) p` and `downset_on (Field ?m) p` and - `extension_on (Field m) m p` and `extension_on (Field ?m) ?m p` and - `Refl m` and `x \ Field m` - by (auto simp: I_def init_seg_of_def refl_on_def) - ultimately - --{*This contradicts maximality of m:*} - show False using max and `x \ Field m` unfolding Field_def by blast - qed - have "p \ m" - using `Field p \ Field m` and `extension_on (Field m) m p` - unfolding Field_def extension_on_def by auto fast - with `Well_order m` show ?thesis by blast -qed - -text {*Every well-founded relation can be extended to a total well-order.*} -corollary total_well_order_extension: - assumes "wf p" - shows "\w. p \ w \ Well_order w \ Field w = UNIV" -proof - - from well_order_extension [OF assms] obtain w - where "p \ w" and wo: "Well_order w" by blast - let ?A = "UNIV - Field w" - from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" .. - have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp - have *: "Field w \ Field w' = {}" by simp - let ?w = "w \o w'" - have "p \ ?w" using `p \ w` by (auto simp: Osum_def) - moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp - moreover have "Field ?w = UNIV" by (simp add: Field_Osum) - ultimately show ?thesis by blast -qed - -corollary well_order_on_extension: - assumes "wf p" and "Field p \ A" - shows "\w. p \ w \ well_order_on A w" -proof - - from total_well_order_extension [OF `wf p`] obtain r - where "p \ r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast - let ?r = "{(x, y). x \ A \ y \ A \ (x, y) \ r}" - from `p \ r` have "p \ ?r" using `Field p \ A` by (auto simp: Field_def) - have 1: "Field ?r = A" using wo univ - by (fastforce simp: Field_def order_on_defs refl_on_def) - have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" - using `Well_order r` by (simp_all add: order_on_defs) - have "refl_on A ?r" using `Refl r` by (auto simp: refl_on_def univ) - moreover have "trans ?r" using `trans r` - unfolding trans_def by blast - moreover have "antisym ?r" using `antisym r` - unfolding antisym_def by blast - moreover have "total_on A ?r" using `Total r` by (simp add: total_on_def univ) - moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf(r - Id)`]) blast - ultimately have "well_order_on A ?r" by (simp add: order_on_defs) - with `p \ ?r` show ?thesis by blast -qed - end -