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