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