Quelle Ordinal_Arithmetic.thy Sprache: Isabelle

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

Ordinal arithmetic.
*)

section \<open>Ordinal Arithmetic\<close>

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 \<in> Field r \<and> a' \<in> 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' \<in> Inr -` A" and "\<forall>a1' \<in> Inr -` A. (a1',a') \<notin> 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) \<in> r' - Id \<and> x1 \<in> Field r \<and> x2 \<in> Field r) \<or>
   ((y1, y2) \<in> Restr Id (Field r') \<and> (x1, x2) \<in> 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 \<open>B \<noteq> {}\<close> obtain x where x: "x \<in> snd ` B" "\<forall>x'\<in>snd ` B. (x', x) \<notin> 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 \<open>B \<noteq> {}\<close> obtain x where x: "x \<in> fst ` B" "\<forall>x'\<in>fst ` B. (x', x) \<notin> 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' \<noteq> {}" 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) \<in> fin_support z A \<and> (f o Inr) \<in> fin_support z B" (is "?L \<longleftrightarrow> ?R1 \<and> ?R2")
proof safe
  assume ?L
  from \<open>?L\<close> show ?R1 unfolding fin_support_def support_def
    by (fastforce simp: image_iff elim: finite_surj[of _ _ "case_sum id undefined"])
  from \<open>?L\<close> 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 \<in> Field s. f a \<noteq> 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 \<in> {a \<in> Field s. f a \<noteq> 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) \<in> s"
  using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast

lemma max_fun_diff:
  "\f \ g; f \ FINFUNC; g \ FINFUNC\ \
  (\<exists>a b. a \<noteq> b \<and> a \<in> Field r \<and> b \<in> Field r \<and>
     f (s.max_fun_diff f g) = a \<and> 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) \<noteq> 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) \<in> r) \<or> 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] * \<open>f \<noteq> h\<close> 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 \<open>f \<in> F\<close> assms(1) have "f \<in> FINFUNC" by blast
    ultimately have "f = const"
      by (auto simp: fun_eq_iff support_def FinFunc_def Func_def const_def)
    with assms(2) \<open>f \<in> F\<close> 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)) \
        (\<exists>f0 \<in> F. \<forall>f \<in> F. (f0, f) \<in> 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 \<in> G}"
              from G SUPPG maxG \<open>G \<noteq> {}\<close> have y'min: "s.isMinim {s.maxim (SUPP f) | f. f \<in> 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 \<open>G \<noteq> {}\<close> have "\<exists>g \<in> 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 \<open>^o\<close> 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 \<open>r =o oone\<close> obtain f where *: "\<forall>x\<in>Field r. \<forall>y\<in>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 \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> 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 \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> 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 \<in> f ` Field s then g (the_inv_into (Field s) f z)
     else if z \<in> 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 \<open>g \<noteq> h\<close> gh(1,2)]
      and max_fun_diff_max = rs.max_fun_diff_max[OF \<open>g \<noteq> h\<close> 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 \<open>t \<noteq> {}\<close> 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 \<open>t \<noteq> {}\<close> False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
        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
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.