src/HOL/Cardinals/Constructions_on_Wellorders.thy
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55066 4e5ddf3162ac
parent 55065 6d0af3c10864
child 55070 235c7661a96b
permissions -rw-r--r--
tuning
blanchet@49310
     1
(*  Title:      HOL/Cardinals/Constructions_on_Wellorders.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Constructions on wellorders.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* Constructions on Wellorders *}
blanchet@48975
     9
blanchet@48975
    10
theory Constructions_on_Wellorders
blanchet@55056
    11
imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@55066
    14
notation
blanchet@55066
    15
  ordLeq2 (infix "<=o" 50) and
blanchet@55065
    16
  ordLeq3 (infix "\<le>o" 50) and
blanchet@55065
    17
  ordLess2 (infix "<o" 50) and
blanchet@55065
    18
  ordIso2 (infix "=o" 50)
blanchet@55065
    19
blanchet@48975
    20
declare
blanchet@48975
    21
  ordLeq_Well_order_simp[simp]
blanchet@48975
    22
  not_ordLeq_iff_ordLess[simp]
blanchet@48975
    23
  not_ordLess_iff_ordLeq[simp]
traytel@54980
    24
  Func_empty[simp]
traytel@54980
    25
  Func_is_emp[simp]
blanchet@48975
    26
traytel@54980
    27
lemma Func_emp2[simp]: "A \<noteq> {} \<Longrightarrow> Func A {} = {}" by auto
blanchet@48975
    28
blanchet@48975
    29
subsection {* Restriction to a set  *}
blanchet@48975
    30
blanchet@48975
    31
lemma Restr_incr2:
blanchet@48975
    32
"r <= r' \<Longrightarrow> Restr r A <= Restr r' A"
blanchet@48975
    33
by blast
blanchet@48975
    34
blanchet@48975
    35
lemma Restr_incr:
blanchet@48975
    36
"\<lbrakk>r \<le> r'; A \<le> A'\<rbrakk> \<Longrightarrow> Restr r A \<le> Restr r' A'"
blanchet@48975
    37
by blast
blanchet@48975
    38
blanchet@48975
    39
lemma Restr_Int:
blanchet@48975
    40
"Restr (Restr r A) B = Restr r (A Int B)"
blanchet@48975
    41
by blast
blanchet@48975
    42
blanchet@48975
    43
lemma Restr_iff: "(a,b) : Restr r A = (a : A \<and> b : A \<and> (a,b) : r)"
blanchet@48975
    44
by (auto simp add: Field_def)
blanchet@48975
    45
blanchet@48975
    46
lemma Restr_subset1: "Restr r A \<le> r"
blanchet@48975
    47
by auto
blanchet@48975
    48
blanchet@48975
    49
lemma Restr_subset2: "Restr r A \<le> A \<times> A"
blanchet@48975
    50
by auto
blanchet@48975
    51
blanchet@48975
    52
lemma wf_Restr:
blanchet@48975
    53
"wf r \<Longrightarrow> wf(Restr r A)"
traytel@51764
    54
using Restr_subset by (elim wf_subset) simp
blanchet@48975
    55
blanchet@48975
    56
lemma Restr_incr1:
blanchet@48975
    57
"A \<le> B \<Longrightarrow> Restr r A \<le> Restr r B"
blanchet@48975
    58
by blast
blanchet@48975
    59
blanchet@48975
    60
blanchet@48975
    61
subsection {* Order filters versus restrictions and embeddings  *}
blanchet@48975
    62
blanchet@48975
    63
lemma ofilter_Restr:
blanchet@48975
    64
assumes WELL: "Well_order r" and
blanchet@48975
    65
        OFA: "ofilter r A" and OFB: "ofilter r B" and SUB: "A \<le> B"
blanchet@48975
    66
shows "ofilter (Restr r B) A"
blanchet@48975
    67
proof-
blanchet@48975
    68
  let ?rB = "Restr r B"
blanchet@48975
    69
  have Well: "wo_rel r" unfolding wo_rel_def using WELL .
blanchet@48975
    70
  hence Refl: "Refl r" by (auto simp add: wo_rel.REFL)
blanchet@48975
    71
  hence Field: "Field ?rB = Field r Int B"
blanchet@48975
    72
  using Refl_Field_Restr by blast
blanchet@48975
    73
  have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
blanchet@48975
    74
  by (auto simp add: Well_order_Restr wo_rel_def)
blanchet@48975
    75
  (* Main proof *)
blanchet@48975
    76
  show ?thesis
blanchet@48975
    77
  proof(auto simp add: WellB wo_rel.ofilter_def)
blanchet@48975
    78
    fix a assume "a \<in> A"
blanchet@48975
    79
    hence "a \<in> Field r \<and> a \<in> B" using assms Well
blanchet@48975
    80
    by (auto simp add: wo_rel.ofilter_def)
blanchet@48975
    81
    with Field show "a \<in> Field(Restr r B)" by auto
blanchet@48975
    82
  next
blanchet@48975
    83
    fix a b assume *: "a \<in> A"  and "b \<in> under (Restr r B) a"
blanchet@48975
    84
    hence "b \<in> under r a"
blanchet@48975
    85
    using WELL OFB SUB ofilter_Restr_under[of r B a] by auto
blanchet@48975
    86
    thus "b \<in> A" using * Well OFA by(auto simp add: wo_rel.ofilter_def)
blanchet@48975
    87
  qed
blanchet@48975
    88
qed
blanchet@48975
    89
blanchet@48975
    90
lemma ofilter_subset_iso:
blanchet@48975
    91
assumes WELL: "Well_order r" and
blanchet@48975
    92
        OFA: "ofilter r A" and OFB: "ofilter r B"
blanchet@48975
    93
shows "(A = B) = iso (Restr r A) (Restr r B) id"
blanchet@48975
    94
using assms
blanchet@48975
    95
by (auto simp add: ofilter_subset_embedS_iso)
blanchet@48975
    96
blanchet@48975
    97
blanchet@54476
    98
subsection {* Ordering the well-orders by existence of embeddings *}
blanchet@48975
    99
blanchet@48975
   100
corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq"
blanchet@48975
   101
using ordLeq_reflexive unfolding ordLeq_def refl_on_def
blanchet@48975
   102
by blast
blanchet@48975
   103
blanchet@48975
   104
corollary ordLeq_trans: "trans ordLeq"
blanchet@48975
   105
using trans_def[of ordLeq] ordLeq_transitive by blast
blanchet@48975
   106
blanchet@48975
   107
corollary ordLeq_preorder_on: "preorder_on {r. Well_order r} ordLeq"
blanchet@48975
   108
by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans)
blanchet@48975
   109
blanchet@48975
   110
corollary ordIso_refl_on: "refl_on {r. Well_order r} ordIso"
blanchet@48975
   111
using ordIso_reflexive unfolding refl_on_def ordIso_def
blanchet@48975
   112
by blast
blanchet@48975
   113
blanchet@48975
   114
corollary ordIso_trans: "trans ordIso"
blanchet@48975
   115
using trans_def[of ordIso] ordIso_transitive by blast
blanchet@48975
   116
blanchet@48975
   117
corollary ordIso_sym: "sym ordIso"
blanchet@48975
   118
by (auto simp add: sym_def ordIso_symmetric)
blanchet@48975
   119
blanchet@48975
   120
corollary ordIso_equiv: "equiv {r. Well_order r} ordIso"
blanchet@48975
   121
by (auto simp add:  equiv_def ordIso_sym ordIso_refl_on ordIso_trans)
blanchet@48975
   122
blanchet@54476
   123
lemma ordLess_Well_order_simp[simp]:
blanchet@54476
   124
assumes "r <o r'"
blanchet@54476
   125
shows "Well_order r \<and> Well_order r'"
blanchet@54476
   126
using assms unfolding ordLess_def by simp
blanchet@54476
   127
blanchet@54476
   128
lemma ordIso_Well_order_simp[simp]:
blanchet@54476
   129
assumes "r =o r'"
blanchet@54476
   130
shows "Well_order r \<and> Well_order r'"
blanchet@54476
   131
using assms unfolding ordIso_def by simp
blanchet@54476
   132
blanchet@48975
   133
lemma ordLess_irrefl: "irrefl ordLess"
blanchet@48975
   134
by(unfold irrefl_def, auto simp add: ordLess_irreflexive)
blanchet@48975
   135
blanchet@48975
   136
lemma ordLess_or_ordIso:
blanchet@48975
   137
assumes WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@48975
   138
shows "r <o r' \<or> r' <o r \<or> r =o r'"
blanchet@48975
   139
unfolding ordLess_def ordIso_def
blanchet@48975
   140
using assms embedS_or_iso[of r r'] by auto
blanchet@48975
   141
blanchet@48975
   142
corollary ordLeq_ordLess_Un_ordIso:
blanchet@48975
   143
"ordLeq = ordLess \<union> ordIso"
blanchet@48975
   144
by (auto simp add: ordLeq_iff_ordLess_or_ordIso)
blanchet@48975
   145
blanchet@48975
   146
lemma not_ordLeq_ordLess:
blanchet@48975
   147
"r \<le>o r' \<Longrightarrow> \<not> r' <o r"
blanchet@48975
   148
using not_ordLess_ordLeq by blast
blanchet@48975
   149
blanchet@48975
   150
lemma ordIso_or_ordLess:
blanchet@48975
   151
assumes WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@48975
   152
shows "r =o r' \<or> r <o r' \<or> r' <o r"
blanchet@48975
   153
using assms ordLess_or_ordLeq ordLeq_iff_ordLess_or_ordIso by blast
blanchet@48975
   154
blanchet@48975
   155
lemmas ord_trans = ordIso_transitive ordLeq_transitive ordLess_transitive
blanchet@48975
   156
                   ordIso_ordLeq_trans ordLeq_ordIso_trans
blanchet@48975
   157
                   ordIso_ordLess_trans ordLess_ordIso_trans
blanchet@48975
   158
                   ordLess_ordLeq_trans ordLeq_ordLess_trans
blanchet@48975
   159
blanchet@48975
   160
lemma ofilter_ordLeq:
blanchet@48975
   161
assumes "Well_order r" and "ofilter r A"
blanchet@48975
   162
shows "Restr r A \<le>o r"
blanchet@48975
   163
proof-
blanchet@48975
   164
  have "A \<le> Field r" using assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
blanchet@48975
   165
  thus ?thesis using assms
blanchet@48975
   166
  by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter
blanchet@48975
   167
      wo_rel_def Restr_Field)
blanchet@48975
   168
qed
blanchet@48975
   169
blanchet@48975
   170
corollary under_Restr_ordLeq:
blanchet@48975
   171
"Well_order r \<Longrightarrow> Restr r (under r a) \<le>o r"
blanchet@48975
   172
by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def)
blanchet@48975
   173
blanchet@48975
   174
blanchet@48975
   175
subsection {* Copy via direct images  *}
blanchet@48975
   176
blanchet@48975
   177
lemma Id_dir_image: "dir_image Id f \<le> Id"
blanchet@48975
   178
unfolding dir_image_def by auto
blanchet@48975
   179
blanchet@48975
   180
lemma Un_dir_image:
blanchet@48975
   181
"dir_image (r1 \<union> r2) f = (dir_image r1 f) \<union> (dir_image r2 f)"
blanchet@48975
   182
unfolding dir_image_def by auto
blanchet@48975
   183
blanchet@48975
   184
lemma Int_dir_image:
blanchet@48975
   185
assumes "inj_on f (Field r1 \<union> Field r2)"
blanchet@48975
   186
shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)"
blanchet@48975
   187
proof
blanchet@48975
   188
  show "dir_image (r1 Int r2) f \<le> (dir_image r1 f) Int (dir_image r2 f)"
blanchet@48975
   189
  using assms unfolding dir_image_def inj_on_def by auto
blanchet@48975
   190
next
blanchet@48975
   191
  show "(dir_image r1 f) Int (dir_image r2 f) \<le> dir_image (r1 Int r2) f"
blanchet@48975
   192
  proof(clarify)
blanchet@48975
   193
    fix a' b'
blanchet@48975
   194
    assume "(a',b') \<in> dir_image r1 f" "(a',b') \<in> dir_image r2 f"
blanchet@48975
   195
    then obtain a1 b1 a2 b2
blanchet@48975
   196
    where 1: "a' = f a1 \<and> b' = f b1 \<and> a' = f a2 \<and> b' = f b2" and
blanchet@48975
   197
          2: "(a1,b1) \<in> r1 \<and> (a2,b2) \<in> r2" and
blanchet@48975
   198
          3: "{a1,b1} \<le> Field r1 \<and> {a2,b2} \<le> Field r2"
blanchet@48975
   199
    unfolding dir_image_def Field_def by blast
blanchet@48975
   200
    hence "a1 = a2 \<and> b1 = b2" using assms unfolding inj_on_def by auto
blanchet@48975
   201
    hence "a' = f a1 \<and> b' = f b1 \<and> (a1,b1) \<in> r1 Int r2 \<and> (a2,b2) \<in> r1 Int r2"
blanchet@48975
   202
    using 1 2 by auto
blanchet@48975
   203
    thus "(a',b') \<in> dir_image (r1 \<inter> r2) f"
blanchet@48975
   204
    unfolding dir_image_def by blast
blanchet@48975
   205
  qed
blanchet@48975
   206
qed
blanchet@48975
   207
popescua@52203
   208
(* More facts on ordinal sum: *)
blanchet@48975
   209
blanchet@48975
   210
lemma Osum_embed:
blanchet@48975
   211
assumes FLD: "Field r Int Field r' = {}" and
blanchet@48975
   212
        WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@48975
   213
shows "embed r (r Osum r') id"
blanchet@48975
   214
proof-
blanchet@48975
   215
  have 1: "Well_order (r Osum r')"
blanchet@48975
   216
  using assms by (auto simp add: Osum_Well_order)
blanchet@48975
   217
  moreover
blanchet@48975
   218
  have "compat r (r Osum r') id"
blanchet@48975
   219
  unfolding compat_def Osum_def by auto
blanchet@48975
   220
  moreover
blanchet@48975
   221
  have "inj_on id (Field r)" by simp
blanchet@48975
   222
  moreover
blanchet@48975
   223
  have "ofilter (r Osum r') (Field r)"
blanchet@48975
   224
  using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def
blanchet@55023
   225
                               Field_Osum under_def)
blanchet@48975
   226
    fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'"
blanchet@48975
   227
    moreover
blanchet@48975
   228
    {assume "(b,a) \<in> r'"
blanchet@48975
   229
     hence "a \<in> Field r'" using Field_def[of r'] by blast
blanchet@48975
   230
     hence False using 2 FLD by blast
blanchet@48975
   231
    }
blanchet@48975
   232
    moreover
blanchet@48975
   233
    {assume "a \<in> Field r'"
blanchet@48975
   234
     hence False using 2 FLD by blast
blanchet@48975
   235
    }
blanchet@48975
   236
    ultimately
blanchet@48975
   237
    show "b \<in> Field r" by (auto simp add: Osum_def Field_def)
blanchet@48975
   238
  qed
blanchet@48975
   239
  ultimately show ?thesis
blanchet@48975
   240
  using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
blanchet@48975
   241
qed
blanchet@48975
   242
blanchet@48975
   243
corollary Osum_ordLeq:
blanchet@48975
   244
assumes FLD: "Field r Int Field r' = {}" and
blanchet@48975
   245
        WELL: "Well_order r" and WELL': "Well_order r'"
blanchet@48975
   246
shows "r \<le>o r Osum r'"
blanchet@48975
   247
using assms Osum_embed Osum_Well_order
blanchet@48975
   248
unfolding ordLeq_def by blast
blanchet@48975
   249
blanchet@48975
   250
lemma Well_order_embed_copy:
blanchet@48975
   251
assumes WELL: "well_order_on A r" and
blanchet@48975
   252
        INJ: "inj_on f A" and SUB: "f ` A \<le> B"
blanchet@48975
   253
shows "\<exists>r'. well_order_on B r' \<and> r \<le>o r'"
blanchet@48975
   254
proof-
blanchet@48975
   255
  have "bij_betw f A (f ` A)"
blanchet@48975
   256
  using INJ inj_on_imp_bij_betw by blast
blanchet@48975
   257
  then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''"
blanchet@48975
   258
  using WELL  Well_order_iso_copy by blast
blanchet@48975
   259
  hence 2: "Well_order r'' \<and> Field r'' = (f ` A)"
blanchet@55023
   260
  using well_order_on_Well_order by blast
blanchet@48975
   261
  (*  *)
blanchet@48975
   262
  let ?C = "B - (f ` A)"
blanchet@48975
   263
  obtain r''' where "well_order_on ?C r'''"
blanchet@48975
   264
  using well_order_on by blast
blanchet@48975
   265
  hence 3: "Well_order r''' \<and> Field r''' = ?C"
blanchet@55023
   266
  using well_order_on_Well_order by blast
blanchet@48975
   267
  (*  *)
blanchet@48975
   268
  let ?r' = "r'' Osum r'''"
blanchet@48975
   269
  have "Field r'' Int Field r''' = {}"
blanchet@48975
   270
  using 2 3 by auto
blanchet@48975
   271
  hence "r'' \<le>o ?r'" using Osum_ordLeq[of r'' r'''] 2 3 by blast
blanchet@48975
   272
  hence 4: "r \<le>o ?r'" using 1 ordIso_ordLeq_trans by blast
blanchet@48975
   273
  (*  *)
blanchet@48975
   274
  hence "Well_order ?r'" unfolding ordLeq_def by auto
blanchet@48975
   275
  moreover
blanchet@48975
   276
  have "Field ?r' = B" using 2 3 SUB by (auto simp add: Field_Osum)
blanchet@48975
   277
  ultimately show ?thesis using 4 by blast
blanchet@48975
   278
qed
blanchet@48975
   279
blanchet@48975
   280
blanchet@48975
   281
subsection {* The maxim among a finite set of ordinals  *}
blanchet@48975
   282
blanchet@48975
   283
text {* The correct phrasing would be ``a maxim of ...", as @{text "\<le>o"} is only a preorder. *}
blanchet@48975
   284
blanchet@48975
   285
definition isOmax :: "'a rel set \<Rightarrow> 'a rel \<Rightarrow> bool"
blanchet@48975
   286
where
blanchet@48975
   287
"isOmax  R r == r \<in> R \<and> (ALL r' : R. r' \<le>o r)"
blanchet@48975
   288
blanchet@48975
   289
definition omax :: "'a rel set \<Rightarrow> 'a rel"
blanchet@48975
   290
where
blanchet@48975
   291
"omax R == SOME r. isOmax R r"
blanchet@48975
   292
blanchet@48975
   293
lemma exists_isOmax:
blanchet@48975
   294
assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
blanchet@48975
   295
shows "\<exists> r. isOmax R r"
blanchet@48975
   296
proof-
blanchet@48975
   297
  have "finite R \<Longrightarrow> R \<noteq> {} \<longrightarrow> (\<forall> r \<in> R. Well_order r) \<longrightarrow> (\<exists> r. isOmax R r)"
blanchet@48975
   298
  apply(erule finite_induct) apply(simp add: isOmax_def)
blanchet@48975
   299
  proof(clarsimp)
blanchet@48975
   300
    fix r :: "('a \<times> 'a) set" and R assume *: "finite R" and **: "r \<notin> R"
blanchet@48975
   301
    and ***: "Well_order r" and ****: "\<forall>r\<in>R. Well_order r"
blanchet@48975
   302
    and IH: "R \<noteq> {} \<longrightarrow> (\<exists>p. isOmax R p)"
blanchet@48975
   303
    let ?R' = "insert r R"
blanchet@48975
   304
    show "\<exists>p'. (isOmax ?R' p')"
blanchet@48975
   305
    proof(cases "R = {}")
blanchet@48975
   306
      assume Case1: "R = {}"
blanchet@48975
   307
      thus ?thesis unfolding isOmax_def using ***
blanchet@48975
   308
      by (simp add: ordLeq_reflexive)
blanchet@48975
   309
    next
blanchet@48975
   310
      assume Case2: "R \<noteq> {}"
blanchet@48975
   311
      then obtain p where p: "isOmax R p" using IH by auto
blanchet@48975
   312
      hence 1: "Well_order p" using **** unfolding isOmax_def by simp
blanchet@48975
   313
      {assume Case21: "r \<le>o p"
blanchet@48975
   314
       hence "isOmax ?R' p" using p unfolding isOmax_def by simp
blanchet@48975
   315
       hence ?thesis by auto
blanchet@48975
   316
      }
blanchet@48975
   317
      moreover
blanchet@48975
   318
      {assume Case22: "p \<le>o r"
blanchet@48975
   319
       {fix r' assume "r' \<in> ?R'"
blanchet@48975
   320
        moreover
blanchet@48975
   321
        {assume "r' \<in> R"
blanchet@48975
   322
         hence "r' \<le>o p" using p unfolding isOmax_def by simp
blanchet@48975
   323
         hence "r' \<le>o r" using Case22 by(rule ordLeq_transitive)
blanchet@48975
   324
        }
blanchet@48975
   325
        moreover have "r \<le>o r" using *** by(rule ordLeq_reflexive)
blanchet@48975
   326
        ultimately have "r' \<le>o r" by auto
blanchet@48975
   327
       }
blanchet@48975
   328
       hence "isOmax ?R' r" unfolding isOmax_def by simp
blanchet@48975
   329
       hence ?thesis by auto
blanchet@48975
   330
      }
blanchet@48975
   331
      moreover have "r \<le>o p \<or> p \<le>o r"
blanchet@48975
   332
      using 1 *** ordLeq_total by auto
blanchet@48975
   333
      ultimately show ?thesis by blast
blanchet@48975
   334
    qed
blanchet@48975
   335
  qed
blanchet@48975
   336
  thus ?thesis using assms by auto
blanchet@48975
   337
qed
blanchet@48975
   338
blanchet@48975
   339
lemma omax_isOmax:
blanchet@48975
   340
assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
blanchet@48975
   341
shows "isOmax R (omax R)"
blanchet@48975
   342
unfolding omax_def using assms
blanchet@48975
   343
by(simp add: exists_isOmax someI_ex)
blanchet@48975
   344
blanchet@48975
   345
lemma omax_in:
blanchet@48975
   346
assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r"
blanchet@48975
   347
shows "omax R \<in> R"
blanchet@48975
   348
using assms omax_isOmax unfolding isOmax_def by blast
blanchet@48975
   349
blanchet@48975
   350
lemma Well_order_omax:
blanchet@48975
   351
assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Well_order r"
blanchet@48975
   352
shows "Well_order (omax R)"
blanchet@48975
   353
using assms apply - apply(drule omax_in) by auto
blanchet@48975
   354
blanchet@48975
   355
lemma omax_maxim:
blanchet@48975
   356
assumes "finite R" and "\<forall> r \<in> R. Well_order r" and "r \<in> R"
blanchet@48975
   357
shows "r \<le>o omax R"
blanchet@48975
   358
using assms omax_isOmax unfolding isOmax_def by blast
blanchet@48975
   359
blanchet@48975
   360
lemma omax_ordLeq:
blanchet@48975
   361
assumes "finite R" and "R \<noteq> {}" and *: "\<forall> r \<in> R. r \<le>o p"
blanchet@48975
   362
shows "omax R \<le>o p"
blanchet@48975
   363
proof-
blanchet@48975
   364
  have "\<forall> r \<in> R. Well_order r" using * unfolding ordLeq_def by simp
blanchet@48975
   365
  thus ?thesis using assms omax_in by auto
blanchet@48975
   366
qed
blanchet@48975
   367
blanchet@48975
   368
lemma omax_ordLess:
blanchet@48975
   369
assumes "finite R" and "R \<noteq> {}" and *: "\<forall> r \<in> R. r <o p"
blanchet@48975
   370
shows "omax R <o p"
blanchet@48975
   371
proof-
blanchet@48975
   372
  have "\<forall> r \<in> R. Well_order r" using * unfolding ordLess_def by simp
blanchet@48975
   373
  thus ?thesis using assms omax_in by auto
blanchet@48975
   374
qed
blanchet@48975
   375
blanchet@48975
   376
lemma omax_ordLeq_elim:
blanchet@48975
   377
assumes "finite R" and "\<forall> r \<in> R. Well_order r"
blanchet@48975
   378
and "omax R \<le>o p" and "r \<in> R"
blanchet@48975
   379
shows "r \<le>o p"
blanchet@48975
   380
using assms omax_maxim[of R r] apply simp
blanchet@48975
   381
using ordLeq_transitive by blast
blanchet@48975
   382
blanchet@48975
   383
lemma omax_ordLess_elim:
blanchet@48975
   384
assumes "finite R" and "\<forall> r \<in> R. Well_order r"
blanchet@48975
   385
and "omax R <o p" and "r \<in> R"
blanchet@48975
   386
shows "r <o p"
blanchet@48975
   387
using assms omax_maxim[of R r] apply simp
blanchet@48975
   388
using ordLeq_ordLess_trans by blast
blanchet@48975
   389
blanchet@48975
   390
lemma ordLeq_omax:
blanchet@48975
   391
assumes "finite R" and "\<forall> r \<in> R. Well_order r"
blanchet@48975
   392
and "r \<in> R" and "p \<le>o r"
blanchet@48975
   393
shows "p \<le>o omax R"
blanchet@48975
   394
using assms omax_maxim[of R r] apply simp
blanchet@48975
   395
using ordLeq_transitive by blast
blanchet@48975
   396
blanchet@48975
   397
lemma ordLess_omax:
blanchet@48975
   398
assumes "finite R" and "\<forall> r \<in> R. Well_order r"
blanchet@48975
   399
and "r \<in> R" and "p <o r"
blanchet@48975
   400
shows "p <o omax R"
blanchet@48975
   401
using assms omax_maxim[of R r] apply simp
blanchet@48975
   402
using ordLess_ordLeq_trans by blast
blanchet@48975
   403
blanchet@48975
   404
lemma omax_ordLeq_mono:
blanchet@48975
   405
assumes P: "finite P" and R: "finite R"
blanchet@48975
   406
and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r"
blanchet@48975
   407
and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p \<le>o r"
blanchet@48975
   408
shows "omax P \<le>o omax R"
blanchet@48975
   409
proof-
blanchet@48975
   410
  let ?mp = "omax P"  let ?mr = "omax R"
blanchet@48975
   411
  {fix p assume "p : P"
blanchet@48975
   412
   then obtain r where r: "r : R" and "p \<le>o r"
blanchet@48975
   413
   using LEQ by blast
blanchet@48975
   414
   moreover have "r <=o ?mr"
blanchet@48975
   415
   using r R Well_R omax_maxim by blast
blanchet@48975
   416
   ultimately have "p <=o ?mr"
blanchet@48975
   417
   using ordLeq_transitive by blast
blanchet@48975
   418
  }
blanchet@48975
   419
  thus "?mp <=o ?mr"
blanchet@48975
   420
  using NE_P P using omax_ordLeq by blast
blanchet@48975
   421
qed
blanchet@48975
   422
blanchet@48975
   423
lemma omax_ordLess_mono:
blanchet@48975
   424
assumes P: "finite P" and R: "finite R"
blanchet@48975
   425
and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r"
blanchet@48975
   426
and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p <o r"
blanchet@48975
   427
shows "omax P <o omax R"
blanchet@48975
   428
proof-
blanchet@48975
   429
  let ?mp = "omax P"  let ?mr = "omax R"
blanchet@48975
   430
  {fix p assume "p : P"
blanchet@48975
   431
   then obtain r where r: "r : R" and "p <o r"
blanchet@48975
   432
   using LEQ by blast
blanchet@48975
   433
   moreover have "r <=o ?mr"
blanchet@48975
   434
   using r R Well_R omax_maxim by blast
blanchet@48975
   435
   ultimately have "p <o ?mr"
blanchet@48975
   436
   using ordLess_ordLeq_trans by blast
blanchet@48975
   437
  }
blanchet@48975
   438
  thus "?mp <o ?mr"
blanchet@48975
   439
  using NE_P P omax_ordLess by blast
blanchet@48975
   440
qed
blanchet@48975
   441
traytel@54980
   442
traytel@54980
   443
traytel@54980
   444
section {* Limit and Succesor Ordinals *}
traytel@54980
   445
traytel@54980
   446
lemma embed_underS2:
traytel@54980
   447
assumes r: "Well_order r" and s: "Well_order s"  and g: "embed r s g" and a: "a \<in> Field r"
traytel@54980
   448
shows "g ` underS r a = underS s (g a)"
traytel@54980
   449
using embed_underS[OF assms] unfolding bij_betw_def by auto
traytel@54980
   450
traytel@54980
   451
lemma bij_betw_insert:
traytel@54980
   452
assumes "b \<notin> A" and "f b \<notin> A'" and "bij_betw f A A'"
traytel@54980
   453
shows "bij_betw f (insert b A) (insert (f b) A')"
traytel@54980
   454
using notIn_Un_bij_betw[OF assms] by auto
traytel@54980
   455
traytel@54980
   456
context wo_rel
traytel@54980
   457
begin
traytel@54980
   458
traytel@54980
   459
lemma underS_induct:
traytel@54980
   460
  assumes "\<And>a. (\<And> a1. a1 \<in> underS a \<Longrightarrow> P a1) \<Longrightarrow> P a"
traytel@54980
   461
  shows "P a"
traytel@54980
   462
  by (induct rule: well_order_induct) (rule assms, simp add: underS_def)
traytel@54980
   463
traytel@54980
   464
lemma suc_underS:
traytel@54980
   465
assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
traytel@54980
   466
shows "b \<in> underS (suc B)"
traytel@54980
   467
using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto
traytel@54980
   468
traytel@54980
   469
lemma underS_supr:
traytel@54980
   470
assumes bA: "b \<in> underS (supr A)" and A: "A \<subseteq> Field r"
traytel@54980
   471
shows "\<exists> a \<in> A. b \<in> underS a"
traytel@54980
   472
proof(rule ccontr, auto)
traytel@54980
   473
  have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
traytel@54980
   474
  assume "\<forall>a\<in>A.  b \<notin> underS a"
traytel@54980
   475
  hence 0: "\<forall>a \<in> A. (a,b) \<in> r" using A bA unfolding underS_def
traytel@54980
   476
  by simp (metis REFL in_mono max2_def max2_greater refl_on_domain)
traytel@54980
   477
  have "(supr A, b) \<in> r" apply(rule supr_least[OF A bb]) using 0 by auto
traytel@54980
   478
  thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
traytel@54980
   479
qed
traytel@54980
   480
traytel@54980
   481
lemma underS_suc:
traytel@54980
   482
assumes bA: "b \<in> underS (suc A)" and A: "A \<subseteq> Field r"
traytel@54980
   483
shows "\<exists> a \<in> A. b \<in> under a"
traytel@54980
   484
proof(rule ccontr, auto)
traytel@54980
   485
  have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
traytel@54980
   486
  assume "\<forall>a\<in>A.  b \<notin> under a"
traytel@54980
   487
  hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
blanchet@55023
   488
  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp)
blanchet@55023
   489
  have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto
traytel@54980
   490
  thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
traytel@54980
   491
qed
traytel@54980
   492
traytel@54980
   493
lemma (in wo_rel) in_underS_supr:
traytel@54980
   494
assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
traytel@54980
   495
shows "j \<in> underS (supr A)"
traytel@54980
   496
proof-
traytel@54980
   497
  have "(i,supr A) \<in> r" using supr_greater[OF A AA i] .
traytel@54980
   498
  thus ?thesis using j unfolding underS_def
blanchet@55023
   499
  by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD)
traytel@54980
   500
qed
traytel@54980
   501
traytel@54980
   502
lemma inj_on_Field:
traytel@54980
   503
assumes A: "A \<subseteq> Field r" and f: "\<And> a b. \<lbrakk>a \<in> A; b \<in> A; a \<in> underS b\<rbrakk> \<Longrightarrow> f a \<noteq> f b"
traytel@54980
   504
shows "inj_on f A"
traytel@54980
   505
unfolding inj_on_def proof safe
traytel@54980
   506
  fix a b assume a: "a \<in> A" and b: "b \<in> A" and fab: "f a = f b"
traytel@54980
   507
  {assume "a \<in> underS b"
traytel@54980
   508
   hence False using f[OF a b] fab by auto
traytel@54980
   509
  }
traytel@54980
   510
  moreover
traytel@54980
   511
  {assume "b \<in> underS a"
traytel@54980
   512
   hence False using f[OF b a] fab by auto
traytel@54980
   513
  }
traytel@54980
   514
  ultimately show "a = b" using TOTALS A a b unfolding underS_def by auto
traytel@54980
   515
qed
traytel@54980
   516
traytel@54980
   517
lemma in_notinI:
traytel@54980
   518
assumes "(j,i) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
traytel@54980
   519
shows "(i,j) \<in> r" by (metis assms max2_def max2_greater_among)
traytel@54980
   520
traytel@54980
   521
lemma ofilter_init_seg_of:
traytel@54980
   522
assumes "ofilter F"
traytel@54980
   523
shows "Restr r F initial_segment_of r"
traytel@54980
   524
using assms unfolding ofilter_def init_seg_of_def under_def by auto
traytel@54980
   525
traytel@54980
   526
lemma underS_init_seg_of_Collect:
traytel@54980
   527
assumes "\<And>j1 j2. \<lbrakk>j2 \<in> underS i; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
traytel@54980
   528
shows "{R j |j. j \<in> underS i} \<in> Chains init_seg_of"
traytel@54980
   529
unfolding Chains_def proof safe
traytel@54980
   530
  fix j ja assume jS: "j \<in> underS i" and jaS: "ja \<in> underS i"
traytel@54980
   531
  and init: "(R ja, R j) \<notin> init_seg_of"
traytel@54980
   532
  hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
traytel@54980
   533
  and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
blanchet@55023
   534
  and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto
traytel@54980
   535
  have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
traytel@54980
   536
  show "R j initial_segment_of R ja"
traytel@54980
   537
  using jja init jjai i
traytel@54980
   538
  by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: underS_def)
traytel@54980
   539
qed
traytel@54980
   540
traytel@54980
   541
lemma (in wo_rel) Field_init_seg_of_Collect:
traytel@54980
   542
assumes "\<And>j1 j2. \<lbrakk>j2 \<in> Field r; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
traytel@54980
   543
shows "{R j |j. j \<in> Field r} \<in> Chains init_seg_of"
traytel@54980
   544
unfolding Chains_def proof safe
traytel@54980
   545
  fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r"
traytel@54980
   546
  and init: "(R ja, R j) \<notin> init_seg_of"
traytel@54980
   547
  hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
blanchet@55023
   548
  unfolding Field_def underS_def by auto
traytel@54980
   549
  have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
traytel@54980
   550
  show "R j initial_segment_of R ja"
traytel@54980
   551
  using jja init
traytel@54980
   552
  by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: Field_def)
traytel@54980
   553
qed
traytel@54980
   554
traytel@54980
   555
subsection {* Successor and limit elements of an ordinal *}
traytel@54980
   556
traytel@54980
   557
definition "succ i \<equiv> suc {i}"
traytel@54980
   558
traytel@54980
   559
definition "isSucc i \<equiv> \<exists> j. aboveS j \<noteq> {} \<and> i = succ j"
traytel@54980
   560
traytel@54980
   561
definition "zero = minim (Field r)"
traytel@54980
   562
traytel@54980
   563
definition "isLim i \<equiv> \<not> isSucc i"
traytel@54980
   564
traytel@54980
   565
lemma zero_smallest[simp]:
traytel@54980
   566
assumes "j \<in> Field r" shows "(zero, j) \<in> r"
traytel@54980
   567
unfolding zero_def
traytel@54980
   568
by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS)
traytel@54980
   569
traytel@54980
   570
lemma zero_in_Field: assumes "Field r \<noteq> {}"  shows "zero \<in> Field r"
traytel@54980
   571
using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def)
traytel@54980
   572
traytel@54980
   573
lemma leq_zero_imp[simp]:
traytel@54980
   574
"(x, zero) \<in> r \<Longrightarrow> x = zero"
traytel@54980
   575
by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest)
traytel@54980
   576
traytel@54980
   577
lemma leq_zero[simp]:
traytel@54980
   578
assumes "Field r \<noteq> {}"  shows "(x, zero) \<in> r \<longleftrightarrow> x = zero"
traytel@54980
   579
using zero_in_Field[OF assms] in_notinI[of x zero] by auto
traytel@54980
   580
traytel@54980
   581
lemma under_zero[simp]:
traytel@54980
   582
assumes "Field r \<noteq> {}" shows "under zero = {zero}"
traytel@54980
   583
using assms unfolding under_def by auto
traytel@54980
   584
traytel@54980
   585
lemma underS_zero[simp,intro]: "underS zero = {}"
traytel@54980
   586
unfolding underS_def by auto
traytel@54980
   587
traytel@54980
   588
lemma isSucc_succ: "aboveS i \<noteq> {} \<Longrightarrow> isSucc (succ i)"
traytel@54980
   589
unfolding isSucc_def succ_def by auto
traytel@54980
   590
traytel@54980
   591
lemma succ_in_diff:
traytel@54980
   592
assumes "aboveS i \<noteq> {}"  shows "(i,succ i) \<in> r \<and> succ i \<noteq> i"
traytel@54980
   593
using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto
traytel@54980
   594
traytel@54980
   595
lemmas succ_in[simp] = succ_in_diff[THEN conjunct1]
traytel@54980
   596
lemmas succ_diff[simp] = succ_in_diff[THEN conjunct2]
traytel@54980
   597
traytel@54980
   598
lemma succ_in_Field[simp]:
traytel@54980
   599
assumes "aboveS i \<noteq> {}"  shows "succ i \<in> Field r"
traytel@54980
   600
using succ_in[OF assms] unfolding Field_def by auto
traytel@54980
   601
traytel@54980
   602
lemma succ_not_in:
traytel@54980
   603
assumes "aboveS i \<noteq> {}" shows "(succ i, i) \<notin> r"
traytel@54980
   604
proof
traytel@54980
   605
  assume 1: "(succ i, i) \<in> r"
traytel@54980
   606
  hence "succ i \<in> Field r \<and> i \<in> Field r" unfolding Field_def by auto
traytel@54980
   607
  hence "(i, succ i) \<in> r \<and> succ i \<noteq> i" using assms by auto
traytel@54980
   608
  thus False using 1 by (metis ANTISYM antisymD)
traytel@54980
   609
qed
traytel@54980
   610
traytel@54980
   611
lemma not_isSucc_zero: "\<not> isSucc zero"
traytel@54980
   612
proof
traytel@54980
   613
  assume "isSucc zero"
traytel@54980
   614
  moreover
traytel@54980
   615
  then obtain i where "aboveS i \<noteq> {}" and 1: "minim (Field r) = succ i"
traytel@54980
   616
  unfolding isSucc_def zero_def by auto
traytel@54980
   617
  hence "succ i \<in> Field r" by auto
traytel@54980
   618
  ultimately show False by (metis REFL isSucc_def minim_least refl_on_domain
traytel@54980
   619
    subset_refl succ_in succ_not_in zero_def)
traytel@54980
   620
qed
traytel@54980
   621
traytel@54980
   622
lemma isLim_zero[simp]: "isLim zero"
traytel@54980
   623
  by (metis isLim_def not_isSucc_zero)
traytel@54980
   624
traytel@54980
   625
lemma succ_smallest:
traytel@54980
   626
assumes "(i,j) \<in> r" and "i \<noteq> j"
traytel@54980
   627
shows "(succ i, j) \<in> r"
traytel@54980
   628
unfolding succ_def apply(rule suc_least)
traytel@54980
   629
using assms unfolding Field_def by auto
traytel@54980
   630
traytel@54980
   631
lemma isLim_supr:
traytel@54980
   632
assumes f: "i \<in> Field r" and l: "isLim i"
traytel@54980
   633
shows "i = supr (underS i)"
traytel@54980
   634
proof(rule equals_supr)
traytel@54980
   635
  fix j assume j: "j \<in> Field r" and 1: "\<And> j'. j' \<in> underS i \<Longrightarrow> (j',j) \<in> r"
traytel@54980
   636
  show "(i,j) \<in> r" proof(intro in_notinI[OF _ f j], safe)
traytel@54980
   637
    assume ji: "(j,i) \<in> r" "j \<noteq> i"
traytel@54980
   638
    hence a: "aboveS j \<noteq> {}" unfolding aboveS_def by auto
traytel@54980
   639
    hence "i \<noteq> succ j" using l unfolding isLim_def isSucc_def by auto
traytel@54980
   640
    moreover have "(succ j, i) \<in> r" using succ_smallest[OF ji] by auto
traytel@54980
   641
    ultimately have "succ j \<in> underS i" unfolding underS_def by auto
traytel@54980
   642
    hence "(succ j, j) \<in> r" using 1 by auto
traytel@54980
   643
    thus False using succ_not_in[OF a] by simp
traytel@54980
   644
  qed
traytel@54980
   645
qed(insert f, unfold underS_def Field_def, auto)
traytel@54980
   646
traytel@54980
   647
definition "pred i \<equiv> SOME j. j \<in> Field r \<and> aboveS j \<noteq> {} \<and> succ j = i"
traytel@54980
   648
traytel@54980
   649
lemma pred_Field_succ:
traytel@54980
   650
assumes "isSucc i" shows "pred i \<in> Field r \<and> aboveS (pred i) \<noteq> {} \<and> succ (pred i) = i"
traytel@54980
   651
proof-
traytel@54980
   652
  obtain j where a: "aboveS j \<noteq> {}" and i: "i = succ j" using assms unfolding isSucc_def by auto
traytel@54980
   653
  have 1: "j \<in> Field r" "j \<noteq> i" unfolding Field_def i
traytel@54980
   654
  using succ_diff[OF a] a unfolding aboveS_def by auto
traytel@54980
   655
  show ?thesis unfolding pred_def apply(rule someI_ex) using 1 i a by auto
traytel@54980
   656
qed
traytel@54980
   657
traytel@54980
   658
lemmas pred_Field[simp] = pred_Field_succ[THEN conjunct1]
traytel@54980
   659
lemmas aboveS_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct1]
traytel@54980
   660
lemmas succ_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct2]
traytel@54980
   661
traytel@54980
   662
lemma isSucc_pred_in:
traytel@54980
   663
assumes "isSucc i"  shows "(pred i, i) \<in> r"
traytel@54980
   664
proof-
traytel@54980
   665
  def j \<equiv> "pred i"
traytel@54980
   666
  have i: "i = succ j" using assms unfolding j_def by simp
traytel@54980
   667
  have a: "aboveS j \<noteq> {}" unfolding j_def using assms by auto
traytel@54980
   668
  show ?thesis unfolding j_def[symmetric] unfolding i using succ_in[OF a] .
traytel@54980
   669
qed
traytel@54980
   670
traytel@54980
   671
lemma isSucc_pred_diff:
traytel@54980
   672
assumes "isSucc i"  shows "pred i \<noteq> i"
traytel@54980
   673
by (metis aboveS_pred assms succ_diff succ_pred)
traytel@54980
   674
traytel@54980
   675
(* todo: pred maximal, pred injective? *)
traytel@54980
   676
traytel@54980
   677
lemma succ_inj[simp]:
traytel@54980
   678
assumes "aboveS i \<noteq> {}" and "aboveS j \<noteq> {}"
traytel@54980
   679
shows "succ i = succ j \<longleftrightarrow> i = j"
traytel@54980
   680
proof safe
traytel@54980
   681
  assume s: "succ i = succ j"
traytel@54980
   682
  {assume "i \<noteq> j" and "(i,j) \<in> r"
traytel@54980
   683
   hence "(succ i, j) \<in> r" using assms by (metis succ_smallest)
traytel@54980
   684
   hence False using s assms by (metis succ_not_in)
traytel@54980
   685
  }
traytel@54980
   686
  moreover
traytel@54980
   687
  {assume "i \<noteq> j" and "(j,i) \<in> r"
traytel@54980
   688
   hence "(succ j, i) \<in> r" using assms by (metis succ_smallest)
traytel@54980
   689
   hence False using s assms by (metis succ_not_in)
traytel@54980
   690
  }
traytel@54980
   691
  ultimately show "i = j" by (metis TOTALS WELL assms(1) assms(2) succ_in_diff well_order_on_domain)
traytel@54980
   692
qed
traytel@54980
   693
traytel@54980
   694
lemma pred_succ[simp]:
traytel@54980
   695
assumes "aboveS j \<noteq> {}"  shows "pred (succ j) = j"
traytel@54980
   696
unfolding pred_def apply(rule some_equality)
traytel@54980
   697
using assms apply(force simp: Field_def aboveS_def)
traytel@54980
   698
by (metis assms succ_inj)
traytel@54980
   699
traytel@54980
   700
lemma less_succ[simp]:
traytel@54980
   701
assumes "aboveS i \<noteq> {}"
traytel@54980
   702
shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i"
traytel@54980
   703
apply safe
blanchet@55023
   704
  apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff)
blanchet@55023
   705
  apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD)
traytel@54980
   706
  apply (metis assms in_notinI succ_in_Field)
traytel@54980
   707
done
traytel@54980
   708
traytel@54980
   709
lemma underS_succ[simp]:
traytel@54980
   710
assumes "aboveS i \<noteq> {}"
traytel@54980
   711
shows "underS (succ i) = under i"
traytel@54980
   712
unfolding underS_def under_def by (auto simp: assms succ_not_in)
traytel@54980
   713
traytel@54980
   714
lemma succ_mono:
traytel@54980
   715
assumes "aboveS j \<noteq> {}" and "(i,j) \<in> r"
traytel@54980
   716
shows "(succ i, succ j) \<in> r"
traytel@54980
   717
by (metis (full_types) assms less_succ succ_smallest)
traytel@54980
   718
traytel@54980
   719
lemma under_succ[simp]:
traytel@54980
   720
assumes "aboveS i \<noteq> {}"
traytel@54980
   721
shows "under (succ i) = insert (succ i) (under i)"
traytel@54980
   722
using less_succ[OF assms] unfolding under_def by auto
traytel@54980
   723
traytel@54980
   724
definition mergeSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
traytel@54980
   725
where
traytel@54980
   726
"mergeSL S L f i \<equiv>
traytel@54980
   727
 if isSucc i then S (pred i) (f (pred i))
traytel@54980
   728
 else L f i"
traytel@54980
   729
traytel@54980
   730
traytel@54980
   731
subsection {* Well-order recursion with (zero), succesor, and limit *}
traytel@54980
   732
traytel@54980
   733
definition worecSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
traytel@54980
   734
where "worecSL S L \<equiv> worec (mergeSL S L)"
traytel@54980
   735
traytel@54980
   736
definition "adm_woL L \<equiv> \<forall>f g i. isLim i \<and> (\<forall>j\<in>underS i. f j = g j) \<longrightarrow> L f i = L g i"
traytel@54980
   737
traytel@54980
   738
lemma mergeSL:
traytel@54980
   739
assumes "adm_woL L"  shows "adm_wo (mergeSL S L)"
traytel@54980
   740
unfolding adm_wo_def proof safe
traytel@54980
   741
  fix f g :: "'a => 'b" and i :: 'a
traytel@54980
   742
  assume 1: "\<forall>j\<in>underS i. f j = g j"
traytel@54980
   743
  show "mergeSL S L f i = mergeSL S L g i"
traytel@54980
   744
  proof(cases "isSucc i")
traytel@54980
   745
    case True
traytel@54980
   746
    hence "pred i \<in> underS i" unfolding underS_def using isSucc_pred_in isSucc_pred_diff by auto
traytel@54980
   747
    thus ?thesis using True 1 unfolding mergeSL_def by auto
traytel@54980
   748
  next
traytel@54980
   749
    case False hence "isLim i" unfolding isLim_def by auto
traytel@54980
   750
    thus ?thesis using assms False 1 unfolding mergeSL_def adm_woL_def by auto
traytel@54980
   751
  qed
traytel@54980
   752
qed
traytel@54980
   753
traytel@54980
   754
lemma worec_fixpoint1: "adm_wo H \<Longrightarrow> worec H i = H (worec H) i"
traytel@54980
   755
by (metis worec_fixpoint)
traytel@54980
   756
traytel@54980
   757
lemma worecSL_isSucc:
traytel@54980
   758
assumes a: "adm_woL L" and i: "isSucc i"
traytel@54980
   759
shows "worecSL S L i = S (pred i) (worecSL S L (pred i))"
traytel@54980
   760
proof-
traytel@54980
   761
  let ?H = "mergeSL S L"
traytel@54980
   762
  have "worecSL S L i = ?H (worec ?H) i"
traytel@54980
   763
  unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] .
traytel@54980
   764
  also have "... = S (pred i) (worecSL S L (pred i))"
traytel@54980
   765
  unfolding worecSL_def mergeSL_def using i by simp
traytel@54980
   766
  finally show ?thesis .
traytel@54980
   767
qed
traytel@54980
   768
traytel@54980
   769
lemma worecSL_succ:
traytel@54980
   770
assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}"
traytel@54980
   771
shows "worecSL S L (succ j) = S j (worecSL S L j)"
traytel@54980
   772
proof-
traytel@54980
   773
  def i \<equiv> "succ j"
traytel@54980
   774
  have i: "isSucc i" by (metis i i_def isSucc_succ)
traytel@54980
   775
  have ij: "j = pred i" unfolding i_def using assms by simp
traytel@54980
   776
  have 0: "succ (pred i) = i" using i by simp
traytel@54980
   777
  show ?thesis unfolding ij using worecSL_isSucc[OF a i] unfolding 0 .
traytel@54980
   778
qed
traytel@54980
   779
traytel@54980
   780
lemma worecSL_isLim:
traytel@54980
   781
assumes a: "adm_woL L" and i: "isLim i"
traytel@54980
   782
shows "worecSL S L i = L (worecSL S L) i"
traytel@54980
   783
proof-
traytel@54980
   784
  let ?H = "mergeSL S L"
traytel@54980
   785
  have "worecSL S L i = ?H (worec ?H) i"
traytel@54980
   786
  unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] .
traytel@54980
   787
  also have "... = L (worecSL S L) i"
traytel@54980
   788
  using i unfolding worecSL_def mergeSL_def isLim_def by simp
traytel@54980
   789
  finally show ?thesis .
traytel@54980
   790
qed
traytel@54980
   791
traytel@54980
   792
definition worecZSL :: "'b \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
traytel@54980
   793
where "worecZSL Z S L \<equiv> worecSL S (\<lambda> f a. if a = zero then Z else L f a)"
traytel@54980
   794
traytel@54980
   795
lemma worecZSL_zero:
traytel@54980
   796
assumes a: "adm_woL L"
traytel@54980
   797
shows "worecZSL Z S L zero = Z"
traytel@54980
   798
proof-
traytel@54980
   799
  let ?L = "\<lambda> f a. if a = zero then Z else L f a"
traytel@54980
   800
  have "worecZSL Z S L zero = ?L (worecZSL Z S L) zero"
traytel@54980
   801
  unfolding worecZSL_def apply(rule worecSL_isLim)
traytel@54980
   802
  using assms unfolding adm_woL_def by auto
traytel@54980
   803
  also have "... = Z" by simp
traytel@54980
   804
  finally show ?thesis .
traytel@54980
   805
qed
traytel@54980
   806
traytel@54980
   807
lemma worecZSL_succ:
traytel@54980
   808
assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}"
traytel@54980
   809
shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)"
traytel@54980
   810
unfolding worecZSL_def apply(rule  worecSL_succ)
traytel@54980
   811
using assms unfolding adm_woL_def by auto
traytel@54980
   812
traytel@54980
   813
lemma worecZSL_isLim:
traytel@54980
   814
assumes a: "adm_woL L" and "isLim i" and "i \<noteq> zero"
traytel@54980
   815
shows "worecZSL Z S L i = L (worecZSL Z S L) i"
traytel@54980
   816
proof-
traytel@54980
   817
  let ?L = "\<lambda> f a. if a = zero then Z else L f a"
traytel@54980
   818
  have "worecZSL Z S L i = ?L (worecZSL Z S L) i"
traytel@54980
   819
  unfolding worecZSL_def apply(rule worecSL_isLim)
traytel@54980
   820
  using assms unfolding adm_woL_def by auto
traytel@54980
   821
  also have "... = L (worecZSL Z S L) i" using assms by simp
traytel@54980
   822
  finally show ?thesis .
traytel@54980
   823
qed
traytel@54980
   824
traytel@54980
   825
traytel@54980
   826
subsection {* Well-order succ-lim induction: *}
traytel@54980
   827
traytel@54980
   828
lemma ord_cases:
traytel@54980
   829
obtains j where "i = succ j" and "aboveS j \<noteq> {}"  | "isLim i"
traytel@54980
   830
by (metis isLim_def isSucc_def)
traytel@54980
   831
traytel@54980
   832
lemma well_order_inductSL[case_names Suc Lim]:
traytel@54980
   833
assumes SUCC: "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" and
traytel@54980
   834
LIM: "\<And>i. \<lbrakk>isLim i; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i"
traytel@54980
   835
shows "P i"
traytel@54980
   836
proof(induction rule: well_order_induct)
traytel@54980
   837
  fix i assume 0:  "\<forall>j. j \<noteq> i \<and> (j, i) \<in> r \<longrightarrow> P j"
traytel@54980
   838
  show "P i" proof(cases i rule: ord_cases)
traytel@54980
   839
    fix j assume i: "i = succ j" and j: "aboveS j \<noteq> {}"
traytel@54980
   840
    hence "j \<noteq> i \<and> (j, i) \<in> r" by (metis  succ_diff succ_in)
traytel@54980
   841
    hence 1: "P j" using 0 by simp
traytel@54980
   842
    show "P i" unfolding i apply(rule SUCC) using 1 j by auto
traytel@54980
   843
  qed(insert 0 LIM, unfold underS_def, auto)
traytel@54980
   844
qed
traytel@54980
   845
traytel@54980
   846
lemma well_order_inductZSL[case_names Zero Suc Lim]:
traytel@54980
   847
assumes ZERO: "P zero"
traytel@54980
   848
and SUCC: "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" and
traytel@54980
   849
LIM: "\<And>i. \<lbrakk>isLim i; i \<noteq> zero; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i"
traytel@54980
   850
shows "P i"
traytel@54980
   851
apply(induction rule: well_order_inductSL) using assms by auto
traytel@54980
   852
traytel@54980
   853
(* Succesor and limit ordinals *)
traytel@54980
   854
definition "isSuccOrd \<equiv> \<exists> j \<in> Field r. \<forall> i \<in> Field r. (i,j) \<in> r"
traytel@54980
   855
definition "isLimOrd \<equiv> \<not> isSuccOrd"
traytel@54980
   856
traytel@54980
   857
lemma isLimOrd_succ:
traytel@54980
   858
assumes isLimOrd and "i \<in> Field r"
traytel@54980
   859
shows "succ i \<in> Field r"
traytel@54980
   860
using assms unfolding isLimOrd_def isSuccOrd_def
traytel@54980
   861
by (metis REFL in_notinI refl_on_domain succ_smallest)
traytel@54980
   862
traytel@54980
   863
lemma isLimOrd_aboveS:
traytel@54980
   864
assumes l: isLimOrd and i: "i \<in> Field r"
traytel@54980
   865
shows "aboveS i \<noteq> {}"
traytel@54980
   866
proof-
traytel@54980
   867
  obtain j where "j \<in> Field r" and "(j,i) \<notin> r"
traytel@54980
   868
  using assms unfolding isLimOrd_def isSuccOrd_def by auto
traytel@54980
   869
  hence "(i,j) \<in> r \<and> j \<noteq> i" by (metis i max2_def max2_greater)
traytel@54980
   870
  thus ?thesis unfolding aboveS_def by auto
traytel@54980
   871
qed
traytel@54980
   872
traytel@54980
   873
lemma succ_aboveS_isLimOrd:
traytel@54980
   874
assumes "\<forall> i \<in> Field r. aboveS i \<noteq> {} \<and> succ i \<in> Field r"
traytel@54980
   875
shows isLimOrd
traytel@54980
   876
unfolding isLimOrd_def isSuccOrd_def proof safe
traytel@54980
   877
  fix j assume j: "j \<in> Field r" "\<forall>i\<in>Field r. (i, j) \<in> r"
traytel@54980
   878
  hence "(succ j, j) \<in> r" using assms by auto
traytel@54980
   879
  moreover have "aboveS j \<noteq> {}" using assms j unfolding aboveS_def by auto
traytel@54980
   880
  ultimately show False by (metis succ_not_in)
traytel@54980
   881
qed
traytel@54980
   882
traytel@54980
   883
lemma isLim_iff:
traytel@54980
   884
assumes l: "isLim i" and j: "j \<in> underS i"
traytel@54980
   885
shows "\<exists> k. k \<in> underS i \<and> j \<in> underS k"
traytel@54980
   886
proof-
traytel@54980
   887
  have a: "aboveS j \<noteq> {}" using j unfolding underS_def aboveS_def by auto
traytel@54980
   888
  show ?thesis apply(rule exI[of _ "succ j"]) apply safe
traytel@54980
   889
  using assms a unfolding underS_def isLim_def
traytel@54980
   890
  apply (metis (lifting, full_types) isSucc_def mem_Collect_eq succ_smallest)
traytel@54980
   891
  by (metis (lifting, full_types) a mem_Collect_eq succ_diff succ_in)
traytel@54980
   892
qed
traytel@54980
   893
traytel@54980
   894
traytel@54980
   895
end (* context wo_rel *)
traytel@54980
   896
traytel@54980
   897
abbreviation "zero \<equiv> wo_rel.zero"
traytel@54980
   898
abbreviation "succ \<equiv> wo_rel.succ"
traytel@54980
   899
abbreviation "pred \<equiv> wo_rel.pred"
traytel@54980
   900
abbreviation "isSucc \<equiv> wo_rel.isSucc"
traytel@54980
   901
abbreviation "isLim \<equiv> wo_rel.isLim"
traytel@54980
   902
abbreviation "isLimOrd \<equiv> wo_rel.isLimOrd"
traytel@54980
   903
abbreviation "isSuccOrd \<equiv> wo_rel.isSuccOrd"
traytel@54980
   904
abbreviation "adm_woL \<equiv> wo_rel.adm_woL"
traytel@54980
   905
abbreviation "worecSL \<equiv> wo_rel.worecSL"
traytel@54980
   906
abbreviation "worecZSL \<equiv> wo_rel.worecZSL"
traytel@54980
   907
traytel@54980
   908
section {* Projections of Wellorders *}
traytel@54980
   909
 
traytel@54980
   910
definition "oproj r s f \<equiv> Field s \<subseteq> f ` (Field r) \<and> compat r s f"
traytel@54980
   911
traytel@54980
   912
lemma oproj_in: 
traytel@54980
   913
assumes "oproj r s f" and "(a,a') \<in> r"
traytel@54980
   914
shows "(f a, f a') \<in> s"
traytel@54980
   915
using assms unfolding oproj_def compat_def by auto
traytel@54980
   916
traytel@54980
   917
lemma oproj_Field:
traytel@54980
   918
assumes f: "oproj r s f" and a: "a \<in> Field r"
traytel@54980
   919
shows "f a \<in> Field s"
traytel@54980
   920
using oproj_in[OF f] a unfolding Field_def by auto
traytel@54980
   921
traytel@54980
   922
lemma oproj_Field2:
traytel@54980
   923
assumes f: "oproj r s f" and a: "b \<in> Field s"
traytel@54980
   924
shows "\<exists> a \<in> Field r. f a = b"
traytel@54980
   925
using assms unfolding oproj_def by auto
traytel@54980
   926
traytel@54980
   927
lemma oproj_under: 
traytel@54980
   928
assumes f:  "oproj r s f" and a: "a \<in> under r a'"
traytel@54980
   929
shows "f a \<in> under s (f a')"
blanchet@55023
   930
using oproj_in[OF f] a unfolding under_def by auto
traytel@54980
   931
traytel@54980
   932
(* An ordinal is embedded in another whenever it is embedded as an order 
traytel@54980
   933
(not necessarily as initial segment):*)
traytel@54980
   934
theorem embedI:
traytel@54980
   935
assumes r: "Well_order r" and s: "Well_order s" 
traytel@54980
   936
and f: "\<And> a. a \<in> Field r \<Longrightarrow> f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
traytel@54980
   937
shows "\<exists> g. embed r s g"
traytel@54980
   938
proof-  
traytel@54980
   939
  interpret r!: wo_rel r by unfold_locales (rule r)
traytel@54980
   940
  interpret s!: wo_rel s by unfold_locales (rule s)
traytel@54980
   941
  let ?G = "\<lambda> g a. suc s (g ` underS r a)"
traytel@54980
   942
  def g \<equiv> "worec r ?G"
traytel@54980
   943
  have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto
traytel@54980
   944
  (*  *)
traytel@54980
   945
  {fix a assume "a \<in> Field r"
traytel@54980
   946
   hence "bij_betw g (under r a) (under s (g a)) \<and> 
traytel@54980
   947
          g a \<in> under s (f a)"
traytel@54980
   948
   proof(induction a rule: r.underS_induct)
traytel@54980
   949
     case (1 a)
traytel@54980
   950
     hence a: "a \<in> Field r"
traytel@54980
   951
     and IH1a: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> inj_on g (under r a1)"
traytel@54980
   952
     and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)"
traytel@54980
   953
     and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)"
blanchet@55023
   954
     unfolding underS_def Field_def bij_betw_def by auto
traytel@54980
   955
     have fa: "f a \<in> Field s" using f[OF a] by auto
traytel@54980
   956
     have g: "g a = suc s (g ` underS r a)" 
traytel@54980
   957
     using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp
traytel@54980
   958
     have A0: "g ` underS r a \<subseteq> Field s" 
blanchet@55023
   959
     using IH1b by (metis IH2 image_subsetI in_mono under_Field)
traytel@54980
   960
     {fix a1 assume a1: "a1 \<in> underS r a"
traytel@54980
   961
      from IH2[OF this] have "g a1 \<in> under s (f a1)" .
traytel@54980
   962
      moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
blanchet@55023
   963
      ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
traytel@54980
   964
     }
blanchet@55023
   965
     hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def 
blanchet@55023
   966
     using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
traytel@54980
   967
     hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
traytel@54980
   968
     have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
traytel@54980
   969
     unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
traytel@54980
   970
     {fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
traytel@54980
   971
      hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
blanchet@55023
   972
      unfolding underS_def under_def refl_on_def Field_def by auto 
traytel@54980
   973
      hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
traytel@54980
   974
      hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12 
blanchet@55023
   975
      unfolding underS_def under_def by auto
traytel@54980
   976
     } note C = this
traytel@54980
   977
     have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
traytel@54980
   978
     have aa: "a \<in> under r a" 
blanchet@55023
   979
     using a r.REFL unfolding under_def underS_def refl_on_def by auto
traytel@54980
   980
     show ?case proof safe
traytel@54980
   981
       show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
traytel@54980
   982
         show "inj_on g (under r a)" proof(rule r.inj_on_Field)
traytel@54980
   983
           fix a1 a2 assume "a1 \<in> under r a" and a2: "a2 \<in> under r a" and a1: "a1 \<in> underS r a2"
traytel@54980
   984
           hence a22: "a2 \<in> under r a2" and a12: "a1 \<in> under r a2" "a1 \<noteq> a2"
blanchet@55023
   985
           using a r.REFL unfolding under_def underS_def refl_on_def by auto
traytel@54980
   986
           show "g a1 \<noteq> g a2"
traytel@54980
   987
           proof(cases "a2 = a")
traytel@54980
   988
             case False hence "a2 \<in> underS r a" 
blanchet@55023
   989
             using a2 unfolding underS_def under_def by auto 
traytel@54980
   990
             from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto
blanchet@55023
   991
           qed(insert B a1, unfold underS_def, auto)
blanchet@55023
   992
         qed(unfold under_def Field_def, auto)
traytel@54980
   993
       next
traytel@54980
   994
         fix a1 assume a1: "a1 \<in> under r a" 
traytel@54980
   995
         show "g a1 \<in> under s (g a)"
traytel@54980
   996
         proof(cases "a1 = a")
traytel@54980
   997
           case True thus ?thesis 
blanchet@55023
   998
           using ga s.REFL unfolding refl_on_def under_def by auto
traytel@54980
   999
         next
traytel@54980
  1000
           case False
blanchet@55023
  1001
           hence a1: "a1 \<in> underS r a" using a1 unfolding underS_def under_def by auto 
blanchet@55023
  1002
           thus ?thesis using B unfolding underS_def under_def by auto
traytel@54980
  1003
         qed
traytel@54980
  1004
       next
traytel@54980
  1005
         fix b1 assume b1: "b1 \<in> under s (g a)"
traytel@54980
  1006
         show "b1 \<in> g ` under r a"
traytel@54980
  1007
         proof(cases "b1 = g a")
traytel@54980
  1008
           case True thus ?thesis using aa by auto
traytel@54980
  1009
         next
traytel@54980
  1010
           case False 
blanchet@55023
  1011
           hence "b1 \<in> underS s (g a)" using b1 unfolding underS_def under_def by auto
traytel@54980
  1012
           from s.underS_suc[OF this[unfolded g] A0]
traytel@54980
  1013
           obtain a1 where a1: "a1 \<in> underS r a" and b1: "b1 \<in> under s (g a1)" by auto
traytel@54980
  1014
           obtain a2 where "a2 \<in> under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto
traytel@54980
  1015
           hence "a2 \<in> under r a" using a1 
blanchet@55023
  1016
           by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans)
traytel@54980
  1017
           thus ?thesis using b1 by auto
traytel@54980
  1018
         qed
traytel@54980
  1019
       qed
traytel@54980
  1020
     next
traytel@54980
  1021
       have "(g a, f a) \<in> s" unfolding g proof(rule s.suc_least[OF A0])
traytel@54980
  1022
         fix b1 assume "b1 \<in> g ` underS r a" 
traytel@54980
  1023
         then obtain a1 where a1: "b1 = g a1" and a1: "a1 \<in> underS r a" by auto
traytel@54980
  1024
         hence "b1 \<in> underS s (f a)" 
traytel@54980
  1025
         using a by (metis `\<And>a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (f a)`)
blanchet@55023
  1026
         thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding underS_def by auto
traytel@54980
  1027
       qed(insert fa, auto)
blanchet@55023
  1028
       thus "g a \<in> under s (f a)" unfolding under_def by auto
traytel@54980
  1029
     qed
traytel@54980
  1030
   qed
traytel@54980
  1031
  }
traytel@54980
  1032
  thus ?thesis unfolding embed_def by auto
traytel@54980
  1033
qed
traytel@54980
  1034
traytel@54980
  1035
corollary ordLeq_def2:
traytel@54980
  1036
  "r \<le>o s \<longleftrightarrow> Well_order r \<and> Well_order s \<and>
traytel@54980
  1037
               (\<exists> f. \<forall> a \<in> Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a))"
traytel@54980
  1038
using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s]
traytel@54980
  1039
unfolding ordLeq_def by fast
traytel@54980
  1040
traytel@54980
  1041
lemma iso_oproj:
traytel@54980
  1042
  assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
traytel@54980
  1043
  shows "oproj r s f"
traytel@54980
  1044
using assms unfolding oproj_def
traytel@54980
  1045
by (subst (asm) iso_iff3) (auto simp: bij_betw_def)
traytel@54980
  1046
traytel@54980
  1047
theorem oproj_embed:
traytel@54980
  1048
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
traytel@54980
  1049
shows "\<exists> g. embed s r g"
blanchet@55023
  1050
proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe)
traytel@54980
  1051
  fix b assume "b \<in> Field s"
traytel@54980
  1052
  thus "inv_into (Field r) f b \<in> Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into)
traytel@54980
  1053
next
traytel@54980
  1054
  fix a b assume "b \<in> Field s" "a \<noteq> b" "(a, b) \<in> s"
traytel@54980
  1055
    "inv_into (Field r) f a = inv_into (Field r) f b"
traytel@54980
  1056
  with f show False by (auto dest!: inv_into_injective simp: Field_def oproj_def)
traytel@54980
  1057
next
traytel@54980
  1058
  fix a b assume *: "b \<in> Field s" "a \<noteq> b" "(a, b) \<in> s"
traytel@54980
  1059
  { assume "(inv_into (Field r) f a, inv_into (Field r) f b) \<notin> r"
traytel@54980
  1060
    moreover
traytel@54980
  1061
    from *(3) have "a \<in> Field s" unfolding Field_def by auto
traytel@54980
  1062
    with *(1,2) have
traytel@54980
  1063
      "inv_into (Field r) f a \<in> Field r" "inv_into (Field r) f b \<in> Field r"
traytel@54980
  1064
      "inv_into (Field r) f a \<noteq> inv_into (Field r) f b"
traytel@54980
  1065
      by (auto dest!: oproj_Field2[OF f] inv_into_injective intro!: inv_into_into)
traytel@54980
  1066
    ultimately have "(inv_into (Field r) f b, inv_into (Field r) f a) \<in> r"
traytel@54980
  1067
      using r by (auto simp: well_order_on_def linear_order_on_def total_on_def)
traytel@54980
  1068
    with f[unfolded oproj_def compat_def] *(1) `a \<in> Field s`
traytel@54980
  1069
      f_inv_into_f[of b f "Field r"] f_inv_into_f[of a f "Field r"]
traytel@54980
  1070
      have "(b, a) \<in> s" by (metis in_mono)
traytel@54980
  1071
    with *(2,3) s have False
traytel@54980
  1072
      by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def antisym_def)
traytel@54980
  1073
  } thus "(inv_into (Field r) f a, inv_into (Field r) f b) \<in> r" by blast
traytel@54980
  1074
qed
traytel@54980
  1075
traytel@54980
  1076
corollary oproj_ordLeq:
traytel@54980
  1077
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
traytel@54980
  1078
shows "s \<le>o r"
traytel@54980
  1079
using oproj_embed[OF assms] r s unfolding ordLeq_def by auto
traytel@54980
  1080
blanchet@48975
  1081
end