|
1 (* Title: HOL/Cardinals/Ordinal_Arithmetic.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Copyright 2014 |
|
4 |
|
5 Ordinal arithmetic. |
|
6 *) |
|
7 |
|
8 header {* Ordinal Arithmetic *} |
|
9 |
|
10 theory Ordinal_Arithmetic |
|
11 imports Constructions_on_Wellorders |
|
12 begin |
|
13 |
|
14 definition osum :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a + 'b) rel" (infixr "+o" 70) |
|
15 where |
|
16 "r +o r' = map_pair Inl Inl ` r \<union> map_pair Inr Inr ` r' \<union> |
|
17 {(Inl a, Inr a') | a a' . a \<in> Field r \<and> a' \<in> Field r'}" |
|
18 |
|
19 lemma Field_osum: "Field(r +o r') = Inl ` Field r \<union> Inr ` Field r'" |
|
20 unfolding osum_def Field_def by auto |
|
21 |
|
22 lemma osum_Refl:"\<lbrakk>Refl r; Refl r'\<rbrakk> \<Longrightarrow> Refl (r +o r')" |
|
23 (*Need first unfold Field_osum, only then osum_def*) |
|
24 unfolding refl_on_def Field_osum unfolding osum_def by blast |
|
25 |
|
26 lemma osum_trans: |
|
27 assumes TRANS: "trans r" and TRANS': "trans r'" |
|
28 shows "trans (r +o r')" |
|
29 proof(unfold trans_def, safe) |
|
30 fix x y z assume *: "(x, y) \<in> r +o r'" "(y, z) \<in> r +o r'" |
|
31 thus "(x, z) \<in> r +o r'" |
|
32 proof (cases x y z rule: sum.exhaust[case_product sum.exhaust sum.exhaust]) |
|
33 case (Inl_Inl_Inl a b c) |
|
34 with * have "(a,b) \<in> r" "(b,c) \<in> r" unfolding osum_def by auto |
|
35 with TRANS have "(a,c) \<in> r" unfolding trans_def by blast |
|
36 with Inl_Inl_Inl show ?thesis unfolding osum_def by auto |
|
37 next |
|
38 case (Inl_Inl_Inr a b c) |
|
39 with * have "a \<in> Field r" "c \<in> Field r'" unfolding osum_def Field_def by auto |
|
40 with Inl_Inl_Inr show ?thesis unfolding osum_def by auto |
|
41 next |
|
42 case (Inl_Inr_Inr a b c) |
|
43 with * have "a \<in> Field r" "c \<in> Field r'" unfolding osum_def Field_def by auto |
|
44 with Inl_Inr_Inr show ?thesis unfolding osum_def by auto |
|
45 next |
|
46 case (Inr_Inr_Inr a b c) |
|
47 with * have "(a,b) \<in> r'" "(b,c) \<in> r'" unfolding osum_def by auto |
|
48 with TRANS' have "(a,c) \<in> r'" unfolding trans_def by blast |
|
49 with Inr_Inr_Inr show ?thesis unfolding osum_def by auto |
|
50 qed (auto simp: osum_def) |
|
51 qed |
|
52 |
|
53 lemma osum_Preorder: "\<lbrakk>Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r +o r')" |
|
54 unfolding preorder_on_def using osum_Refl osum_trans by blast |
|
55 |
|
56 lemma osum_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r +o r')" |
|
57 unfolding antisym_def osum_def by auto |
|
58 |
|
59 lemma osum_Partial_order: "\<lbrakk>Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow> Partial_order (r +o r')" |
|
60 unfolding partial_order_on_def using osum_Preorder osum_antisym by blast |
|
61 |
|
62 lemma osum_Total: "\<lbrakk>Total r; Total r'\<rbrakk> \<Longrightarrow> Total (r +o r')" |
|
63 unfolding total_on_def Field_osum unfolding osum_def by blast |
|
64 |
|
65 lemma osum_Linear_order: "\<lbrakk>Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> Linear_order (r +o r')" |
|
66 unfolding linear_order_on_def using osum_Partial_order osum_Total by blast |
|
67 |
|
68 lemma osum_wf: |
|
69 assumes WF: "wf r" and WF': "wf r'" |
|
70 shows "wf (r +o r')" |
|
71 unfolding wf_eq_minimal2 unfolding Field_osum |
|
72 proof(intro allI impI, elim conjE) |
|
73 fix A assume *: "A \<subseteq> Inl ` Field r \<union> Inr ` Field r'" and **: "A \<noteq> {}" |
|
74 obtain B where B_def: "B = A Int Inl ` Field r" by blast |
|
75 show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r +o r'" |
|
76 proof(cases "B = {}") |
|
77 case False |
|
78 hence "B \<noteq> {}" "B \<le> Inl ` Field r" using B_def by auto |
|
79 hence "Inl -` B \<noteq> {}" "Inl -` B \<le> Field r" unfolding vimage_def by auto |
|
80 then obtain a where 1: "a \<in> Inl -` B" and "\<forall>a1 \<in> Inl -` B. (a1, a) \<notin> r" |
|
81 using WF unfolding wf_eq_minimal2 by metis |
|
82 hence "\<forall>a1 \<in> A. (a1, Inl a) \<notin> r +o r'" |
|
83 unfolding osum_def using B_def ** by (auto simp: vimage_def Field_def) |
|
84 thus ?thesis using 1 unfolding B_def by auto |
|
85 next |
|
86 case True |
|
87 hence 1: "A \<le> Inr ` Field r'" using * B_def by auto |
|
88 with ** have "Inr -`A \<noteq> {}" "Inr -` A \<le> Field r'" unfolding vimage_def by auto |
|
89 with ** obtain a' where 2: "a' \<in> Inr -` A" and "\<forall>a1' \<in> Inr -` A. (a1',a') \<notin> r'" |
|
90 using WF' unfolding wf_eq_minimal2 by metis |
|
91 hence "\<forall>a1' \<in> A. (a1', Inr a') \<notin> r +o r'" |
|
92 unfolding osum_def using ** 1 by (auto simp: vimage_def Field_def) |
|
93 thus ?thesis using 2 by blast |
|
94 qed |
|
95 qed |
|
96 |
|
97 lemma osum_minus_Id: |
|
98 assumes r: "Total r" "\<not> (r \<le> Id)" and r': "Total r'" "\<not> (r' \<le> Id)" |
|
99 shows "(r +o r') - Id \<le> (r - Id) +o (r' - Id)" |
|
100 unfolding osum_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto |
|
101 |
|
102 lemma osum_minus_Id1: |
|
103 "r \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (Inl ` Field r \<times> Inr ` Field r') \<union> (map_pair Inr Inr ` (r' - Id))" |
|
104 unfolding osum_def by auto |
|
105 |
|
106 lemma osum_minus_Id2: |
|
107 "r' \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (map_pair Inl Inl ` (r - Id)) \<union> (Inl ` Field r \<times> Inr ` Field r')" |
|
108 unfolding osum_def by auto |
|
109 |
|
110 lemma osum_wf_Id: |
|
111 assumes TOT: "Total r" and TOT': "Total r'" and WF: "wf(r - Id)" and WF': "wf(r' - Id)" |
|
112 shows "wf ((r +o r') - Id)" |
|
113 proof(cases "r \<le> Id \<or> r' \<le> Id") |
|
114 case False |
|
115 thus ?thesis |
|
116 using osum_minus_Id[of r r'] assms osum_wf[of "r - Id" "r' - Id"] |
|
117 wf_subset[of "(r - Id) +o (r' - Id)" "(r +o r') - Id"] by auto |
|
118 next |
|
119 have 1: "wf (Inl ` Field r \<times> Inr ` Field r')" by (rule wf_Int_Times) auto |
|
120 case True |
|
121 thus ?thesis |
|
122 proof (elim disjE) |
|
123 assume "r \<subseteq> Id" |
|
124 thus "wf ((r +o r') - Id)" |
|
125 by (rule wf_subset[rotated, OF osum_minus_Id1 wf_Un[OF 1 wf_map_pair_image[OF WF']]]) auto |
|
126 next |
|
127 assume "r' \<subseteq> Id" |
|
128 thus "wf ((r +o r') - Id)" |
|
129 by (rule wf_subset[rotated, OF osum_minus_Id2 wf_Un[OF wf_map_pair_image[OF WF] 1]]) auto |
|
130 qed |
|
131 qed |
|
132 |
|
133 lemma osum_Well_order: |
|
134 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
135 shows "Well_order (r +o r')" |
|
136 proof- |
|
137 have "Total r \<and> Total r'" using WELL WELL' by (auto simp add: order_on_defs) |
|
138 thus ?thesis using assms unfolding well_order_on_def |
|
139 using osum_Linear_order osum_wf_Id by blast |
|
140 qed |
|
141 |
|
142 lemma osum_embedL: |
|
143 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
144 shows "embed r (r +o r') Inl" |
|
145 proof - |
|
146 have 1: "Well_order (r +o r')" using assms by (auto simp add: osum_Well_order) |
|
147 moreover |
|
148 have "compat r (r +o r') Inl" unfolding compat_def osum_def by auto |
|
149 moreover |
|
150 have "ofilter (r +o r') (Inl ` Field r)" |
|
151 unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum rel.under_def |
|
152 unfolding osum_def Field_def by auto |
|
153 ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter) |
|
154 qed |
|
155 |
|
156 corollary osum_ordLeqL: |
|
157 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
158 shows "r \<le>o r +o r'" |
|
159 using assms osum_embedL osum_Well_order unfolding ordLeq_def by blast |
|
160 |
|
161 lemma dir_image_alt: "dir_image r f = map_pair f f ` r" |
|
162 unfolding dir_image_def map_pair_def by auto |
|
163 |
|
164 lemma map_pair_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_pair f f ` r =o r" |
|
165 unfolding dir_image_alt[symmetric] by (rule ordIso_symmetric[OF dir_image_ordIso]) |
|
166 |
|
167 definition oprod :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> 'b) rel" (infixr "*o" 80) |
|
168 where "r *o r' = {((x1, y1), (x2, y2)). |
|
169 (((y1, y2) \<in> r' - Id \<and> x1 \<in> Field r \<and> x2 \<in> Field r) \<or> |
|
170 ((y1, y2) \<in> Restr Id (Field r') \<and> (x1, x2) \<in> r))}" |
|
171 |
|
172 lemma Field_oprod: "Field (r *o r') = Field r \<times> Field r'" |
|
173 unfolding oprod_def Field_def by auto blast+ |
|
174 |
|
175 lemma oprod_Refl:"\<lbrakk>Refl r; Refl r'\<rbrakk> \<Longrightarrow> Refl (r *o r')" |
|
176 unfolding refl_on_def Field_oprod unfolding oprod_def by auto |
|
177 |
|
178 lemma oprod_trans: |
|
179 assumes "trans r" "trans r'" "antisym r" "antisym r'" |
|
180 shows "trans (r *o r')" |
|
181 proof(unfold trans_def, safe) |
|
182 fix x y z assume *: "(x, y) \<in> r *o r'" "(y, z) \<in> r *o r'" |
|
183 thus "(x, z) \<in> r *o r'" |
|
184 unfolding oprod_def |
|
185 apply safe |
|
186 apply (metis assms(2) transE) |
|
187 apply (metis assms(2) transE) |
|
188 apply (metis assms(2) transE) |
|
189 apply (metis assms(4) antisymD) |
|
190 apply (metis assms(4) antisymD) |
|
191 apply (metis assms(2) transE) |
|
192 apply (metis assms(4) antisymD) |
|
193 apply (metis Field_def Range_iff Un_iff) |
|
194 apply (metis Field_def Range_iff Un_iff) |
|
195 apply (metis Field_def Range_iff Un_iff) |
|
196 apply (metis Field_def Domain_iff Un_iff) |
|
197 apply (metis Field_def Domain_iff Un_iff) |
|
198 apply (metis Field_def Domain_iff Un_iff) |
|
199 apply (metis assms(1) transE) |
|
200 apply (metis assms(1) transE) |
|
201 apply (metis assms(1) transE) |
|
202 apply (metis assms(1) transE) |
|
203 done |
|
204 qed |
|
205 |
|
206 lemma oprod_Preorder: "\<lbrakk>Preorder r; Preorder r'; antisym r; antisym r'\<rbrakk> \<Longrightarrow> Preorder (r *o r')" |
|
207 unfolding preorder_on_def using oprod_Refl oprod_trans by blast |
|
208 |
|
209 lemma oprod_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r *o r')" |
|
210 unfolding antisym_def oprod_def by auto |
|
211 |
|
212 lemma oprod_Partial_order: "\<lbrakk>Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow> Partial_order (r *o r')" |
|
213 unfolding partial_order_on_def using oprod_Preorder oprod_antisym by blast |
|
214 |
|
215 lemma oprod_Total: "\<lbrakk>Total r; Total r'\<rbrakk> \<Longrightarrow> Total (r *o r')" |
|
216 unfolding total_on_def Field_oprod unfolding oprod_def by auto |
|
217 |
|
218 lemma oprod_Linear_order: "\<lbrakk>Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> Linear_order (r *o r')" |
|
219 unfolding linear_order_on_def using oprod_Partial_order oprod_Total by blast |
|
220 |
|
221 lemma oprod_wf: |
|
222 assumes WF: "wf r" and WF': "wf r'" |
|
223 shows "wf (r *o r')" |
|
224 unfolding wf_eq_minimal2 unfolding Field_oprod |
|
225 proof(intro allI impI, elim conjE) |
|
226 fix A assume *: "A \<subseteq> Field r \<times> Field r'" and **: "A \<noteq> {}" |
|
227 then obtain y where y: "y \<in> snd ` A" "\<forall>y'\<in>snd ` A. (y', y) \<notin> r'" |
|
228 using spec[OF WF'[unfolded wf_eq_minimal2], of "snd ` A"] by auto |
|
229 let ?A = "fst ` A \<inter> {x. (x, y) \<in> A}" |
|
230 from * y have "?A \<noteq> {}" "?A \<subseteq> Field r" by auto |
|
231 then obtain x where x: "x \<in> ?A" and "\<forall>x'\<in> ?A. (x', x) \<notin> r" |
|
232 using spec[OF WF[unfolded wf_eq_minimal2], of "?A"] by auto |
|
233 with y have "\<forall>a'\<in>A. (a', (x, y)) \<notin> r *o r'" |
|
234 unfolding oprod_def mem_Collect_eq split_beta fst_conv snd_conv Id_def by auto |
|
235 moreover from x have "(x, y) \<in> A" by auto |
|
236 ultimately show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r *o r'" by blast |
|
237 qed |
|
238 |
|
239 lemma oprod_minus_Id: |
|
240 assumes r: "Total r" "\<not> (r \<le> Id)" and r': "Total r'" "\<not> (r' \<le> Id)" |
|
241 shows "(r *o r') - Id \<le> (r - Id) *o (r' - Id)" |
|
242 unfolding oprod_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto |
|
243 |
|
244 lemma oprod_minus_Id1: |
|
245 "r \<le> Id \<Longrightarrow> r *o r' - Id \<le> {((x,y1), (x,y2)). x \<in> Field r \<and> (y1, y2) \<in> (r' - Id)}" |
|
246 unfolding oprod_def by auto |
|
247 |
|
248 lemma wf_extend_oprod1: |
|
249 assumes "wf r" |
|
250 shows "wf {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" |
|
251 proof (unfold wf_eq_minimal2, intro allI impI, elim conjE) |
|
252 fix B |
|
253 assume *: "B \<subseteq> Field {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" and "B \<noteq> {}" |
|
254 from image_mono[OF *, of snd] have "snd ` B \<subseteq> Field r" unfolding Field_def by force |
|
255 with `B \<noteq> {}` obtain x where x: "x \<in> snd ` B" "\<forall>x'\<in>snd ` B. (x', x) \<notin> r" |
|
256 using spec[OF assms[unfolded wf_eq_minimal2], of "snd ` B"] by auto |
|
257 then obtain a where "(a, x) \<in> B" by auto |
|
258 moreover |
|
259 from * x have "\<forall>a'\<in>B. (a', (a, x)) \<notin> {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" by auto |
|
260 ultimately show "\<exists>ax\<in>B. \<forall>a'\<in>B. (a', ax) \<notin> {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" by blast |
|
261 qed |
|
262 |
|
263 lemma oprod_minus_Id2: |
|
264 "r' \<le> Id \<Longrightarrow> r *o r' - Id \<le> {((x1,y), (x2,y)). (x1, x2) \<in> (r - Id) \<and> y \<in> Field r'}" |
|
265 unfolding oprod_def by auto |
|
266 |
|
267 lemma wf_extend_oprod2: |
|
268 assumes "wf r" |
|
269 shows "wf {((x1,y), (x2,y)) . (x1, x2) \<in> r \<and> y \<in> A}" |
|
270 proof (unfold wf_eq_minimal2, intro allI impI, elim conjE) |
|
271 fix B |
|
272 assume *: "B \<subseteq> Field {((x1, y), (x2, y)). (x1, x2) \<in> r \<and> y \<in> A}" and "B \<noteq> {}" |
|
273 from image_mono[OF *, of fst] have "fst ` B \<subseteq> Field r" unfolding Field_def by force |
|
274 with `B \<noteq> {}` obtain x where x: "x \<in> fst ` B" "\<forall>x'\<in>fst ` B. (x', x) \<notin> r" |
|
275 using spec[OF assms[unfolded wf_eq_minimal2], of "fst ` B"] by auto |
|
276 then obtain a where "(x, a) \<in> B" by auto |
|
277 moreover |
|
278 from * x have "\<forall>a'\<in>B. (a', (x, a)) \<notin> {((x1, y), x2, y). (x1, x2) \<in> r \<and> y \<in> A}" by auto |
|
279 ultimately show "\<exists>xa\<in>B. \<forall>a'\<in>B. (a', xa) \<notin> {((x1, y), x2, y). (x1, x2) \<in> r \<and> y \<in> A}" by blast |
|
280 qed |
|
281 |
|
282 lemma oprod_wf_Id: |
|
283 assumes TOT: "Total r" and TOT': "Total r'" and WF: "wf(r - Id)" and WF': "wf(r' - Id)" |
|
284 shows "wf ((r *o r') - Id)" |
|
285 proof(cases "r \<le> Id \<or> r' \<le> Id") |
|
286 case False |
|
287 thus ?thesis |
|
288 using oprod_minus_Id[of r r'] assms oprod_wf[of "r - Id" "r' - Id"] |
|
289 wf_subset[of "(r - Id) *o (r' - Id)" "(r *o r') - Id"] by auto |
|
290 next |
|
291 case True |
|
292 thus ?thesis using wf_subset[OF wf_extend_oprod1[OF WF'] oprod_minus_Id1] |
|
293 wf_subset[OF wf_extend_oprod2[OF WF] oprod_minus_Id2] by auto |
|
294 qed |
|
295 |
|
296 lemma oprod_Well_order: |
|
297 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
298 shows "Well_order (r *o r')" |
|
299 proof- |
|
300 have "Total r \<and> Total r'" using WELL WELL' by (auto simp add: order_on_defs) |
|
301 thus ?thesis using assms unfolding well_order_on_def |
|
302 using oprod_Linear_order oprod_wf_Id by blast |
|
303 qed |
|
304 |
|
305 lemma oprod_embed: |
|
306 assumes WELL: "Well_order r" and WELL': "Well_order r'" and "r' \<noteq> {}" |
|
307 shows "embed r (r *o r') (\<lambda>x. (x, minim r' (Field r')))" (is "embed _ _ ?f") |
|
308 proof - |
|
309 from assms(3) have r': "Field r' \<noteq> {}" unfolding Field_def by auto |
|
310 have minim[simp]: "minim r' (Field r') \<in> Field r'" |
|
311 using wo_rel.minim_inField[unfolded wo_rel_def, OF WELL' _ r'] by auto |
|
312 { fix b |
|
313 assume "(b, minim r' (Field r')) \<in> r'" |
|
314 moreover hence "b \<in> Field r'" unfolding Field_def by auto |
|
315 hence "(minim r' (Field r'), b) \<in> r'" |
|
316 using wo_rel.minim_least[unfolded wo_rel_def, OF WELL' subset_refl] r' by auto |
|
317 ultimately have "b = minim r' (Field r')" |
|
318 by (metis WELL' antisym_def linear_order_on_def partial_order_on_def well_order_on_def) |
|
319 } note * = this |
|
320 have 1: "Well_order (r *o r')" using assms by (auto simp add: oprod_Well_order) |
|
321 moreover |
|
322 from r' have "compat r (r *o r') ?f" unfolding compat_def oprod_def by auto |
|
323 moreover |
|
324 from * have "ofilter (r *o r') (?f ` Field r)" |
|
325 unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod rel.under_def |
|
326 unfolding oprod_def by auto (auto simp: image_iff Field_def) |
|
327 moreover have "inj_on ?f (Field r)" unfolding inj_on_def by auto |
|
328 ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter) |
|
329 qed |
|
330 |
|
331 corollary oprod_ordLeq: "\<lbrakk>Well_order r; Well_order r'; r' \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o r *o r'" |
|
332 using oprod_embed oprod_Well_order unfolding ordLeq_def by blast |
|
333 |
|
334 definition "support z A f = {x \<in> A. f x \<noteq> z}" |
|
335 |
|
336 lemma support_Un[simp]: "support z (A \<union> B) f = support z A f \<union> support z B f" |
|
337 unfolding support_def by auto |
|
338 |
|
339 lemma support_upd[simp]: "support z A (f(x := z)) = support z A f - {x}" |
|
340 unfolding support_def by auto |
|
341 |
|
342 lemma support_upd_subset[simp]: "support z A (f(x := y)) \<subseteq> support z A f \<union> {x}" |
|
343 unfolding support_def by auto |
|
344 |
|
345 lemma fun_unequal_in_support: |
|
346 assumes "f \<noteq> g" "f \<in> Func A B" "g \<in> Func A C" |
|
347 shows "(support z A f \<union> support z A g) \<inter> {a. f a \<noteq> g a} \<noteq> {}" (is "?L \<inter> ?R \<noteq> {}") |
|
348 proof - |
|
349 from assms(1) obtain x where x: "f x \<noteq> g x" by blast |
|
350 hence "x \<in> ?R" by simp |
|
351 moreover from assms(2-3) x have "x \<in> A" unfolding Func_def by fastforce |
|
352 with x have "x \<in> ?L" unfolding support_def by auto |
|
353 ultimately show ?thesis by auto |
|
354 qed |
|
355 |
|
356 definition fin_support where |
|
357 "fin_support z A = {f. finite (support z A f)}" |
|
358 |
|
359 lemma finite_support: "f \<in> fin_support z A \<Longrightarrow> finite (support z A f)" |
|
360 unfolding support_def fin_support_def by auto |
|
361 |
|
362 lemma fin_support_Field_osum: |
|
363 "f \<in> fin_support z (Inl ` A \<union> Inr ` B) \<longleftrightarrow> |
|
364 (f o Inl) \<in> fin_support z A \<and> (f o Inr) \<in> fin_support z B" (is "?L \<longleftrightarrow> ?R1 \<and> ?R2") |
|
365 proof safe |
|
366 assume ?L |
|
367 from `?L` show ?R1 unfolding fin_support_def support_def |
|
368 by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case id undefined"]) |
|
369 from `?L` show ?R2 unfolding fin_support_def support_def |
|
370 by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case undefined id"]) |
|
371 next |
|
372 assume ?R1 ?R2 |
|
373 thus ?L unfolding fin_support_def support_Un |
|
374 by (auto simp: support_def elim: finite_surj[of _ _ Inl] finite_surj[of _ _ Inr]) |
|
375 qed |
|
376 |
|
377 lemma Func_upd: "\<lbrakk>f \<in> Func A B; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> f(x := y) \<in> Func A B" |
|
378 unfolding Func_def by auto |
|
379 |
|
380 context wo_rel |
|
381 begin |
|
382 |
|
383 definition isMaxim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" |
|
384 where "isMaxim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (a,b) \<in> r)" |
|
385 |
|
386 definition maxim :: "'a set \<Rightarrow> 'a" |
|
387 where "maxim A \<equiv> THE b. isMaxim A b" |
|
388 |
|
389 lemma isMaxim_unique[intro]: "\<lbrakk>isMaxim A x; isMaxim A y\<rbrakk> \<Longrightarrow> x = y" |
|
390 unfolding isMaxim_def using antisymD[OF ANTISYM, of x y] by auto |
|
391 |
|
392 lemma maxim_isMaxim: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> isMaxim A (maxim A)" |
|
393 unfolding maxim_def |
|
394 proof (rule theI', rule ex_ex1I[OF _ isMaxim_unique, rotated], assumption+, |
|
395 induct A rule: finite_induct) |
|
396 case (insert x A) |
|
397 thus ?case |
|
398 proof (cases "A = {}") |
|
399 case True |
|
400 moreover have "isMaxim {x} x" unfolding isMaxim_def using refl_onD[OF REFL] insert(5) by auto |
|
401 ultimately show ?thesis by blast |
|
402 next |
|
403 case False |
|
404 with insert(3,5) obtain y where "isMaxim A y" by blast |
|
405 with insert(2,5) have "if (y, x) \<in> r then isMaxim (insert x A) x else isMaxim (insert x A) y" |
|
406 unfolding isMaxim_def subset_eq by (metis insert_iff max2_def max2_equals1 max2_iff) |
|
407 thus ?thesis by metis |
|
408 qed |
|
409 qed simp |
|
410 |
|
411 lemma maxim_in: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> maxim A \<in> A" |
|
412 using maxim_isMaxim unfolding isMaxim_def by auto |
|
413 |
|
414 lemma maxim_greatest: "\<lbrakk>finite A; x \<in> A; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> (x, maxim A) \<in> r" |
|
415 using maxim_isMaxim unfolding isMaxim_def by auto |
|
416 |
|
417 lemma isMaxim_zero: "isMaxim A zero \<Longrightarrow> A = {zero}" |
|
418 unfolding isMaxim_def by auto |
|
419 |
|
420 lemma maxim_insert: |
|
421 assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r" "x \<in> Field r" |
|
422 shows "maxim (insert x A) = max2 x (maxim A)" |
|
423 proof - |
|
424 from assms have *: "isMaxim (insert x A) (maxim (insert x A))" "isMaxim A (maxim A)" |
|
425 using maxim_isMaxim by auto |
|
426 show ?thesis |
|
427 proof (cases "(x, maxim A) \<in> r") |
|
428 case True |
|
429 with *(2) have "isMaxim (insert x A) (maxim A)" unfolding isMaxim_def |
|
430 using transD[OF TRANS, of _ x "maxim A"] by blast |
|
431 with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique) |
|
432 next |
|
433 case False |
|
434 hence "(maxim A, x) \<in> r" by (metis *(2) assms(3,4) in_mono in_notinI isMaxim_def) |
|
435 with *(2) assms(4) have "isMaxim (insert x A) x" unfolding isMaxim_def |
|
436 using transD[OF TRANS, of _ "maxim A" x] refl_onD[OF REFL, of x] by blast |
|
437 with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique) |
|
438 qed |
|
439 qed |
|
440 |
|
441 lemma maxim_Un: |
|
442 assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r" "finite B" "B \<noteq> {}" "B \<subseteq> Field r" |
|
443 shows "maxim (A \<union> B) = max2 (maxim A) (maxim B)" |
|
444 proof - |
|
445 from assms have *: "isMaxim (A \<union> B) (maxim (A \<union> B))" "isMaxim A (maxim A)" "isMaxim B (maxim B)" |
|
446 using maxim_isMaxim by auto |
|
447 show ?thesis |
|
448 proof (cases "(maxim A, maxim B) \<in> r") |
|
449 case True |
|
450 with *(2,3) have "isMaxim (A \<union> B) (maxim B)" unfolding isMaxim_def |
|
451 using transD[OF TRANS, of _ "maxim A" "maxim B"] by blast |
|
452 with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique) |
|
453 next |
|
454 case False |
|
455 hence "(maxim B, maxim A) \<in> r" by (metis *(2,3) assms(3,6) in_mono in_notinI isMaxim_def) |
|
456 with *(2,3) have "isMaxim (A \<union> B) (maxim A)" unfolding isMaxim_def |
|
457 using transD[OF TRANS, of _ "maxim B" "maxim A"] by blast |
|
458 with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique) |
|
459 qed |
|
460 qed |
|
461 |
|
462 lemma maxim_insert_zero: |
|
463 assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r" |
|
464 shows "maxim (insert zero A) = maxim A" |
|
465 using assms zero_in_Field maxim_in[OF assms] by (subst maxim_insert[unfolded max2_def]) auto |
|
466 |
|
467 lemma maxim_equality: "isMaxim A x \<Longrightarrow> maxim A = x" |
|
468 unfolding maxim_def by (rule the_equality) auto |
|
469 |
|
470 lemma maxim_singleton: |
|
471 "x \<in> Field r \<Longrightarrow> maxim {x} = x" |
|
472 using refl_onD[OF REFL] by (intro maxim_equality) (simp add: isMaxim_def) |
|
473 |
|
474 lemma maxim_Int: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r; maxim A \<in> B\<rbrakk> \<Longrightarrow> maxim (A \<inter> B) = maxim A" |
|
475 by (rule maxim_equality) (auto simp: isMaxim_def intro: maxim_in maxim_greatest) |
|
476 |
|
477 lemma maxim_mono: "\<lbrakk>X \<subseteq> Y; finite Y; X \<noteq> {}; Y \<subseteq> Field r\<rbrakk> \<Longrightarrow> (maxim X, maxim Y) \<in> r" |
|
478 using maxim_in[OF finite_subset, of X Y] by (auto intro: maxim_greatest) |
|
479 |
|
480 definition "max_fun_diff f g \<equiv> maxim ({a \<in> Field r. f a \<noteq> g a})" |
|
481 |
|
482 lemma max_fun_diff_commute: "max_fun_diff f g = max_fun_diff g f" |
|
483 unfolding max_fun_diff_def by metis |
|
484 |
|
485 lemma zero_under: "x \<in> Field r \<Longrightarrow> zero \<in> under x" |
|
486 unfolding under_def by (auto intro: zero_smallest) |
|
487 |
|
488 end |
|
489 |
|
490 definition "FinFunc r s = Func (Field s) (Field r) \<inter> fin_support (zero r) (Field s)" |
|
491 |
|
492 lemma FinFuncD: "\<lbrakk>f \<in> FinFunc r s; x \<in> Field s\<rbrakk> \<Longrightarrow> f x \<in> Field r" |
|
493 unfolding FinFunc_def Func_def by (fastforce split: option.splits) |
|
494 |
|
495 locale wo_rel2 = |
|
496 fixes r s |
|
497 assumes rWELL: "Well_order r" |
|
498 and sWELL: "Well_order s" |
|
499 begin |
|
500 |
|
501 interpretation r!: wo_rel r by unfold_locales (rule rWELL) |
|
502 interpretation s!: wo_rel s by unfold_locales (rule sWELL) |
|
503 |
|
504 abbreviation "SUPP \<equiv> support r.zero (Field s)" |
|
505 abbreviation "FINFUNC \<equiv> FinFunc r s" |
|
506 lemmas FINFUNCD = FinFuncD[of _ r s] |
|
507 |
|
508 lemma fun_diff_alt: "{a \<in> Field s. f a \<noteq> g a} = (SUPP f \<union> SUPP g) \<inter> {a. f a \<noteq> g a}" |
|
509 by (auto simp: support_def) |
|
510 |
|
511 lemma max_fun_diff_alt: |
|
512 "s.max_fun_diff f g = s.maxim ((SUPP f \<union> SUPP g) \<inter> {a. f a \<noteq> g a})" |
|
513 unfolding s.max_fun_diff_def fun_diff_alt .. |
|
514 |
|
515 lemma isMaxim_max_fun_diff: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow> |
|
516 s.isMaxim {a \<in> Field s. f a \<noteq> g a} (s.max_fun_diff f g)" |
|
517 using fun_unequal_in_support[of f g] unfolding max_fun_diff_alt fun_diff_alt fun_eq_iff |
|
518 by (intro s.maxim_isMaxim) (auto simp: FinFunc_def fin_support_def support_def) |
|
519 |
|
520 lemma max_fun_diff_in: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow> |
|
521 s.max_fun_diff f g \<in> {a \<in> Field s. f a \<noteq> g a}" |
|
522 using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast |
|
523 |
|
524 lemma max_fun_diff_max: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC; x \<in> {a \<in> Field s. f a \<noteq> g a}\<rbrakk> \<Longrightarrow> |
|
525 (x, s.max_fun_diff f g) \<in> s" |
|
526 using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast |
|
527 |
|
528 lemma max_fun_diff: |
|
529 "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow> |
|
530 (\<exists>a b. a \<noteq> b \<and> a \<in> Field r \<and> b \<in> Field r \<and> |
|
531 f (s.max_fun_diff f g) = a \<and> g (s.max_fun_diff f g) = b)" |
|
532 using isMaxim_max_fun_diff[of f g] unfolding s.isMaxim_def FinFunc_def Func_def by auto |
|
533 |
|
534 lemma max_fun_diff_le_eq: |
|
535 "\<lbrakk>(s.max_fun_diff f g, x) \<in> s; f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC; x \<noteq> s.max_fun_diff f g\<rbrakk> \<Longrightarrow> |
|
536 f x = g x" |
|
537 using max_fun_diff_max[of f g x] antisymD[OF s.ANTISYM, of "s.max_fun_diff f g" x] |
|
538 by (auto simp: Field_def) |
|
539 |
|
540 lemma max_fun_diff_max2: |
|
541 assumes ineq: "s.max_fun_diff f g = s.max_fun_diff g h \<longrightarrow> |
|
542 f (s.max_fun_diff f g) \<noteq> h (s.max_fun_diff g h)" and |
|
543 fg: "f \<noteq> g" and gh: "g \<noteq> h" and fh: "f \<noteq> h" and |
|
544 f: "f \<in> FINFUNC" and g: "g \<in> FINFUNC" and h: "h \<in> FINFUNC" |
|
545 shows "s.max_fun_diff f h = s.max2 (s.max_fun_diff f g) (s.max_fun_diff g h)" |
|
546 (is "?fh = s.max2 ?fg ?gh") |
|
547 proof (cases "?fg = ?gh") |
|
548 case True |
|
549 with ineq have "f ?fg \<noteq> h ?fg" by simp |
|
550 moreover |
|
551 { fix x assume x: "x \<in> {a \<in> Field s. f a \<noteq> h a}" |
|
552 hence "(x, ?fg) \<in> s" |
|
553 proof (cases "x = ?fg") |
|
554 case False show ?thesis |
|
555 proof (rule ccontr) |
|
556 assume "(x, ?fg) \<notin> s" |
|
557 with max_fun_diff_in[OF fg f g] x False have *: "(?fg, x) \<in> s" by (blast intro: s.in_notinI) |
|
558 hence "f x = g x" by (rule max_fun_diff_le_eq[OF _ fg f g False]) |
|
559 moreover have "g x = h x" using max_fun_diff_le_eq[OF _ gh g h] False True * by simp |
|
560 ultimately show False using x by simp |
|
561 qed |
|
562 qed (simp add: refl_onD[OF s.REFL]) |
|
563 } |
|
564 ultimately have "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg" |
|
565 unfolding s.isMaxim_def using max_fun_diff_in[OF fg f g] by simp |
|
566 hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast |
|
567 thus ?thesis unfolding True s.max2_def by simp |
|
568 next |
|
569 case False note * = this |
|
570 show ?thesis |
|
571 proof (cases "(?fg, ?gh) \<in> s") |
|
572 case True |
|
573 hence *: "f ?gh = g ?gh" by (rule max_fun_diff_le_eq[OF _ fg f g *[symmetric]]) |
|
574 hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?gh" using isMaxim_max_fun_diff[OF gh g h] |
|
575 isMaxim_max_fun_diff[OF fg f g] transD[OF s.TRANS _ True] |
|
576 unfolding s.isMaxim_def by auto |
|
577 hence "?fh = ?gh" using isMaxim_max_fun_diff[OF fh f h] by blast |
|
578 thus ?thesis using True unfolding s.max2_def by simp |
|
579 next |
|
580 case False |
|
581 with max_fun_diff_in[OF fg f g] max_fun_diff_in[OF gh g h] have True: "(?gh, ?fg) \<in> s" |
|
582 by (blast intro: s.in_notinI) |
|
583 hence *: "g ?fg = h ?fg" by (rule max_fun_diff_le_eq[OF _ gh g h *]) |
|
584 hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg" using isMaxim_max_fun_diff[OF gh g h] |
|
585 isMaxim_max_fun_diff[OF fg f g] True transD[OF s.TRANS, of _ _ ?fg] |
|
586 unfolding s.isMaxim_def by auto |
|
587 hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast |
|
588 thus ?thesis using False unfolding s.max2_def by simp |
|
589 qed |
|
590 qed |
|
591 |
|
592 |
|
593 definition oexp where |
|
594 "oexp = {(f, g) . f \<in> FINFUNC \<and> g \<in> FINFUNC \<and> |
|
595 ((let m = s.max_fun_diff f g in (f m, g m) \<in> r) \<or> f = g)}" |
|
596 |
|
597 lemma Field_oexp: "Field oexp = FINFUNC" |
|
598 unfolding oexp_def FinFunc_def by (auto simp: Let_def Field_def) |
|
599 |
|
600 lemma oexp_Refl: "Refl oexp" |
|
601 unfolding refl_on_def Field_oexp unfolding oexp_def by (auto simp: Let_def) |
|
602 |
|
603 lemma oexp_trans: "trans oexp" |
|
604 proof (unfold trans_def, safe) |
|
605 fix f g h :: "'b \<Rightarrow> 'a" |
|
606 let ?fg = "s.max_fun_diff f g" |
|
607 and ?gh = "s.max_fun_diff g h" |
|
608 and ?fh = "s.max_fun_diff f h" |
|
609 assume oexp: "(f, g) \<in> oexp" "(g, h) \<in> oexp" |
|
610 thus "(f, h) \<in> oexp" |
|
611 proof (cases "f = g \<or> g = h") |
|
612 case False |
|
613 with oexp have "f \<in> FINFUNC" "g \<in> FINFUNC" "h \<in> FINFUNC" |
|
614 "(f ?fg, g ?fg) \<in> r" "(g ?gh, h ?gh) \<in> r" unfolding oexp_def Let_def by auto |
|
615 note * = this False |
|
616 show ?thesis |
|
617 proof (cases "f \<noteq> h") |
|
618 case True |
|
619 show ?thesis |
|
620 proof (cases "?fg = ?gh \<longrightarrow> f ?fg \<noteq> h ?gh") |
|
621 case True |
|
622 show ?thesis using max_fun_diff_max2[of f g h, OF True] * `f \<noteq> h` max_fun_diff_in |
|
623 r.max2_iff[OF FINFUNCD FINFUNCD] r.max2_equals1[OF FINFUNCD FINFUNCD] max_fun_diff_le_eq |
|
624 s.in_notinI[OF disjI1] unfolding oexp_def Let_def s.max2_def mem_Collect_eq by safe metis |
|
625 next |
|
626 case False with * show ?thesis unfolding oexp_def Let_def |
|
627 using antisymD[OF r.ANTISYM, of "g ?gh" "h ?gh"] max_fun_diff_in[of g h] by auto |
|
628 qed |
|
629 qed (auto simp: oexp_def *(3)) |
|
630 qed auto |
|
631 qed |
|
632 |
|
633 lemma oexp_Preorder: "Preorder oexp" |
|
634 unfolding preorder_on_def using oexp_Refl oexp_trans by blast |
|
635 |
|
636 lemma oexp_antisym: "antisym oexp" |
|
637 proof (unfold antisym_def, safe, rule ccontr) |
|
638 fix f g assume "(f, g) \<in> oexp" "(g, f) \<in> oexp" "g \<noteq> f" |
|
639 thus False using refl_onD[OF r.REFL FINFUNCD] max_fun_diff_in unfolding oexp_def Let_def |
|
640 by (auto dest!: antisymD[OF r.ANTISYM] simp: s.max_fun_diff_commute) |
|
641 qed |
|
642 |
|
643 lemma oexp_Partial_order: "Partial_order oexp" |
|
644 unfolding partial_order_on_def using oexp_Preorder oexp_antisym by blast |
|
645 |
|
646 lemma oexp_Total: "Total oexp" |
|
647 unfolding total_on_def Field_oexp unfolding oexp_def using FINFUNCD max_fun_diff_in |
|
648 by (auto simp: Let_def s.max_fun_diff_commute intro!: r.in_notinI) |
|
649 |
|
650 lemma oexp_Linear_order: "Linear_order oexp" |
|
651 unfolding linear_order_on_def using oexp_Partial_order oexp_Total by blast |
|
652 |
|
653 definition "const = (\<lambda>x. if x \<in> Field s then r.zero else undefined)" |
|
654 |
|
655 lemma const_in[simp]: "x \<in> Field s \<Longrightarrow> const x = r.zero" |
|
656 unfolding const_def by auto |
|
657 |
|
658 lemma const_notin[simp]: "x \<notin> Field s \<Longrightarrow> const x = undefined" |
|
659 unfolding const_def by auto |
|
660 |
|
661 lemma const_Int_Field[simp]: "Field s \<inter> - {x. const x = r.zero} = {}" |
|
662 by auto |
|
663 |
|
664 lemma const_FINFUNC[simp]: "Field r \<noteq> {} \<Longrightarrow> const \<in> FINFUNC" |
|
665 unfolding FinFunc_def Func_def fin_support_def support_def const_def Int_iff mem_Collect_eq |
|
666 using r.zero_in_Field by (metis (lifting) Collect_empty_eq finite.emptyI) |
|
667 |
|
668 lemma const_least: |
|
669 assumes "Field r \<noteq> {}" "f \<in> FINFUNC" |
|
670 shows "(const, f) \<in> oexp" |
|
671 proof (cases "f = const") |
|
672 case True thus ?thesis using refl_onD[OF oexp_Refl] assms(2) unfolding Field_oexp by auto |
|
673 next |
|
674 case False |
|
675 with assms show ?thesis using max_fun_diff_in[of f const] |
|
676 unfolding oexp_def Let_def by (auto intro: r.zero_smallest FinFuncD simp: s.max_fun_diff_commute) |
|
677 qed |
|
678 |
|
679 lemma support_not_const: |
|
680 assumes "F \<subseteq> FINFUNC" and "const \<notin> F" |
|
681 shows "\<forall>f \<in> F. finite (SUPP f) \<and> SUPP f \<noteq> {} \<and> SUPP f \<subseteq> Field s" |
|
682 proof (intro ballI conjI) |
|
683 fix f assume "f \<in> F" |
|
684 thus "finite (SUPP f)" "SUPP f \<subseteq> Field s" |
|
685 using assms(1) unfolding FinFunc_def fin_support_def support_def by auto |
|
686 show "SUPP f \<noteq> {}" |
|
687 proof (rule ccontr, unfold not_not) |
|
688 assume "SUPP f = {}" |
|
689 moreover from `f \<in> F` assms(1) have "f \<in> FINFUNC" by blast |
|
690 ultimately have "f = const" |
|
691 by (auto simp: fun_eq_iff support_def FinFunc_def Func_def const_def) |
|
692 with assms(2) `f \<in> F` show False by blast |
|
693 qed |
|
694 qed |
|
695 |
|
696 lemma maxim_isMaxim_support: |
|
697 assumes f: "F \<subseteq> FINFUNC" and "const \<notin> F" |
|
698 shows "\<forall>f \<in> F. s.isMaxim (SUPP f) (s.maxim (SUPP f))" |
|
699 using support_not_const[OF assms] by (auto intro!: s.maxim_isMaxim) |
|
700 |
|
701 lemma oexp_empty2: "Field s = {} \<Longrightarrow> oexp = {(\<lambda>x. undefined, \<lambda>x. undefined)}" |
|
702 unfolding oexp_def FinFunc_def fin_support_def support_def by auto |
|
703 |
|
704 lemma oexp_empty: "\<lbrakk>Field r = {}; Field s \<noteq> {}\<rbrakk> \<Longrightarrow> oexp = {}" |
|
705 unfolding oexp_def FinFunc_def Let_def by auto |
|
706 |
|
707 lemma fun_upd_FINFUNC: "\<lbrakk>f \<in> FINFUNC; x \<in> Field s; y \<in> Field r\<rbrakk> \<Longrightarrow> f(x := y) \<in> FINFUNC" |
|
708 unfolding FinFunc_def Func_def fin_support_def |
|
709 by (auto intro: finite_subset[OF support_upd_subset]) |
|
710 |
|
711 lemma fun_upd_same_oexp: |
|
712 assumes "(f, g) \<in> oexp" "f x = g x" "x \<in> Field s" "y \<in> Field r" |
|
713 shows "(f(x := y), g(x := y)) \<in> oexp" |
|
714 proof - |
|
715 from assms(1) fun_upd_FINFUNC[OF _ assms(3,4)] have fg: "f(x := y) \<in> FINFUNC" "g(x := y) \<in> FINFUNC" |
|
716 unfolding oexp_def by auto |
|
717 moreover from assms(2) have "s.max_fun_diff (f(x := y)) (g(x := y)) = s.max_fun_diff f g" |
|
718 unfolding s.max_fun_diff_def by auto metis |
|
719 ultimately show ?thesis using assms refl_onD[OF r.REFL] unfolding oexp_def Let_def by auto |
|
720 qed |
|
721 |
|
722 lemma fun_upd_smaller_oexp: |
|
723 assumes "f \<in> FINFUNC" "x \<in> Field s" "y \<in> Field r" "(y, f x) \<in> r" |
|
724 shows "(f(x := y), f) \<in> oexp" |
|
725 using assms fun_upd_FINFUNC[OF assms(1-3)] s.maxim_singleton[of "x"] |
|
726 unfolding oexp_def FinFunc_def Let_def fin_support_def s.max_fun_diff_def by (auto simp: fun_eq_iff) |
|
727 |
|
728 lemma oexp_wf_Id: "wf (oexp - Id)" |
|
729 proof (cases "Field r = {} \<or> Field s = {}") |
|
730 case True thus ?thesis using oexp_empty oexp_empty2 by fastforce |
|
731 next |
|
732 case False |
|
733 hence Fields: "Field s \<noteq> {}" "Field r \<noteq> {}" by simp_all |
|
734 hence [simp]: "r.zero \<in> Field r" by (intro r.zero_in_Field) |
|
735 have const[simp]: "\<And>F. \<lbrakk>const \<in> F; F \<subseteq> FINFUNC\<rbrakk> \<Longrightarrow> \<exists>f0\<in>F. \<forall>f\<in>F. (f0, f) \<in> oexp" |
|
736 using const_least[OF Fields(2)] by auto |
|
737 show ?thesis |
|
738 unfolding Linear_order_wf_diff_Id[OF oexp_Linear_order] Field_oexp |
|
739 proof (intro allI impI) |
|
740 fix A assume A: "A \<subseteq> FINFUNC" "A \<noteq> {}" |
|
741 { fix y F |
|
742 have "F \<subseteq> FINFUNC \<and> (\<exists>f \<in> F. y = s.maxim (SUPP f)) \<longrightarrow> |
|
743 (\<exists>f0 \<in> F. \<forall>f \<in> F. (f0, f) \<in> oexp)" (is "?P F y") |
|
744 proof (induct y arbitrary: F rule: s.well_order_induct) |
|
745 case (1 y) |
|
746 show ?case |
|
747 proof (intro impI, elim conjE bexE) |
|
748 fix f assume F: "F \<subseteq> FINFUNC" "f \<in> F" "y = s.maxim (SUPP f)" |
|
749 thus "\<exists>f0\<in>F. \<forall>f\<in>F. (f0, f) \<in> oexp" |
|
750 proof (cases "const \<in> F") |
|
751 case False |
|
752 with F have maxF: "\<forall>f \<in> F. s.isMaxim (SUPP f) (s.maxim (SUPP f))" |
|
753 and SUPPF: "\<forall>f \<in> F. finite (SUPP f) \<and> SUPP f \<noteq> {} \<and> SUPP f \<subseteq> Field s" |
|
754 using maxim_isMaxim_support support_not_const by auto |
|
755 def z \<equiv> "s.minim {s.maxim (SUPP f) | f. f \<in> F}" |
|
756 from F SUPPF maxF have zmin: "s.isMinim {s.maxim (SUPP f) | f. f \<in> F} z" |
|
757 unfolding z_def by (intro s.minim_isMinim) (auto simp: s.isMaxim_def) |
|
758 with F have zy: "(z, y) \<in> s" unfolding s.isMinim_def by auto |
|
759 hence zField: "z \<in> Field s" unfolding Field_def by auto |
|
760 def x0 \<equiv> "r.minim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)}" |
|
761 from F(1,2) maxF(1) SUPPF zmin |
|
762 have x0min: "r.isMinim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)} x0" |
|
763 unfolding x0_def s.isMaxim_def s.isMinim_def |
|
764 by (blast intro!: r.minim_isMinim FinFuncD[of _ r s]) |
|
765 with maxF(1) SUPPF F(1) have x0Field: "x0 \<in> Field r" |
|
766 unfolding r.isMinim_def s.isMaxim_def by (auto intro!: FINFUNCD) |
|
767 from x0min maxF(1) SUPPF F(1) have x0notzero: "x0 \<noteq> r.zero" |
|
768 unfolding r.isMinim_def s.isMaxim_def FinFunc_def Func_def support_def |
|
769 by fastforce |
|
770 def G \<equiv> "{f(z := r.zero) | f. f \<in> F \<and> z = s.maxim (SUPP f) \<and> f z = x0}" |
|
771 from zmin x0min have "G \<noteq> {}" unfolding G_def z_def s.isMinim_def r.isMinim_def by blast |
|
772 have GF: "G \<subseteq> (\<lambda>f. f(z := r.zero)) ` F" unfolding G_def by auto |
|
773 have "G \<subseteq> fin_support r.zero (Field s)" |
|
774 unfolding FinFunc_def fin_support_def proof safe |
|
775 fix g assume "g \<in> G" |
|
776 with GF obtain f where "f \<in> F" "g = f(z := r.zero)" by auto |
|
777 moreover with SUPPF have "finite (SUPP f)" by blast |
|
778 ultimately show "finite (SUPP g)" |
|
779 by (elim finite_subset[rotated]) (auto simp: support_def) |
|
780 qed |
|
781 moreover from F GF zField have "G \<subseteq> Func (Field s) (Field r)" |
|
782 using Func_upd[of _ "Field s" "Field r" z r.zero] unfolding FinFunc_def by auto |
|
783 ultimately have G: "G \<subseteq> FINFUNC" unfolding FinFunc_def by blast |
|
784 hence "\<exists>g0\<in>G. \<forall>g\<in>G. (g0, g) \<in> oexp" |
|
785 proof (cases "const \<in> G") |
|
786 case False |
|
787 with G have maxG: "\<forall>g \<in> G. s.isMaxim (SUPP g) (s.maxim (SUPP g))" |
|
788 and SUPPG: "\<forall>g \<in> G. finite (SUPP g) \<and> SUPP g \<noteq> {} \<and> SUPP g \<subseteq> Field s" |
|
789 using maxim_isMaxim_support support_not_const by auto |
|
790 def y' \<equiv> "s.minim {s.maxim (SUPP f) | f. f \<in> G}" |
|
791 from G SUPPG maxG `G \<noteq> {}` have y'min: "s.isMinim {s.maxim (SUPP f) | f. f \<in> G} y'" |
|
792 unfolding y'_def by (intro s.minim_isMinim) (auto simp: s.isMaxim_def) |
|
793 moreover |
|
794 have "\<forall>g \<in> G. z \<notin> SUPP g" unfolding support_def G_def by auto |
|
795 moreover |
|
796 { fix g assume g: "g \<in> G" |
|
797 then obtain f where "f \<in> F" "g = f(z := r.zero)" and z: "z = s.maxim (SUPP f)" |
|
798 unfolding G_def by auto |
|
799 with SUPPF bspec[OF SUPPG g] have "(s.maxim (SUPP g), z) \<in> s" |
|
800 unfolding z by (intro s.maxim_mono) auto |
|
801 } |
|
802 moreover from y'min have "\<And>g. g \<in> G \<Longrightarrow> (y', s.maxim (SUPP g)) \<in> s" |
|
803 unfolding s.isMinim_def by auto |
|
804 ultimately have "y' \<noteq> z" "(y', z) \<in> s" using maxG |
|
805 unfolding s.isMinim_def s.isMaxim_def by auto |
|
806 with zy have "y' \<noteq> y" "(y', y) \<in> s" using antisymD[OF s.ANTISYM] transD[OF s.TRANS] |
|
807 by blast+ |
|
808 moreover from `G \<noteq> {}` have "\<exists>g \<in> G. y' = wo_rel.maxim s (SUPP g)" using y'min |
|
809 by (auto simp: G_def s.isMinim_def) |
|
810 ultimately show ?thesis using mp[OF spec[OF mp[OF spec[OF 1]]], of y' G] G by auto |
|
811 qed simp |
|
812 then obtain g0 where g0: "g0 \<in> G" "\<forall>g \<in> G. (g0, g) \<in> oexp" by blast |
|
813 hence g0z: "g0 z = r.zero" unfolding G_def by auto |
|
814 def f0 \<equiv> "g0(z := x0)" |
|
815 with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 \<union> {z}" unfolding support_def by auto |
|
816 from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto |
|
817 have f0: "f0 \<in> F" using x0min g0(1) |
|
818 Func_elim[OF set_mp[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField] |
|
819 unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem) |
|
820 from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def |
|
821 by (intro s.maxim_equality) (auto simp: s.isMaxim_def) |
|
822 show ?thesis |
|
823 proof (intro bexI[OF _ f0] ballI) |
|
824 fix f assume f: "f \<in> F" |
|
825 show "(f0, f) \<in> oexp" |
|
826 proof (cases "f0 = f") |
|
827 case True thus ?thesis by (metis F(1) Field_oexp f0 in_mono oexp_Refl refl_onD) |
|
828 next |
|
829 case False |
|
830 thus ?thesis |
|
831 proof (cases "s.maxim (SUPP f) = z \<and> f z = x0") |
|
832 case True |
|
833 with f have "f(z := r.zero) \<in> G" unfolding G_def by blast |
|
834 with g0(2) f0z have "(f0(z := r.zero), f(z := r.zero)) \<in> oexp" by auto |
|
835 hence "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp" |
|
836 by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp |
|
837 moreover |
|
838 with f F(1) x0min True |
|
839 have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def |
|
840 by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto |
|
841 ultimately show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f] |
|
842 unfolding f0_def by auto |
|
843 next |
|
844 case False note notG = this |
|
845 thus ?thesis |
|
846 proof (cases "s.maxim (SUPP f) = z") |
|
847 case True |
|
848 with notG have "f0 z \<noteq> f z" unfolding f0_def by auto |
|
849 hence "f0 z \<noteq> f z" by metis |
|
850 with True maxf0 f0 f SUPPF have "s.max_fun_diff f0 f = z" |
|
851 using s.maxim_Un[of "SUPP f0" "SUPP f", unfolded s.max2_def] |
|
852 unfolding max_fun_diff_alt by (intro trans[OF s.maxim_Int]) auto |
|
853 moreover |
|
854 from x0min True f have "(x0, f z) \<in> r" unfolding r.isMinim_def by auto |
|
855 ultimately show ?thesis using f f0 F(1) unfolding oexp_def f0_def by auto |
|
856 next |
|
857 case False |
|
858 with notG have *: "(z, s.maxim (SUPP f)) \<in> s" "z \<noteq> s.maxim (SUPP f)" |
|
859 using zmin f unfolding s.isMinim_def G_def by auto |
|
860 have f0f: "f0 (s.maxim (SUPP f)) = r.zero" |
|
861 proof (rule ccontr) |
|
862 assume "f0 (s.maxim (SUPP f)) \<noteq> r.zero" |
|
863 with f SUPPF maxF(1) have "s.maxim (SUPP f) \<in> SUPP f0" |
|
864 unfolding support_def[of _ _ f0] s.isMaxim_def by auto |
|
865 with SUPPF f0 have "(s.maxim (SUPP f), z) \<in> s" unfolding maxf0[symmetric] |
|
866 by (auto intro: s.maxim_greatest) |
|
867 with * antisymD[OF s.ANTISYM] show False by simp |
|
868 qed |
|
869 moreover |
|
870 have "f (s.maxim (SUPP f)) \<noteq> r.zero" |
|
871 using bspec[OF maxF(1) f, unfolded s.isMaxim_def] by (auto simp: support_def) |
|
872 with f0f * f f0 maxf0 SUPPF |
|
873 have "s.max_fun_diff f0 f = s.maxim (SUPP f0 \<union> SUPP f)" |
|
874 unfolding max_fun_diff_alt using s.maxim_Un[of "SUPP f0" "SUPP f"] |
|
875 by (intro s.maxim_Int) (auto simp: s.max2_def) |
|
876 moreover have "s.maxim (SUPP f0 \<union> SUPP f) = s.maxim (SUPP f)" |
|
877 using s.maxim_Un[of "SUPP f0" "SUPP f"] * maxf0 SUPPF f0 f |
|
878 by (auto simp: s.max2_def) |
|
879 ultimately show ?thesis using f f0 F(1) maxF(1) SUPPF unfolding oexp_def Let_def |
|
880 by (fastforce simp: s.isMaxim_def intro!: r.zero_smallest FINFUNCD) |
|
881 qed |
|
882 qed |
|
883 qed |
|
884 qed |
|
885 qed simp |
|
886 qed |
|
887 qed |
|
888 } note * = mp[OF this] |
|
889 from A(2) obtain f where f: "f \<in> A" by blast |
|
890 with A(1) show "\<exists>a\<in>A. \<forall>a'\<in>A. (a, a') \<in> oexp" |
|
891 proof (cases "f = const") |
|
892 case False with f A(1) show ?thesis using maxim_isMaxim_support[of "{f}"] |
|
893 by (intro *[of _ "s.maxim (SUPP f)"]) (auto simp: s.isMaxim_def support_def) |
|
894 qed simp |
|
895 qed |
|
896 qed |
|
897 |
|
898 lemma oexp_Well_order: "Well_order oexp" |
|
899 unfolding well_order_on_def using oexp_Linear_order oexp_wf_Id by blast |
|
900 |
|
901 interpretation o: wo_rel oexp by unfold_locales (rule oexp_Well_order) |
|
902 |
|
903 lemma zero_oexp: "Field r \<noteq> {} \<Longrightarrow> o.zero = const" |
|
904 by (rule sym[OF o.leq_zero_imp[OF const_least]]) |
|
905 (auto intro!: o.zero_in_Field[unfolded Field_oexp] dest!: const_FINFUNC) |
|
906 |
|
907 end |
|
908 |
|
909 notation wo_rel2.oexp (infixl "^o" 90) |
|
910 lemmas oexp_def = wo_rel2.oexp_def[unfolded wo_rel2_def, OF conjI] |
|
911 lemmas oexp_Well_order = wo_rel2.oexp_Well_order[unfolded wo_rel2_def, OF conjI] |
|
912 lemmas Field_oexp = wo_rel2.Field_oexp[unfolded wo_rel2_def, OF conjI] |
|
913 |
|
914 definition "ozero = {}" |
|
915 |
|
916 lemma ozero_Well_order[simp]: "Well_order ozero" |
|
917 unfolding ozero_def by simp |
|
918 |
|
919 lemma ozero_ordIso[simp]: "ozero =o ozero" |
|
920 unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def by auto |
|
921 |
|
922 lemma Field_ozero[simp]: "Field ozero = {}" |
|
923 unfolding ozero_def by simp |
|
924 |
|
925 lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})" |
|
926 unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def |
|
927 by (auto dest: rel.well_order_on_domain) |
|
928 |
|
929 lemma ozero_ordLeq: |
|
930 assumes "Well_order r" shows "ozero \<le>o r" |
|
931 using assms unfolding ozero_def ordLeq_def embed_def[abs_def] rel.under_def by auto |
|
932 |
|
933 definition "oone = {((),())}" |
|
934 |
|
935 lemma oone_Well_order[simp]: "Well_order oone" |
|
936 unfolding oone_def unfolding well_order_on_def linear_order_on_def partial_order_on_def |
|
937 preorder_on_def total_on_def refl_on_def trans_def antisym_def by auto |
|
938 |
|
939 lemma Field_oone[simp]: "Field oone = {()}" |
|
940 unfolding oone_def by simp |
|
941 |
|
942 lemma oone_ordIso: "oone =o {(x,x)}" |
|
943 unfolding ordIso_def oone_def well_order_on_def linear_order_on_def partial_order_on_def |
|
944 preorder_on_def total_on_def refl_on_def trans_def antisym_def |
|
945 by (auto simp: iso_def embed_def bij_betw_def rel.under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"]) |
|
946 |
|
947 lemma osum_ordLeqR: "Well_order r \<Longrightarrow> Well_order s \<Longrightarrow> s \<le>o r +o s" |
|
948 unfolding ordLeq_def2 rel.underS_def |
|
949 by (auto intro!: exI[of _ Inr] osum_Well_order) (auto simp add: osum_def Field_def) |
|
950 |
|
951 lemma osum_congL: |
|
952 assumes "r =o s" and t: "Well_order t" |
|
953 shows "r +o t =o s +o t" (is "?L =o ?R") |
|
954 proof - |
|
955 from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f" |
|
956 unfolding ordIso_def by blast |
|
957 let ?f = "sum_map f id" |
|
958 from f have "inj_on ?f (Field ?L)" |
|
959 unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce |
|
960 with f have "bij_betw ?f (Field ?L) (Field ?R)" |
|
961 unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto |
|
962 moreover from f have "compat ?L ?R ?f" |
|
963 unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def |
|
964 by (auto simp: map_pair_imageI) |
|
965 ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t) |
|
966 thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t) |
|
967 qed |
|
968 |
|
969 lemma osum_congR: |
|
970 assumes "r =o s" and t: "Well_order t" |
|
971 shows "t +o r =o t +o s" (is "?L =o ?R") |
|
972 proof - |
|
973 from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f" |
|
974 unfolding ordIso_def by blast |
|
975 let ?f = "sum_map id f" |
|
976 from f have "inj_on ?f (Field ?L)" |
|
977 unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce |
|
978 with f have "bij_betw ?f (Field ?L) (Field ?R)" |
|
979 unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto |
|
980 moreover from f have "compat ?L ?R ?f" |
|
981 unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def |
|
982 by (auto simp: map_pair_imageI) |
|
983 ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t) |
|
984 thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t) |
|
985 qed |
|
986 |
|
987 lemma osum_cong: |
|
988 assumes "t =o u" and "r =o s" |
|
989 shows "t +o r =o u +o s" |
|
990 using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]] |
|
991 assms[unfolded ordIso_def] by auto |
|
992 |
|
993 lemma Well_order_empty[simp]: "Well_order {}" |
|
994 unfolding Field_empty by (rule well_order_on_empty) |
|
995 |
|
996 lemma well_order_on_singleton[simp]: "well_order_on {x} {(x, x)}" |
|
997 unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def total_on_def |
|
998 Field_def refl_on_def trans_def antisym_def by auto |
|
999 |
|
1000 lemma oexp_empty[simp]: |
|
1001 assumes "Well_order r" |
|
1002 shows "r ^o {} = {(\<lambda>x. undefined, \<lambda>x. undefined)}" |
|
1003 unfolding oexp_def[OF assms Well_order_empty] FinFunc_def fin_support_def support_def by auto |
|
1004 |
|
1005 lemma oexp_empty2[simp]: |
|
1006 assumes "Well_order r" "r \<noteq> {}" |
|
1007 shows "{} ^o r = {}" |
|
1008 proof - |
|
1009 from assms(2) have "Field r \<noteq> {}" unfolding Field_def by auto |
|
1010 thus ?thesis unfolding oexp_def[OF Well_order_empty assms(1)] FinFunc_def fin_support_def support_def |
|
1011 by auto |
|
1012 qed |
|
1013 |
|
1014 lemma oprod_zero[simp]: "{} *o r = {}" "r *o {} = {}" |
|
1015 unfolding oprod_def by simp_all |
|
1016 |
|
1017 lemma oprod_congL: |
|
1018 assumes "r =o s" and t: "Well_order t" |
|
1019 shows "r *o t =o s *o t" (is "?L =o ?R") |
|
1020 proof - |
|
1021 from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f" |
|
1022 unfolding ordIso_def by blast |
|
1023 let ?f = "map_pair f id" |
|
1024 from f have "inj_on ?f (Field ?L)" |
|
1025 unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce |
|
1026 with f have "bij_betw ?f (Field ?L) (Field ?R)" |
|
1027 unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on) |
|
1028 moreover from f have "compat ?L ?R ?f" |
|
1029 unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def |
|
1030 by (auto simp: map_pair_imageI) |
|
1031 ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t) |
|
1032 thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t) |
|
1033 qed |
|
1034 |
|
1035 lemma oprod_congR: |
|
1036 assumes "r =o s" and t: "Well_order t" |
|
1037 shows "t *o r =o t *o s" (is "?L =o ?R") |
|
1038 proof - |
|
1039 from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f" |
|
1040 unfolding ordIso_def by blast |
|
1041 let ?f = "map_pair id f" |
|
1042 from f have "inj_on ?f (Field ?L)" |
|
1043 unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce |
|
1044 with f have "bij_betw ?f (Field ?L) (Field ?R)" |
|
1045 unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on) |
|
1046 moreover from f rel.well_order_on_domain[OF r] have "compat ?L ?R ?f" |
|
1047 unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def |
|
1048 by (auto simp: map_pair_imageI dest: inj_onD) |
|
1049 ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t) |
|
1050 thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t) |
|
1051 qed |
|
1052 |
|
1053 lemma oprod_cong: |
|
1054 assumes "t =o u" and "r =o s" |
|
1055 shows "t *o r =o u *o s" |
|
1056 using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]] |
|
1057 assms[unfolded ordIso_def] by auto |
|
1058 |
|
1059 lemma Field_singleton[simp]: "Field {(z,z)} = {z}" |
|
1060 by (metis rel.well_order_on_Field well_order_on_singleton) |
|
1061 |
|
1062 lemma zero_singleton[simp]: "zero {(z,z)} = z" |
|
1063 using wo_rel.zero_in_Field[unfolded wo_rel_def, of "{(z, z)}"] well_order_on_singleton[of z] |
|
1064 by auto |
|
1065 |
|
1066 lemma FinFunc_singleton: "FinFunc {(z,z)} s = {\<lambda>x. if x \<in> Field s then z else undefined}" |
|
1067 unfolding FinFunc_def Func_def fin_support_def support_def |
|
1068 by (auto simp: fun_eq_iff split: split_if_asm intro!: finite_subset[of _ "{}"]) |
|
1069 |
|
1070 lemma oone_ordIso_oexp: |
|
1071 assumes "r =o oone" and s: "Well_order s" |
|
1072 shows "r ^o s =o oone" (is "?L =o ?R") |
|
1073 proof - |
|
1074 from assms obtain f where *: "\<forall>x\<in>Field r. \<forall>y\<in>Field r. x = y" and "f ` Field r = {()}" |
|
1075 and r: "Well_order r" |
|
1076 unfolding ordIso_def oone_def by (auto simp: iso_def bij_betw_def inj_on_def) |
|
1077 then obtain x where "x \<in> Field r" by auto |
|
1078 with * have Fr: "Field r = {x}" by auto |
|
1079 interpret r: wo_rel r by unfold_locales (rule r) |
|
1080 from Fr r.well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast |
|
1081 interpret wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1082 have "bij_betw (\<lambda>x. ()) (Field ?L) (Field ?R)" |
|
1083 unfolding bij_betw_def Field_oexp by (auto simp: r_def FinFunc_singleton) |
|
1084 moreover have "compat ?L ?R (\<lambda>x. ())" unfolding compat_def oone_def by auto |
|
1085 ultimately have "iso ?L ?R (\<lambda>x. ())" using s oone_Well_order |
|
1086 by (subst iso_iff3) (auto intro: oexp_Well_order) |
|
1087 thus ?thesis using s oone_Well_order unfolding ordIso_def by (auto intro: oexp_Well_order) |
|
1088 qed |
|
1089 |
|
1090 (*Lemma 1.4.3 from Holz et al.*) |
|
1091 context |
|
1092 fixes r s t |
|
1093 assumes r: "Well_order r" |
|
1094 assumes s: "Well_order s" |
|
1095 assumes t: "Well_order t" |
|
1096 begin |
|
1097 |
|
1098 lemma osum_ozeroL: "ozero +o r =o r" |
|
1099 using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso) |
|
1100 |
|
1101 lemma osum_ozeroR: "r +o ozero =o r" |
|
1102 using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso) |
|
1103 |
|
1104 lemma osum_assoc: "(r +o s) +o t =o r +o s +o t" (is "?L =o ?R") |
|
1105 proof - |
|
1106 let ?f = |
|
1107 "\<lambda>rst. case rst of Inl (Inl r) \<Rightarrow> Inl r | Inl (Inr s) \<Rightarrow> Inr (Inl s) | Inr t \<Rightarrow> Inr (Inr t)" |
|
1108 have "bij_betw ?f (Field ?L) (Field ?R)" |
|
1109 unfolding Field_osum bij_betw_def inj_on_def by (auto simp: image_Un image_iff) |
|
1110 moreover |
|
1111 have "compat ?L ?R ?f" |
|
1112 proof (unfold compat_def, safe) |
|
1113 fix a b |
|
1114 assume "(a, b) \<in> ?L" |
|
1115 thus "(?f a, ?f b) \<in> ?R" |
|
1116 unfolding osum_def[of "r +o s" t] osum_def[of r "s +o t"] Field_osum |
|
1117 unfolding osum_def Field_osum image_iff image_Un map_pair_def |
|
1118 by fastforce |
|
1119 qed |
|
1120 ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: osum_Well_order) |
|
1121 thus ?thesis using r s t unfolding ordIso_def by (auto intro: osum_Well_order) |
|
1122 qed |
|
1123 |
|
1124 lemma osum_monoR: |
|
1125 assumes "s <o t" |
|
1126 shows "r +o s <o r +o t" (is "?L <o ?R") |
|
1127 proof - |
|
1128 from assms obtain f where s: "Well_order s" and t:" Well_order t" and "embedS s t f" |
|
1129 unfolding ordLess_def by blast |
|
1130 hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t" |
|
1131 using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f] |
|
1132 unfolding embedS_def by auto |
|
1133 let ?f = "sum_map id f" |
|
1134 from *(1) have "inj_on ?f (Field ?L)" unfolding Field_osum inj_on_def by fastforce |
|
1135 moreover |
|
1136 from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_pair_def by fastforce |
|
1137 moreover |
|
1138 interpret t!: wo_rel t by unfold_locales (rule t) |
|
1139 interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t]) |
|
1140 from *(3) have "ofilter ?R (?f ` Field ?L)" |
|
1141 unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image rel.under_def |
|
1142 by (auto simp: osum_def intro!: imageI) (auto simp: Field_def) |
|
1143 ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f] |
|
1144 by (auto intro: osum_Well_order r s t) |
|
1145 moreover |
|
1146 from *(4) have "?f ` Field ?L \<subset> Field ?R" unfolding Field_osum image_Un image_image by auto |
|
1147 ultimately have "embedS ?L ?R ?f" using embedS_iff[OF osum_Well_order[OF r s], of ?R ?f] by auto |
|
1148 thus ?thesis unfolding ordLess_def by (auto intro: osum_Well_order r s t) |
|
1149 qed |
|
1150 |
|
1151 lemma osum_monoL: |
|
1152 assumes "r \<le>o s" |
|
1153 shows "r +o t \<le>o s +o t" |
|
1154 proof - |
|
1155 from assms obtain f where f: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)" |
|
1156 unfolding ordLeq_def2 by blast |
|
1157 let ?f = "sum_map f id" |
|
1158 from f have "\<forall>a\<in>Field (r +o t). |
|
1159 ?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)" |
|
1160 unfolding Field_osum rel.underS_def by (fastforce simp: osum_def) |
|
1161 thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t) |
|
1162 qed |
|
1163 |
|
1164 lemma oprod_ozeroL: "ozero *o r =o ozero" |
|
1165 using ozero_ordIso unfolding ozero_def by simp |
|
1166 |
|
1167 lemma oprod_ozeroR: "r *o ozero =o ozero" |
|
1168 using ozero_ordIso unfolding ozero_def by simp |
|
1169 |
|
1170 lemma oprod_ooneR: "r *o oone =o r" (is "?L =o ?R") |
|
1171 proof - |
|
1172 have "bij_betw fst (Field ?L) (Field ?R)" unfolding Field_oprod bij_betw_def inj_on_def by simp |
|
1173 moreover have "compat ?L ?R fst" unfolding compat_def oprod_def by auto |
|
1174 ultimately have "iso ?L ?R fst" using r oone_Well_order |
|
1175 by (subst iso_iff3) (auto intro: oprod_Well_order) |
|
1176 thus ?thesis using r oone_Well_order unfolding ordIso_def by (auto intro: oprod_Well_order) |
|
1177 qed |
|
1178 |
|
1179 lemma oprod_ooneL: "oone *o r =o r" (is "?L =o ?R") |
|
1180 proof - |
|
1181 have "bij_betw snd (Field ?L) (Field ?R)" unfolding Field_oprod bij_betw_def inj_on_def by simp |
|
1182 moreover have "Refl r" by (rule wo_rel.REFL[unfolded wo_rel_def, OF r]) |
|
1183 hence "compat ?L ?R snd" unfolding compat_def oprod_def refl_on_def by auto |
|
1184 ultimately have "iso ?L ?R snd" using r oone_Well_order |
|
1185 by (subst iso_iff3) (auto intro: oprod_Well_order) |
|
1186 thus ?thesis using r oone_Well_order unfolding ordIso_def by (auto intro: oprod_Well_order) |
|
1187 qed |
|
1188 |
|
1189 lemma oprod_monoR: |
|
1190 assumes "ozero <o r" "s <o t" |
|
1191 shows "r *o s <o r *o t" (is "?L <o ?R") |
|
1192 proof - |
|
1193 from assms obtain f where s: "Well_order s" and t:" Well_order t" and "embedS s t f" |
|
1194 unfolding ordLess_def by blast |
|
1195 hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t" |
|
1196 using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f] |
|
1197 unfolding embedS_def by auto |
|
1198 let ?f = "map_pair id f" |
|
1199 from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce |
|
1200 moreover |
|
1201 from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def |
|
1202 by auto (metis rel.well_order_on_domain t, metis rel.well_order_on_domain s) |
|
1203 moreover |
|
1204 interpret t!: wo_rel t by unfold_locales (rule t) |
|
1205 interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t]) |
|
1206 from *(3) have "ofilter ?R (?f ` Field ?L)" |
|
1207 unfolding t.ofilter_def rt.ofilter_def Field_oprod rel.under_def |
|
1208 by (auto simp: oprod_def image_iff) (fast | metis r rel.well_order_on_domain)+ |
|
1209 ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f] |
|
1210 by (auto intro: oprod_Well_order r s t) |
|
1211 moreover |
|
1212 from not_ordLess_ordIso[OF assms(1)] have "r \<noteq> {}" by (metis ozero_def ozero_ordIso) |
|
1213 hence "Field r \<noteq> {}" unfolding Field_def by auto |
|
1214 with *(4) have "?f ` Field ?L \<subset> Field ?R" unfolding Field_oprod |
|
1215 by auto (metis SigmaD2 SigmaI map_pair_surj_on) |
|
1216 ultimately have "embedS ?L ?R ?f" using embedS_iff[OF oprod_Well_order[OF r s], of ?R ?f] by auto |
|
1217 thus ?thesis unfolding ordLess_def by (auto intro: oprod_Well_order r s t) |
|
1218 qed |
|
1219 |
|
1220 lemma oprod_monoL: |
|
1221 assumes "r \<le>o s" |
|
1222 shows "r *o t \<le>o s *o t" |
|
1223 proof - |
|
1224 from assms obtain f where f: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)" |
|
1225 unfolding ordLeq_def2 by blast |
|
1226 let ?f = "map_pair f id" |
|
1227 from f have "\<forall>a\<in>Field (r *o t). |
|
1228 ?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)" |
|
1229 unfolding Field_oprod rel.underS_def unfolding map_pair_def oprod_def by auto |
|
1230 thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t) |
|
1231 qed |
|
1232 |
|
1233 lemma oprod_assoc: "(r *o s) *o t =o r *o s *o t" (is "?L =o ?R") |
|
1234 proof - |
|
1235 let ?f = "\<lambda>((a,b),c). (a,b,c)" |
|
1236 have "bij_betw ?f (Field ?L) (Field ?R)" |
|
1237 unfolding Field_oprod bij_betw_def inj_on_def by (auto simp: image_Un image_iff) |
|
1238 moreover |
|
1239 have "compat ?L ?R ?f" |
|
1240 proof (unfold compat_def, safe) |
|
1241 fix a1 a2 a3 b1 b2 b3 |
|
1242 assume "(((a1, a2), a3), ((b1, b2), b3)) \<in> ?L" |
|
1243 thus "((a1, a2, a3), (b1, b2, b3)) \<in> ?R" |
|
1244 unfolding oprod_def[of "r *o s" t] oprod_def[of r "s *o t"] Field_oprod |
|
1245 unfolding oprod_def Field_oprod image_iff image_Un by fast |
|
1246 qed |
|
1247 ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: oprod_Well_order) |
|
1248 thus ?thesis using r s t unfolding ordIso_def by (auto intro: oprod_Well_order) |
|
1249 qed |
|
1250 |
|
1251 lemma oprod_osum: "r *o (s +o t) =o r *o s +o r *o t" (is "?L =o ?R") |
|
1252 proof - |
|
1253 let ?f = "\<lambda>(a,bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)" |
|
1254 have "bij_betw ?f (Field ?L) (Field ?R)" unfolding Field_oprod Field_osum bij_betw_def inj_on_def |
|
1255 by (fastforce simp: image_Un image_iff split: sum.splits) |
|
1256 moreover |
|
1257 have "compat ?L ?R ?f" |
|
1258 proof (unfold compat_def, intro allI impI) |
|
1259 fix a b |
|
1260 assume "(a, b) \<in> ?L" |
|
1261 thus "(?f a, ?f b) \<in> ?R" |
|
1262 unfolding oprod_def[of r "s +o t"] osum_def[of "r *o s" "r *o t"] Field_oprod Field_osum |
|
1263 unfolding oprod_def osum_def Field_oprod Field_osum image_iff image_Un by auto |
|
1264 qed |
|
1265 ultimately have "iso ?L ?R ?f" using r s t |
|
1266 by (subst iso_iff3) (auto intro: oprod_Well_order osum_Well_order) |
|
1267 thus ?thesis using r s t unfolding ordIso_def by (auto intro: oprod_Well_order osum_Well_order) |
|
1268 qed |
|
1269 |
|
1270 lemma ozero_oexp: "\<not> (s =o ozero) \<Longrightarrow> ozero ^o s =o ozero" |
|
1271 unfolding oexp_def[OF ozero_Well_order s] FinFunc_def |
|
1272 by simp (metis Func_emp2 bot.extremum_uniqueI emptyE rel.well_order_on_domain s subrelI) |
|
1273 |
|
1274 lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R") |
|
1275 by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s]) |
|
1276 |
|
1277 lemma oexp_monoR: |
|
1278 assumes "oone <o r" "s <o t" |
|
1279 shows "r ^o s <o r ^o t" (is "?L <o ?R") |
|
1280 proof - |
|
1281 interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1282 interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t) |
|
1283 interpret rexpt!: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order) |
|
1284 interpret r!: wo_rel r by unfold_locales (rule r) |
|
1285 interpret s!: wo_rel s by unfold_locales (rule s) |
|
1286 interpret t!: wo_rel t by unfold_locales (rule t) |
|
1287 have "Field r \<noteq> {}" by (metis assms(1) internalize_ordLess not_psubset_empty) |
|
1288 moreover |
|
1289 { assume "Field r = {r.zero}" |
|
1290 hence "r = {(r.zero, r.zero)}" using refl_onD[OF r.REFL, of r.zero] unfolding Field_def by auto |
|
1291 hence "r =o oone" by (metis oone_ordIso ordIso_symmetric) |
|
1292 with not_ordLess_ordIso[OF assms(1)] have False by (metis ordIso_symmetric) |
|
1293 } |
|
1294 ultimately obtain x where x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero" |
|
1295 by (metis insert_iff r.zero_in_Field subsetI subset_singletonD) |
|
1296 moreover from assms(2) obtain f where "embedS s t f" unfolding ordLess_def by blast |
|
1297 hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t" |
|
1298 using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f] |
|
1299 unfolding embedS_def by auto |
|
1300 note invff = the_inv_into_f_f[OF *(1)] and injfD = inj_onD[OF *(1)] |
|
1301 def F \<equiv> "\<lambda>g z. if z \<in> f ` Field s then g (the_inv_into (Field s) f z) else |
|
1302 if z \<in> Field t then r.zero else undefined" |
|
1303 from *(4) x(2) the_inv_into_f_eq[OF *(1)] have FLR: "F ` Field ?L \<subseteq> Field ?R" |
|
1304 unfolding rt.Field_oexp rs.Field_oexp FinFunc_def Func_def fin_support_def support_def F_def |
|
1305 by (fastforce split: option.splits split_if_asm elim!: finite_surj[of _ _ f]) |
|
1306 have "inj_on F (Field ?L)" unfolding rs.Field_oexp inj_on_def fun_eq_iff |
|
1307 proof safe |
|
1308 fix g h x assume "g \<in> FinFunc r s" "h \<in> FinFunc r s" "\<forall>y. F g y = F h y" |
|
1309 with invff show "g x = h x" unfolding F_def fun_eq_iff FinFunc_def Func_def |
|
1310 by auto (metis image_eqI) |
|
1311 qed |
|
1312 moreover |
|
1313 have "compat ?L ?R F" unfolding compat_def rs.oexp_def rt.oexp_def |
|
1314 proof (safe elim!: bspec[OF iffD1[OF image_subset_iff FLR[unfolded rs.Field_oexp rt.Field_oexp]]]) |
|
1315 fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r s" "F g \<noteq> F h" |
|
1316 "let m = s.max_fun_diff g h in (g m, h m) \<in> r" |
|
1317 hence "g \<noteq> h" by auto |
|
1318 note max_fun_diff_in = rs.max_fun_diff_in[OF `g \<noteq> h` gh(1,2)] |
|
1319 and max_fun_diff_max = rs.max_fun_diff_max[OF `g \<noteq> h` gh(1,2)] |
|
1320 with *(4) invff *(2) have "t.max_fun_diff (F g) (F h) = f (s.max_fun_diff g h)" |
|
1321 unfolding t.max_fun_diff_def compat_def |
|
1322 by (intro t.maxim_equality) (auto simp: t.isMaxim_def F_def dest: injfD) |
|
1323 with gh invff max_fun_diff_in |
|
1324 show "let m = t.max_fun_diff (F g) (F h) in (F g m, F h m) \<in> r" |
|
1325 unfolding F_def Let_def by (auto simp: dest: injfD) |
|
1326 qed |
|
1327 moreover |
|
1328 from FLR have "ofilter ?R (F ` Field ?L)" |
|
1329 unfolding rexpt.ofilter_def rel.under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def |
|
1330 proof (safe elim!: imageI) |
|
1331 fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r t" "F g \<in> FinFunc r t" |
|
1332 "let m = t.max_fun_diff h (F g) in (h m, F g m) \<in> r" |
|
1333 thus "h \<in> F ` FinFunc r s" |
|
1334 proof (cases "h = F g") |
|
1335 case False |
|
1336 hence max_Field: "t.max_fun_diff h (F g) \<in> {a \<in> Field t. h a \<noteq> F g a}" |
|
1337 by (rule rt.max_fun_diff_in[OF _ gh(2,3)]) |
|
1338 { assume *: "t.max_fun_diff h (F g) \<notin> f ` Field s" |
|
1339 with max_Field have "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto |
|
1340 moreover |
|
1341 with * gh(4) have "h (t.max_fun_diff h (F g)) = r.zero" unfolding Let_def by auto |
|
1342 ultimately have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto |
|
1343 } |
|
1344 hence max_f_Field: "t.max_fun_diff h (F g) \<in> f ` Field s" by blast |
|
1345 { fix z assume z: "z \<in> Field t - f ` Field s" |
|
1346 have "(t.max_fun_diff h (F g), z) \<in> t" |
|
1347 proof (rule ccontr) |
|
1348 assume "(t.max_fun_diff h (F g), z) \<notin> t" |
|
1349 hence "(z, t.max_fun_diff h (F g)) \<in> t" using t.in_notinI[of "t.max_fun_diff h (F g)" z] |
|
1350 z max_Field by auto |
|
1351 hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def rel.under_def |
|
1352 by fastforce |
|
1353 with z show False by blast |
|
1354 qed |
|
1355 hence "h z = r.zero" using rt.max_fun_diff_le_eq[OF _ False gh(2,3), of z] |
|
1356 z max_f_Field unfolding F_def by auto |
|
1357 } note ** = this |
|
1358 with *(3) gh(2) have "h = F (\<lambda>x. if x \<in> Field s then h (f x) else undefined)" using invff |
|
1359 unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def rel.under_def by auto |
|
1360 moreover from gh(2) *(1,3) have "(\<lambda>x. if x \<in> Field s then h (f x) else undefined) \<in> FinFunc r s" |
|
1361 unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def rel.under_def |
|
1362 by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]]) |
|
1363 ultimately show "?thesis" by (rule image_eqI) |
|
1364 qed simp |
|
1365 qed |
|
1366 ultimately have "embed ?L ?R F" using embed_iff_compat_inj_on_ofilter[of ?L ?R F] |
|
1367 by (auto intro: oexp_Well_order r s t) |
|
1368 moreover |
|
1369 from FLR have "F ` Field ?L \<subset> Field ?R" |
|
1370 proof (intro psubsetI) |
|
1371 from *(4) obtain z where z: "z \<in> Field t" "z \<notin> f ` Field s" by auto |
|
1372 def h \<equiv> "\<lambda>z'. if z' \<in> Field t then if z' = z then x else r.zero else undefined" |
|
1373 from z x(3) have "rt.SUPP h = {z}" unfolding support_def h_def by simp |
|
1374 with x have "h \<in> Field ?R" unfolding h_def rt.Field_oexp FinFunc_def Func_def fin_support_def |
|
1375 by auto |
|
1376 moreover |
|
1377 { fix g |
|
1378 from z have "F g z = r.zero" "h z = x" unfolding support_def h_def F_def by auto |
|
1379 with x(3) have "F g \<noteq> h" unfolding fun_eq_iff by fastforce |
|
1380 } |
|
1381 hence "h \<notin> F ` Field ?L" by blast |
|
1382 ultimately show "F ` Field ?L \<noteq> Field ?R" by blast |
|
1383 qed |
|
1384 ultimately have "embedS ?L ?R F" using embedS_iff[OF rs.oexp_Well_order, of ?R F] by auto |
|
1385 thus ?thesis unfolding ordLess_def using r s t by (auto intro: oexp_Well_order) |
|
1386 qed |
|
1387 |
|
1388 lemma oexp_monoL: |
|
1389 assumes "r \<le>o s" |
|
1390 shows "r ^o t \<le>o s ^o t" |
|
1391 proof - |
|
1392 interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t) |
|
1393 interpret st!: wo_rel2 s t by unfold_locales (rule s, rule t) |
|
1394 interpret r!: wo_rel r by unfold_locales (rule r) |
|
1395 interpret s!: wo_rel s by unfold_locales (rule s) |
|
1396 interpret t!: wo_rel t by unfold_locales (rule t) |
|
1397 show ?thesis |
|
1398 proof (cases "t = {}") |
|
1399 case True thus ?thesis using r s unfolding ordLeq_def2 rel.underS_def by auto |
|
1400 next |
|
1401 case False thus ?thesis |
|
1402 proof (cases "r = {}") |
|
1403 case True thus ?thesis using t `t \<noteq> {}` st.oexp_Well_order ozero_ordLeq[unfolded ozero_def] |
|
1404 by auto |
|
1405 next |
|
1406 case False |
|
1407 from assms obtain f where f: "embed r s f" unfolding ordLeq_def by blast |
|
1408 hence f_underS: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)" |
|
1409 using embed_in_Field[OF rt.rWELL f] embed_underS2[OF rt.rWELL st.rWELL f] by auto |
|
1410 from f `t \<noteq> {}` False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}" |
|
1411 unfolding Field_def embed_def rel.under_def bij_betw_def by auto |
|
1412 with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def |
|
1413 using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF r.under_Field] by blast |
|
1414 with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f" |
|
1415 unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def |
|
1416 by (fastforce intro: s.leq_zero_imp)+ |
|
1417 let ?f = "\<lambda>g x. if x \<in> Field t then f (g x) else undefined" |
|
1418 { fix g assume g: "g \<in> Field (r ^o t)" |
|
1419 with fz f_underS have Field_fg: "?f g \<in> Field (s ^o t)" |
|
1420 unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def |
|
1421 by (auto elim!: finite_subset[rotated]) |
|
1422 moreover |
|
1423 have "?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)" |
|
1424 proof safe |
|
1425 fix h |
|
1426 assume h_underS: "h \<in> underS (r ^o t) g" |
|
1427 hence "h \<in> Field (r ^o t)" unfolding rel.underS_def Field_def by auto |
|
1428 with fz f_underS have Field_fh: "?f h \<in> Field (s ^o t)" |
|
1429 unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def |
|
1430 by (auto elim!: finite_subset[rotated]) |
|
1431 from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding rel.underS_def by auto |
|
1432 with f inj have neq: "?f h \<noteq> ?f g" |
|
1433 unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def |
|
1434 by simp metis |
|
1435 moreover |
|
1436 with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def |
|
1437 using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`] |
|
1438 by (subst t.max_fun_diff_def, intro t.maxim_equality) |
|
1439 (auto simp: t.isMaxim_def intro: inj_onD[OF inj] intro!: rt.max_fun_diff_max) |
|
1440 with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp" |
|
1441 using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`] unfolding st.Field_oexp |
|
1442 unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto |
|
1443 ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding rel.underS_def by auto |
|
1444 qed |
|
1445 ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)" |
|
1446 by blast |
|
1447 } |
|
1448 thus ?thesis unfolding ordLeq_def2 by (fastforce intro: oexp_Well_order r s t) |
|
1449 qed |
|
1450 qed |
|
1451 qed |
|
1452 |
|
1453 lemma ordLeq_oexp2: |
|
1454 assumes "oone <o r" |
|
1455 shows "s \<le>o r ^o s" |
|
1456 proof - |
|
1457 interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1458 interpret r!: wo_rel r by unfold_locales (rule r) |
|
1459 interpret s!: wo_rel s by unfold_locales (rule s) |
|
1460 from assms rel.well_order_on_domain[OF r] obtain x where |
|
1461 x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero" |
|
1462 unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def rel.under_def |
|
1463 by (auto simp: image_def) |
|
1464 (metis equals0D insert_not_empty r.under_def r.zero_in_Field rel.under_empty) |
|
1465 let ?f = "\<lambda>a b. if b \<in> Field s then if b = a then x else r.zero else undefined" |
|
1466 from x(3) have SUPP: "\<And>y. y \<in> Field s \<Longrightarrow> rs.SUPP (?f y) = {y}" unfolding support_def by auto |
|
1467 { fix y assume y: "y \<in> Field s" |
|
1468 with x(1,2) SUPP have "?f y \<in> Field (r ^o s)" unfolding rs.Field_oexp |
|
1469 by (auto simp: FinFunc_def Func_def fin_support_def) |
|
1470 moreover |
|
1471 have "?f ` underS s y \<subseteq> underS (r ^o s) (?f y)" |
|
1472 proof safe |
|
1473 fix z |
|
1474 assume "z \<in> underS s y" |
|
1475 hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding rel.underS_def Field_def by auto |
|
1476 from x(3) y z(1,3) have "?f z \<noteq> ?f y" unfolding fun_eq_iff by auto |
|
1477 moreover |
|
1478 { from x(1,2) have "?f z \<in> FinFunc r s" "?f y \<in> FinFunc r s" |
|
1479 unfolding FinFunc_def Func_def fin_support_def by (auto simp: SUPP[OF z(3)] SUPP[OF y]) |
|
1480 moreover |
|
1481 from x(3) y z(1,2) refl_onD[OF s.REFL] have "s.max_fun_diff (?f z) (?f y) = y" |
|
1482 unfolding rs.max_fun_diff_alt SUPP[OF z(3)] SUPP[OF y] |
|
1483 by (intro s.maxim_equality) (auto simp: s.isMaxim_def) |
|
1484 ultimately have "(?f z, ?f y) \<in> rs.oexp" using y x(1) |
|
1485 unfolding rs.oexp_def Let_def by auto |
|
1486 } |
|
1487 ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding rel.underS_def by blast |
|
1488 qed |
|
1489 ultimately have "?f y \<in> Field (r ^o s) \<and> ?f ` underS s y \<subseteq> underS (r ^o s) (?f y)" by blast |
|
1490 } |
|
1491 thus ?thesis unfolding ordLeq_def2 by (fast intro: oexp_Well_order r s) |
|
1492 qed |
|
1493 |
|
1494 lemma FinFunc_osum: |
|
1495 "fg \<in> FinFunc r (s +o t) = (fg o Inl \<in> FinFunc r s \<and> fg o Inr \<in> FinFunc r t)" |
|
1496 (is "?L = (?R1 \<and> ?R2)") |
|
1497 proof safe |
|
1498 assume ?L |
|
1499 from `?L` show ?R1 unfolding FinFunc_def Field_osum Func_def Int_iff fin_support_Field_osum o_def |
|
1500 by (auto split: sum.splits) |
|
1501 from `?L` show ?R2 unfolding FinFunc_def Field_osum Func_def Int_iff fin_support_Field_osum o_def |
|
1502 by (auto split: sum.splits) |
|
1503 next |
|
1504 assume ?R1 ?R2 |
|
1505 thus "?L" unfolding FinFunc_def Field_osum Func_def |
|
1506 by (auto simp: fin_support_Field_osum o_def image_iff split: sum.splits) (metis sumE) |
|
1507 qed |
|
1508 |
|
1509 lemma max_fun_diff_eq_Inl: |
|
1510 assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inl x" |
|
1511 "sum_case f1 g1 \<noteq> sum_case f2 g2" |
|
1512 "sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)" |
|
1513 shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q) |
|
1514 proof - |
|
1515 interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t]) |
|
1516 interpret s!: wo_rel s by unfold_locales (rule s) |
|
1517 interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t]) |
|
1518 from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). sum_case f1 g1 a \<noteq> sum_case f2 g2 a} (Inl x)" |
|
1519 using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp |
|
1520 hence "s.isMaxim {a \<in> Field s. f1 a \<noteq> f2 a} x" |
|
1521 unfolding st.isMaxim_def s.isMaxim_def Field_osum by (auto simp: osum_def) |
|
1522 thus ?P unfolding s.max_fun_diff_def by (rule s.maxim_equality) |
|
1523 from assms(3,4) have **: "g1 \<in> FinFunc r t" "g2 \<in> FinFunc r t" unfolding FinFunc_osum |
|
1524 by (auto simp: o_def) |
|
1525 show ?Q |
|
1526 proof |
|
1527 fix x |
|
1528 from * ** show "g1 x = g2 x" unfolding st.isMaxim_def Field_osum FinFunc_def Func_def fun_eq_iff |
|
1529 unfolding osum_def by (case_tac "x \<in> Field t") auto |
|
1530 qed |
|
1531 qed |
|
1532 |
|
1533 lemma max_fun_diff_eq_Inr: |
|
1534 assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inr x" |
|
1535 "sum_case f1 g1 \<noteq> sum_case f2 g2" |
|
1536 "sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)" |
|
1537 shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 \<noteq> g2" (is ?Q) |
|
1538 proof - |
|
1539 interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t]) |
|
1540 interpret t!: wo_rel t by unfold_locales (rule t) |
|
1541 interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t]) |
|
1542 from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). sum_case f1 g1 a \<noteq> sum_case f2 g2 a} (Inr x)" |
|
1543 using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp |
|
1544 hence "t.isMaxim {a \<in> Field t. g1 a \<noteq> g2 a} x" |
|
1545 unfolding st.isMaxim_def t.isMaxim_def Field_osum by (auto simp: osum_def) |
|
1546 thus ?P ?Q unfolding t.max_fun_diff_def fun_eq_iff |
|
1547 by (auto intro: t.maxim_equality simp: t.isMaxim_def) |
|
1548 qed |
|
1549 |
|
1550 lemma oexp_osum: "r ^o (s +o t) =o (r ^o s) *o (r ^o t)" (is "?R =o ?L") |
|
1551 proof (rule ordIso_symmetric) |
|
1552 interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t]) |
|
1553 interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1554 interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t) |
|
1555 let ?f = "\<lambda>(f, g). sum_case f g" |
|
1556 have "bij_betw ?f (Field ?L) (Field ?R)" |
|
1557 unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI) |
|
1558 show "inj_on ?f (FinFunc r s \<times> FinFunc r t)" unfolding inj_on_def |
|
1559 by (auto simp: fun_eq_iff split: sum.splits) |
|
1560 show "?f ` (FinFunc r s \<times> FinFunc r t) = FinFunc r (s +o t)" |
|
1561 proof safe |
|
1562 fix fg assume "fg \<in> FinFunc r (s +o t)" |
|
1563 thus "fg \<in> ?f ` (FinFunc r s \<times> FinFunc r t)" |
|
1564 by (intro image_eqI[of _ _ "(fg o Inl, fg o Inr)"]) |
|
1565 (auto simp: FinFunc_osum fun_eq_iff split: sum.splits) |
|
1566 qed (auto simp: FinFunc_osum o_def) |
|
1567 qed |
|
1568 moreover have "compat ?L ?R ?f" |
|
1569 unfolding compat_def rst.Field_oexp rs.Field_oexp rt.Field_oexp oprod_def |
|
1570 unfolding rst.oexp_def Let_def rs.oexp_def rt.oexp_def |
|
1571 by (fastforce simp: Field_osum FinFunc_osum o_def split: sum.splits |
|
1572 dest: max_fun_diff_eq_Inl max_fun_diff_eq_Inr) |
|
1573 ultimately have "iso ?L ?R ?f" using r s t |
|
1574 by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order osum_Well_order) |
|
1575 thus "?L =o ?R" using r s t unfolding ordIso_def |
|
1576 by (auto intro: oexp_Well_order oprod_Well_order osum_Well_order) |
|
1577 qed |
|
1578 |
|
1579 definition "rev_curr f b = (if b \<in> Field t then \<lambda>a. f (a, b) else undefined)" |
|
1580 |
|
1581 lemma rev_curr_FinFunc: |
|
1582 assumes Field: "Field r \<noteq> {}" |
|
1583 shows "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t" |
|
1584 proof safe |
|
1585 interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1586 interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t) |
|
1587 fix g assume g: "g \<in> FinFunc r (s *o t)" |
|
1588 hence "finite (rst.SUPP (rev_curr g))" "\<forall>x \<in> Field t. finite (rs.SUPP (rev_curr g x))" |
|
1589 unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def fin_support_def support_def |
|
1590 rs.zero_oexp[OF Field] rev_curr_def by (auto simp: fun_eq_iff rs.const_def elim!: finite_surj) |
|
1591 with g show "rev_curr g \<in> FinFunc (r ^o s) t" |
|
1592 unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def |
|
1593 by (auto simp: rev_curr_def fin_support_def) |
|
1594 next |
|
1595 interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1596 interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t) |
|
1597 fix fg assume *: "fg \<in> FinFunc (r ^o s) t" |
|
1598 let ?g = "\<lambda>(a, b). if (a, b) \<in> Field (s *o t) then fg b a else undefined" |
|
1599 show "fg \<in> rev_curr ` FinFunc r (s *o t)" |
|
1600 proof (rule image_eqI[of _ _ ?g]) |
|
1601 show "fg = rev_curr ?g" |
|
1602 proof |
|
1603 fix x |
|
1604 from * show "fg x = rev_curr ?g x" |
|
1605 unfolding FinFunc_def rs.Field_oexp Func_def rev_curr_def Field_oprod by auto |
|
1606 qed |
|
1607 next |
|
1608 have **: "(\<Union>g \<in> fg ` Field t. rs.SUPP g) = |
|
1609 (\<Union>g \<in> fg ` Field t - {rs.const}. rs.SUPP g)" |
|
1610 unfolding support_def by auto |
|
1611 from * have "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)" |
|
1612 unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def these_def by force+ |
|
1613 moreover hence "finite (fg ` Field t - {rs.const})" using * |
|
1614 unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def |
|
1615 by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff these_def) |
|
1616 ultimately have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)" |
|
1617 by (subst **) (auto intro!: finite_cartesian_product) |
|
1618 with * show "?g \<in> FinFunc r (s *o t)" |
|
1619 unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def these_def |
|
1620 support_def rs.zero_oexp[OF Field] by (auto elim!: finite_subset[rotated]) |
|
1621 qed |
|
1622 qed |
|
1623 |
|
1624 lemma rev_curr_app_FinFunc[elim!]: |
|
1625 "\<lbrakk>f \<in> FinFunc r (s *o t); z \<in> Field t\<rbrakk> \<Longrightarrow> rev_curr f z \<in> FinFunc r s" |
|
1626 unfolding rev_curr_def FinFunc_def Func_def Field_oprod fin_support_def support_def |
|
1627 by (auto elim: finite_surj) |
|
1628 |
|
1629 lemma max_fun_diff_oprod: |
|
1630 assumes Field: "Field r \<noteq> {}" and "f \<noteq> g" "f \<in> FinFunc r (s *o t)" "g \<in> FinFunc r (s *o t)" |
|
1631 defines "m \<equiv> wo_rel.max_fun_diff t (rev_curr f) (rev_curr g)" |
|
1632 shows "wo_rel.max_fun_diff (s *o t) f g = |
|
1633 (wo_rel.max_fun_diff s (rev_curr f m) (rev_curr g m), m)" |
|
1634 proof - |
|
1635 interpret st!: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t]) |
|
1636 interpret s!: wo_rel s by unfold_locales (rule s) |
|
1637 interpret t!: wo_rel t by unfold_locales (rule t) |
|
1638 interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t]) |
|
1639 interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1640 interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t) |
|
1641 from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4) |
|
1642 have diff1: "rev_curr f \<noteq> rev_curr g" |
|
1643 "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field] |
|
1644 unfolding fun_eq_iff rev_curr_def[abs_def] FinFunc_def support_def Field_oprod |
|
1645 by auto fast |
|
1646 hence diff2: "rev_curr f m \<noteq> rev_curr g m" "rev_curr f m \<in> FinFunc r s" "rev_curr g m \<in> FinFunc r s" |
|
1647 using rst.max_fun_diff[OF diff1] assms(3,4) rst.max_fun_diff_in unfolding m_def by auto |
|
1648 show ?thesis unfolding st.max_fun_diff_def |
|
1649 proof (intro st.maxim_equality, unfold st.isMaxim_def Field_oprod, safe) |
|
1650 show "s.max_fun_diff (rev_curr f m) (rev_curr g m) \<in> Field s" |
|
1651 using rs.max_fun_diff_in[OF diff2] by auto |
|
1652 next |
|
1653 show "m \<in> Field t" using rst.max_fun_diff_in[OF diff1] unfolding m_def by auto |
|
1654 next |
|
1655 assume "f (s.max_fun_diff (rev_curr f m) (rev_curr g m), m) = |
|
1656 g (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)" |
|
1657 (is "f (?x, m) = g (?x, m)") |
|
1658 hence "rev_curr f m ?x = rev_curr g m ?x" unfolding rev_curr_def by auto |
|
1659 with rs.max_fun_diff[OF diff2] show False by auto |
|
1660 next |
|
1661 fix x y assume "f (x, y) \<noteq> g (x, y)" "x \<in> Field s" "y \<in> Field t" |
|
1662 thus "((x, y), (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)) \<in> s *o t" |
|
1663 using rst.max_fun_diff_in[OF diff1] rs.max_fun_diff_in[OF diff2] diff1 diff2 |
|
1664 rst.max_fun_diff_max[OF diff1, of y] rs.max_fun_diff_le_eq[OF _ diff2, of x] |
|
1665 unfolding oprod_def m_def rev_curr_def fun_eq_iff by auto (metis s.in_notinI) |
|
1666 qed |
|
1667 qed |
|
1668 |
|
1669 lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L") |
|
1670 proof (cases "r = {}") |
|
1671 case True |
|
1672 interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1673 interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t) |
|
1674 show ?thesis |
|
1675 proof (cases "s = {} \<or> t = {}") |
|
1676 case True with `r = {}` show ?thesis |
|
1677 by (auto simp: oexp_empty[OF oexp_Well_order[OF Well_order_empty s]] |
|
1678 intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso] |
|
1679 ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso]) |
|
1680 next |
|
1681 case False |
|
1682 moreover hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce |
|
1683 ultimately show ?thesis using `r = {}` ozero_ordIso |
|
1684 by (auto simp add: s t oprod_Well_order ozero_def) |
|
1685 qed |
|
1686 next |
|
1687 case False |
|
1688 hence Field: "Field r \<noteq> {}" by (metis Field_def Range_empty_iff Un_empty) |
|
1689 show ?thesis |
|
1690 proof (rule ordIso_symmetric) |
|
1691 interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t]) |
|
1692 interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s) |
|
1693 interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t) |
|
1694 have bij: "bij_betw rev_curr (Field ?L) (Field ?R)" |
|
1695 unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI) |
|
1696 show "inj_on rev_curr (FinFunc r (s *o t))" |
|
1697 unfolding inj_on_def FinFunc_def Func_def Field_oprod rs.Field_oexp rev_curr_def[abs_def] |
|
1698 by (auto simp: fun_eq_iff) metis |
|
1699 show "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t" by (rule rev_curr_FinFunc[OF Field]) |
|
1700 qed |
|
1701 moreover |
|
1702 have "compat ?L ?R rev_curr" |
|
1703 unfolding compat_def proof safe |
|
1704 fix fg1 fg2 assume fg: "(fg1, fg2) \<in> r ^o (s *o t)" |
|
1705 show "(rev_curr fg1, rev_curr fg2) \<in> r ^o s ^o t" |
|
1706 proof (cases "fg1 = fg2") |
|
1707 assume "fg1 \<noteq> fg2" |
|
1708 with fg show ?thesis |
|
1709 using rst.max_fun_diff_in[of "rev_curr fg1" "rev_curr fg2"] |
|
1710 max_fun_diff_oprod[OF Field, of fg1 fg2] rev_curr_FinFunc[OF Field, symmetric] |
|
1711 unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp unfolding r_st.oexp_def rst.oexp_def |
|
1712 by (auto simp: rs.oexp_def Let_def) (auto simp: rev_curr_def[abs_def]) |
|
1713 next |
|
1714 assume "fg1 = fg2" |
|
1715 with fg bij show ?thesis unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp bij_betw_def |
|
1716 by (auto simp: r_st.oexp_def rst.oexp_def) |
|
1717 qed |
|
1718 qed |
|
1719 ultimately have "iso ?L ?R rev_curr" using r s t |
|
1720 by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order) |
|
1721 thus "?L =o ?R" using r s t unfolding ordIso_def |
|
1722 by (auto intro: oexp_Well_order oprod_Well_order) |
|
1723 qed |
|
1724 qed |
|
1725 |
|
1726 end (* context with 3 wellorders *) |
|
1727 |
|
1728 end |