1 (* Title: HOL/Library/Well_Order_Extension.thy |
|
2 Author: Christian Sternagel, JAIST |
|
3 *) |
|
4 |
|
5 header {*Extending Well-founded Relations to Well-Orders.*} |
|
6 |
|
7 theory Well_Order_Extension |
|
8 imports Zorn Order_Union |
|
9 begin |
|
10 |
|
11 text {*A \emph{downset} (also lower set, decreasing set, initial segment, or |
|
12 downward closed set) is closed w.r.t.\ smaller elements.*} |
|
13 definition downset_on where |
|
14 "downset_on A r = (\<forall>x y. (x, y) \<in> r \<and> y \<in> A \<longrightarrow> x \<in> A)" |
|
15 |
|
16 (* |
|
17 text {*Connection to order filters of the @{theory Cardinals} theory.*} |
|
18 lemma (in wo_rel) ofilter_downset_on_conv: |
|
19 "ofilter A \<longleftrightarrow> downset_on A r \<and> A \<subseteq> Field r" |
|
20 by (auto simp: downset_on_def ofilter_def under_def) |
|
21 *) |
|
22 |
|
23 lemma downset_onI: |
|
24 "(\<And>x y. (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A) \<Longrightarrow> downset_on A r" |
|
25 by (auto simp: downset_on_def) |
|
26 |
|
27 lemma downset_onD: |
|
28 "downset_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A" |
|
29 by (auto simp: downset_on_def) |
|
30 |
|
31 text {*Extensions of relations w.r.t.\ a given set.*} |
|
32 definition extension_on where |
|
33 "extension_on A r s = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y) \<in> s \<longrightarrow> (x, y) \<in> r)" |
|
34 |
|
35 lemma extension_onI: |
|
36 "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; (x, y) \<in> s\<rbrakk> \<Longrightarrow> (x, y) \<in> r) \<Longrightarrow> extension_on A r s" |
|
37 by (auto simp: extension_on_def) |
|
38 |
|
39 lemma extension_onD: |
|
40 "extension_on A r s \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> s \<Longrightarrow> (x, y) \<in> r" |
|
41 by (auto simp: extension_on_def) |
|
42 |
|
43 lemma downset_on_Union: |
|
44 assumes "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" |
|
45 shows "downset_on (Field (\<Union>R)) p" |
|
46 using assms by (auto intro: downset_onI dest: downset_onD) |
|
47 |
|
48 lemma chain_subset_extension_on_Union: |
|
49 assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p" |
|
50 shows "extension_on (Field (\<Union>R)) (\<Union>R) p" |
|
51 using assms |
|
52 by (simp add: chain_subset_def extension_on_def) |
|
53 (metis Field_def mono_Field set_mp) |
|
54 |
|
55 lemma downset_on_empty [simp]: "downset_on {} p" |
|
56 by (auto simp: downset_on_def) |
|
57 |
|
58 lemma extension_on_empty [simp]: "extension_on {} p q" |
|
59 by (auto simp: extension_on_def) |
|
60 |
|
61 text {*Every well-founded relation can be extended to a well-order.*} |
|
62 theorem well_order_extension: |
|
63 assumes "wf p" |
|
64 shows "\<exists>w. p \<subseteq> w \<and> Well_order w" |
|
65 proof - |
|
66 let ?K = "{r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p}" |
|
67 def I \<equiv> "init_seg_of \<inter> ?K \<times> ?K" |
|
68 have I_init: "I \<subseteq> init_seg_of" by (simp add: I_def) |
|
69 then have subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R" |
|
70 by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
71 have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> |
|
72 Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p" |
|
73 by (simp add: Chains_def I_def) blast |
|
74 have FI: "Field I = ?K" by (auto simp: I_def init_seg_of_def Field_def) |
|
75 then have 0: "Partial_order I" |
|
76 by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def |
|
77 trans_def I_def elim: trans_init_seg_of) |
|
78 { fix R assume "R \<in> Chains I" |
|
79 then have Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast |
|
80 have subch: "chain\<^sub>\<subseteq> R" using `R \<in> Chains I` I_init |
|
81 by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
82 have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" and |
|
83 "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)" and |
|
84 "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" and |
|
85 "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p" |
|
86 using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs) |
|
87 have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by (auto simp: refl_on_def) |
|
88 moreover have "trans (\<Union>R)" |
|
89 by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`]) |
|
90 moreover have "antisym (\<Union>R)" |
|
91 by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`]) |
|
92 moreover have "Total (\<Union>R)" |
|
93 by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`]) |
|
94 moreover have "wf ((\<Union>R) - Id)" |
|
95 proof - |
|
96 have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast |
|
97 with `\<forall>r\<in>R. wf (r - Id)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] |
|
98 show ?thesis by (simp (no_asm_simp)) blast |
|
99 qed |
|
100 ultimately have "Well_order (\<Union>R)" by (simp add: order_on_defs) |
|
101 moreover have "\<forall>r\<in>R. r initial_segment_of \<Union>R" using Ris |
|
102 by (simp add: Chains_init_seg_of_Union) |
|
103 moreover have "downset_on (Field (\<Union>R)) p" |
|
104 by (rule downset_on_Union [OF `\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p`]) |
|
105 moreover have "extension_on (Field (\<Union>R)) (\<Union>R) p" |
|
106 by (rule chain_subset_extension_on_Union [OF subch `\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p`]) |
|
107 ultimately have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)" |
|
108 using mono_Chains [OF I_init] and `R \<in> Chains I` |
|
109 by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) |
|
110 } |
|
111 then have 1: "\<forall>R\<in>Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast |
|
112 txt {*Zorn's Lemma yields a maximal well-order m.*} |
|
113 from Zorns_po_lemma [OF 0 1] obtain m :: "('a \<times> 'a) set" |
|
114 where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and |
|
115 max: "\<forall>r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p \<and> |
|
116 (m, r) \<in> I \<longrightarrow> r = m" |
|
117 by (auto simp: FI) |
|
118 have "Field p \<subseteq> Field m" |
|
119 proof (rule ccontr) |
|
120 let ?Q = "Field p - Field m" |
|
121 assume "\<not> (Field p \<subseteq> Field m)" |
|
122 with assms [unfolded wf_eq_minimal, THEN spec, of ?Q] |
|
123 obtain x where "x \<in> Field p" and "x \<notin> Field m" and |
|
124 min: "\<forall>y. (y, x) \<in> p \<longrightarrow> y \<notin> ?Q" by blast |
|
125 txt {*Add @{term x} as topmost element to @{term m}.*} |
|
126 let ?s = "{(y, x) | y. y \<in> Field m}" |
|
127 let ?m = "insert (x, x) m \<union> ?s" |
|
128 have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def) |
|
129 have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" |
|
130 using `Well_order m` by (simp_all add: order_on_defs) |
|
131 txt {*We show that the extension is a well-order.*} |
|
132 have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def) |
|
133 moreover have "trans ?m" using `trans m` `x \<notin> Field m` |
|
134 unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast |
|
135 moreover have "antisym ?m" using `antisym m` `x \<notin> Field m` |
|
136 unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast |
|
137 moreover have "Total ?m" using `Total m` Fm by (auto simp: Relation.total_on_def) |
|
138 moreover have "wf (?m - Id)" |
|
139 proof - |
|
140 have "wf ?s" using `x \<notin> Field m` |
|
141 by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis |
|
142 thus ?thesis using `wf (m - Id)` `x \<notin> Field m` |
|
143 wf_subset [OF `wf ?s` Diff_subset] |
|
144 by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) |
|
145 qed |
|
146 ultimately have "Well_order ?m" by (simp add: order_on_defs) |
|
147 moreover have "extension_on (Field ?m) ?m p" |
|
148 using `extension_on (Field m) m p` `downset_on (Field m) p` |
|
149 by (subst Fm) (auto simp: extension_on_def dest: downset_onD) |
|
150 moreover have "downset_on (Field ?m) p" |
|
151 using `downset_on (Field m) p` and min |
|
152 by (subst Fm, simp add: downset_on_def Field_def) (metis Domain_iff) |
|
153 moreover have "(m, ?m) \<in> I" |
|
154 using `Well_order m` and `Well_order ?m` and |
|
155 `downset_on (Field m) p` and `downset_on (Field ?m) p` and |
|
156 `extension_on (Field m) m p` and `extension_on (Field ?m) ?m p` and |
|
157 `Refl m` and `x \<notin> Field m` |
|
158 by (auto simp: I_def init_seg_of_def refl_on_def) |
|
159 ultimately |
|
160 --{*This contradicts maximality of m:*} |
|
161 show False using max and `x \<notin> Field m` unfolding Field_def by blast |
|
162 qed |
|
163 have "p \<subseteq> m" |
|
164 using `Field p \<subseteq> Field m` and `extension_on (Field m) m p` |
|
165 by (force simp: Field_def extension_on_def) |
|
166 with `Well_order m` show ?thesis by blast |
|
167 qed |
|
168 |
|
169 text {*Every well-founded relation can be extended to a total well-order.*} |
|
170 corollary total_well_order_extension: |
|
171 assumes "wf p" |
|
172 shows "\<exists>w. p \<subseteq> w \<and> Well_order w \<and> Field w = UNIV" |
|
173 proof - |
|
174 from well_order_extension [OF assms] obtain w |
|
175 where "p \<subseteq> w" and wo: "Well_order w" by blast |
|
176 let ?A = "UNIV - Field w" |
|
177 from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" .. |
|
178 have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp |
|
179 have *: "Field w \<inter> Field w' = {}" by simp |
|
180 let ?w = "w \<union>o w'" |
|
181 have "p \<subseteq> ?w" using `p \<subseteq> w` by (auto simp: Osum_def) |
|
182 moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp |
|
183 moreover have "Field ?w = UNIV" by (simp add: Field_Osum) |
|
184 ultimately show ?thesis by blast |
|
185 qed |
|
186 |
|
187 corollary well_order_on_extension: |
|
188 assumes "wf p" and "Field p \<subseteq> A" |
|
189 shows "\<exists>w. p \<subseteq> w \<and> well_order_on A w" |
|
190 proof - |
|
191 from total_well_order_extension [OF `wf p`] obtain r |
|
192 where "p \<subseteq> r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast |
|
193 let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}" |
|
194 from `p \<subseteq> r` have "p \<subseteq> ?r" using `Field p \<subseteq> A` by (auto simp: Field_def) |
|
195 have 1: "Field ?r = A" using wo univ |
|
196 by (fastforce simp: Field_def order_on_defs refl_on_def) |
|
197 have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" |
|
198 using `Well_order r` by (simp_all add: order_on_defs) |
|
199 have "refl_on A ?r" using `Refl r` by (auto simp: refl_on_def univ) |
|
200 moreover have "trans ?r" using `trans r` |
|
201 unfolding trans_def by blast |
|
202 moreover have "antisym ?r" using `antisym r` |
|
203 unfolding antisym_def by blast |
|
204 moreover have "total_on A ?r" using `Total r` by (simp add: total_on_def univ) |
|
205 moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf(r - Id)`]) blast |
|
206 ultimately have "well_order_on A ?r" by (simp add: order_on_defs) |
|
207 with `p \<subseteq> ?r` show ?thesis by blast |
|
208 qed |
|
209 |
|
210 end |
|
211 |
|