src/HOL/BNF_Wellorder_Embedding.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 55936 f6591f8c629d child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
1 (*  Title:      HOL/BNF_Wellorder_Embedding.thy
2     Author:     Andrei Popescu, TU Muenchen
5 Well-order embeddings as needed by bounded natural functors.
6 *)
8 header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
10 theory BNF_Wellorder_Embedding
11 imports Hilbert_Choice BNF_Wellorder_Relation
12 begin
14 text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
15 prove their basic properties.  The notion of embedding is considered from the point
16 of view of the theory of ordinals, and therefore requires the source to be injected
17 as an {\em initial segment} (i.e., {\em order filter}) of the target.  A main result
18 of this section is the existence of embeddings (in one direction or another) between
19 any two well-orders, having as a consequence the fact that, given any two sets on
20 any two types, one is smaller than (i.e., can be injected into) the other. *}
23 subsection {* Auxiliaries *}
25 lemma UNION_inj_on_ofilter:
26 assumes WELL: "Well_order r" and
27         OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
28        INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
29 shows "inj_on f (\<Union> i \<in> I. A i)"
30 proof-
31   have "wo_rel r" using WELL by (simp add: wo_rel_def)
32   hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"
33   using wo_rel.ofilter_linord[of r] OF by blast
34   with WELL INJ show ?thesis
35   by (auto simp add: inj_on_UNION_chain)
36 qed
38 lemma under_underS_bij_betw:
39 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
40         IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
41         BIJ: "bij_betw f (underS r a) (underS r' (f a))"
42 shows "bij_betw f (under r a) (under r' (f a))"
43 proof-
44   have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
45   unfolding underS_def by auto
46   moreover
47   {have "Refl r \<and> Refl r'" using WELL WELL'
48    by (auto simp add: order_on_defs)
49    hence "under r a = underS r a \<union> {a} \<and>
50           under r' (f a) = underS r' (f a) \<union> {f a}"
51    using IN IN' by(auto simp add: Refl_under_underS)
52   }
53   ultimately show ?thesis
54   using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
55 qed
58 subsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
59 functions *}
61 text{* Standardly, a function is an embedding of a well-order in another if it injectively and
62 order-compatibly maps the former into an order filter of the latter.
63 Here we opt for a more succinct definition (operator @{text "embed"}),
64 asking that, for any element in the source, the function should be a bijection
65 between the set of strict lower bounds of that element
66 and the set of strict lower bounds of its image.  (Later we prove equivalence with
67 the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.)
68 A {\em strict embedding} (operator @{text "embedS"})  is a non-bijective embedding
69 and an isomorphism (operator @{text "iso"}) is a bijective embedding. *}
71 definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
72 where
73 "embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
75 lemmas embed_defs = embed_def embed_def[abs_def]
77 text {* Strict embeddings: *}
79 definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
80 where
81 "embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')"
83 lemmas embedS_defs = embedS_def embedS_def[abs_def]
85 definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
86 where
87 "iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')"
89 lemmas iso_defs = iso_def iso_def[abs_def]
91 definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
92 where
93 "compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'"
95 lemma compat_wf:
96 assumes CMP: "compat r r' f" and WF: "wf r'"
97 shows "wf r"
98 proof-
99   have "r \<le> inv_image r' f"
100   unfolding inv_image_def using CMP
101   by (auto simp add: compat_def)
102   with WF show ?thesis
103   using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto
104 qed
106 lemma id_embed: "embed r r id"
107 by(auto simp add: id_def embed_def bij_betw_def)
109 lemma id_iso: "iso r r id"
110 by(auto simp add: id_def embed_def iso_def bij_betw_def)
112 lemma embed_in_Field:
113 assumes WELL: "Well_order r" and
114         EMB: "embed r r' f" and IN: "a \<in> Field r"
115 shows "f a \<in> Field r'"
116 proof-
117   have Well: "wo_rel r"
118   using WELL by (auto simp add: wo_rel_def)
119   hence 1: "Refl r"
120   by (auto simp add: wo_rel.REFL)
121   hence "a \<in> under r a" using IN Refl_under_in by fastforce
122   hence "f a \<in> under r' (f a)"
123   using EMB IN by (auto simp add: embed_def bij_betw_def)
124   thus ?thesis unfolding Field_def
125   by (auto simp: under_def)
126 qed
128 lemma comp_embed:
129 assumes WELL: "Well_order r" and
130         EMB: "embed r r' f" and EMB': "embed r' r'' f'"
131 shows "embed r r'' (f' o f)"
132 proof(unfold embed_def, auto)
133   fix a assume *: "a \<in> Field r"
134   hence "bij_betw f (under r a) (under r' (f a))"
135   using embed_def[of r] EMB by auto
136   moreover
137   {have "f a \<in> Field r'"
138    using EMB WELL * by (auto simp add: embed_in_Field)
139    hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))"
140    using embed_def[of r'] EMB' by auto
141   }
142   ultimately
143   show "bij_betw (f' \<circ> f) (under r a) (under r'' (f'(f a)))"
145 qed
147 lemma comp_iso:
148 assumes WELL: "Well_order r" and
149         EMB: "iso r r' f" and EMB': "iso r' r'' f'"
150 shows "iso r r'' (f' o f)"
151 using assms unfolding iso_def
152 by (auto simp add: comp_embed bij_betw_trans)
154 text{* That @{text "embedS"} is also preserved by function composition shall be proved only later. *}
156 lemma embed_Field:
157 "\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f(Field r) \<le> Field r'"
158 by (auto simp add: embed_in_Field)
160 lemma embed_preserves_ofilter:
161 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
162         EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
163 shows "wo_rel.ofilter r' (fA)"
164 proof-
165   (* Preliminary facts *)
166   from WELL have Well: "wo_rel r" unfolding wo_rel_def .
167   from WELL' have Well': "wo_rel r'" unfolding wo_rel_def .
168   from OF have 0: "A \<le> Field r" by(auto simp add: Well wo_rel.ofilter_def)
169   (* Main proof *)
170   show ?thesis  using Well' WELL EMB 0 embed_Field[of r r' f]
171   proof(unfold wo_rel.ofilter_def, auto simp add: image_def)
172     fix a b'
173     assume *: "a \<in> A" and **: "b' \<in> under r' (f a)"
174     hence "a \<in> Field r" using 0 by auto
175     hence "bij_betw f (under r a) (under r' (f a))"
176     using * EMB by (auto simp add: embed_def)
177     hence "f(under r a) = under r' (f a)"
179     with ** image_def[of f "under r a"] obtain b where
180     1: "b \<in> under r a \<and> b' = f b" by blast
181     hence "b \<in> A" using Well * OF
182     by (auto simp add: wo_rel.ofilter_def)
183     with 1 show "\<exists>b \<in> A. b' = f b" by blast
184   qed
185 qed
187 lemma embed_Field_ofilter:
188 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
189         EMB: "embed r r' f"
190 shows "wo_rel.ofilter r' (f(Field r))"
191 proof-
192   have "wo_rel.ofilter r (Field r)"
193   using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter)
194   with WELL WELL' EMB
195   show ?thesis by (auto simp add: embed_preserves_ofilter)
196 qed
198 lemma embed_compat:
199 assumes EMB: "embed r r' f"
200 shows "compat r r' f"
201 proof(unfold compat_def, clarify)
202   fix a b
203   assume *: "(a,b) \<in> r"
204   hence 1: "b \<in> Field r" using Field_def[of r] by blast
205   have "a \<in> under r b"
206   using * under_def[of r] by simp
207   hence "f a \<in> under r' (f b)"
208   using EMB embed_def[of r r' f]
209         bij_betw_def[of f "under r b" "under r' (f b)"]
210         image_def[of f "under r b"] 1 by auto
211   thus "(f a, f b) \<in> r'"
212   by (auto simp add: under_def)
213 qed
215 lemma embed_inj_on:
216 assumes WELL: "Well_order r" and EMB: "embed r r' f"
217 shows "inj_on f (Field r)"
218 proof(unfold inj_on_def, clarify)
219   (* Preliminary facts *)
220   from WELL have Well: "wo_rel r" unfolding wo_rel_def .
221   with wo_rel.TOTAL[of r]
222   have Total: "Total r" by simp
223   from Well wo_rel.REFL[of r]
224   have Refl: "Refl r" by simp
225   (* Main proof *)
226   fix a b
227   assume *: "a \<in> Field r" and **: "b \<in> Field r" and
228          ***: "f a = f b"
229   hence 1: "a \<in> Field r \<and> b \<in> Field r"
230   unfolding Field_def by auto
231   {assume "(a,b) \<in> r"
232    hence "a \<in> under r b \<and> b \<in> under r b"
233    using Refl by(auto simp add: under_def refl_on_def)
234    hence "a = b"
235    using EMB 1 ***
236    by (auto simp add: embed_def bij_betw_def inj_on_def)
237   }
238   moreover
239   {assume "(b,a) \<in> r"
240    hence "a \<in> under r a \<and> b \<in> under r a"
241    using Refl by(auto simp add: under_def refl_on_def)
242    hence "a = b"
243    using EMB 1 ***
244    by (auto simp add: embed_def bij_betw_def inj_on_def)
245   }
246   ultimately
247   show "a = b" using Total 1
248   by (auto simp add: total_on_def)
249 qed
251 lemma embed_underS:
252 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
253         EMB: "embed r r' f" and IN: "a \<in> Field r"
254 shows "bij_betw f (underS r a) (underS r' (f a))"
255 proof-
256   have "bij_betw f (under r a) (under r' (f a))"
257   using assms by (auto simp add: embed_def)
258   moreover
259   {have "f a \<in> Field r'" using assms  embed_Field[of r r' f] by auto
260    hence "under r a = underS r a \<union> {a} \<and>
261           under r' (f a) = underS r' (f a) \<union> {f a}"
262    using assms by (auto simp add: order_on_defs Refl_under_underS)
263   }
264   moreover
265   {have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
266    unfolding underS_def by blast
267   }
268   ultimately show ?thesis
269   by (auto simp add: notIn_Un_bij_betw3)
270 qed
272 lemma embed_iff_compat_inj_on_ofilter:
273 assumes WELL: "Well_order r" and WELL': "Well_order r'"
274 shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f(Field r)))"
275 using assms
276 proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter,
277       unfold embed_def, auto) (* get rid of one implication *)
278   fix a
279   assume *: "inj_on f (Field r)" and
280          **: "compat r r' f" and
281          ***: "wo_rel.ofilter r' (f(Field r))" and
282          ****: "a \<in> Field r"
283   (* Preliminary facts *)
284   have Well: "wo_rel r"
285   using WELL wo_rel_def[of r] by simp
286   hence Refl: "Refl r"
287   using wo_rel.REFL[of r] by simp
288   have Total: "Total r"
289   using Well wo_rel.TOTAL[of r] by simp
290   have Well': "wo_rel r'"
291   using WELL' wo_rel_def[of r'] by simp
292   hence Antisym': "antisym r'"
293   using wo_rel.ANTISYM[of r'] by simp
294   have "(a,a) \<in> r"
295   using **** Well wo_rel.REFL[of r]
296         refl_on_def[of _ r] by auto
297   hence "(f a, f a) \<in> r'"
298   using ** by(auto simp add: compat_def)
299   hence 0: "f a \<in> Field r'"
300   unfolding Field_def by auto
301   have "f a \<in> f(Field r)"
302   using **** by auto
303   hence 2: "under r' (f a) \<le> f(Field r)"
304   using Well' *** wo_rel.ofilter_def[of r' "f(Field r)"] by fastforce
305   (* Main proof *)
306   show "bij_betw f (under r a) (under r' (f a))"
307   proof(unfold bij_betw_def, auto)
308     show  "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
309   next
310     fix b assume "b \<in> under r a"
311     thus "f b \<in> under r' (f a)"
312     unfolding under_def using **
313     by (auto simp add: compat_def)
314   next
315     fix b' assume *****: "b' \<in> under r' (f a)"
316     hence "b' \<in> f(Field r)"
317     using 2 by auto
318     with Field_def[of r] obtain b where
319     3: "b \<in> Field r" and 4: "b' = f b" by auto
320     have "(b,a): r"
321     proof-
322       {assume "(a,b) \<in> r"
323        with ** 4 have "(f a, b'): r'"
324        by (auto simp add: compat_def)
325        with ***** Antisym' have "f a = b'"
326        by(auto simp add: under_def antisym_def)
327        with 3 **** 4 * have "a = b"
329       }
330       moreover
331       {assume "a = b"
332        hence "(b,a) \<in> r" using Refl **** 3
333        by (auto simp add: refl_on_def)
334       }
335       ultimately
336       show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
337     qed
338     with 4 show  "b' \<in> f(under r a)"
339     unfolding under_def by auto
340   qed
341 qed
343 lemma inv_into_ofilter_embed:
344 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
345         BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
346         IMAGE: "f  A = Field r'"
347 shows "embed r' r (inv_into A f)"
348 proof-
349   (* Preliminary facts *)
350   have Well: "wo_rel r"
351   using WELL wo_rel_def[of r] by simp
352   have Refl: "Refl r"
353   using Well wo_rel.REFL[of r] by simp
354   have Total: "Total r"
355   using Well wo_rel.TOTAL[of r] by simp
356   (* Main proof *)
357   have 1: "bij_betw f A (Field r')"
358   proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE)
359     fix b1 b2
360     assume *: "b1 \<in> A" and **: "b2 \<in> A" and
361            ***: "f b1 = f b2"
362     have 11: "b1 \<in> Field r \<and> b2 \<in> Field r"
363     using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
364     moreover
365     {assume "(b1,b2) \<in> r"
366      hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
367      unfolding under_def using 11 Refl
368      by (auto simp add: refl_on_def)
369      hence "b1 = b2" using BIJ * ** ***
370      by (simp add: bij_betw_def inj_on_def)
371     }
372     moreover
373      {assume "(b2,b1) \<in> r"
374      hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
375      unfolding under_def using 11 Refl
376      by (auto simp add: refl_on_def)
377      hence "b1 = b2" using BIJ * ** ***
378      by (simp add: bij_betw_def inj_on_def)
379     }
380     ultimately
381     show "b1 = b2"
382     using Total by (auto simp add: total_on_def)
383   qed
384   (*  *)
385   let ?f' = "(inv_into A f)"
386   (*  *)
387   have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)"
388   proof(clarify)
389     fix b assume *: "b \<in> A"
390     hence "under r b \<le> A"
391     using Well OF by(auto simp add: wo_rel.ofilter_def)
392     moreover
393     have "f  (under r b) = under r' (f b)"
394     using * BIJ by (auto simp add: bij_betw_def)
395     ultimately
396     show "bij_betw ?f' (under r' (f b)) (under r b)"
397     using 1 by (auto simp add: bij_betw_inv_into_subset)
398   qed
399   (*  *)
400   have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))"
401   proof(clarify)
402     fix b' assume *: "b' \<in> Field r'"
403     have "b' = f (?f' b')" using * 1
404     by (auto simp add: bij_betw_inv_into_right)
405     moreover
406     {obtain b where 31: "b \<in> A" and "f b = b'" using IMAGE * by force
407      hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)
408      with 31 have "?f' b' \<in> A" by auto
409     }
410     ultimately
411     show  "bij_betw ?f' (under r' b') (under r (?f' b'))"
412     using 2 by auto
413   qed
414   (*  *)
415   thus ?thesis unfolding embed_def .
416 qed
418 lemma inv_into_underS_embed:
419 assumes WELL: "Well_order r" and
420         BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
421         IN: "a \<in> Field r" and
422         IMAGE: "f  (underS r a) = Field r'"
423 shows "embed r' r (inv_into (underS r a) f)"
424 using assms
425 by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
427 lemma inv_into_Field_embed:
428 assumes WELL: "Well_order r" and EMB: "embed r r' f" and
429         IMAGE: "Field r' \<le> f  (Field r)"
430 shows "embed r' r (inv_into (Field r) f)"
431 proof-
432   have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))"
433   using EMB by (auto simp add: embed_def)
434   moreover
435   have "f  (Field r) \<le> Field r'"
436   using EMB WELL by (auto simp add: embed_Field)
437   ultimately
438   show ?thesis using assms
439   by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
440 qed
442 lemma inv_into_Field_embed_bij_betw:
443 assumes WELL: "Well_order r" and
444         EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"
445 shows "embed r' r (inv_into (Field r) f)"
446 proof-
447   have "Field r' \<le> f  (Field r)"
448   using BIJ by (auto simp add: bij_betw_def)
449   thus ?thesis using assms
451 qed
454 subsection {* Given any two well-orders, one can be embedded in the other *}
456 text{* Here is an overview of the proof of of this fact, stated in theorem
457 @{text "wellorders_totally_ordered"}:
459    Fix the well-orders @{text "r::'a rel"} and @{text "r'::'a' rel"}.
460    Attempt to define an embedding @{text "f::'a \<Rightarrow> 'a'"} from @{text "r"} to @{text "r'"} in the
461    natural way by well-order recursion ("hoping" that @{text "Field r"} turns out to be smaller
462    than @{text "Field r'"}), but also record, at the recursive step, in a function
463    @{text "g::'a \<Rightarrow> bool"}, the extra information of whether @{text "Field r'"}
464    gets exhausted or not.
466    If @{text "Field r'"} does not get exhausted, then @{text "Field r"} is indeed smaller
467    and @{text "f"} is the desired embedding from @{text "r"} to @{text "r'"}
468    (lemma @{text "wellorders_totally_ordered_aux"}).
470    Otherwise, it means that @{text "Field r'"} is the smaller one, and the inverse of
471    (the "good" segment of) @{text "f"} is the desired embedding from @{text "r'"} to @{text "r"}
472    (lemma @{text "wellorders_totally_ordered_aux2"}).
473 *}
475 lemma wellorders_totally_ordered_aux:
476 fixes r ::"'a rel"  and r'::"'a' rel" and
477       f :: "'a \<Rightarrow> 'a'" and a::'a
478 assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
479         IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
480         NOT: "f  (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f(underS r a))"
481 shows "bij_betw f (under r a) (under r' (f a))"
482 proof-
483   (* Preliminary facts *)
484   have Well: "wo_rel r" using WELL unfolding wo_rel_def .
485   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
486   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
487   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
488   have OF: "wo_rel.ofilter r (underS r a)"
489   by (auto simp add: Well wo_rel.underS_ofilter)
490   hence UN: "underS r a = (\<Union>  b \<in> underS r a. under r b)"
491   using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
492   (* Gather facts about elements of underS r a *)
493   {fix b assume *: "b \<in> underS r a"
494    hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
495    have t1: "b \<in> Field r"
496    using * underS_Field[of r a] by auto
497    have t2: "f(under r b) = under r' (f b)"
498    using IH * by (auto simp add: bij_betw_def)
499    hence t3: "wo_rel.ofilter r' (f(under r b))"
500    using Well' by (auto simp add: wo_rel.under_ofilter)
501    have "f(under r b) \<le> Field r'"
502    using t2 by (auto simp add: under_Field)
503    moreover
504    have "b \<in> under r b"
505    using t1 by(auto simp add: Refl Refl_under_in)
506    ultimately
507    have t4:  "f b \<in> Field r'" by auto
508    have "f(under r b) = under r' (f b) \<and>
509          wo_rel.ofilter r' (f(under r b)) \<and>
510          f b \<in> Field r'"
511    using t2 t3 t4 by auto
512   }
513   hence bFact:
514   "\<forall>b \<in> underS r a. f(under r b) = under r' (f b) \<and>
515                        wo_rel.ofilter r' (f(under r b)) \<and>
516                        f b \<in> Field r'" by blast
517   (*  *)
518   have subField: "f(underS r a) \<le> Field r'"
519   using bFact by blast
520   (*  *)
521   have OF': "wo_rel.ofilter r' (f(underS r a))"
522   proof-
523     have "f(underS r a) = f(\<Union>  b \<in> underS r a. under r b)"
524     using UN by auto
525     also have "\<dots> = (\<Union>  b \<in> underS r a. f(under r b))" by blast
526     also have "\<dots> = (\<Union>  b \<in> underS r a. (under r' (f b)))"
527     using bFact by auto
528     finally
529     have "f(underS r a) = (\<Union>  b \<in> underS r a. (under r' (f b)))" .
530     thus ?thesis
531     using Well' bFact
532           wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
533   qed
534   (*  *)
535   have "f(underS r a) \<union> AboveS r' (f(underS r a)) = Field r'"
536   using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
537   hence NE: "AboveS r' (f(underS r a)) \<noteq> {}"
538   using subField NOT by blast
539   (* Main proof *)
540   have INCL1: "f(underS r a) \<le> underS r' (f a) "
541   proof(auto)
542     fix b assume *: "b \<in> underS r a"
543     have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"
544     using subField Well' SUC NE *
545           wo_rel.suc_greater[of r' "f(underS r a)" "f b"] by force
546     thus "f b \<in> underS r' (f a)"
547     unfolding underS_def by simp
548   qed
549   (*  *)
550   have INCL2: "underS r' (f a) \<le> f(underS r a)"
551   proof
552     fix b' assume "b' \<in> underS r' (f a)"
553     hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"
554     unfolding underS_def by simp
555     thus "b' \<in> f(underS r a)"
556     using Well' SUC NE OF'
557           wo_rel.suc_ofilter_in[of r' "f  underS r a" b'] by auto
558   qed
559   (*  *)
560   have INJ: "inj_on f (underS r a)"
561   proof-
562     have "\<forall>b \<in> underS r a. inj_on f (under r b)"
563     using IH by (auto simp add: bij_betw_def)
564     moreover
565     have "\<forall>b. wo_rel.ofilter r (under r b)"
566     using Well by (auto simp add: wo_rel.under_ofilter)
567     ultimately show  ?thesis
568     using WELL bFact UN
569           UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
570     by auto
571   qed
572   (*  *)
573   have BIJ: "bij_betw f (underS r a) (underS r' (f a))"
574   unfolding bij_betw_def
575   using INJ INCL1 INCL2 by auto
576   (*  *)
577   have "f a \<in> Field r'"
578   using Well' subField NE SUC
579   by (auto simp add: wo_rel.suc_inField)
580   thus ?thesis
581   using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
582 qed
584 lemma wellorders_totally_ordered_aux2:
585 fixes r ::"'a rel"  and r'::"'a' rel" and
586       f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a
587 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
588 MAIN1:
589   "\<And> a. (False \<notin> g(underS r a) \<and> f(underS r a) \<noteq> Field r'
590           \<longrightarrow> f a = wo_rel.suc r' (f(underS r a)) \<and> g a = True)
591          \<and>
592          (\<not>(False \<notin> (g(underS r a)) \<and> f(underS r a) \<noteq> Field r')
593           \<longrightarrow> g a = False)" and
594 MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g(under r a) \<longrightarrow>
595               bij_betw f (under r a) (under r' (f a))" and
596 Case: "a \<in> Field r \<and> False \<in> g(under r a)"
597 shows "\<exists>f'. embed r' r f'"
598 proof-
599   have Well: "wo_rel r" using WELL unfolding wo_rel_def .
600   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
601   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
602   have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto
603   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
604   (*  *)
605   have 0: "under r a = underS r a \<union> {a}"
606   using Refl Case by(auto simp add: Refl_under_underS)
607   (*  *)
608   have 1: "g a = False"
609   proof-
610     {assume "g a \<noteq> False"
611      with 0 Case have "False \<in> g(underS r a)" by blast
612      with MAIN1 have "g a = False" by blast}
613     thus ?thesis by blast
614   qed
615   let ?A = "{a \<in> Field r. g a = False}"
616   let ?a = "(wo_rel.minim r ?A)"
617   (*  *)
618   have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast
619   (*  *)
620   have 3: "False \<notin> g(underS r ?a)"
621   proof
622     assume "False \<in> g(underS r ?a)"
623     then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto
624     hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"
625     by (auto simp add: underS_def)
626     hence "b \<in> Field r" unfolding Field_def by auto
627     with 31 have "b \<in> ?A" by auto
628     hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce
629     (* again: why worked without type annotations? *)
630     with 32 Antisym show False
631     by (auto simp add: antisym_def)
632   qed
633   have temp: "?a \<in> ?A"
634   using Well 2 wo_rel.minim_in[of r ?A] by auto
635   hence 4: "?a \<in> Field r" by auto
636   (*   *)
637   have 5: "g ?a = False" using temp by blast
638   (*  *)
639   have 6: "f(underS r ?a) = Field r'"
640   using MAIN1[of ?a] 3 5 by blast
641   (*  *)
642   have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))"
643   proof
644     fix b assume as: "b \<in> underS r ?a"
645     moreover
646     have "wo_rel.ofilter r (underS r ?a)"
647     using Well by (auto simp add: wo_rel.underS_ofilter)
648     ultimately
649     have "False \<notin> g(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
650     moreover have "b \<in> Field r"
651     unfolding Field_def using as by (auto simp add: underS_def)
652     ultimately
653     show "bij_betw f (under r b) (under r' (f b))"
654     using MAIN2 by auto
655   qed
656   (*  *)
657   have "embed r' r (inv_into (underS r ?a) f)"
658   using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
659   thus ?thesis
660   unfolding embed_def by blast
661 qed
663 theorem wellorders_totally_ordered:
664 fixes r ::"'a rel"  and r'::"'a' rel"
665 assumes WELL: "Well_order r" and WELL': "Well_order r'"
666 shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')"
667 proof-
668   (* Preliminary facts *)
669   have Well: "wo_rel r" using WELL unfolding wo_rel_def .
670   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
671   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
672   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
673   (* Main proof *)
674   obtain H where H_def: "H =
675   (\<lambda>h a. if False \<notin> (snd o h)(underS r a) \<and> (fst o h)(underS r a) \<noteq> Field r'
676                 then (wo_rel.suc r' ((fst o h)(underS r a)), True)
677                 else (undefined, False))" by blast
679   using Well
681     fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x
682     assume "\<forall>y\<in>underS r x. h1 y = h2 y"
683     hence "\<forall>y\<in>underS r x. (fst o h1) y = (fst o h2) y \<and>
684                           (snd o h1) y = (snd o h2) y" by auto
685     hence "(fst o h1)(underS r x) = (fst o h2)(underS r x) \<and>
686            (snd o h1)(underS r x) = (snd o h2)(underS r x)"
687       by (auto simp add: image_def)
688     thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
689   qed
690   (* More constant definitions:  *)
691   obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"
692   where h_def: "h = wo_rel.worec r H" and
693         f_def: "f = fst o h" and g_def: "g = snd o h" by blast
694   obtain test where test_def:
695   "test = (\<lambda> a. False \<notin> (g(underS r a)) \<and> f(underS r a) \<noteq> Field r')" by blast
696   (*  *)
697   have *: "\<And> a. h a  = H h a"
699   have Main1:
700   "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f(underS r a)) \<and> g a = True) \<and>
701          (\<not>(test a) \<longrightarrow> g a = False)"
702   proof-  (* How can I prove this withou fixing a? *)
703     fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f(underS r a)) \<and> g a = True) \<and>
704                 (\<not>(test a) \<longrightarrow> g a = False)"
705     using *[of a] test_def f_def g_def H_def by auto
706   qed
707   (*  *)
708   let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g(under r a) \<longrightarrow>
709                    bij_betw f (under r a) (under r' (f a))"
710   have Main2: "\<And> a. ?phi a"
711   proof-
712     fix a show "?phi a"
713     proof(rule wo_rel.well_order_induct[of r ?phi],
714           simp only: Well, clarify)
715       fix a
716       assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and
717              *: "a \<in> Field r" and
718              **: "False \<notin> g(under r a)"
719       have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))"
720       proof(clarify)
721         fix b assume ***: "b \<in> underS r a"
722         hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
723         moreover have "b \<in> Field r"
724         using *** underS_Field[of r a] by auto
725         moreover have "False \<notin> g(under r b)"
726         using 0 ** Trans under_incr[of r b a] by auto
727         ultimately show "bij_betw f (under r b) (under r' (f b))"
728         using IH by auto
729       qed
730       (*  *)
731       have 21: "False \<notin> g(underS r a)"
732       using ** underS_subset_under[of r a] by auto
733       have 22: "g(under r a) \<le> {True}" using ** by auto
734       moreover have 23: "a \<in> under r a"
735       using Refl * by (auto simp add: Refl_under_in)
736       ultimately have 24: "g a = True" by blast
737       have 2: "f(underS r a) \<noteq> Field r'"
738       proof
739         assume "f(underS r a) = Field r'"
740         hence "g a = False" using Main1 test_def by blast
741         with 24 show False using ** by blast
742       qed
743       (*  *)
744       have 3: "f a = wo_rel.suc r' (f(underS r a))"
745       using 21 2 Main1 test_def by blast
746       (*  *)
747       show "bij_betw f (under r a) (under r' (f a))"
748       using WELL  WELL' 1 2 3 *
749             wellorders_totally_ordered_aux[of r r' a f] by auto
750     qed
751   qed
752   (*  *)
753   let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g(under r a))"
754   show ?thesis
755   proof(cases "\<exists>a. ?chi a")
756     assume "\<not> (\<exists>a. ?chi a)"
757     hence "\<forall>a \<in> Field r.  bij_betw f (under r a) (under r' (f a))"
758     using Main2 by blast
759     thus ?thesis unfolding embed_def by blast
760   next
761     assume "\<exists>a. ?chi a"
762     then obtain a where "?chi a" by blast
763     hence "\<exists>f'. embed r' r f'"
764     using wellorders_totally_ordered_aux2[of r r' g f a]
765           WELL WELL' Main1 Main2 test_def by fast
766     thus ?thesis by blast
767   qed
768 qed
771 subsection {* Uniqueness of embeddings *}
773 text{* Here we show a fact complementary to the one from the previous subsection -- namely,
774 that between any two well-orders there is {\em at most} one embedding, and is the one
775 definable by the expected well-order recursive equation.  As a consequence, any two
776 embeddings of opposite directions are mutually inverse. *}
778 lemma embed_determined:
779 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
780         EMB: "embed r r' f" and IN: "a \<in> Field r"
781 shows "f a = wo_rel.suc r' (f(underS r a))"
782 proof-
783   have "bij_betw f (underS r a) (underS r' (f a))"
784   using assms by (auto simp add: embed_underS)
785   hence "f(underS r a) = underS r' (f a)"
786   by (auto simp add: bij_betw_def)
787   moreover
788   {have "f a \<in> Field r'" using IN
789    using EMB WELL embed_Field[of r r' f] by auto
790    hence "f a = wo_rel.suc r' (underS r' (f a))"
791    using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
792   }
793   ultimately show ?thesis by simp
794 qed
796 lemma embed_unique:
797 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
798         EMBf: "embed r r' f" and EMBg: "embed r r' g"
799 shows "a \<in> Field r \<longrightarrow> f a = g a"
800 proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def)
801   fix a
802   assume IH: "\<forall>b. b \<noteq> a \<and> (b,a): r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and
803          *: "a \<in> Field r"
804   hence "\<forall>b \<in> underS r a. f b = g b"
805   unfolding underS_def by (auto simp add: Field_def)
806   hence "f(underS r a) = g(underS r a)" by force
807   thus "f a = g a"
808   using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
809 qed
811 lemma embed_bothWays_inverse:
812 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
813         EMB: "embed r r' f" and EMB': "embed r' r f'"
814 shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
815 proof-
816   have "embed r r (f' o f)" using assms
818   moreover have "embed r r id" using assms
819   by (auto simp add: id_embed)
820   ultimately have "\<forall>a \<in> Field r. f'(f a) = a"
821   using assms embed_unique[of r r "f' o f" id] id_def by auto
822   moreover
823   {have "embed r' r' (f o f')" using assms
825    moreover have "embed r' r' id" using assms
826    by (auto simp add: id_embed)
827    ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'"
828    using assms embed_unique[of r' r' "f o f'" id] id_def by auto
829   }
830   ultimately show ?thesis by blast
831 qed
833 lemma embed_bothWays_bij_betw:
834 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
835         EMB: "embed r r' f" and EMB': "embed r' r g"
836 shows "bij_betw f (Field r) (Field r')"
837 proof-
838   let ?A = "Field r"  let ?A' = "Field r'"
839   have "embed r r (g o f) \<and> embed r' r' (f o g)"
840   using assms by (auto simp add: comp_embed)
841   hence 1: "(\<forall>a \<in> ?A. g(f a) = a) \<and> (\<forall>a' \<in> ?A'. f(g a') = a')"
842   using WELL id_embed[of r] embed_unique[of r r "g o f" id]
843         WELL' id_embed[of r'] embed_unique[of r' r' "f o g" id]
844         id_def by auto
845   have 2: "(\<forall>a \<in> ?A. f a \<in> ?A') \<and> (\<forall>a' \<in> ?A'. g a' \<in> ?A)"
846   using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast
847   (*  *)
848   show ?thesis
849   proof(unfold bij_betw_def inj_on_def, auto simp add: 2)
850     fix a b assume *: "a \<in> ?A" "b \<in> ?A" and **: "f a = f b"
851     have "a = g(f a) \<and> b = g(f b)" using * 1 by auto
852     with ** show "a = b" by auto
853   next
854     fix a' assume *: "a' \<in> ?A'"
855     hence "g a' \<in> ?A \<and> f(g a') = a'" using 1 2 by auto
856     thus "a' \<in> f  ?A" by force
857   qed
858 qed
860 lemma embed_bothWays_iso:
861 assumes WELL: "Well_order r"  and WELL': "Well_order r'" and
862         EMB: "embed r r' f" and EMB': "embed r' r g"
863 shows "iso r r' f"
864 unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
867 subsection {* More properties of embeddings, strict embeddings and isomorphisms *}
869 lemma embed_bothWays_Field_bij_betw:
870 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
871         EMB: "embed r r' f" and EMB': "embed r' r f'"
872 shows "bij_betw f (Field r) (Field r')"
873 proof-
874   have "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
875   using assms by (auto simp add: embed_bothWays_inverse)
876   moreover
877   have "f(Field r) \<le> Field r' \<and> f'  (Field r') \<le> Field r"
878   using assms by (auto simp add: embed_Field)
879   ultimately
880   show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
881 qed
883 lemma embedS_comp_embed:
884 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
885         and  EMB: "embedS r r' f" and EMB': "embed r' r'' f'"
886 shows "embedS r r'' (f' o f)"
887 proof-
888   let ?g = "(f' o f)"  let ?h = "inv_into (Field r) ?g"
889   have 1: "embed r r' f \<and> \<not> (bij_betw f (Field r) (Field r'))"
890   using EMB by (auto simp add: embedS_def)
891   hence 2: "embed r r'' ?g"
892   using WELL EMB' comp_embed[of r r' f r'' f'] by auto
893   moreover
894   {assume "bij_betw ?g (Field r) (Field r'')"
895    hence "embed r'' r ?h" using 2 WELL
896    by (auto simp add: inv_into_Field_embed_bij_betw)
897    hence "embed r' r (?h o f')" using WELL' EMB'
898    by (auto simp add: comp_embed)
899    hence "bij_betw f (Field r) (Field r')" using WELL WELL' 1
900    by (auto simp add: embed_bothWays_Field_bij_betw)
901    with 1 have False by blast
902   }
903   ultimately show ?thesis unfolding embedS_def by auto
904 qed
906 lemma embed_comp_embedS:
907 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
908         and  EMB: "embed r r' f" and EMB': "embedS r' r'' f'"
909 shows "embedS r r'' (f' o f)"
910 proof-
911   let ?g = "(f' o f)"  let ?h = "inv_into (Field r) ?g"
912   have 1: "embed r' r'' f' \<and> \<not> (bij_betw f' (Field r') (Field r''))"
913   using EMB' by (auto simp add: embedS_def)
914   hence 2: "embed r r'' ?g"
915   using WELL EMB comp_embed[of r r' f r'' f'] by auto
916   moreover
917   {assume "bij_betw ?g (Field r) (Field r'')"
918    hence "embed r'' r ?h" using 2 WELL
919    by (auto simp add: inv_into_Field_embed_bij_betw)
920    hence "embed r'' r' (f o ?h)" using WELL'' EMB
921    by (auto simp add: comp_embed)
922    hence "bij_betw f' (Field r') (Field r'')" using WELL' WELL'' 1
923    by (auto simp add: embed_bothWays_Field_bij_betw)
924    with 1 have False by blast
925   }
926   ultimately show ?thesis unfolding embedS_def by auto
927 qed
929 lemma embed_comp_iso:
930 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
931         and  EMB: "embed r r' f" and EMB': "iso r' r'' f'"
932 shows "embed r r'' (f' o f)"
933 using assms unfolding iso_def
934 by (auto simp add: comp_embed)
936 lemma iso_comp_embed:
937 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
938         and  EMB: "iso r r' f" and EMB': "embed r' r'' f'"
939 shows "embed r r'' (f' o f)"
940 using assms unfolding iso_def
941 by (auto simp add: comp_embed)
943 lemma embedS_comp_iso:
944 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
945         and  EMB: "embedS r r' f" and EMB': "iso r' r'' f'"
946 shows "embedS r r'' (f' o f)"
947 using assms unfolding iso_def
948 by (auto simp add: embedS_comp_embed)
950 lemma iso_comp_embedS:
951 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
952         and  EMB: "iso r r' f" and EMB': "embedS r' r'' f'"
953 shows "embedS r r'' (f' o f)"
954 using assms unfolding iso_def  using embed_comp_embedS
955 by (auto simp add: embed_comp_embedS)
957 lemma embedS_Field:
958 assumes WELL: "Well_order r" and EMB: "embedS r r' f"
959 shows "f  (Field r) < Field r'"
960 proof-
961   have "f(Field r) \<le> Field r'" using assms
962   by (auto simp add: embed_Field embedS_def)
963   moreover
964   {have "inj_on f (Field r)" using assms
965    by (auto simp add: embedS_def embed_inj_on)
966    hence "f(Field r) \<noteq> Field r'" using EMB
967    by (auto simp add: embedS_def bij_betw_def)
968   }
969   ultimately show ?thesis by blast
970 qed
972 lemma embedS_iff:
973 assumes WELL: "Well_order r" and ISO: "embed r r' f"
974 shows "embedS r r' f = (f  (Field r) < Field r')"
975 proof
976   assume "embedS r r' f"
977   thus "f  Field r \<subset> Field r'"
978   using WELL by (auto simp add: embedS_Field)
979 next
980   assume "f  Field r \<subset> Field r'"
981   hence "\<not> bij_betw f (Field r) (Field r')"
982   unfolding bij_betw_def by blast
983   thus "embedS r r' f" unfolding embedS_def
984   using ISO by auto
985 qed
987 lemma iso_Field:
988 "iso r r' f \<Longrightarrow> f  (Field r) = Field r'"
989 using assms by (auto simp add: iso_def bij_betw_def)
991 lemma iso_iff:
992 assumes "Well_order r"
993 shows "iso r r' f = (embed r r' f \<and> f  (Field r) = Field r')"
994 proof
995   assume "iso r r' f"
996   thus "embed r r' f \<and> f  (Field r) = Field r'"
997   by (auto simp add: iso_Field iso_def)
998 next
999   assume *: "embed r r' f \<and> f  Field r = Field r'"
1000   hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on)
1001   with * have "bij_betw f (Field r) (Field r')"
1002   unfolding bij_betw_def by simp
1003   with * show "iso r r' f" unfolding iso_def by auto
1004 qed
1006 lemma iso_iff2:
1007 assumes "Well_order r"
1008 shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
1009                      (\<forall>a \<in> Field r. \<forall>b \<in> Field r.
1010                          (((a,b) \<in> r) = ((f a, f b) \<in> r'))))"
1011 using assms
1013   fix a b
1014   assume "embed r r' f"
1015   hence "compat r r' f" using embed_compat[of r] by auto
1016   moreover assume "(a,b) \<in> r"
1017   ultimately show "(f a, f b) \<in> r'" using compat_def[of r] by auto
1018 next
1019   let ?f' = "inv_into (Field r) f"
1020   assume "embed r r' f" and 1: "bij_betw f (Field r) (Field r')"
1021   hence "embed r' r ?f'" using assms
1022   by (auto simp add: inv_into_Field_embed_bij_betw)
1023   hence 2: "compat r' r ?f'" using embed_compat[of r'] by auto
1024   fix a b assume *: "a \<in> Field r" "b \<in> Field r" and **: "(f a,f b) \<in> r'"
1025   hence "?f'(f a) = a \<and> ?f'(f b) = b" using 1
1026   by (auto simp add: bij_betw_inv_into_left)
1027   thus "(a,b) \<in> r" using ** 2 compat_def[of r' r ?f'] by fastforce
1028 next
1029   assume *: "bij_betw f (Field r) (Field r')" and
1030          **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"
1031   have 1: "\<And> a. under r a \<le> Field r \<and> under r' (f a) \<le> Field r'"
1032   by (auto simp add: under_Field)
1033   have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)
1034   {fix a assume ***: "a \<in> Field r"
1035    have "bij_betw f (under r a) (under r' (f a))"
1036    proof(unfold bij_betw_def, auto)
1037      show "inj_on f (under r a)" using 1 2 subset_inj_on by blast
1038    next
1039      fix b assume "b \<in> under r a"
1040      hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
1041      unfolding under_def by (auto simp add: Field_def Range_def Domain_def)
1042      with 1 ** show "f b \<in> under r' (f a)"
1043      unfolding under_def by auto
1044    next
1045      fix b' assume "b' \<in> under r' (f a)"
1046      hence 3: "(b',f a) \<in> r'" unfolding under_def by simp
1047      hence "b' \<in> Field r'" unfolding Field_def by auto
1048      with * obtain b where "b \<in> Field r \<and> f b = b'"
1049      unfolding bij_betw_def by force
1050      with 3 ** ***
1051      show "b' \<in> f  (under r a)" unfolding under_def by blast
1052    qed
1053   }
1054   thus "embed r r' f" unfolding embed_def using * by auto
1055 qed
1057 lemma iso_iff3:
1058 assumes WELL: "Well_order r" and WELL': "Well_order r'"
1059 shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)"
1060 proof
1061   assume "iso r r' f"
1062   thus "bij_betw f (Field r) (Field r') \<and> compat r r' f"
1063   unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def)
1064 next
1065   have Well: "wo_rel r \<and> wo_rel r'" using WELL WELL'
1066   by (auto simp add: wo_rel_def)
1067   assume *: "bij_betw f (Field r) (Field r') \<and> compat r r' f"
1068   thus "iso r r' f"
1069   unfolding "compat_def" using assms
1071     fix a b assume **: "a \<in> Field r" "b \<in> Field r" and
1072                   ***: "(f a, f b) \<in> r'"
1073     {assume "(b,a) \<in> r \<or> b = a"
1074      hence "(b,a): r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
1075      hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto
1076      hence "f a = f b"
1077      using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast
1078      hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto
1079      hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
1080     }
1081     thus "(a,b) \<in> r"
1082     using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast
1083   qed
1084 qed
1086 end