Quelle  Ordinal_Arithmetic.thy

(*  Title:      HOL/Cardinals/Ordinal_Arithmetic.thy
  Author: Dmitriy Traytel, TU Muenchen
  Copyright 2014
 
 Ordinal arithmetic.
*)

section ‹Ordinal Arithmetic›

theory Ordinal_Arithmetic
  imports Wellorder_Constructions
begin

definition osum :: "'a rel ==> 'b rel ==> ('a + 'b) rel"  (infixr ‹+o› 70)
  where
    "r +o r' = map_prod Inl Inl ` r ∪ map_prod Inr Inr ` r' ∪
     {(Inl a, Inr a') | a a' . a ∈ Field r ∧ a' ∈ Field r'}"

lemma Field_osum: "Field(r +o r') = Inl ` Field r ∪ Inr ` Field r'"
  unfolding osum_def Field_def by auto

lemma osum_Refl:"[Refl r; Refl r'] ==> Refl (r +o r')"
  (*Need first unfold Field_osum, only then osum_def*)
  unfolding refl_on_def Field_osum unfolding osum_def by blast

lemma osum_trans:
  assumes TRANS: "trans r" and TRANS': "trans r'"
  shows "trans (r +o r')"
  unfolding trans_def
proof(safe)
  fix x y z assume *: "(x, y) ∈ r +o r'" "(y, z) ∈ r +o r'"
  thus "(x, z) ∈ r +o r'"
  proof (cases x y z rule: sum.exhaust[case_product sum.exhaust sum.exhaust])
    case (Inl_Inl_Inl a b c)
    with * have "(a,b) ∈ r" "(b,c) ∈ r" unfolding osum_def by auto
    with TRANS have "(a,c) ∈ r" unfolding trans_def by blast
    with Inl_Inl_Inl show ?thesis unfolding osum_def by auto
  next
    case (Inl_Inl_Inr a b c)
    with * have "a ∈ Field r" "c ∈ Field r'" unfolding osum_def Field_def by auto
    with Inl_Inl_Inr show ?thesis unfolding osum_def by auto
  next
    case (Inl_Inr_Inr a b c)
    with * have "a ∈ Field r" "c ∈ Field r'" unfolding osum_def Field_def by auto
    with Inl_Inr_Inr show ?thesis unfolding osum_def by auto
  next
    case (Inr_Inr_Inr a b c)
    with * have "(a,b) ∈ r'" "(b,c) ∈ r'" unfolding osum_def by auto
    with TRANS' have "(a,c) ∈ r'" unfolding trans_def by blast
    with Inr_Inr_Inr show ?thesis unfolding osum_def by auto
  qed (auto simp: osum_def)
qed

lemma osum_Preorder: "[Preorder r; Preorder r'] ==> Preorder (r +o r')"
  unfolding preorder_on_def using osum_Refl osum_trans
  by (metis inf.cobounded2[of "r +o r'" "Field (r +o r') × Field (r +o r')"]
      Restr_Field[of "r +o r'"])

lemma osum_antisym: "[antisym r; antisym r'] ==> antisym (r +o r')"
  unfolding antisym_def osum_def by auto

lemma osum_Partial_order: "[Partial_order r; Partial_order r'] ==> Partial_order (r +o r')"
  unfolding partial_order_on_def using osum_Preorder osum_antisym by blast

lemma osum_Total: "[Total r; Total r'] ==> Total (r +o r')"
  unfolding total_on_def Field_osum unfolding osum_def by blast

lemma osum_Linear_order: "[Linear_order r; Linear_order r'] ==> Linear_order (r +o r')"
  unfolding linear_order_on_def using osum_Partial_order osum_Total by blast

lemma osum_wf:
  assumes WF: "wf r" and WF': "wf r'"
  shows "wf (r +o r')"
  unfolding wf_eq_minimal2 unfolding Field_osum
proof(intro allI impI, elim conjE)
  fix A assume *: "A ⊆ Inl ` Field r ∪ Inr ` Field r'" and **: "A ≠ {}"
  obtain B where B_def: "B = A Int Inl ` Field r" by blast
  show "∃a∈A. ∀a'∈A. (a', a) ∉ r +o r'"
  proof(cases "B = {}")
    case False
    hence "B ≠ {}" "B ≤ Inl ` Field r" using B_def by auto
    hence "Inl -` B ≠ {}" "Inl -` B ≤ Field r" unfolding vimage_def by auto
    then obtain a where 1: "a ∈ Inl -` B" and "∀a1 ∈ Inl -` B. (a1, a) ∉ r"
      using WF unfolding wf_eq_minimal2 by metis
    hence "∀a1 ∈ A. (a1, Inl a) ∉ r +o r'"
      unfolding osum_def using B_def ** by (auto simp: vimage_def Field_def)
    thus ?thesis using 1 unfolding B_def by auto
  next
    case True
    hence 1: "A ≤ Inr ` Field r'" using * B_def by auto
    with ** have "Inr -`A ≠ {}" "Inr -` A ≤ Field r'" unfolding vimage_def by auto
    with ** obtain a' where 2: "a' ∈ Inr -` A" and "∀a1' ∈ Inr -` A. (a1',a') ∉ r'"
      using WF' unfolding wf_eq_minimal2 by metis
    hence "∀a1' ∈ A. (a1', Inr a') ∉ r +o r'"
      unfolding osum_def using ** 1 by (auto simp: vimage_def Field_def)
    thus ?thesis using 2 by blast
  qed
qed

lemma osum_minus_Id:
  assumes r: "Total r" "¬ (r ≤ Id)" and r': "Total r'" "¬ (r' ≤ Id)"
  shows "(r +o r') - Id ≤ (r - Id) +o (r' - Id)"
  unfolding osum_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto

lemma osum_minus_Id1:
  "r ≤ Id ==> (r +o r') - Id ≤ (Inl ` Field r × Inr ` Field r') ∪ (map_prod Inr Inr ` (r' - Id))"
  unfolding osum_def by auto

lemma osum_minus_Id2:
  "r' ≤ Id ==> (r +o r') - Id ≤ (map_prod Inl Inl ` (r - Id)) ∪ (Inl ` Field r × Inr ` Field r')"
  unfolding osum_def by auto

lemma osum_wf_Id:
  assumes TOT: "Total r" and TOT': "Total r'" and WF: "wf(r - Id)" and WF': "wf(r' - Id)"
  shows "wf ((r +o r') - Id)"
proof(cases "r ≤ Id ∨ r' ≤ Id")
  case False
  thus ?thesis
    using osum_minus_Id[of r r'] assms osum_wf[of "r - Id" "r' - Id"]
      wf_subset[of "(r - Id) +o (r' - Id)" "(r +o r') - Id"] by auto
next
  have 1: "wf (Inl ` Field r × Inr ` Field r')" by (rule wf_Int_Times) auto
  case True
  thus ?thesis
  proof (elim disjE)
    assume "r ⊆ Id"
    thus "wf ((r +o r') - Id)"
      by (rule wf_subset[rotated, OF osum_minus_Id1 wf_Un[OF 1 wf_map_prod_image[OF WF']]]) auto
  next
    assume "r' ⊆ Id"
    thus "wf ((r +o r') - Id)"
      by (rule wf_subset[rotated, OF osum_minus_Id2 wf_Un[OF wf_map_prod_image[OF WF] 1]]) auto
  qed
qed

lemma osum_Well_order:
  assumes WELL: "Well_order r" and WELL': "Well_order r'"
  shows "Well_order (r +o r')"
  by (meson WELL WELL' osum_Linear_order osum_wf_Id well_order_on_def wo_rel.TOTAL wo_rel.intro)

lemma osum_embedL:
  assumes WELL: "Well_order r" and WELL': "Well_order r'"
  shows "embed r (r +o r') Inl"
proof -
  have 1: "Well_order (r +o r')" using assms by (auto simp add: osum_Well_order)
  moreover
  have "compat r (r +o r') Inl" unfolding compat_def osum_def by auto
  moreover
  have "ofilter (r +o r') (Inl ` Field r)"
    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum under_def
    unfolding osum_def Field_def by auto
  ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
qed

corollary osum_ordLeqL:
  assumes WELL: "Well_order r" and WELL': "Well_order r'"
  shows "r ≤o r +o r'"
  using assms osum_embedL osum_Well_order unfolding ordLeq_def by blast

lemma dir_image_alt: "dir_image r f = map_prod f f ` r"
  unfolding dir_image_def map_prod_def by auto

lemma map_prod_ordIso: "[Well_order r; inj_on f (Field r)] ==> map_prod f f ` r =o r"
  by (metis dir_image_alt dir_image_ordIso ordIso_symmetric)

definition oprod :: "'a rel ==> 'b rel ==> ('a × 'b) rel"  (infixr ‹*o› 80)
  where "r *o r' = {((x1, y1), (x2, y2)).
  (((y1, y2) ∈ r' - Id ∧ x1 ∈ Field r ∧ x2 ∈ Field r) ∨
   ((y1, y2) ∈ Restr Id (Field r') ∧ (x1, x2) ∈ r))}"

lemma Field_oprod: "Field (r *o r') = Field r × Field r'"
  unfolding oprod_def Field_def by auto blast+

lemma oprod_Refl:"[Refl r; Refl r'] ==> Refl (r *o r')"
  unfolding refl_on_def Field_oprod unfolding oprod_def by auto

lemma oprod_trans:
  assumes "trans r" "trans r'" "antisym r" "antisym r'"
  shows "trans (r *o r')"
  using assms by (clarsimp simp: trans_def antisym_def oprod_def) (metis FieldI1 FieldI2)

lemma oprod_Preorder: "[Preorder r; Preorder r'; antisym r; antisym r'] ==> Preorder (r *o r')"
  unfolding preorder_on_def using oprod_Refl oprod_trans
  by (metis Restr_Field[of "r *o r'"]
      inf.cobounded2[of "r *o r'" "Field (r *o r') × Field (r *o r')"])

lemma oprod_antisym: "[antisym r; antisym r'] ==> antisym (r *o r')"
  unfolding antisym_def oprod_def by auto

lemma oprod_Partial_order: "[Partial_order r; Partial_order r'] ==> Partial_order (r *o r')"
  unfolding partial_order_on_def using oprod_Preorder oprod_antisym by blast

lemma oprod_Total: "[Total r; Total r'] ==> Total (r *o r')"
  unfolding total_on_def Field_oprod unfolding oprod_def by auto

lemma oprod_Linear_order: "[Linear_order r; Linear_order r'] ==> Linear_order (r *o r')"
  unfolding linear_order_on_def using oprod_Partial_order oprod_Total by blast

lemma oprod_wf:
  assumes WF: "wf r" and WF': "wf r'"
  shows "wf (r *o r')"
  unfolding wf_eq_minimal2 unfolding Field_oprod
proof(intro allI impI, elim conjE)
  fix A assume *: "A ⊆ Field r × Field r'" and **: "A ≠ {}"
  then obtain y where y: "y ∈ snd ` A" "∀y'∈snd ` A. (y', y) ∉ r'"
    using spec[OF WF'[unfolded wf_eq_minimal2], of "snd ` A"] by auto
  let ?A = "fst ` A ∩ {x. (x, y) ∈ A}"
  from * y have "?A ≠ {}" "?A ⊆ Field r" by auto
  then obtain x where x: "x ∈ ?A" and "∀x'∈ ?A. (x', x) ∉ r"
    using spec[OF WF[unfolded wf_eq_minimal2], of "?A"] by auto
  with y have "∀a'∈A. (a', (x, y)) ∉ r *o r'"
    unfolding oprod_def mem_Collect_eq split_beta fst_conv snd_conv Id_def by auto
  moreover from x have "(x, y) ∈ A" by auto
  ultimately show "∃a∈A. ∀a'∈A. (a', a) ∉ r *o r'" by blast
qed

lemma oprod_minus_Id:
  assumes r: "Total r" "¬ (r ≤ Id)" and r': "Total r'" "¬ (r' ≤ Id)"
  shows "(r *o r') - Id ≤ (r - Id) *o (r' - Id)"
  unfolding oprod_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto

lemma oprod_minus_Id1:
  "r ≤ Id ==> r *o r' - Id ≤ {((x,y1), (x,y2)). x ∈ Field r ∧ (y1, y2) ∈ (r' - Id)}"
  unfolding oprod_def by auto

lemma wf_extend_oprod1:
  assumes "wf r"
  shows "wf {((x,y1), (x,y2)) . x ∈ A ∧ (y1, y2) ∈ r}"
proof (unfold wf_eq_minimal2, intro allI impI, elim conjE)
  fix B
  assume *: "B ⊆ Field {((x,y1), (x,y2)) . x ∈ A ∧ (y1, y2) ∈ r}" and "B ≠ {}"
  from image_mono[OF *, of snd] have "snd ` B ⊆ Field r" unfolding Field_def by force
  with ‹B ≠ {}› obtain x where x: "x ∈ snd ` B" "∀x'∈snd ` B. (x', x) ∉ r"
    using spec[OF assms[unfolded wf_eq_minimal2], of "snd ` B"] by auto
  then obtain a where "(a, x) ∈ B" by auto
  moreover
  from * x have "∀a'∈B. (a', (a, x)) ∉ {((x,y1), (x,y2)) . x ∈ A ∧ (y1, y2) ∈ r}" by auto
  ultimately show "∃ax∈B. ∀a'∈B. (a', ax) ∉ {((x,y1), (x,y2)) . x ∈ A ∧ (y1, y2) ∈ r}" by blast
qed

lemma oprod_minus_Id2:
  "r' ≤ Id ==> r *o r' - Id ≤ {((x1,y), (x2,y)). (x1, x2) ∈ (r - Id) ∧ y ∈ Field r'}"
  unfolding oprod_def by auto

lemma wf_extend_oprod2:
  assumes "wf r"
  shows "wf {((x1,y), (x2,y)) . (x1, x2) ∈ r ∧ y ∈ A}"
proof (unfold wf_eq_minimal2, intro allI impI, elim conjE)
  fix B
  assume *: "B ⊆ Field {((x1, y), (x2, y)). (x1, x2) ∈ r ∧ y ∈ A}" and "B ≠ {}"
  from image_mono[OF *, of fst] have "fst ` B ⊆ Field r" unfolding Field_def by force
  with ‹B ≠ {}› obtain x where x: "x ∈ fst ` B" "∀x'∈fst ` B. (x', x) ∉ r"
    using spec[OF assms[unfolded wf_eq_minimal2], of "fst ` B"] by auto
  then obtain a where "(x, a) ∈ B" by auto
  moreover
  from * x have "∀a'∈B. (a', (x, a)) ∉ {((x1, y), x2, y). (x1, x2) ∈ r ∧ y ∈ A}" by auto
  ultimately show "∃xa∈B. ∀a'∈B. (a', xa) ∉ {((x1, y), x2, y). (x1, x2) ∈ r ∧ y ∈ A}" by blast
qed

lemma oprod_wf_Id:
  assumes TOT: "Total r" and TOT': "Total r'" and WF: "wf(r - Id)" and WF': "wf(r' - Id)"
  shows "wf ((r *o r') - Id)"
proof(cases "r ≤ Id ∨ r' ≤ Id")
  case False
  thus ?thesis
    by (meson TOT TOT' WF WF' oprod_minus_Id oprod_wf wf_subset)
next
  case True
  thus ?thesis using wf_subset[OF wf_extend_oprod1[OF WF'] oprod_minus_Id1]
      wf_subset[OF wf_extend_oprod2[OF WF] oprod_minus_Id2] by auto
qed

lemma oprod_Well_order:
  assumes WELL: "Well_order r" and WELL': "Well_order r'"
  shows "Well_order (r *o r')"
  by (meson WELL WELL' linear_order_on_def oprod_Linear_order oprod_wf_Id well_order_on_def)

lemma oprod_embed:
  assumes WELL: "Well_order r" and WELL': "Well_order r'" and "r' ≠ {}"
  shows "embed r (r *o r') (λx. (x, minim r' (Field r')))" (is "embed _ _ ?f")
proof -
  from assms(3) have r': "Field r' ≠ {}" unfolding Field_def by auto
  have minim[simp]: "minim r' (Field r') ∈ Field r'"
    using wo_rel.minim_inField[unfolded wo_rel_def, OF WELL' _ r'] by auto
  { fix b
    assume b: "(b, minim r' (Field r')) ∈ r'"
    hence "b ∈ Field r'" unfolding Field_def by auto
    hence "(minim r' (Field r'), b) ∈ r'"
      using wo_rel.minim_least[unfolded wo_rel_def, OF WELL' subset_refl] r' by auto
    with b have "b = minim r' (Field r')"
      by (metis WELL' antisym_def linear_order_on_def partial_order_on_def well_order_on_def)
  } note * = this
  have 1: "Well_order (r *o r')" using assms by (auto simp add: oprod_Well_order)
  moreover
  from r' have "compat r (r *o r') ?f"  unfolding compat_def oprod_def by auto
  moreover
  from * have "ofilter (r *o r') (?f ` Field r)"
    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod under_def
    unfolding oprod_def by auto (auto simp: image_iff Field_def)
  moreover have "inj_on ?f (Field r)" unfolding inj_on_def by auto
  ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
qed

corollary oprod_ordLeq: "[Well_order r; Well_order r'; r' ≠ {}] ==> r ≤o r *o r'"
  using oprod_embed oprod_Well_order unfolding ordLeq_def by blast

definition "support z A f = {x ∈ A. f x ≠ z}"

lemma support_Un[simp]: "support z (A ∪ B) f = support z A f ∪ support z B f"
  unfolding support_def by auto

lemma support_upd[simp]: "support z A (f(x := z)) = support z A f - {x}"
  unfolding support_def by auto

lemma support_upd_subset[simp]: "support z A (f(x := y)) ⊆ support z A f ∪ {x}"
  unfolding support_def by auto

lemma fun_unequal_in_support:
  assumes "f ≠ g" "f ∈ Func A B" "g ∈ Func A C"
  shows "(support z A f ∪ support z A g) ∩ {a. f a ≠ g a} ≠ {}" 
  using assms by (simp add: Func_def support_def disjoint_iff fun_eq_iff) metis

definition fin_support where
  "fin_support z A = {f. finite (support z A f)}"

lemma finite_support: "f ∈ fin_support z A ==> finite (support z A f)"
  unfolding support_def fin_support_def by auto

lemma fin_support_Field_osum:
  "f ∈ fin_support z (Inl ` A ∪ Inr ` B) ⟷
  (f o Inl) ∈ fin_support z A ∧ (f o Inr) ∈ fin_support z B" (is "?L ⟷ ?R1 ∧ ?R2")
proof safe
  assume ?L
  from ‹?L› show ?R1 unfolding fin_support_def support_def
    by (fastforce simp: image_iff elim: finite_surj[of _ _ "case_sum id undefined"])
  from ‹?L› show ?R2 unfolding fin_support_def support_def
    by (fastforce simp: image_iff elim: finite_surj[of _ _ "case_sum undefined id"])
next
  assume ?R1 ?R2
  thus ?L unfolding fin_support_def support_Un
    by (auto simp: support_def elim: finite_surj[of _ _ Inl] finite_surj[of _ _ Inr])
qed

lemma Func_upd: "[f ∈ Func A B; x ∈ A; y ∈ B] ==> f(x := y) ∈ Func A B"
  unfolding Func_def by auto

context wo_rel
begin

definition isMaxim :: "'a set ==> 'a ==> bool"
  where "isMaxim A b ≡ b ∈ A ∧ (∀a ∈ A. (a,b) ∈ r)"

definition maxim :: "'a set ==> 'a"
  where "maxim A ≡ THE b. isMaxim A b"

lemma isMaxim_unique[intro]: "[isMaxim A x; isMaxim A y] ==> x = y"
  unfolding isMaxim_def using antisymD[OF ANTISYM, of x y] by auto

lemma maxim_isMaxim: "[finite A; A ≠ {}; A ⊆ Field r] ==> isMaxim A (maxim A)"
  unfolding maxim_def
proof (rule theI', rule ex_ex1I[OF _ isMaxim_unique, rotated], assumption+,
    induct A rule: finite_induct)
  case (insert x A)
  thus ?case
  proof (cases "A = {}")
    case True
    moreover have "isMaxim {x} x" unfolding isMaxim_def using refl_onD[OF REFL] insert(5) by auto
    ultimately show ?thesis by blast
  next
    case False
    with insert(3,5) obtain y where "isMaxim A y" by blast
    with insert(2,5) have "if (y, x) ∈ r then isMaxim (insert x A) x else isMaxim (insert x A) y"
      unfolding isMaxim_def subset_eq by (metis insert_iff max2_def max2_equals1 max2_iff)
    thus ?thesis by metis
  qed
qed simp

lemma maxim_in: "[finite A; A ≠ {}; A ⊆ Field r] ==> maxim A ∈ A"
  using maxim_isMaxim unfolding isMaxim_def by auto

lemma maxim_greatest: "[finite A; x ∈ A; A ⊆ Field r] ==> (x, maxim A) ∈ r"
  using maxim_isMaxim unfolding isMaxim_def by auto

lemma isMaxim_zero: "isMaxim A zero ==> A = {zero}"
  unfolding isMaxim_def by auto

lemma maxim_insert:
  assumes "finite A" "A ≠ {}" "A ⊆ Field r" "x ∈ Field r"
  shows "maxim (insert x A) = max2 x (maxim A)"
proof -
  from assms have *: "isMaxim (insert x A) (maxim (insert x A))" "isMaxim A (maxim A)"
    using maxim_isMaxim by auto
  show ?thesis
  proof (cases "(x, maxim A) ∈ r")
    case True
    with *(2) have "isMaxim (insert x A) (maxim A)"
      by (simp add: isMaxim_def)
    with *(1) True show ?thesis 
      unfolding max2_def by (metis isMaxim_unique)
  next
    case False
    hence "(maxim A, x) ∈ r" by (metis *(2) assms(3,4) in_mono in_notinI isMaxim_def)
    with *(2) assms(4) have "isMaxim (insert x A) x" unfolding isMaxim_def
      using transD[OF TRANS, of _ "maxim A" x] refl_onD[OF REFL, of x] by blast
    with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique)
  qed
qed

lemma maxim_Un:
  assumes "finite A" "A ≠ {}" "A ⊆ Field r" "finite B" "B ≠ {}" "B ⊆ Field r"
  shows   "maxim (A ∪ B) = max2 (maxim A) (maxim B)"
proof -
  from assms have *: "isMaxim (A ∪ B) (maxim (A ∪ B))" "isMaxim A (maxim A)" "isMaxim B (maxim B)"
    using maxim_isMaxim by auto
  show ?thesis
  proof (cases "(maxim A, maxim B) ∈ r")
    case True
    with *(2,3) have "isMaxim (A ∪ B) (maxim B)" unfolding isMaxim_def
      using transD[OF TRANS, of _ "maxim A" "maxim B"] by blast
    with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique)
  next
    case False
    hence "(maxim B, maxim A) ∈ r" by (metis *(2,3) assms(3,6) in_mono in_notinI isMaxim_def)
    with *(2,3) have "isMaxim (A ∪ B) (maxim A)"
      by (metis "*"(1) False Un_iff isMaxim_def isMaxim_unique)
    with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique)
  qed
qed

lemma maxim_insert_zero:
  assumes "finite A" "A ≠ {}" "A ⊆ Field r"
  shows "maxim (insert zero A) = maxim A"
  using assms finite.cases in_mono max2_def maxim_in maxim_insert subset_empty zero_in_Field zero_smallest by fastforce

lemma maxim_equality: "isMaxim A x ==> maxim A = x"
  unfolding maxim_def by (rule the_equality) auto

lemma maxim_singleton:
  "x ∈ Field r ==> maxim {x} = x"
  using refl_onD[OF REFL] by (intro maxim_equality) (simp add: isMaxim_def)

lemma maxim_Int: "[finite A; A ≠ {}; A ⊆ Field r; maxim A ∈ B] ==> maxim (A ∩ B) = maxim A"
  by (rule maxim_equality) (auto simp: isMaxim_def intro: maxim_in maxim_greatest)

lemma maxim_mono: "[X ⊆ Y; finite Y; X ≠ {}; Y ⊆ Field r] ==> (maxim X, maxim Y) ∈ r"
  using maxim_in[OF finite_subset, of X Y] by (auto intro: maxim_greatest)

definition "max_fun_diff f g ≡ maxim ({a ∈ Field r. f a ≠ g a})"

lemma max_fun_diff_commute: "max_fun_diff f g = max_fun_diff g f"
  unfolding max_fun_diff_def by metis

lemma zero_under: "x ∈ Field r ==> zero ∈ under x"
  unfolding under_def by (auto intro: zero_smallest)

end

definition "FinFunc r s = Func (Field s) (Field r) ∩ fin_support (zero r) (Field s)"

lemma FinFuncD: "[f ∈ FinFunc r s; x ∈ Field s] ==> f x ∈ Field r"
  unfolding FinFunc_def Func_def by (fastforce split: option.splits)

locale wo_rel2 =
  fixes r s
  assumes rWELL: "Well_order r"
    and     sWELL: "Well_order s"
begin

interpretation r: wo_rel r by unfold_locales (rule rWELL)
interpretation s: wo_rel s by unfold_locales (rule sWELL)

abbreviation "SUPP ≡ support r.zero (Field s)"
abbreviation "FINFUNC ≡ FinFunc r s"
lemmas FINFUNCD = FinFuncD[of _ r s]

lemma fun_diff_alt: "{a ∈ Field s. f a ≠ g a} = (SUPP f ∪ SUPP g) ∩ {a. f a ≠ g a}"
  by (auto simp: support_def)

lemma max_fun_diff_alt:
  "s.max_fun_diff f g = s.maxim ((SUPP f ∪ SUPP g) ∩ {a. f a ≠ g a})"
  unfolding s.max_fun_diff_def fun_diff_alt ..

lemma isMaxim_max_fun_diff: "[f ≠ g; f ∈ FINFUNC; g ∈ FINFUNC] ==>
  s.isMaxim {a ∈ Field s. f a ≠ g a} (s.max_fun_diff f g)"
  using fun_unequal_in_support[of f g] unfolding max_fun_diff_alt fun_diff_alt fun_eq_iff
  by (intro s.maxim_isMaxim) (auto simp: FinFunc_def fin_support_def support_def)

lemma max_fun_diff_in: "[f ≠ g; f ∈ FINFUNC; g ∈ FINFUNC] ==>
  s.max_fun_diff f g ∈ {a ∈ Field s. f a ≠ g a}"
  using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast

lemma max_fun_diff_max: "[f ≠ g; f ∈ FINFUNC; g ∈ FINFUNC; x ∈ {a ∈ Field s. f a ≠ g a}] ==>
  (x, s.max_fun_diff f g) ∈ s"
  using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast

lemma max_fun_diff:
  "[f ≠ g; f ∈ FINFUNC; g ∈ FINFUNC] ==>
  (∃a b. a ≠ b ∧ a ∈ Field r ∧ b ∈ Field r ∧
     f (s.max_fun_diff f g) = a ∧ g (s.max_fun_diff f g) = b)"
  using isMaxim_max_fun_diff[of f g] unfolding s.isMaxim_def FinFunc_def Func_def by auto

lemma max_fun_diff_le_eq:
  "[(s.max_fun_diff f g, x) ∈ s; f ≠ g; f ∈ FINFUNC; g ∈ FINFUNC; x ≠ s.max_fun_diff f g] ==>
  f x = g x"
  using max_fun_diff_max[of f g x] antisymD[OF s.ANTISYM, of "s.max_fun_diff f g" x]
  by (auto simp: Field_def)

lemma max_fun_diff_max2:
  assumes ineq: "s.max_fun_diff f g = s.max_fun_diff g h ⟶
    f (s.max_fun_diff f g) ≠ h (s.max_fun_diff g h)" and
    fg: "f ≠ g" and gh: "g ≠ h" and fh: "f ≠ h" and
    f: "f ∈ FINFUNC" and g: "g ∈ FINFUNC" and h: "h ∈ FINFUNC"
  shows "s.max_fun_diff f h = s.max2 (s.max_fun_diff f g) (s.max_fun_diff g h)"
    (is "?fh = s.max2 ?fg ?gh")
proof (cases "?fg = ?gh")
  case True
  with ineq have "f ?fg ≠ h ?fg" by simp
  moreover
  { fix x assume x: "x ∈ {a ∈ Field s. f a ≠ h a}"
    hence "(x, ?fg) ∈ s"
    proof (cases "x = ?fg")
      case False show ?thesis
        by (metis (mono_tags, lifting) True assms(5-7) max_fun_diff_max mem_Collect_eq x)
    qed (simp add: refl_onD[OF s.REFL])
  }
  ultimately have "s.isMaxim {a ∈ Field s. f a ≠ h a} ?fg"
    unfolding s.isMaxim_def using max_fun_diff_in[OF fg f g] by simp
  hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast
  thus ?thesis unfolding True s.max2_def by simp
next
  case False note * = this
  show ?thesis
  proof (cases "(?fg, ?gh) ∈ s")
    case True
    hence *: "f ?gh = g ?gh" by (rule max_fun_diff_le_eq[OF _ fg f g *[symmetric]])
    hence "s.isMaxim {a ∈ Field s. f a ≠ h a} ?gh" using isMaxim_max_fun_diff[OF gh g h]
        isMaxim_max_fun_diff[OF fg f g] transD[OF s.TRANS _ True]
      unfolding s.isMaxim_def by auto
    hence "?fh = ?gh" using isMaxim_max_fun_diff[OF fh f h] by blast
    thus ?thesis using True unfolding s.max2_def by simp
  next
    case False
    with max_fun_diff_in[OF fg f g] max_fun_diff_in[OF gh g h] have True: "(?gh, ?fg) ∈ s"
      by (blast intro: s.in_notinI)
    hence *: "g ?fg = h ?fg" by (rule max_fun_diff_le_eq[OF _ gh g h *])
    hence "s.isMaxim {a ∈ Field s. f a ≠ h a} ?fg" using isMaxim_max_fun_diff[OF gh g h]
        isMaxim_max_fun_diff[OF fg f g] True transD[OF s.TRANS, of _ _ ?fg]
      unfolding s.isMaxim_def by auto
    hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast
    thus ?thesis using False unfolding s.max2_def by simp
  qed
qed

definition oexp where
  "oexp = {(f, g) . f ∈ FINFUNC ∧ g ∈ FINFUNC ∧
    ((let m = s.max_fun_diff f g in (f m, g m) ∈ r) ∨ f = g)}"

lemma Field_oexp: "Field oexp = FINFUNC"
  unfolding oexp_def FinFunc_def by (auto simp: Let_def Field_def)

lemma oexp_Refl: "Refl oexp"
  unfolding refl_on_def Field_oexp unfolding oexp_def by (auto simp: Let_def)

lemma oexp_trans: "trans oexp"
proof (unfold trans_def, safe)
  fix f g h :: "'b ==> 'a"
  let ?fg = "s.max_fun_diff f g"
    and ?gh = "s.max_fun_diff g h"
    and ?fh = "s.max_fun_diff f h"
  assume oexp: "(f, g) ∈ oexp" "(g, h) ∈ oexp"
  thus "(f, h) ∈ oexp"
  proof (cases "f = g ∨ g = h")
    case False
    with oexp have "f ∈ FINFUNC" "g ∈ FINFUNC" "h ∈ FINFUNC"
      "(f ?fg, g ?fg) ∈ r" "(g ?gh, h ?gh) ∈ r" unfolding oexp_def Let_def by auto
    note * = this False
    show ?thesis
    proof (cases "f ≠ h")
      case True
      show ?thesis
      proof (cases "?fg = ?gh ⟶ f ?fg ≠ h ?gh")
        case True
        show ?thesis using max_fun_diff_max2[of f g h, OF True] * ‹f ≠ h› max_fun_diff_in
            r.max2_iff[OF FINFUNCD FINFUNCD] r.max2_equals1[OF FINFUNCD FINFUNCD] max_fun_diff_le_eq
            s.in_notinI[OF disjI1] unfolding oexp_def Let_def s.max2_def mem_Collect_eq by safe metis
      next
        case False with * show ?thesis unfolding oexp_def Let_def
          using antisymD[OF r.ANTISYM, of "g ?gh" "h ?gh"] max_fun_diff_in[of g h] by auto
      qed
    qed (auto simp: oexp_def *(3))
  qed auto
qed

lemma oexp_Preorder: "Preorder oexp"
  unfolding preorder_on_def using oexp_Refl oexp_trans Restr_Field[of oexp] by blast

lemma oexp_antisym: "antisym oexp"
proof (unfold antisym_def, safe, rule ccontr)
  fix f g assume "(f, g) ∈ oexp" "(g, f) ∈ oexp" "g ≠ f"
  thus False using refl_onD[OF r.REFL FINFUNCD] max_fun_diff_in unfolding oexp_def Let_def
    by (auto dest!: antisymD[OF r.ANTISYM] simp: s.max_fun_diff_commute)
qed

lemma oexp_Partial_order: "Partial_order oexp"
  unfolding partial_order_on_def using oexp_Preorder oexp_antisym by blast

lemma oexp_Total: "Total oexp"
  unfolding total_on_def Field_oexp unfolding oexp_def using FINFUNCD max_fun_diff_in
  by (auto simp: Let_def s.max_fun_diff_commute intro!: r.in_notinI)

lemma oexp_Linear_order: "Linear_order oexp"
  unfolding linear_order_on_def using oexp_Partial_order oexp_Total by blast

definition "const = (λx. if x ∈ Field s then r.zero else undefined)"

lemma const_in[simp]: "x ∈ Field s ==> const x = r.zero"
  unfolding const_def by auto

lemma const_notin[simp]: "x ∉ Field s ==> const x = undefined"
  unfolding const_def by auto

lemma const_Int_Field[simp]: "Field s ∩ - {x. const x = r.zero} = {}"
  by auto

lemma const_FINFUNC[simp]: "Field r ≠ {} ==> const ∈ FINFUNC"
  unfolding FinFunc_def Func_def fin_support_def support_def const_def Int_iff mem_Collect_eq
  using r.zero_in_Field by (metis (lifting) Collect_empty_eq finite.emptyI)

lemma const_least:
  assumes "Field r ≠ {}" "f ∈ FINFUNC"
  shows "(const, f) ∈ oexp"
  using assms const_FINFUNC max_fun_diff max_fun_diff_in oexp_def by fastforce

lemma support_not_const:
  assumes "F ⊆ FINFUNC" and "const ∉ F"
  shows "∀f ∈ F. finite (SUPP f) ∧ SUPP f ≠ {} ∧ SUPP f ⊆ Field s"
proof (intro ballI conjI)
  fix f assume "f ∈ F"
  thus "finite (SUPP f)" "SUPP f ⊆ Field s"
    using assms(1) unfolding FinFunc_def fin_support_def support_def by auto
  show "SUPP f ≠ {}"
  proof (rule ccontr, unfold not_not)
    assume "SUPP f = {}"
    moreover from ‹f ∈ F› assms(1) have "f ∈ FINFUNC" by blast
    ultimately have "f = const"
      by (auto simp: fun_eq_iff support_def FinFunc_def Func_def const_def)
    with assms(2) ‹f ∈ F› show False by blast
  qed
qed

lemma maxim_isMaxim_support:
  assumes "F ⊆ FINFUNC" and "const ∉ F"
  shows "∀f ∈ F. s.isMaxim (SUPP f) (s.maxim (SUPP f))"
  using assms s.maxim_isMaxim support_not_const by force

lemma oexp_empty2: "Field s = {} ==> oexp = {(λx. undefined, λx. undefined)}"
  unfolding oexp_def FinFunc_def fin_support_def support_def by auto

lemma oexp_empty: "[Field r = {}; Field s ≠ {}] ==> oexp = {}"
  using FINFUNCD oexp_def by auto

lemma fun_upd_FINFUNC: "[f ∈ FINFUNC; x ∈ Field s; y ∈ Field r] ==> f(x := y) ∈ FINFUNC"
  unfolding FinFunc_def Func_def fin_support_def
  by (auto intro: finite_subset[OF support_upd_subset])

lemma fun_upd_same_oexp:
  assumes "(f, g) ∈ oexp" "f x = g x" "x ∈ Field s" "y ∈ Field r"
  shows   "(f(x := y), g(x := y)) ∈ oexp"
proof -
  from assms(1) fun_upd_FINFUNC[OF _ assms(3,4)] have fg: "f(x := y) ∈ FINFUNC" "g(x := y) ∈ FINFUNC"
    unfolding oexp_def by auto
  moreover from assms(2) have "s.max_fun_diff (f(x := y)) (g(x := y)) = s.max_fun_diff f g"
    unfolding s.max_fun_diff_def by auto metis
  ultimately show ?thesis using assms refl_onD[OF r.REFL] unfolding oexp_def Let_def by auto
qed

lemma fun_upd_smaller_oexp:
  assumes "f ∈ FINFUNC" "x ∈ Field s" "y ∈ Field r"  "(y, f x) ∈ r"
  shows   "(f(x := y), f) ∈ oexp"
  using assms fun_upd_FINFUNC[OF assms(1-3)] s.maxim_singleton[of "x"]
  unfolding oexp_def FinFunc_def Let_def fin_support_def s.max_fun_diff_def by (auto simp: fun_eq_iff)

lemma oexp_wf_Id: "wf (oexp - Id)"
proof (cases "Field r = {} ∨ Field s = {}")
  case True thus ?thesis using oexp_empty oexp_empty2 by fastforce
next
  case False
  hence Fields: "Field s ≠ {}" "Field r ≠ {}" by simp_all
  hence [simp]: "r.zero ∈ Field r" by (intro r.zero_in_Field)
  have const[simp]: "∧F. [const ∈ F; F ⊆ FINFUNC] ==> ∃f0∈F. ∀f∈F. (f0, f) ∈ oexp"
    using const_least[OF Fields(2)] by auto
  show ?thesis
    unfolding Linear_order_wf_diff_Id[OF oexp_Linear_order] Field_oexp
  proof (intro allI impI)
    fix A assume A: "A ⊆ FINFUNC" "A ≠ {}"
    { fix y F
      have "F ⊆ FINFUNC ∧ (∃f ∈ F. y = s.maxim (SUPP f)) ⟶
        (∃f0 ∈ F. ∀f ∈ F. (f0, f) ∈ oexp)" (is "?P F y")
      proof (induct y arbitrary: F rule: s.well_order_induct)
        case (1 y)
        show ?case
        proof (intro impI, elim conjE bexE)
          fix f assume F: "F ⊆ FINFUNC" "f ∈ F" "y = s.maxim (SUPP f)"
          thus "∃f0∈F. ∀f∈F. (f0, f) ∈ oexp"
          proof (cases "const ∈ F")
            case False
            with F have maxF: "∀f ∈ F. s.isMaxim (SUPP f) (s.maxim (SUPP f))"
              and SUPPF: "∀f ∈ F. finite (SUPP f) ∧ SUPP f ≠ {} ∧ SUPP f ⊆ Field s"
              using maxim_isMaxim_support support_not_const by auto
            define z where "z = s.minim {s.maxim (SUPP f) | f. f ∈ F}"
            from F SUPPF maxF have zmin: "s.isMinim {s.maxim (SUPP f) | f. f ∈ F} z"
              unfolding z_def by (intro s.minim_isMinim) (auto simp: s.isMaxim_def)
            with F have zy: "(z, y) ∈ s" unfolding s.isMinim_def by auto
            hence zField: "z ∈ Field s" unfolding Field_def by auto
            define x0 where "x0 = r.minim {f z | f. f ∈ F ∧ z = s.maxim (SUPP f)}"
            from F(1,2) maxF(1) SUPPF zmin
            have x0min: "r.isMinim {f z | f. f ∈ F ∧ z = s.maxim (SUPP f)} x0"
              unfolding x0_def s.isMaxim_def s.isMinim_def
              by (blast intro!: r.minim_isMinim FinFuncD[of _ r s])
            with maxF(1) SUPPF F(1) have x0Field: "x0 ∈ Field r"
              unfolding r.isMinim_def s.isMaxim_def by (auto intro!: FINFUNCD)
            from x0min maxF(1) SUPPF F(1) have x0notzero: "x0 ≠ r.zero"
              unfolding r.isMinim_def s.isMaxim_def FinFunc_def Func_def support_def
              by fastforce
            define G where "G = {f(z := r.zero) | f. f ∈ F ∧ z = s.maxim (SUPP f) ∧ f z = x0}"
            from zmin x0min have "G ≠ {}" unfolding G_def z_def s.isMinim_def r.isMinim_def by blast
            have GF: "G ⊆ (λf. f(z := r.zero)) ` F" unfolding G_def by auto
            have "G ⊆ fin_support r.zero (Field s)"
              unfolding FinFunc_def fin_support_def
              using F(1) FinFunc_def G_def fin_support_def by fastforce
            moreover from F GF zField have "G ⊆ Func (Field s) (Field r)"
              using Func_upd[of _ "Field s" "Field r" z r.zero] unfolding FinFunc_def by auto
            ultimately have G: "G ⊆ FINFUNC" unfolding FinFunc_def by blast
            hence "∃g0∈G. ∀g∈G. (g0, g) ∈ oexp"
            proof (cases "const ∈ G")
              case False
              with G have maxG: "∀g ∈ G. s.isMaxim (SUPP g) (s.maxim (SUPP g))"
                and SUPPG: "∀g ∈ G. finite (SUPP g) ∧ SUPP g ≠ {} ∧ SUPP g ⊆ Field s"
                using maxim_isMaxim_support support_not_const by auto
              define y' where "y' = s.minim {s.maxim (SUPP f) | f. f ∈ G}"
              from G SUPPG maxG ‹G ≠ {}› have y'min: "s.isMinim {s.maxim (SUPP f) | f. f ∈ G} y'"
                unfolding y'_def by (intro s.minim_isMinim) (auto simp: s.isMaxim_def)
              moreover
              have "∀g ∈ G. z ∉ SUPP g" unfolding support_def G_def by auto
              moreover
              { fix g assume g: "g ∈ G"
                then obtain f where "f ∈ F" "g = f(z := r.zero)" and z: "z = s.maxim (SUPP f)"
                  unfolding G_def by auto
                with SUPPF bspec[OF SUPPG g] have "(s.maxim (SUPP g), z) ∈ s"
                  unfolding z by (intro s.maxim_mono) auto
              }
              moreover from y'min have "∧g. g ∈ G ==> (y', s.maxim (SUPP g)) ∈ s"
                unfolding s.isMinim_def by auto
              ultimately have "y' ≠ z" "(y', z) ∈ s" using maxG
                unfolding s.isMinim_def s.isMaxim_def by auto
              with zy have "y' ≠ y" "(y', y) ∈ s" using antisymD[OF s.ANTISYM] transD[OF s.TRANS]
                by blast+
              moreover from ‹G ≠ {}› have "∃g ∈ G. y' = wo_rel.maxim s (SUPP g)" using y'min
                by (auto simp: G_def s.isMinim_def)
              ultimately show ?thesis using mp[OF spec[OF mp[OF spec[OF 1]]], of y' G] G by auto
            qed simp
            then obtain g0 where g0: "g0 ∈ G" "∀g ∈ G. (g0, g) ∈ oexp" by blast
            hence g0z: "g0 z = r.zero" unfolding G_def by auto
            define f0 where "f0 = g0(z := x0)"
            with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 ∪ {z}" unfolding support_def by auto
            from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto
            have f0: "f0 ∈ F" using x0min g0(1)
                Func_elim[OF subsetD[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
              unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem)
            from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def
              by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
            show ?thesis
            proof (intro bexI[OF _ f0] ballI)
              fix f assume f: "f ∈ F"
              show "(f0, f) ∈ oexp"
              proof (cases "f0 = f")
                case True thus ?thesis by (metis F(1) Field_oexp f0 in_mono oexp_Refl refl_onD)
              next
                case False
                thus ?thesis
                proof (cases "s.maxim (SUPP f) = z ∧ f z = x0")
                  case True
                  with f have "f(z := r.zero) ∈ G" unfolding G_def by blast
                  with g0(2) f0z have "(f0(z := r.zero), f(z := r.zero)) ∈ oexp" by auto
                  hence oexp: "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) ∈ oexp"
                    by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp
                  with f F(1) x0min True
                  have "(f(z := x0), f) ∈ oexp" unfolding G_def r.isMinim_def
                    by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto
                  with oexp show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
                    unfolding f0_def by auto
                next
                  case False note notG = this
                  thus ?thesis
                  proof (cases "s.maxim (SUPP f) = z")
                    case True
                    with notG have "f0 z ≠ f z" unfolding f0_def by auto
                    hence "f0 z ≠ f z" by metis
                    with True maxf0 f0 f SUPPF have "s.max_fun_diff f0 f = z"
                      using s.maxim_Un[of "SUPP f0" "SUPP f", unfolded s.max2_def]
                      unfolding max_fun_diff_alt by (intro trans[OF s.maxim_Int]) auto
                    moreover
                    from x0min True f have "(x0, f z) ∈ r" unfolding r.isMinim_def by auto
                    ultimately show ?thesis using f f0 F(1) unfolding oexp_def f0_def by auto
                  next
                    case False
                    with notG have *: "(z, s.maxim (SUPP f)) ∈ s" "z ≠ s.maxim (SUPP f)"
                      using zmin f unfolding s.isMinim_def G_def by auto
                    have f0f: "f0 (s.maxim (SUPP f)) = r.zero"
                    proof (rule ccontr)
                      assume "f0 (s.maxim (SUPP f)) ≠ r.zero"
                      with f SUPPF maxF(1) have "s.maxim (SUPP f) ∈ SUPP f0"
                        unfolding support_def[of _ _ f0] s.isMaxim_def by auto
                      with SUPPF f0 have "(s.maxim (SUPP f), z) ∈ s" unfolding maxf0[symmetric]
                        by (auto intro: s.maxim_greatest)
                      with * antisymD[OF s.ANTISYM] show False by simp
                    qed
                    moreover
                    have "f (s.maxim (SUPP f)) ≠ r.zero"
                      using bspec[OF maxF(1) f, unfolded s.isMaxim_def] by (auto simp: support_def)
                    with f0f * f f0 maxf0 SUPPF
                    have "s.max_fun_diff f0 f = s.maxim (SUPP f0 ∪ SUPP f)"
                      unfolding max_fun_diff_alt using s.maxim_Un[of "SUPP f0" "SUPP f"]
                      by (intro s.maxim_Int) (auto simp: s.max2_def)
                    moreover have "s.maxim (SUPP f0 ∪ SUPP f) = s.maxim (SUPP f)"
                      using s.maxim_Un[of "SUPP f0" "SUPP f"] * maxf0 SUPPF f0 f
                      by (auto simp: s.max2_def)
                    ultimately show ?thesis using f f0 F(1) maxF(1) SUPPF unfolding oexp_def Let_def
                      by (fastforce simp: s.isMaxim_def intro!: r.zero_smallest FINFUNCD)
                  qed
                qed
              qed
            qed
          qed simp
        qed
      qed
    } 
    with A show "∃a∈A. ∀a'∈A. (a, a') ∈ oexp"
      by blast
  qed
qed

lemma oexp_Well_order: "Well_order oexp"
  unfolding well_order_on_def using oexp_Linear_order oexp_wf_Id by blast

interpretation o: wo_rel oexp by unfold_locales (rule oexp_Well_order)

lemma zero_oexp: "Field r ≠ {} ==> o.zero = const"
  by (metis Field_oexp const_FINFUNC const_least o.Field_ofilter o.equals_minim o.ofilter_def o.zero_def)

end

notation wo_rel2.oexp (infixl ‹^o› 90)
lemmas oexp_def = wo_rel2.oexp_def[unfolded wo_rel2_def, OF conjI]
lemmas oexp_Well_order = wo_rel2.oexp_Well_order[unfolded wo_rel2_def, OF conjI]
lemmas Field_oexp = wo_rel2.Field_oexp[unfolded wo_rel2_def, OF conjI]

definition "ozero = {}"

lemma ozero_Well_order[simp]: "Well_order ozero"
  unfolding ozero_def by simp

lemma ozero_ordIso[simp]: "ozero =o ozero"
  unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def by auto

lemma Field_ozero[simp]: "Field ozero = {}"
  unfolding ozero_def by simp

lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})"
  unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def
  by (auto dest: well_order_on_domain)

lemma ozero_ordLeq:
  assumes "Well_order r"  shows "ozero ≤o r"
  using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto

definition "oone = {((),())}"

lemma oone_Well_order[simp]: "Well_order oone"
  unfolding oone_def unfolding well_order_on_def linear_order_on_def partial_order_on_def
    preorder_on_def total_on_def refl_on_def trans_def antisym_def by auto

lemma Field_oone[simp]: "Field oone = {()}"
  unfolding oone_def by simp

lemma oone_ordIso: "oone =o {(x,x)}"
  unfolding ordIso_def oone_def well_order_on_def linear_order_on_def partial_order_on_def
    preorder_on_def total_on_def refl_on_def trans_def antisym_def
  by (auto simp: iso_def embed_def bij_betw_def under_def inj_on_def intro!: exI[of _ "λ_. x"])

lemma osum_ordLeqR: "Well_order r ==> Well_order s ==> s ≤o r +o s"
  unfolding ordLeq_def2 underS_def
  by (auto intro!: exI[of _ Inr] osum_Well_order) (auto simp add: osum_def Field_def)

lemma osum_congL:
  assumes "r =o s" and t: "Well_order t"
  shows "r +o t =o s +o t" (is "?L =o ?R")
proof -
  from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
    unfolding ordIso_def by blast
  let ?f = "map_sum f id"
  from f have "inj_on ?f (Field ?L)"
    unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce
  with f have "bij_betw ?f (Field ?L) (Field ?R)"
    unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto
  moreover from f have "compat ?L ?R ?f"
    unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def
    by (auto simp: map_prod_imageI)
  ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t)
  thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t)
qed

lemma osum_congR:
  assumes "r =o s" and t: "Well_order t"
  shows "t +o r =o t +o s" (is "?L =o ?R")
proof -
  from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
    unfolding ordIso_def by blast
  let ?f = "map_sum id f"
  from f have "inj_on ?f (Field ?L)"
    unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce
  with f have "bij_betw ?f (Field ?L) (Field ?R)"
    unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto
  moreover from f have "compat ?L ?R ?f"
    unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def
    by (auto simp: map_prod_imageI)
  ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t)
  thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t)
qed

lemma osum_cong:
  assumes "t =o u" and "r =o s"
  shows "t +o r =o u +o s"
  using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]]
    assms[unfolded ordIso_def] by auto

lemma Well_order_empty[simp]: "Well_order {}"
  unfolding Field_empty by (rule well_order_on_empty)

lemma well_order_on_singleton[simp]: "well_order_on {x} {(x, x)}"
  unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def total_on_def
    Field_def refl_on_def trans_def antisym_def by auto

lemma oexp_empty[simp]:
  assumes "Well_order r"
  shows "r ^o {} = {(λx. undefined, λx. undefined)}"
  unfolding oexp_def[OF assms Well_order_empty] FinFunc_def fin_support_def support_def by auto

lemma oexp_empty2[simp]:
  assumes "Well_order r" "r ≠ {}"
  shows "{} ^o r = {}"
proof -
  from assms(2) have "Field r ≠ {}" unfolding Field_def by auto
  thus ?thesis
    by (simp add: assms(1) wo_rel2.intro wo_rel2.oexp_empty)
qed

lemma oprod_zero[simp]: "{} *o r = {}" "r *o {} = {}"
  unfolding oprod_def by simp_all

lemma oprod_congL:
  assumes "r =o s" and t: "Well_order t"
  shows "r *o t =o s *o t" (is "?L =o ?R")
proof -
  from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
    unfolding ordIso_def by blast
  let ?f = "map_prod f id"
  from f have "inj_on ?f (Field ?L)"
    unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
  with f have "bij_betw ?f (Field ?L) (Field ?R)"
    unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_prod_surj_on)
  moreover from f have "compat ?L ?R ?f"
    unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
    by (auto simp: map_prod_imageI)
  ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
  thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t)
qed

lemma oprod_congR:
  assumes "r =o s" and t: "Well_order t"
  shows "t *o r =o t *o s" (is "?L =o ?R")
proof -
  from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
    unfolding ordIso_def by blast
  let ?f = "map_prod id f"
  from f have "inj_on ?f (Field ?L)"
    unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
  with f have "bij_betw ?f (Field ?L) (Field ?R)"
    unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_prod_surj_on)
  moreover from f well_order_on_domain[OF r] have "compat ?L ?R ?f"
    unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
    by (auto simp: map_prod_imageI dest: inj_onD)
  ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
  thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t)
qed

lemma oprod_cong:
  assumes "t =o u" and "r =o s"
  shows "t *o r =o u *o s"
  using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]]
    assms[unfolded ordIso_def] by auto

lemma Field_singleton[simp]: "Field {(z,z)} = {z}"
  by (metis well_order_on_Field well_order_on_singleton)

lemma zero_singleton[simp]: "zero {(z,z)} = z"
  using wo_rel.zero_in_Field[unfolded wo_rel_def, of "{(z, z)}"] well_order_on_singleton[of z]
  by auto

lemma FinFunc_singleton: "FinFunc {(z,z)} s = {λx. if x ∈ Field s then z else undefined}"
  unfolding FinFunc_def Func_def fin_support_def support_def
  by (auto simp: fun_eq_iff split: if_split_asm intro!: finite_subset[of _ "{}"])

lemma oone_ordIso_oexp:
  assumes "r =o oone" and s: "Well_order s"
  shows "r ^o s =o oone" (is "?L =o ?R")
proof -
  from ‹r =o oone› obtain f where *: "∀x∈Field r. ∀y∈Field r. x = y" and "f ` Field r = {()}"
    and r: "Well_order r"
    unfolding ordIso_def oone_def by (auto simp add: iso_def [abs_def] bij_betw_def inj_on_def)
  then obtain x where "x ∈ Field r" by auto
  with * have Fr: "Field r = {x}" by auto
  interpret r: wo_rel r by unfold_locales (rule r)
  from Fr well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
  interpret wo_rel2 r s by unfold_locales (rule r, rule s)
  have "bij_betw (λx. ()) (Field ?L) (Field ?R)"
    unfolding bij_betw_def Field_oexp by (auto simp: r_def FinFunc_singleton)
  moreover have "compat ?L ?R (λx. ())" unfolding compat_def oone_def by auto
  ultimately have "iso ?L ?R (λx. ())" using s oone_Well_order
    by (subst iso_iff3) (auto intro: oexp_Well_order)
  thus ?thesis using s oone_Well_order unfolding ordIso_def by (auto intro: oexp_Well_order)
qed

(*Lemma 1.4.3 from Holz et al.*)
context
  fixes r s t
  assumes r: "Well_order r"
  assumes s: "Well_order s"
  assumes t: "Well_order t"
begin

lemma osum_ozeroL: "ozero +o r =o r"
  using r unfolding osum_def ozero_def by (auto intro: map_prod_ordIso)

lemma osum_ozeroR: "r +o ozero =o r"
  using r unfolding osum_def ozero_def by (auto intro: map_prod_ordIso)

lemma osum_assoc: "(r +o s) +o t =o r +o s +o t" (is "?L =o ?R")
proof -
  let ?f =
    "λrst. case rst of Inl (Inl r) ==> Inl r | Inl (Inr s) ==> Inr (Inl s) | Inr t ==> Inr (Inr t)"
  have "bij_betw ?f (Field ?L) (Field ?R)"
    unfolding Field_osum bij_betw_def inj_on_def by (auto simp: image_Un image_iff)
  moreover
  have "compat ?L ?R ?f"
  proof (unfold compat_def, safe)
    fix a b
    assume "(a, b) ∈ ?L"
    thus "(?f a, ?f b) ∈ ?R"
      unfolding osum_def[of "r +o s" t] osum_def[of r "s +o t"] Field_osum
      unfolding osum_def Field_osum image_iff image_Un map_prod_def
      by fastforce
  qed
  ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: osum_Well_order)
  thus ?thesis using r s t unfolding ordIso_def by (auto intro: osum_Well_order)
qed

lemma osum_monoR:
  assumes "s
  shows "r +o s  (is "?L )
proof -
  from assms obtain f where s: "Well_order s" and t:" Well_order t" and "embedS s t f"
    unfolding ordLess_def by blast
  hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s ⊂ Field t"
    using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
    unfolding embedS_def by auto
  let ?f = "map_sum id f"
  from *(1) have "inj_on ?f (Field ?L)" unfolding Field_osum inj_on_def by fastforce
  moreover
  from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_prod_def by fastforce
  moreover
  interpret t: wo_rel t by unfold_locales (rule t)
  interpret rt: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
  from *(3) have "ofilter ?R (?f ` Field ?L)"
    unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image under_def
    by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
  ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
    by (auto intro: osum_Well_order r s t)
  moreover
  from *(4) have "?f ` Field ?L ⊂ Field ?R" unfolding Field_osum image_Un image_image by auto
  ultimately have "embedS ?L ?R ?f" using embedS_iff[OF osum_Well_order[OF r s], of ?R ?f] by auto
  thus ?thesis unfolding ordLess_def by (auto intro: osum_Well_order r s t)
qed

lemma osum_monoL:
  assumes "r ≤o s"
  shows "r +o t ≤o s +o t"
proof -
  from assms obtain f where f: "∀a∈Field r. f a ∈ Field s ∧ f ` underS r a ⊆ underS s (f a)"
    unfolding ordLeq_def2 by blast
  let ?f = "map_sum f id"
  from f have "∀a∈Field (r +o t).
     ?f a ∈ Field (s +o t) ∧ ?f ` underS (r +o t) a ⊆ underS (s +o t) (?f a)"
    unfolding Field_osum underS_def by (fastforce simp: osum_def)
  thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t)
qed

lemma oprod_ozeroL: "ozero *o r =o ozero"
  using ozero_ordIso unfolding ozero_def by simp

lemma oprod_ozeroR: "r *o ozero =o ozero"
  using ozero_ordIso unfolding ozero_def by simp

lemma oprod_ooneR: "r *o oone =o r" (is "?L =o ?R")
proof -
  have "bij_betw fst (Field ?L) (Field ?R)" unfolding Field_oprod bij_betw_def inj_on_def by simp
  moreover have "compat ?L ?R fst" unfolding compat_def oprod_def by auto
  ultimately have "iso ?L ?R fst" using r oone_Well_order
    by (subst iso_iff3) (auto intro: oprod_Well_order)
  thus ?thesis using r oone_Well_order unfolding ordIso_def by (auto intro: oprod_Well_order)
qed

lemma oprod_ooneL: "oone *o r =o r" (is "?L =o ?R")
proof -
  have "bij_betw snd (Field ?L) (Field ?R)" unfolding Field_oprod bij_betw_def inj_on_def by simp
  moreover have "Refl r" by (rule wo_rel.REFL[unfolded wo_rel_def, OF r])
  hence "compat ?L ?R snd" unfolding compat_def oprod_def refl_on_def by auto
  ultimately have "iso ?L ?R snd" using r oone_Well_order
    by (subst iso_iff3) (auto intro: oprod_Well_order)
  thus ?thesis using r oone_Well_order unfolding ordIso_def by (auto intro: oprod_Well_order)
qed

lemma oprod_monoR:
  assumes "ozero  "s
  shows "r *o s  (is "?L )
proof -
  from assms obtain f where s: "Well_order s" and t:" Well_order t" and "embedS s t f"
    unfolding ordLess_def by blast
  hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s ⊂ Field t"
    using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
    unfolding embedS_def by auto
  let ?f = "map_prod id f"
  from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce
  moreover
  from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
    by auto (metis well_order_on_domain t, metis well_order_on_domain s)
  moreover
  interpret t: wo_rel t by unfold_locales (rule t)
  interpret rt: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
  from *(3) have "ofilter ?R (?f ` Field ?L)"
    unfolding t.ofilter_def rt.ofilter_def Field_oprod under_def
    by (auto simp: oprod_def image_iff) (fast | metis r well_order_on_domain)+
  ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
    by (auto intro: oprod_Well_order r s t)
  moreover
  from not_ordLess_ordIso[OF assms(1)] have "r ≠ {}" by (metis ozero_def ozero_ordIso)
  hence "Field r ≠ {}" unfolding Field_def by auto
  with *(4) have "?f ` Field ?L ⊂ Field ?R" unfolding Field_oprod
    by auto (metis SigmaD2 SigmaI map_prod_surj_on)
  ultimately have "embedS ?L ?R ?f" using embedS_iff[OF oprod_Well_order[OF r s], of ?R ?f] by auto
  thus ?thesis unfolding ordLess_def by (auto intro: oprod_Well_order r s t)
qed

lemma oprod_monoL:
  assumes "r ≤o s"
  shows "r *o t ≤o s *o t"
proof -
  from assms obtain f where f: "∀a∈Field r. f a ∈ Field s ∧ f ` underS r a ⊆ underS s (f a)"
    unfolding ordLeq_def2 by blast
  let ?f = "map_prod f id"
  from f have "∀a∈Field (r *o t).
     ?f a ∈ Field (s *o t) ∧ ?f ` underS (r *o t) a ⊆ underS (s *o t) (?f a)"
    unfolding Field_oprod underS_def unfolding map_prod_def oprod_def by auto
  thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
qed

lemma oprod_assoc: "(r *o s) *o t =o r *o s *o t" (is "?L =o ?R")
proof -
  let ?f = "λ((a,b),c). (a,b,c)"
  have "bij_betw ?f (Field ?L) (Field ?R)"
    unfolding Field_oprod bij_betw_def inj_on_def by (auto simp: image_Un image_iff)
  moreover
  have "compat ?L ?R ?f"
  proof (unfold compat_def, safe)
    fix a1 a2 a3 b1 b2 b3
    assume "(((a1, a2), a3), ((b1, b2), b3)) ∈ ?L"
    thus "((a1, a2, a3), (b1, b2, b3)) ∈ ?R"
      unfolding oprod_def[of "r *o s" t] oprod_def[of r "s *o t"] Field_oprod
      unfolding oprod_def Field_oprod image_iff image_Un by fast
  qed
  ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: oprod_Well_order)
  thus ?thesis using r s t unfolding ordIso_def by (auto intro: oprod_Well_order)
qed

lemma oprod_osum: "r *o (s +o t) =o r *o s +o r *o t" (is "?L =o ?R")
proof -
  let ?f = "λ(a,bc). case bc of Inl b ==> Inl (a, b) | Inr c ==> Inr (a, c)"
  have "bij_betw ?f (Field ?L) (Field ?R)" unfolding Field_oprod Field_osum bij_betw_def inj_on_def
    by (fastforce simp: image_Un image_iff split: sum.splits)
  moreover
  have "compat ?L ?R ?f"
  proof (unfold compat_def, intro allI impI)
    fix a b
    assume "(a, b) ∈ ?L"
    thus "(?f a, ?f b) ∈ ?R"
      unfolding oprod_def[of r "s +o t"] osum_def[of "r *o s" "r *o t"] Field_oprod Field_osum
      unfolding oprod_def osum_def Field_oprod Field_osum image_iff image_Un by auto
  qed
  ultimately have "iso ?L ?R ?f" using r s t
    by (subst iso_iff3) (auto intro: oprod_Well_order osum_Well_order)
  thus ?thesis using r s t unfolding ordIso_def by (auto intro: oprod_Well_order osum_Well_order)
qed

lemma ozero_oexp: "¬ (s =o ozero) ==> ozero ^o s =o ozero"
  by (fastforce simp add: oexp_def[OF ozero_Well_order s] FinFunc_def Func_def intro: FieldI1)

lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R")
  by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s])

lemma oexp_monoR:
  assumes "oone  "s
  shows   "r ^o s  (is "?L )
proof -
  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
  interpret rexpt: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
  interpret r: wo_rel r by unfold_locales (rule r)
  interpret s: wo_rel s by unfold_locales (rule s)
  interpret t: wo_rel t by unfold_locales (rule t)
  have "Field r ≠ {}" by (metis assms(1) internalize_ordLess not_psubset_empty)
  moreover
  { assume "Field r = {r.zero}"
    hence "r = {(r.zero, r.zero)}" using refl_onD[OF r.REFL, of r.zero] unfolding Field_def by auto
    hence "r =o oone" by (metis oone_ordIso ordIso_symmetric)
    with not_ordLess_ordIso[OF assms(1)] have False by (metis ordIso_symmetric)
  }
  ultimately obtain x where x: "x ∈ Field r" "r.zero ∈ Field r" "x ≠ r.zero"
    by (metis insert_iff r.zero_in_Field subsetI subset_singletonD)
  moreover from assms(2) obtain f where "embedS s t f" unfolding ordLess_def by blast
  hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s ⊂ Field t"
    using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
    unfolding embedS_def by auto
  note invff = the_inv_into_f_f[OF *(1)] and injfD = inj_onD[OF *(1)]
  define F where [abs_def]: "F g z =
    (if z ∈ f ` Field s then g (the_inv_into (Field s) f z)
     else if z ∈ Field t then r.zero else undefined)" for g z
  from *(4) x(2) the_inv_into_f_eq[OF *(1)] have FLR: "F ` Field ?L ⊆ Field ?R"
    unfolding rt.Field_oexp rs.Field_oexp FinFunc_def Func_def fin_support_def support_def F_def
    by (fastforce split: option.splits if_split_asm elim!: finite_surj[of _ _ f])
  have "inj_on F (Field ?L)" unfolding rs.Field_oexp inj_on_def fun_eq_iff
  proof safe
    fix g h x assume "g ∈ FinFunc r s" "h ∈ FinFunc r s" "∀y. F g y = F h y"
    with invff show "g x = h x" unfolding F_def fun_eq_iff FinFunc_def Func_def
      by auto (metis image_eqI)
  qed
  moreover
  have "compat ?L ?R F" unfolding compat_def rs.oexp_def rt.oexp_def
  proof (safe elim!: bspec[OF iffD1[OF image_subset_iff FLR[unfolded rs.Field_oexp rt.Field_oexp]]])
    fix g h assume gh: "g ∈ FinFunc r s" "h ∈ FinFunc r s" "F g ≠ F h"
      "let m = s.max_fun_diff g h in (g m, h m) ∈ r"
    hence "g ≠ h" by auto
    note max_fun_diff_in = rs.max_fun_diff_in[OF ‹g ≠ h› gh(1,2)]
      and max_fun_diff_max = rs.max_fun_diff_max[OF ‹g ≠ h› gh(1,2)]
    with *(4) invff *(2) have "t.max_fun_diff (F g) (F h) = f (s.max_fun_diff g h)"
      unfolding t.max_fun_diff_def compat_def
      by (intro t.maxim_equality) (auto simp: t.isMaxim_def F_def dest: injfD)
    with gh invff max_fun_diff_in
    show "let m = t.max_fun_diff (F g) (F h) in (F g m, F h m) ∈ r"
      unfolding F_def Let_def by (auto simp: dest: injfD)
  qed
  moreover
  from FLR have "ofilter ?R (F ` Field ?L)"
    unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
  proof (safe elim!: imageI)
    fix g h assume gh: "g ∈ FinFunc r s" "h ∈ FinFunc r t" "F g ∈ FinFunc r t"
      "let m = t.max_fun_diff h (F g) in (h m, F g m) ∈ r"
    thus "h ∈ F ` FinFunc r s"
    proof (cases "h = F g")
      case False
      hence max_Field: "t.max_fun_diff h (F g) ∈ {a ∈ Field t. h a ≠ F g a}"
        by (rule rt.max_fun_diff_in[OF _ gh(2,3)])
      { assume *: "t.max_fun_diff h (F g) ∉ f ` Field s"
        with max_Field have **: "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
        with * gh(4) have "h (t.max_fun_diff h (F g)) = r.zero" unfolding Let_def by auto
        with ** have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
      }
      hence max_f_Field: "t.max_fun_diff h (F g) ∈ f ` Field s" by blast
      { fix z assume z: "z ∈ Field t - f ` Field s"
        have "(t.max_fun_diff h (F g), z) ∈ t"
        proof (rule ccontr)
          assume "(t.max_fun_diff h (F g), z) ∉ t"
          hence "(z, t.max_fun_diff h (F g)) ∈ t" using t.in_notinI[of "t.max_fun_diff h (F g)" z]
              z max_Field by auto
          hence "z ∈ f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def under_def
            by fastforce
          with z show False by blast
        qed
        hence "h z = r.zero" using rt.max_fun_diff_le_eq[OF _ False gh(2,3), of z]
            z max_f_Field unfolding F_def by auto
      } note ** = this
      with *(3) gh(2) have "h = F (λx. if x ∈ Field s then h (f x) else undefined)" using invff
        unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto
      moreover from gh(2) *(1,3) have "(λx. if x ∈ Field s then h (f x) else undefined) ∈ FinFunc r s"
        unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def under_def
        by (auto intro: inj_on_subset elim!: finite_imageD[OF finite_subset[rotated]])
      ultimately show "?thesis" by (rule image_eqI)
    qed simp
  qed
  ultimately have "embed ?L ?R F" using embed_iff_compat_inj_on_ofilter[of ?L ?R F]
    by (auto intro: oexp_Well_order r s t)
  moreover
  from FLR have "F ` Field ?L ⊂ Field ?R"
  proof (intro psubsetI)
    from *(4) obtain z where z: "z ∈ Field t" "z ∉ f ` Field s" by auto
    define h where [abs_def]: "h z' =
      (if z' ∈ Field t then if z' = z then x else r.zero else undefined)" for z'
    from z x(3) have "rt.SUPP h = {z}" unfolding support_def h_def by simp
    with x have "h ∈ Field ?R" unfolding h_def rt.Field_oexp FinFunc_def Func_def fin_support_def
      by auto
    moreover
    { fix g
      from z have "F g z = r.zero" "h z = x" unfolding support_def h_def F_def by auto
      with x(3) have "F g ≠ h" unfolding fun_eq_iff by fastforce
    }
    hence "h ∉ F ` Field ?L" by blast
    ultimately show "F ` Field ?L ≠ Field ?R" by blast
  qed
  ultimately have "embedS ?L ?R F" using embedS_iff[OF rs.oexp_Well_order, of ?R F] by auto
  thus ?thesis unfolding ordLess_def using r s t by (auto intro: oexp_Well_order)
qed

lemma oexp_monoL:
  assumes "r ≤o s"
  shows   "r ^o t ≤o s ^o t"
proof -
  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
  interpret st: wo_rel2 s t by unfold_locales (rule s, rule t)
  interpret r: wo_rel r by unfold_locales (rule r)
  interpret s: wo_rel s by unfold_locales (rule s)
  interpret t: wo_rel t by unfold_locales (rule t)
  show ?thesis
  proof (cases "t = {}")
    case True thus ?thesis using r s unfolding ordLeq_def2 underS_def by auto
  next
    case False thus ?thesis
    proof (cases "r = {}")
      case True thus ?thesis using t ‹t ≠ {}› st.oexp_Well_order ozero_ordLeq[unfolded ozero_def]
        by auto
    next
      case False
      from assms obtain f where f: "embed r s f" unfolding ordLeq_def by blast
      hence f_underS: "∀a∈Field r. f a ∈ Field s ∧ f ` underS r a ⊆ underS s (f a)"
        using embed_in_Field embed_underS2 rt.rWELL by fastforce
      from f ‹t ≠ {}› False have *: "Field r ≠ {}" "Field s ≠ {}" "Field t ≠ {}"
        unfolding Field_def embed_def under_def bij_betw_def by auto
      with f obtain x where "s.zero = f x" "x ∈ Field r" unfolding embed_def bij_betw_def
        using s.zero_under subsetD[OF under_Field[of r]]
        by (metis (no_types, lifting) f_inv_into_f f_underS inv_into_into r.zero_in_Field)
      with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
        unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
        by (fastforce intro: s.leq_zero_imp)+
      let ?f = "λg x. if x ∈ Field t then f (g x) else undefined"
      { fix g assume g: "g ∈ Field (r ^o t)"
        with fz f_underS have Field_fg: "?f g ∈ Field (s ^o t)"
          unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
          by (auto elim!: finite_subset[rotated])
        moreover
        have "?f ` underS (r ^o t) g ⊆ underS (s ^o t) (?f g)"
        proof safe
          fix h
          assume h_underS: "h ∈ underS (r ^o t) g"
          hence "h ∈ Field (r ^o t)" unfolding underS_def Field_def by auto
          with fz f_underS have Field_fh: "?f h ∈ Field (s ^o t)"
            unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
            by (auto elim!: finite_subset[rotated])
          from h_underS have "h ≠ g" and hg: "(h, g) ∈ rt.oexp" unfolding underS_def by auto
          with f inj have neq: "?f h ≠ ?f g"
            unfolding fun_eq_iff inj_on_def rt.oexp_def map_option_case FinFunc_def Func_def Let_def
            by simp metis
          with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def
            using rt.max_fun_diff[OF ‹h ≠ g›] rt.max_fun_diff_in[OF ‹h ≠ g›]
            by (subst t.max_fun_diff_def, intro t.maxim_equality)
              (auto simp: t.isMaxim_def intro: inj_onD[OF inj] intro!: rt.max_fun_diff_max)
          with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) ∈ st.oexp"
            using rt.max_fun_diff[OF ‹h ≠ g›] rt.max_fun_diff_in[OF ‹h ≠ g›] unfolding st.Field_oexp
            unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
          with neq show "?f h ∈ underS (s ^o t) (?f g)" unfolding underS_def by auto
        qed
        ultimately have "?f g ∈ Field (s ^o t) ∧ ?f ` underS (r ^o t) g ⊆ underS (s ^o t) (?f g)"
          by blast
      }
      thus ?thesis unfolding ordLeq_def2 by (fastforce intro: oexp_Well_order r s t)
    qed
  qed
qed

lemma ordLeq_oexp2:
  assumes "oone
  shows   "s ≤o r ^o s"
proof -
  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
  interpret r: wo_rel r by unfold_locales (rule r)
  interpret s: wo_rel s by unfold_locales (rule s)
  from assms well_order_on_domain[OF r] obtain x where
    x: "x ∈ Field r" "r.zero ∈ Field r" "x ≠ r.zero"
    unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
    by (auto simp: image_def)
      (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)
  let ?f = "λa b. if b ∈ Field s then if b = a then x else r.zero else undefined"
  from x(3) have SUPP: "∧y. y ∈ Field s ==> rs.SUPP (?f y) = {y}" unfolding support_def by auto
  { fix y assume y: "y ∈ Field s"
    with x(1,2) SUPP have "?f y ∈ Field (r ^o s)" unfolding rs.Field_oexp
      by (auto simp: FinFunc_def Func_def fin_support_def)
    moreover
    have "?f ` underS s y ⊆ underS (r ^o s) (?f y)"
    proof safe
      fix z
      assume "z ∈ underS s y"
      hence z: "z ≠ y" "(z, y) ∈ s" "z ∈ Field s" unfolding underS_def Field_def by auto
      from x(3) y z(1,3) have "?f z ≠ ?f y" unfolding fun_eq_iff by auto
      moreover
      { from x(1,2) have "?f z ∈ FinFunc r s" "?f y ∈ FinFunc r s"
          unfolding FinFunc_def Func_def fin_support_def by (auto simp: SUPP[OF z(3)] SUPP[OF y])
        moreover
        from x(3) y z(1,2) refl_onD[OF s.REFL] have "s.max_fun_diff (?f z) (?f y) = y"
          unfolding rs.max_fun_diff_alt SUPP[OF z(3)] SUPP[OF y]
          by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
        ultimately have "(?f z, ?f y) ∈ rs.oexp" using y x(1)
          unfolding rs.oexp_def Let_def by auto
      }
      ultimately show "?f z ∈ underS (r ^o s) (?f y)" unfolding underS_def by blast
    qed
    ultimately have "?f y ∈ Field (r ^o s) ∧ ?f ` underS s y ⊆ underS (r ^o s) (?f y)" by blast
  }
  thus ?thesis unfolding ordLeq_def2 by (fast intro: oexp_Well_order r s)
qed

lemma FinFunc_osum:
  "fg ∈ FinFunc r (s +o t) = (fg o Inl ∈ FinFunc r s ∧ fg o Inr ∈ FinFunc r t)"
  (is "?L = (?R1 ∧ ?R2)")
proof safe
  assume ?L
  from ‹?L› show ?R1 unfolding FinFunc_def Field_osum Func_def Int_iff fin_support_Field_osum o_def
    by (auto split: sum.splits)
  from ‹?L› show ?R2 unfolding FinFunc_def Field_osum Func_def Int_iff fin_support_Field_osum o_def
    by (auto split: sum.splits)
next
  assume ?R1 ?R2
  thus "?L" unfolding FinFunc_def Field_osum Func_def
    by (auto simp: fin_support_Field_osum o_def image_iff split: sum.splits) (metis sumE)
qed

lemma max_fun_diff_eq_Inl:
  assumes "wo_rel.max_fun_diff (s +o t) (case_sum f1 g1) (case_sum f2 g2) = Inl x"
    "case_sum f1 g1 ≠ case_sum f2 g2"
    "case_sum f1 g1 ∈ FinFunc r (s +o t)" "case_sum f2 g2 ∈ FinFunc r (s +o t)"
  shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q)
proof -
  interpret st: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
  interpret s: wo_rel s by unfold_locales (rule s)
  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
  from assms(1) have *: "st.isMaxim {a ∈ Field (s +o t). case_sum f1 g1 a ≠ case_sum f2 g2 a} (Inl x)"
    using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
  hence "s.isMaxim {a ∈ Field s. f1 a ≠ f2 a} x"
    unfolding st.isMaxim_def s.isMaxim_def Field_osum by (auto simp: osum_def)
  thus ?P unfolding s.max_fun_diff_def by (rule s.maxim_equality)
  from assms(3,4) have **: "g1 ∈ FinFunc r t" "g2 ∈ FinFunc r t" unfolding FinFunc_osum
    by (auto simp: o_def)
  show ?Q
  proof
    fix x
    from * ** show "g1 x = g2 x" unfolding st.isMaxim_def Field_osum FinFunc_def Func_def fun_eq_iff
      unfolding osum_def by (case_tac "x ∈ Field t") auto
  qed
qed

lemma max_fun_diff_eq_Inr:
  assumes "wo_rel.max_fun_diff (s +o t) (case_sum f1 g1) (case_sum f2 g2) = Inr x"
    "case_sum f1 g1 ≠ case_sum f2 g2"
    "case_sum f1 g1 ∈ FinFunc r (s +o t)" "case_sum f2 g2 ∈ FinFunc r (s +o t)"
  shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 ≠ g2" (is ?Q)
proof -
  interpret st: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
  interpret t: wo_rel t by unfold_locales (rule t)
  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
  from assms(1) have *: "st.isMaxim {a ∈ Field (s +o t). case_sum f1 g1 a ≠ case_sum f2 g2 a} (Inr x)"
    using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
  hence "t.isMaxim {a ∈ Field t. g1 a ≠ g2 a} x"
    unfolding st.isMaxim_def t.isMaxim_def Field_osum by (auto simp: osum_def)
  thus ?P ?Q unfolding t.max_fun_diff_def fun_eq_iff
    by (auto intro: t.maxim_equality simp: t.isMaxim_def)
qed

lemma oexp_osum: "r ^o (s +o t) =o (r ^o s) *o (r ^o t)" (is "?R =o ?L")
proof (rule ordIso_symmetric)
  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
  let ?f = "λ(f, g). case_sum f g"
  have "bij_betw ?f (Field ?L) (Field ?R)"
    unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
    show "inj_on ?f (FinFunc r s × FinFunc r t)" unfolding inj_on_def
      by (auto simp: fun_eq_iff split: sum.splits)
    show "?f ` (FinFunc r s × FinFunc r t) = FinFunc r (s +o t)"
    proof safe
      fix fg assume "fg ∈ FinFunc r (s +o t)"
      thus "fg ∈ ?f ` (FinFunc r s × FinFunc r t)"
        by (intro image_eqI[of _ _ "(fg o Inl, fg o Inr)"])
          (auto simp: FinFunc_osum fun_eq_iff split: sum.splits)
    qed (auto simp: FinFunc_osum o_def)
  qed
  moreover have "compat ?L ?R ?f"
    unfolding compat_def rst.Field_oexp rs.Field_oexp rt.Field_oexp oprod_def
    unfolding rst.oexp_def Let_def rs.oexp_def rt.oexp_def
    by (fastforce simp: Field_osum FinFunc_osum o_def split: sum.splits
        dest: max_fun_diff_eq_Inl max_fun_diff_eq_Inr)
  ultimately have "iso ?L ?R ?f" using r s t
    by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order osum_Well_order)
  thus "?L =o ?R" using r s t unfolding ordIso_def
    by (auto intro: oexp_Well_order oprod_Well_order osum_Well_order)
qed

definition "rev_curr f b = (if b ∈ Field t then λa. f (a, b) else undefined)"

lemma rev_curr_FinFunc:
  assumes Field: "Field r ≠ {}"
  shows "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t"
proof safe
  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
  fix g assume g: "g ∈ FinFunc r (s *o t)"
  hence "finite (rst.SUPP (rev_curr g))" "∀x ∈ Field t. finite (rs.SUPP (rev_curr g x))"
    unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def fin_support_def support_def
      rs.zero_oexp[OF Field] rev_curr_def by (auto simp: fun_eq_iff rs.const_def elim!: finite_surj)
  with g show "rev_curr g ∈ FinFunc (r ^o s) t"
    unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def
    by (auto simp: rev_curr_def fin_support_def)
next
  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
  fix fg assume *: "fg ∈ FinFunc (r ^o s) t"
  let ?g = "λ(a, b). if (a, b) ∈ Field (s *o t) then fg b a else undefined"
  show "fg ∈ rev_curr ` FinFunc r (s *o t)"
  proof (rule image_eqI[of _ _ ?g])
    show "fg = rev_curr ?g"
    proof
      fix x
      from * show "fg x = rev_curr ?g x"
        unfolding FinFunc_def rs.Field_oexp Func_def rev_curr_def Field_oprod by auto
    qed
  next
    have **: "(∪g ∈ fg ` Field t. rs.SUPP g) =
              (∪g ∈ fg ` Field t - {rs.const}. rs.SUPP g)"
      unfolding support_def by auto
    from * have ***: "∀g ∈ fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
      unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def by force+
    hence "finite (fg ` Field t - {rs.const})" using *
      unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def
      by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff Option.these_def)
    with *** have "finite ((∪g ∈ fg ` Field t. rs.SUPP g) × rst.SUPP fg)"
      by (subst **) (auto intro!: finite_cartesian_product)
    with * show "?g ∈ FinFunc r (s *o t)"
      unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def
        support_def rs.zero_oexp[OF Field] by (auto elim!: finite_subset[rotated])
  qed
qed

lemma rev_curr_app_FinFunc[elim!]:
  "[f ∈ FinFunc r (s *o t); z ∈ Field t] ==> rev_curr f z ∈ FinFunc r s"
  unfolding rev_curr_def FinFunc_def Func_def Field_oprod fin_support_def support_def
  by (auto elim: finite_surj)

lemma max_fun_diff_oprod:
  assumes Field: "Field r ≠ {}" and "f ≠ g" "f ∈ FinFunc r (s *o t)" "g ∈ FinFunc r (s *o t)"
  defines "m ≡ wo_rel.max_fun_diff t (rev_curr f) (rev_curr g)"
  shows "wo_rel.max_fun_diff (s *o t) f g =
    (wo_rel.max_fun_diff s (rev_curr f m) (rev_curr g m), m)"
proof -
  interpret st: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
  interpret s: wo_rel s by unfold_locales (rule s)
  interpret t: wo_rel t by unfold_locales (rule t)
  interpret r_st: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
  from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4)
  have diff1: "rev_curr f ≠ rev_curr g"
    "rev_curr f ∈ FinFunc (r ^o s) t" "rev_curr g ∈ FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
    unfolding fun_eq_iff rev_curr_def[abs_def] FinFunc_def support_def Field_oprod
    by auto fast
  hence diff2: "rev_curr f m ≠ rev_curr g m" "rev_curr f m ∈ FinFunc r s" "rev_curr g m ∈ FinFunc r s"
    using rst.max_fun_diff[OF diff1] assms(3,4) rst.max_fun_diff_in unfolding m_def by auto
  show ?thesis unfolding st.max_fun_diff_def
  proof (intro st.maxim_equality, unfold st.isMaxim_def Field_oprod, safe)
    show "s.max_fun_diff (rev_curr f m) (rev_curr g m) ∈ Field s"
      using rs.max_fun_diff_in[OF diff2] by auto
  next
    show "m ∈ Field t" using rst.max_fun_diff_in[OF diff1] unfolding m_def by auto
  next
    assume "f (s.max_fun_diff (rev_curr f m) (rev_curr g m), m) =
            g (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)"
      (is "f (?x, m) = g (?x, m)")
    hence "rev_curr f m ?x = rev_curr g m ?x" unfolding rev_curr_def by auto
    with rs.max_fun_diff[OF diff2] show False by auto
  next
    fix x y assume "f (x, y) ≠ g (x, y)" "x ∈ Field s" "y ∈ Field t"
    thus "((x, y), (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)) ∈ s *o t"
      using rst.max_fun_diff_in[OF diff1] rs.max_fun_diff_in[OF diff2] diff1 diff2
        rst.max_fun_diff_max[OF diff1, of y] rs.max_fun_diff_le_eq[OF _ diff2, of x]
      unfolding oprod_def m_def rev_curr_def fun_eq_iff by (auto intro: s.in_notinI)
  qed
qed

lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L")
proof (cases "r = {}")
  case True
  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
  show ?thesis
  proof (cases "s = {} ∨ t = {}")
    case True with ‹r = {}› show ?thesis
      by (auto simp: oexp_empty[OF oexp_Well_order[OF Well_order_empty s]]
          intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso]
          ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso])
  next
    case False
    hence "s *o t ≠ {}" unfolding oprod_def Field_def by fastforce
    with False show ?thesis
      using ‹r = {}› ozero_ordIso
      by (auto simp add: s t oprod_Well_order ozero_def)
  qed
next
  case False
  hence Field: "Field r ≠ {}" by (metis Field_def Range_empty_iff Un_empty)
  show ?thesis
  proof (rule ordIso_symmetric)
    interpret r_st: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
    interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
    interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
    have bij: "bij_betw rev_curr (Field ?L) (Field ?R)"
      unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
      show "inj_on rev_curr (FinFunc r (s *o t))"
        unfolding inj_on_def FinFunc_def Func_def Field_oprod rs.Field_oexp rev_curr_def[abs_def]
        by (auto simp: fun_eq_iff) metis
      show "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t" by (rule rev_curr_FinFunc[OF Field])
    qed
    moreover
    have "compat ?L ?R rev_curr"
      unfolding compat_def proof safe
      fix fg1 fg2 assume fg: "(fg1, fg2) ∈ r ^o (s *o t)"
      show "(rev_curr fg1, rev_curr fg2) ∈ r ^o s ^o t"
      proof (cases "fg1 = fg2")
        assume "fg1 ≠ fg2"
        with fg show ?thesis
          using rst.max_fun_diff_in[of "rev_curr fg1" "rev_curr fg2"]
            max_fun_diff_oprod[OF Field, of fg1 fg2]  rev_curr_FinFunc[OF Field, symmetric]
          unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp unfolding r_st.oexp_def rst.oexp_def
          by (auto simp: rs.oexp_def Let_def) (auto simp: rev_curr_def[abs_def])
      next
        assume "fg1 = fg2"
        with fg bij show ?thesis unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp bij_betw_def
          by (auto simp: r_st.oexp_def rst.oexp_def)
      qed
    qed
    ultimately have "iso ?L ?R rev_curr" using r s t
      by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order)
    thus "?L =o ?R" using r s t unfolding ordIso_def
      by (auto intro: oexp_Well_order oprod_Well_order)
  qed
qed

end (* context with 3 wellorders *)

end