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
```