1(* Title: HOL/Cardinals/Ordinal_Arithmetic.thy 2 Author: Dmitriy Traytel, TU Muenchen 3 Copyright 2014 4 5Ordinal arithmetic. 6*) 7 8section \<open>Ordinal Arithmetic\<close> 9 10theory Ordinal_Arithmetic 11imports Wellorder_Constructions 12begin 13 14definition osum :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a + 'b) rel" (infixr "+o" 70) 15where 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 19lemma Field_osum: "Field(r +o r') = Inl ` Field r \<union> Inr ` Field r'" 20 unfolding osum_def Field_def by auto 21 22lemma 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 26lemma osum_trans: 27assumes TRANS: "trans r" and TRANS': "trans r'" 28shows "trans (r +o r')" 29proof(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) 51qed 52 53lemma 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 56lemma osum_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r +o r')" 57 unfolding antisym_def osum_def by auto 58 59lemma 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 62lemma 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 65lemma 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 68lemma osum_wf: 69assumes WF: "wf r" and WF': "wf r'" 70shows "wf (r +o r')" 71unfolding wf_eq_minimal2 unfolding Field_osum 72proof(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 95qed 96 97lemma 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 102lemma 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 106lemma 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 110lemma 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)" 113proof(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 118next 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 131qed 132 133lemma osum_Well_order: 134assumes WELL: "Well_order r" and WELL': "Well_order r'" 135shows "Well_order (r +o r')" 136proof- 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 140qed 141 142lemma osum_embedL: 143 assumes WELL: "Well_order r" and WELL': "Well_order r'" 144 shows "embed r (r +o r') Inl" 145proof - 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) 154qed 155 156corollary 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 161lemma dir_image_alt: "dir_image r f = map_prod f f ` r" 162 unfolding dir_image_def map_prod_def by auto 163 164lemma 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 167definition oprod :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> 'b) rel" (infixr "*o" 80) 168where "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 172lemma Field_oprod: "Field (r *o r') = Field r \<times> Field r'" 173 unfolding oprod_def Field_def by auto blast+ 174 175lemma 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 178lemma oprod_trans: 179 assumes "trans r" "trans r'" "antisym r" "antisym r'" 180 shows "trans (r *o r')" 181proof(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 204qed 205 206lemma 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 209lemma oprod_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r *o r')" 210 unfolding antisym_def oprod_def by auto 211 212lemma 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 215lemma 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 218lemma 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 221lemma oprod_wf: 222assumes WF: "wf r" and WF': "wf r'" 223shows "wf (r *o r')" 224unfolding wf_eq_minimal2 unfolding Field_oprod 225proof(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 237qed 238 239lemma 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 244lemma 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 248lemma wf_extend_oprod1: 249 assumes "wf r" 250 shows "wf {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" 251proof (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 261qed 262 263lemma 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 267lemma wf_extend_oprod2: 268 assumes "wf r" 269 shows "wf {((x1,y), (x2,y)) . (x1, x2) \<in> r \<and> y \<in> A}" 270proof (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 280qed 281 282lemma 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)" 285proof(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 290next 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 294qed 295 296lemma oprod_Well_order: 297assumes WELL: "Well_order r" and WELL': "Well_order r'" 298shows "Well_order (r *o r')" 299proof- 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 303qed 304 305lemma 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") 308proof - 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) 329qed 330 331corollary 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 334definition "support z A f = {x \<in> A. f x \<noteq> z}" 335 336lemma 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 339lemma support_upd[simp]: "support z A (f(x := z)) = support z A f - {x}" 340 unfolding support_def by auto 341 342lemma support_upd_subset[simp]: "support z A (f(x := y)) \<subseteq> support z A f \<union> {x}" 343 unfolding support_def by auto 344 345lemma 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> {}") 348proof - 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 354qed 355 356definition fin_support where 357 "fin_support z A = {f. finite (support z A f)}" 358 359lemma finite_support: "f \<in> fin_support z A \<Longrightarrow> finite (support z A f)" 360 unfolding support_def fin_support_def by auto 361 362lemma 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") 365proof 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"]) 371next 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]) 375qed 376 377lemma 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 380context wo_rel 381begin 382 383definition isMaxim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" 384where "isMaxim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (a,b) \<in> r)" 385 386definition maxim :: "'a set \<Rightarrow> 'a" 387where "maxim A \<equiv> THE b. isMaxim A b" 388 389lemma 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 392lemma maxim_isMaxim: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> isMaxim A (maxim A)" 393unfolding maxim_def 394proof (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 409qed simp 410 411lemma 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 414lemma 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 417lemma isMaxim_zero: "isMaxim A zero \<Longrightarrow> A = {zero}" 418 unfolding isMaxim_def by auto 419 420lemma 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)" 423proof - 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 439qed 440 441lemma 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)" 444proof - 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 460qed 461 462lemma maxim_insert_zero: 463 assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r" 464 shows "maxim (insert zero A) = maxim A" 465using assms zero_in_Field maxim_in[OF assms] by (subst maxim_insert[unfolded max2_def]) auto 466 467lemma maxim_equality: "isMaxim A x \<Longrightarrow> maxim A = x" 468 unfolding maxim_def by (rule the_equality) auto 469 470lemma 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 474lemma 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 477lemma 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 480definition "max_fun_diff f g \<equiv> maxim ({a \<in> Field r. f a \<noteq> g a})" 481 482lemma max_fun_diff_commute: "max_fun_diff f g = max_fun_diff g f" 483 unfolding max_fun_diff_def by metis 484 485lemma zero_under: "x \<in> Field r \<Longrightarrow> zero \<in> under x" 486 unfolding under_def by (auto intro: zero_smallest) 487 488end 489 490definition "FinFunc r s = Func (Field s) (Field r) \<inter> fin_support (zero r) (Field s)" 491 492lemma 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 495locale wo_rel2 = 496 fixes r s 497 assumes rWELL: "Well_order r" 498 and sWELL: "Well_order s" 499begin 500 501interpretation r: wo_rel r by unfold_locales (rule rWELL) 502interpretation s: wo_rel s by unfold_locales (rule sWELL) 503 504abbreviation "SUPP \<equiv> support r.zero (Field s)" 505abbreviation "FINFUNC \<equiv> FinFunc r s" 506lemmas FINFUNCD = FinFuncD[of _ r s] 507 508lemma 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 511lemma 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 515lemma 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 520lemma 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 524lemma 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 528lemma 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 534lemma 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 540lemma 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") 547proof (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 568next 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 590qed 591 592definition 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 596lemma Field_oexp: "Field oexp = FINFUNC" 597 unfolding oexp_def FinFunc_def by (auto simp: Let_def Field_def) 598 599lemma oexp_Refl: "Refl oexp" 600 unfolding refl_on_def Field_oexp unfolding oexp_def by (auto simp: Let_def) 601 602lemma oexp_trans: "trans oexp" 603proof (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 630qed 631 632lemma oexp_Preorder: "Preorder oexp" 633 unfolding preorder_on_def using oexp_Refl oexp_trans by blast 634 635lemma oexp_antisym: "antisym oexp" 636proof (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) 640qed 641 642lemma oexp_Partial_order: "Partial_order oexp" 643 unfolding partial_order_on_def using oexp_Preorder oexp_antisym by blast 644 645lemma 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 649lemma oexp_Linear_order: "Linear_order oexp" 650 unfolding linear_order_on_def using oexp_Partial_order oexp_Total by blast 651 652definition "const = (\<lambda>x. if x \<in> Field s then r.zero else undefined)" 653 654lemma const_in[simp]: "x \<in> Field s \<Longrightarrow> const x = r.zero" 655 unfolding const_def by auto 656 657lemma const_notin[simp]: "x \<notin> Field s \<Longrightarrow> const x = undefined" 658 unfolding const_def by auto 659 660lemma const_Int_Field[simp]: "Field s \<inter> - {x. const x = r.zero} = {}" 661 by auto 662 663lemma 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 667lemma const_least: 668 assumes "Field r \<noteq> {}" "f \<in> FINFUNC" 669 shows "(const, f) \<in> oexp" 670proof (cases "f = const") 671 case True thus ?thesis using refl_onD[OF oexp_Refl] assms(2) unfolding Field_oexp by auto 672next 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) 676qed 677 678lemma 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" 681proof (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 693qed 694 695lemma 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 700lemma 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 703lemma oexp_empty: "\<lbrakk>Field r = {}; Field s \<noteq> {}\<rbrakk> \<Longrightarrow> oexp = {}" 704 unfolding oexp_def FinFunc_def Let_def by auto 705 706lemma 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 710lemma 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" 713proof - 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 719qed 720 721lemma 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 727lemma oexp_wf_Id: "wf (oexp - Id)" 728proof (cases "Field r = {} \<or> Field s = {}") 729 case True thus ?thesis using oexp_empty oexp_empty2 by fastforce 730next 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 894qed 895 896lemma oexp_Well_order: "Well_order oexp" 897 unfolding well_order_on_def using oexp_Linear_order oexp_wf_Id by blast 898 899interpretation o: wo_rel oexp by unfold_locales (rule oexp_Well_order) 900 901lemma 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 905end 906 907notation wo_rel2.oexp (infixl "^o" 90) 908lemmas oexp_def = wo_rel2.oexp_def[unfolded wo_rel2_def, OF conjI] 909lemmas oexp_Well_order = wo_rel2.oexp_Well_order[unfolded wo_rel2_def, OF conjI] 910lemmas Field_oexp = wo_rel2.Field_oexp[unfolded wo_rel2_def, OF conjI] 911 912definition "ozero = {}" 913 914lemma ozero_Well_order[simp]: "Well_order ozero" 915 unfolding ozero_def by simp 916 917lemma ozero_ordIso[simp]: "ozero =o ozero" 918 unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def by auto 919 920lemma Field_ozero[simp]: "Field ozero = {}" 921 unfolding ozero_def by simp 922 923lemma 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 927lemma ozero_ordLeq: 928assumes "Well_order r" shows "ozero \<le>o r" 929using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto 930 931definition "oone = {((),())}" 932 933lemma 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 937lemma Field_oone[simp]: "Field oone = {()}" 938 unfolding oone_def by simp 939 940lemma 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 945lemma 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 949lemma 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") 952proof - 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) 965qed 966 967lemma 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") 970proof - 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) 983qed 984 985lemma osum_cong: 986 assumes "t =o u" and "r =o s" 987 shows "t +o r =o u +o s" 988using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]] 989 assms[unfolded ordIso_def] by auto 990 991lemma Well_order_empty[simp]: "Well_order {}" 992 unfolding Field_empty by (rule well_order_on_empty) 993 994lemma 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 998lemma 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 1003lemma oexp_empty2[simp]: 1004 assumes "Well_order r" "r \<noteq> {}" 1005 shows "{} ^o r = {}" 1006proof - 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 1010qed 1011 1012lemma oprod_zero[simp]: "{} *o r = {}" "r *o {} = {}" 1013 unfolding oprod_def by simp_all 1014 1015lemma 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") 1018proof - 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) 1031qed 1032 1033lemma 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") 1036proof - 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) 1049qed 1050 1051lemma oprod_cong: 1052 assumes "t =o u" and "r =o s" 1053 shows "t *o r =o u *o s" 1054using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]] 1055 assms[unfolded ordIso_def] by auto 1056 1057lemma Field_singleton[simp]: "Field {(z,z)} = {z}" 1058 by (metis well_order_on_Field well_order_on_singleton) 1059 1060lemma 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 1064lemma 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 1068lemma oone_ordIso_oexp: 1069 assumes "r =o oone" and s: "Well_order s" 1070 shows "r ^o s =o oone" (is "?L =o ?R") 1071proof - 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) 1086qed 1087 1088(*Lemma 1.4.3 from Holz et al.*) 1089context 1090 fixes r s t 1091 assumes r: "Well_order r" 1092 assumes s: "Well_order s" 1093 assumes t: "Well_order t" 1094begin 1095 1096lemma osum_ozeroL: "ozero +o r =o r" 1097 using r unfolding osum_def ozero_def by (auto intro: map_prod_ordIso) 1098 1099lemma osum_ozeroR: "r +o ozero =o r" 1100 using r unfolding osum_def ozero_def by (auto intro: map_prod_ordIso) 1101 1102lemma osum_assoc: "(r +o s) +o t =o r +o s +o t" (is "?L =o ?R") 1103proof - 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) 1120qed 1121 1122lemma osum_monoR: 1123 assumes "s <o t" 1124 shows "r +o s <o r +o t" (is "?L <o ?R") 1125proof - 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) 1147qed 1148 1149lemma osum_monoL: 1150 assumes "r \<le>o s" 1151 shows "r +o t \<le>o s +o t" 1152proof - 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) 1160qed 1161 1162lemma oprod_ozeroL: "ozero *o r =o ozero" 1163 using ozero_ordIso unfolding ozero_def by simp 1164 1165lemma oprod_ozeroR: "r *o ozero =o ozero" 1166 using ozero_ordIso unfolding ozero_def by simp 1167 1168lemma oprod_ooneR: "r *o oone =o r" (is "?L =o ?R") 1169proof - 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) 1175qed 1176 1177lemma oprod_ooneL: "oone *o r =o r" (is "?L =o ?R") 1178proof - 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) 1185qed 1186 1187lemma oprod_monoR: 1188 assumes "ozero <o r" "s <o t" 1189 shows "r *o s <o r *o t" (is "?L <o ?R") 1190proof - 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) 1216qed 1217 1218lemma oprod_monoL: 1219 assumes "r \<le>o s" 1220 shows "r *o t \<le>o s *o t" 1221proof - 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) 1229qed 1230 1231lemma oprod_assoc: "(r *o s) *o t =o r *o s *o t" (is "?L =o ?R") 1232proof - 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) 1247qed 1248 1249lemma oprod_osum: "r *o (s +o t) =o r *o s +o r *o t" (is "?L =o ?R") 1250proof - 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) 1266qed 1267 1268lemma 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 1272lemma 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 1275lemma oexp_monoR: 1276 assumes "oone <o r" "s <o t" 1277 shows "r ^o s <o r ^o t" (is "?L <o ?R") 1278proof - 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) 1385qed 1386 1387lemma oexp_monoL: 1388 assumes "r \<le>o s" 1389 shows "r ^o t \<le>o s ^o t" 1390proof - 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 1449qed 1450 1451lemma ordLeq_oexp2: 1452 assumes "oone <o r" 1453 shows "s \<le>o r ^o s" 1454proof - 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) 1490qed 1491 1492lemma 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)") 1495proof 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) 1501next 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) 1505qed 1506 1507lemma 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) 1512proof - 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 1529qed 1530 1531lemma 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) 1536proof - 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) 1546qed 1547 1548lemma oexp_osum: "r ^o (s +o t) =o (r ^o s) *o (r ^o t)" (is "?R =o ?L") 1549proof (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) 1575qed 1576 1577definition "rev_curr f b = (if b \<in> Field t then \<lambda>a. f (a, b) else undefined)" 1578 1579lemma rev_curr_FinFunc: 1580 assumes Field: "Field r \<noteq> {}" 1581 shows "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t" 1582proof 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) 1592next 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 1620qed 1621 1622lemma 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 1627lemma 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)" 1632proof - 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 1665qed 1666 1667lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L") 1668proof (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 1685next 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 1723qed 1724 1725end (* context with 3 wellorders *) 1726 1727end 1728