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