Theory Coinductive.Coinductive_Nat

(*  Title:       Coinductive natural numbers
    Author:      Andreas Lochbihler
    Maintainer:  Andreas Lochbihler
*)

section ‹Extended natural numbers as a codatatype›

theory Coinductive_Nat imports
  "HOL-Library.Extended_Nat"
  "HOL-Library.Complete_Partial_Order2"
begin

lemma inj_enat [simp]: "inj_on enat A"
by(simp add: inj_on_def)

lemma Sup_range_enat [simp]: "Sup (range enat) = ∞"
by(auto dest: finite_imageD simp add: Sup_enat_def)

lemmas eSuc_plus = iadd_Suc

lemmas plus_enat_eq_0_conv = iadd_is_0

lemma enat_add_sub_same:
  fixes a b :: enat shows "a ≠ ∞ ⟹ a + b - a = b"
by(cases b) auto

lemma enat_the_enat: "n ≠ ∞ ⟹ enat (the_enat n) = n"
by auto

lemma enat_min_eq_0_iff:
  fixes a b :: enat
  shows "min a b = 0 ⟷ a = 0 ∨ b = 0"
by(auto simp add: min_def)

lemma enat_le_plus_same: "x ≤ (x :: enat) + y" "x ≤ y + x"
by(auto simp add: less_eq_enat_def plus_enat_def split: enat.split)

lemma the_enat_0 [simp]: "the_enat 0 = 0"
by(simp add: zero_enat_def)

lemma the_enat_eSuc: "n ≠ ∞ ⟹ the_enat (eSuc n) = Suc (the_enat n)"
by(cases n)(simp_all add: eSuc_enat)

coinductive_set enat_set :: "enat set"
where "0 ∈ enat_set"
  | "n ∈ enat_set ⟹ (eSuc n) ∈ enat_set"

lemma enat_set_eq_UNIV [simp]: "enat_set = UNIV"
proof
  show "enat_set ⊆ UNIV" by blast
  show "UNIV ⊆ enat_set"
  proof
    fix x :: enat
    assume "x ∈ UNIV"
    thus "x ∈ enat_set"
    proof coinduct
      case (enat_set x)
      show ?case
      proof(cases "x = 0")
        case True thus ?thesis by simp
      next
        case False
        then obtain n where "x = eSuc n"
          by(cases x)(fastforce simp add: eSuc_def zero_enat_def gr0_conv_Suc
                               split: enat.splits)+
        thus ?thesis by auto
      qed
    qed
  qed
qed

subsection ‹Case operator›

lemma enat_coexhaust:
  obtains (0) "n = 0"
     | (eSuc) n' where "n = eSuc n'"
proof -
  have "n ∈ enat_set" by auto
  thus thesis by cases (erule that)+
qed

locale co begin

free_constructors (plugins del: code) case_enat for
    "0::enat"
  | eSuc epred
where
  "epred 0 = 0"
  apply (erule enat_coexhaust, assumption)
 apply (rule eSuc_inject)
by (rule zero_ne_eSuc)

end

lemma enat_cocase_0 [simp]: "co.case_enat z s 0 = z"
by (rule co.enat.case(1))

lemma enat_cocase_eSuc [simp]: "co.case_enat z s (eSuc n) = s n"
by (rule co.enat.case(2))

lemma neq_zero_conv_eSuc: "n ≠ 0 ⟷ (∃n'. n = eSuc n')"
by(cases n rule: enat_coexhaust) simp_all

lemma enat_cocase_cert:
  assumes "CASE ≡ co.case_enat c d"
  shows "(CASE 0 ≡ c) &&& (CASE (eSuc n) ≡ d n)"
  using assms by simp_all

lemma enat_cosplit_asm:
  "P (co.case_enat c d n) = (¬ (n = 0 ∧ ¬ P c ∨ (∃m. n = eSuc m ∧ ¬ P (d m))))"
by (rule co.enat.split_asm)

lemma enat_cosplit:
  "P (co.case_enat c d n) = ((n = 0 ⟶ P c) ∧ (∀m. n = eSuc m ⟶ P (d m)))"
by (rule co.enat.split)

abbreviation epred :: "enat => enat" where "epred ≡ co.epred"

lemma epred_0 [simp]: "epred 0 = 0" by(rule co.enat.sel(1))
lemma epred_eSuc [simp]: "epred (eSuc n) = n" by(rule co.enat.sel(2))
declare co.enat.collapse[simp]
lemma epred_conv_minus: "epred n = n - 1"
by(cases n rule: co.enat.exhaust)(simp_all)

subsection ‹Corecursion for @{typ enat}›

lemma case_enat_numeral [simp]: "case_enat f i (numeral v) = (let n = numeral v in f n)"
by(simp add: numeral_eq_enat)

lemma case_enat_0 [simp]: "case_enat f i 0 = f 0"
by(simp add: zero_enat_def)

lemma [simp]:
  shows max_eSuc_eSuc: "max (eSuc n) (eSuc m) = eSuc (max n m)"
  and min_eSuc_eSuc: "min (eSuc n) (eSuc m) = eSuc (min n m)"
by(simp_all add: eSuc_def split: enat.split)


definition epred_numeral :: "num ⇒ enat"
where [code del]: "epred_numeral = enat ∘ pred_numeral"

lemma numeral_eq_eSuc: "numeral k = eSuc (epred_numeral k)"
by(simp add: numeral_eq_Suc eSuc_def epred_numeral_def numeral_eq_enat)

lemma epred_numeral_simps [simp]:
  "epred_numeral num.One = 0"
  "epred_numeral (num.Bit0 k) = numeral (Num.BitM k)"
  "epred_numeral (num.Bit1 k) = numeral (num.Bit0 k)"
by(simp_all add: epred_numeral_def enat_numeral zero_enat_def)

lemma [simp]:
  shows eq_numeral_eSuc: "numeral k = eSuc n ⟷ epred_numeral k = n"
  and Suc_eq_numeral: "eSuc n = numeral k ⟷ n = epred_numeral k"
  and less_numeral_Suc: "numeral k < eSuc n ⟷ epred_numeral k < n"
  and less_eSuc_numeral: "eSuc n < numeral k ⟷ n < epred_numeral k"
  and le_numeral_eSuc: "numeral k ≤ eSuc n ⟷ epred_numeral k ≤ n"
  and le_eSuc_numeral: "eSuc n ≤ numeral k ⟷ n ≤ epred_numeral k"
  and diff_eSuc_numeral: "eSuc n - numeral k = n - epred_numeral k"
  and diff_numeral_eSuc: "numeral k - eSuc n = epred_numeral k - n"
  and max_eSuc_numeral: "max (eSuc n) (numeral k) = eSuc (max n (epred_numeral k))"
  and max_numeral_eSuc: "max (numeral k) (eSuc n) = eSuc (max (epred_numeral k) n)"
  and min_eSuc_numeral: "min (eSuc n) (numeral k) = eSuc (min n (epred_numeral k))"
  and min_numeral_eSuc: "min (numeral k) (eSuc n) = eSuc (min (epred_numeral k) n)"
by(simp_all add: numeral_eq_eSuc)

lemma enat_cocase_numeral [simp]:
  "co.case_enat a f (numeral v) = (let pv = epred_numeral v in f pv)"
by(simp add: numeral_eq_eSuc)

lemma enat_cocase_add_eq_if [simp]:
  "co.case_enat a f ((numeral v) + n) = (let pv = epred_numeral v in f (pv + n))"
by(simp add: numeral_eq_eSuc iadd_Suc)


lemma [simp]:
  shows epred_1: "epred 1 = 0"
  and epred_numeral: "epred (numeral i) = epred_numeral i"
  and epred_Infty: "epred ∞ = ∞"
  and epred_enat: "epred (enat m) = enat (m - 1)"
by(simp_all add: epred_conv_minus one_enat_def zero_enat_def eSuc_def epred_numeral_def numeral_eq_enat split: enat.split)

lemmas epred_simps = epred_0 epred_1 epred_numeral epred_eSuc epred_Infty epred_enat

lemma epred_iadd1: "a ≠ 0 ⟹ epred (a + b) = epred a + b"
apply(cases a b rule: enat.exhaust[case_product enat.exhaust])
apply(simp_all add: epred_conv_minus eSuc_def one_enat_def zero_enat_def split: enat.splits)
done

lemma epred_min [simp]: "epred (min a b) = min (epred a) (epred b)"
by(cases a b rule: enat_coexhaust[case_product enat_coexhaust]) simp_all

lemma epred_le_epredI: "n ≤ m ⟹ epred n ≤ epred m"
by(cases m n rule: enat_coexhaust[case_product enat_coexhaust]) simp_all

lemma epred_minus_epred [simp]:
  "m ≠ 0 ⟹ epred n - epred m = n - m"
by(cases n m rule: enat_coexhaust[case_product enat_coexhaust])(simp_all add: epred_conv_minus)

lemma eSuc_epred: "n ≠ 0 ⟹ eSuc (epred n) = n"
by(cases n rule: enat_coexhaust) simp_all

lemma epred_inject: "⟦ x ≠ 0; y ≠ 0 ⟧ ⟹ epred x = epred y ⟷ x = y"
by(cases x y rule: enat.exhaust[case_product enat.exhaust])(auto simp add: zero_enat_def)

lemma monotone_fun_eSuc[partial_function_mono]:
    "monotone (fun_ord (λy x. x ≤ y)) (λy x. x ≤ y) (λf. eSuc (f x))"
  by (auto simp: monotone_def fun_ord_def)

partial_function (gfp) enat_unfold :: "('a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ enat" where
  enat_unfold [code, nitpick_simp]:
  "enat_unfold stop next a = (if stop a then 0 else eSuc (enat_unfold stop next (next a)))"

lemma enat_unfold_stop [simp]: "stop a ⟹ enat_unfold stop next a = 0"
by(simp add: enat_unfold)

lemma enat_unfold_next: "¬ stop a ⟹ enat_unfold stop next a = eSuc (enat_unfold stop next (next a))"
by(simp add: enat_unfold)

lemma enat_unfold_eq_0 [simp]:
  "enat_unfold stop next a = 0 ⟷ stop a"
by(simp add: enat_unfold)

lemma epred_enat_unfold [simp]:
  "epred (enat_unfold stop next a) = (if stop a then 0 else enat_unfold stop next (next a))"
by(simp add: enat_unfold_next)

lemma epred_max: "epred (max x y) = max (epred x) (epred y)"
by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all

lemma epred_Max:
  assumes "finite A" "A ≠ {}"
  shows "epred (Max A) = Max (epred ` A)"
using assms
proof induction
  case (insert x A)
  thus ?case by(cases "A = {}")(simp_all add: epred_max)
qed simp

lemma finite_imageD2: "⟦ finite (f ` A); inj_on f (A - B); finite B ⟧ ⟹ finite A"
by (metis Diff_subset finite_Diff2 image_mono inj_on_finite)

lemma epred_Sup: "epred (Sup A) = Sup (epred ` A)"
by(auto 4 4 simp add: bot_enat_def Sup_enat_def epred_Max inj_on_def neq_zero_conv_eSuc dest: finite_imageD2[where B="{0}"])


subsection ‹Less as greatest fixpoint›

coinductive_set Le_enat :: "(enat × enat) set"
where
  Le_enat_zero: "(0, n) ∈ Le_enat"
| Le_enat_add: "⟦ (m, n) ∈ Le_enat; k ≠ 0 ⟧ ⟹ (eSuc m, n + k) ∈ Le_enat"

lemma ile_into_Le_enat:
  "m ≤ n ⟹ (m, n) ∈ Le_enat"
proof -
  assume "m ≤ n"
  hence "(m, n) ∈ {(m, n)|m n. m ≤ n}" by simp
  thus ?thesis
  proof coinduct
    case (Le_enat m n)
    hence "m ≤ n" by simp
    show ?case
    proof(cases "m = 0")
      case True
      hence ?Le_enat_zero by simp
      thus ?thesis ..
    next
      case False
      with ‹m ≤ n› obtain m' n' where "m = eSuc m'" "n = n' + 1" "m' ≤ n'"
        by(cases m rule: enat_coexhaust, simp)
          (cases n rule: enat_coexhaust, auto simp add: eSuc_plus_1[symmetric])
      hence ?Le_enat_add by fastforce
      thus ?thesis ..
    qed
  qed
qed

lemma Le_enat_imp_ile_enat_k:
  "(m, n) ∈ Le_enat ⟹ n < enat l ⟹ m < enat l"
proof(induct l arbitrary: m n)
  case 0
  thus ?case by(simp add: zero_enat_def[symmetric])
next
  case (Suc l)
  from ‹(m, n) ∈ Le_enat› show ?case
  proof cases
    case Le_enat_zero
    with ‹n < enat (Suc l)› show ?thesis by auto
  next
    case (Le_enat_add M N K)
    from ‹n = N + K› ‹n < enat (Suc l)› ‹K ≠ 0›
    have "N < enat l" by(cases N)(cases K, auto simp add: zero_enat_def)
    with ‹(M, N) ∈ Le_enat› have "M < enat l" by(rule Suc)
    with ‹m = eSuc M› show ?thesis by(simp add: eSuc_enat[symmetric])
  qed
qed

lemma enat_less_imp_le:
  assumes k: "!!k. n < enat k ⟹ m < enat k"
  shows "m ≤ n"
proof(cases n)
  case (enat n')
  with k[of "Suc n'"] show ?thesis by(cases m) simp_all
qed simp

lemma Le_enat_imp_ile:
  "(m, n) ∈ Le_enat ⟹ m ≤ n"
by(rule enat_less_imp_le)(erule Le_enat_imp_ile_enat_k)

lemma Le_enat_eq_ile:
  "(m, n) ∈ Le_enat ⟷ m ≤ n"
by(blast intro: Le_enat_imp_ile ile_into_Le_enat)

lemma enat_leI [consumes 1, case_names Leenat, case_conclusion Leenat zero eSuc]:
  assumes major: "(m, n) ∈ X"
  and step:
    "⋀m n. (m, n) ∈ X 
     ⟹ m = 0 ∨ (∃m' n' k. m = eSuc m' ∧ n = n' + enat k ∧ k ≠ 0 ∧
                           ((m', n') ∈ X ∨ m' ≤ n'))"
  shows "m ≤ n"
apply(rule Le_enat.coinduct[unfolded Le_enat_eq_ile, where X="λx y. (x, y) ∈ X"])
apply(fastforce simp add: zero_enat_def dest: step intro: major)+
done

lemma enat_le_coinduct[consumes 1, case_names le, case_conclusion le 0 eSuc]:
  assumes P: "P m n"
  and step:
    "⋀m n. P m n 
     ⟹ (n = 0 ⟶ m = 0) ∧
         (m ≠ 0 ⟶ n ≠ 0 ⟶ (∃k n'. P (epred m) n' ∧ epred n = n' + k) ∨ epred m ≤ epred n)"
  shows "m ≤ n"
proof -
  from P have "(m, n) ∈ {(m, n). P m n}" by simp
  thus ?thesis
  proof(coinduct rule: enat_leI)
    case (Leenat m n)
    hence "P m n" by simp
    show ?case
    proof(cases m rule: enat_coexhaust)
      case 0 
      thus ?thesis by simp
    next
      case (eSuc m')
      with step[OF ‹P m n›]
      have "n ≠ 0" and disj: "(∃k n'. P m' n' ∧ epred n = n' + k) ∨ m' ≤ epred n" by auto
      from ‹n ≠ 0› obtain n' where n': "n = eSuc n'"
        by(cases n rule: enat_coexhaust) auto
      from disj show ?thesis
      proof
        assume "m' ≤ epred n"
        with eSuc n' show ?thesis 
          by(auto 4 3 intro: exI[where x="Suc 0"] simp add: eSuc_enat[symmetric] iadd_Suc_right zero_enat_def[symmetric])
      next
        assume "∃k n'. P m' n' ∧ epred n = n' + k"
        then obtain k n'' where n'': "epred n = n'' + k" and k: "P m' n''" by blast
        show ?thesis using eSuc k n' n''
          by(cases k)(auto 4 3 simp add: iadd_Suc_right[symmetric] eSuc_enat intro: exI[where x=∞])
      qed
    qed
  qed
qed

subsection ‹Equality as greatest fixpoint›

lemma enat_equalityI [consumes 1, case_names Eq_enat,
                                  case_conclusion Eq_enat zero eSuc]:
  assumes major: "(m, n) ∈ X"
  and step:
    "⋀m n. (m, n) ∈ X
     ⟹ m = 0 ∧ n = 0 ∨ (∃m' n'. m = eSuc m' ∧ n = eSuc n' ∧ ((m', n') ∈ X ∨ m' = n'))"
  shows "m = n"
proof(rule antisym)
  from major show "m ≤ n"
    by(coinduct rule: enat_leI)
      (drule step, auto simp add: eSuc_plus_1 enat_1[symmetric])

  from major have "(n, m) ∈ {(n, m). (m, n) ∈ X}" by simp
  thus "n ≤ m"
  proof(coinduct rule: enat_leI)
    case (Leenat n m)
    hence "(m, n) ∈ X" by simp
    from step[OF this] show ?case
      by(auto simp add: eSuc_plus_1 enat_1[symmetric])
  qed
qed

lemma enat_coinduct [consumes 1, case_names Eq_enat, case_conclusion Eq_enat zero eSuc]:
  assumes major: "P m n"
  and step: "⋀m n. P m n 
    ⟹ (m = 0 ⟷ n = 0) ∧
       (m ≠ 0 ⟶ n ≠ 0 ⟶ P (epred m) (epred n) ∨ epred m = epred n)"
  shows "m = n"
proof -
  from major have "(m, n) ∈ {(m, n). P m n}" by simp
  thus ?thesis
  proof(coinduct rule: enat_equalityI)
    case (Eq_enat m n)
    hence "P m n" by simp
    from step[OF this] show ?case
      by(cases m n rule: enat_coexhaust[case_product enat_coexhaust]) auto
  qed
qed

lemma enat_coinduct2 [consumes 1, case_names zero eSuc]:
  "⟦ P m n; ⋀m n. P m n ⟹ m = 0 ⟷ n = 0; 
     ⋀m n. ⟦ P m n; m ≠ 0; n ≠ 0 ⟧ ⟹ P (epred m) (epred n) ∨ epred m = epred n ⟧
  ⟹ m = n"
by(erule enat_coinduct) blast

subsection ‹Uniqueness of corecursion›

lemma enat_unfold_unique:
  assumes h: "!!x. h x = (if stop x then 0 else eSuc (h (next x)))"
  shows "h x = enat_unfold stop next x"
by(coinduction arbitrary: x rule: enat_coinduct)(subst (1 3) h, auto)

subsection ‹Setup for partial\_function›

lemma enat_diff_cancel_left: "⟦ m ≤ x; m ≤ y ⟧ ⟹ x - m = y - m ⟷ x = (y :: enat)"
by(cases x y m rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]])(simp_all, arith)

lemma finite_lessThan_enatI: 
  assumes "m ≠ ∞"
  shows "finite {..<m :: enat}"
proof -
  from assms obtain m' where m: "m = enat m'" by auto
  have "{..<enat m'} ⊆ enat ` {..<m'}"
    by(rule subsetI)(case_tac x, auto)
  thus ?thesis unfolding m by(rule finite_subset) simp
qed

lemma infinite_lessThan_infty: "¬ finite {..<∞ :: enat}"
proof
  have "range enat ⊆ {..<∞}" by auto
  moreover assume "finite {..<∞ :: enat}"
  ultimately have "finite (range enat)" by(rule finite_subset)
  hence "finite (UNIV :: nat set)"
    by(rule finite_imageD)(simp add: inj_on_def)
  thus False by simp
qed

lemma finite_lessThan_enat_iff:
  "finite {..<m :: enat} ⟷ m ≠ ∞"
by(cases m)(auto intro: finite_lessThan_enatI simp add: infinite_lessThan_infty)

lemma enat_minus_mono1: "x ≤ y ⟹ x - m ≤ y - (m :: enat)"
by(cases m x y rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]]) simp_all

lemma max_enat_minus1: "max n m - k = max (n - k) (m - k :: enat)"
by(cases n m k rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]]) simp_all

lemma Max_enat_minus1:
  assumes "finite A" "A ≠ {}"
  shows "Max A - m = Max ((λn :: enat. n - m) ` A)"
using assms proof induct
  case (insert x A)
  thus ?case by(cases "A = {}")(simp_all add: max_enat_minus1)
qed simp

lemma Sup_enat_minus1: 
  assumes "m ≠ ∞"
  shows "⨆A - m = ⨆((λn :: enat. n - m) ` A)"
proof -
  from assms obtain m' where "m = enat m'" by auto
  thus ?thesis
    by(auto simp add: Sup_enat_def Max_enat_minus1 finite_lessThan_enat_iff enat_diff_cancel_left inj_on_def dest!: finite_imageD2[where B="{..<enat m'}"])
qed

lemma Sup_image_eadd1:
  assumes "Y ≠ {}"
  shows "Sup ((λy :: enat. y+x) ` Y) = Sup Y + x"
proof(cases "finite Y")
  case True
  thus ?thesis by(simp add: Sup_enat_def Max_add_commute assms)
next
  case False
  thus ?thesis
  proof(cases x)
    case (enat x')
    hence "¬ finite ((λy. y+x) ` Y)" using False
      by(auto dest!: finite_imageD intro: inj_onI)
    with False show ?thesis by(simp add: Sup_enat_def assms)
  next
    case infinity
    hence "(+) x ` Y = {∞}" using assms by auto
    thus ?thesis using infinity by(simp add: image_constant_conv assms)
  qed
qed

lemma Sup_image_eadd2:
  "Y ≠ {} ⟹ Sup ((λy :: enat. x + y) ` Y) = x + Sup Y"
by(simp add: Sup_image_eadd1 add.commute)

lemma mono2mono_eSuc [THEN lfp.mono2mono, cont_intro, simp]:
  shows monotone_eSuc: "monotone (≤) (≤) eSuc"
by(rule monotoneI) simp

lemma mcont2mcont_eSuc [THEN lfp.mcont2mcont, cont_intro, simp]:
  shows mcont_eSuc: "mcont Sup (≤) Sup (≤) eSuc"
by(intro mcontI contI)(simp_all add: monotone_eSuc eSuc_Sup)

lemma mono2mono_epred [THEN lfp.mono2mono, cont_intro, simp]:
  shows monotone_epred: "monotone (≤) (≤) epred"
by(rule monotoneI)(simp add: epred_le_epredI)

lemma mcont2mcont_epred [THEN lfp.mcont2mcont, cont_intro, simp]:
  shows mcont_epred: "mcont Sup (≤) Sup (≤) epred"
by(simp add: mcont_def monotone_epred cont_def epred_Sup)

lemma enat_cocase_mono [partial_function_mono, cont_intro]: 
  "⟦ monotone orda ordb zero; ⋀n. monotone orda ordb (λf. esuc f n) ⟧
  ⟹ monotone orda ordb (λf. co.case_enat (zero f) (esuc f) x)"
by(cases x rule: co.enat.exhaust) simp_all

lemma enat_cocase_mcont [cont_intro, simp]:
  "⟦ mcont luba orda lubb ordb zero; ⋀n. mcont luba orda lubb ordb (λf. esuc f n) ⟧
  ⟹ mcont luba orda lubb ordb (λf. co.case_enat (zero f) (esuc f) x)"
by(cases x rule: co.enat.exhaust) simp_all

lemma eSuc_mono [partial_function_mono]:
  "monotone (fun_ord (≤)) (≤) f ⟹ monotone (fun_ord (≤)) (≤) (λx. eSuc (f x))"
by(rule mono2mono_eSuc)

lemma mono2mono_enat_minus1 [THEN lfp.mono2mono, cont_intro, simp]:
  shows monotone_enat_minus1: "monotone (≤) (≤) (λn. n - m :: enat)"
by(rule monotoneI)(rule enat_minus_mono1)

lemma mcont2mcont_enat_minus [THEN lfp.mcont2mcont, cont_intro, simp]:
  shows mcont_enat_minus: "m ≠ ∞ ⟹ mcont Sup (≤) Sup (≤) (λn. n - m :: enat)"
by(rule mcontI)(simp_all add: monotone_enat_minus1 contI Sup_enat_minus1)

lemma monotone_eadd1: "monotone (≤) (≤) (λx. x + y :: enat)"
by(auto intro!: monotoneI)

lemma monotone_eadd2: "monotone (≤) (≤) (λy. x + y :: enat)"
by(auto intro!: monotoneI)

lemma mono2mono_eadd[THEN lfp.mono2mono2, cont_intro, simp]:
  shows monotone_eadd: "monotone (rel_prod (≤) (≤)) (≤) (λ(x, y). x + y :: enat)"
by(simp add: monotone_eadd1 monotone_eadd2)

lemma mcont_eadd2: "mcont Sup (≤) Sup (≤) (λy. x + y :: enat)"
by(auto intro: mcontI monotone_eadd2 contI Sup_image_eadd2[symmetric])

lemma mcont_eadd1: "mcont Sup (≤) Sup (≤) (λx. x + y :: enat)"
by(auto intro: mcontI monotone_eadd1 contI Sup_image_eadd1[symmetric])

lemma mcont2mcont_eadd [cont_intro, simp]:
  "⟦ mcont lub ord Sup (≤) (λx. f x);
    mcont lub ord Sup (≤) (λx. g x) ⟧
  ⟹ mcont lub ord Sup (≤) (λx. f x + g x :: enat)"
by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_eadd1 mcont_eadd2 ccpo.mcont_const[OF complete_lattice_ccpo])

lemma eadd_partial_function_mono [partial_function_mono]:
  "⟦ monotone (fun_ord (≤)) (≤) f; monotone (fun_ord (≤)) (≤) g ⟧
  ⟹ monotone (fun_ord (≤)) (≤) (λx. f x + g x :: enat)"
by(rule mono2mono_eadd)

lemma monotone_max_enat1: "monotone (≤) (≤) (λx. max x y :: enat)"
by(auto intro!: monotoneI simp add: max_def)

lemma monotone_max_enat2: "monotone (≤) (≤) (λy. max x y :: enat)"
by(auto intro!: monotoneI simp add: max_def)

lemma mono2mono_max_enat[THEN lfp.mono2mono2, cont_intro, simp]:
  shows monotone_max_enat: "monotone (rel_prod (≤) (≤)) (≤) (λ(x, y). max x y :: enat)"
by(simp add: monotone_max_enat1 monotone_max_enat2)

lemma max_Sup_enat2:
  assumes "Y ≠ {}"
  shows "max x (Sup Y) = Sup ((λy :: enat. max x y) ` Y)"
proof(cases "finite Y")
  case True
  hence "max x (Max Y) = Max (max x ` Y)" using assms
  proof(induct)
    case (insert y Y)
    thus ?case
      by(cases "Y = {}")(simp_all, metis max.assoc max.left_commute max.left_idem)
  qed simp
  thus ?thesis using True by(simp add: Sup_enat_def assms)
next
  case False
  show ?thesis
  proof(cases x)
    case infinity
    hence "max x ` Y = {∞}" using assms by auto
    thus ?thesis using False by(simp add: Sup_enat_def assms)
  next
    case (enat x')
    { assume "finite (max x ` Y)"
      hence "finite (max x ` {y ∈ Y. y > x})"
        by (rule rev_finite_subset) (auto simp add: image_iff dest: max.absorb4 sym)
      hence "finite {y ∈ Y. y > x}"
        by(rule finite_imageD)(auto intro!: inj_onI simp add: max_def split: if_split_asm)
      moreover have "finite {y ∈ Y. y ≤ x}"
        by(rule finite_enat_bounded)(auto simp add: enat)
      ultimately have "finite ({y ∈ Y. y > x} ∪ {y ∈ Y. y ≤ x})" by simp
      also have "{y ∈ Y. y > x} ∪ {y ∈ Y. y ≤ x} = Y" by auto
      finally have "finite Y" . }
    thus ?thesis using False by(auto simp add: Sup_enat_def assms)
  qed
qed

lemma max_Sup_enat1:
  "Y ≠ {} ⟹ max (Sup Y) x = Sup ((λy :: enat. max y x) ` Y)"
by(subst (1 2) max.commute)(rule max_Sup_enat2)

lemma mcont_max_enat1: "mcont Sup (≤) Sup (≤) (λx. max x y :: enat)"
by(auto intro!: mcontI contI max_Sup_enat1 simp add: monotone_max_enat1)

lemma mcont_max_enat2: "mcont Sup (≤) Sup (≤) (λy. max x y :: enat)"
by(auto intro!: mcontI contI max_Sup_enat2 simp add: monotone_max_enat2)

lemma mcont2mcont_max_enat [cont_intro, simp]:
  "⟦ mcont lub ord Sup (≤) (λx. f x);
    mcont lub ord Sup (≤) (λx. g x) ⟧
  ⟹ mcont lub ord Sup (≤) (λx. max (f x) (g x) :: enat)"
by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_max_enat1 mcont_max_enat2 ccpo.mcont_const[OF complete_lattice_ccpo])

lemma max_enat_partial_function_mono [partial_function_mono]:
  "⟦ monotone (fun_ord (≤)) (≤) f; monotone (fun_ord (≤)) (≤) g ⟧
  ⟹ monotone (fun_ord (≤)) (≤) (λx. max (f x) (g x) :: enat)"
by(rule mono2mono_max_enat)

lemma chain_epredI:
  "Complete_Partial_Order.chain (≤) Y
  ⟹ Complete_Partial_Order.chain (≤) (epred ` (Y ∩ {x. x ≠ 0}))"
by(auto intro: chainI dest: chainD)

lemma monotone_enat_le_case:
  fixes bot
  assumes mono: "monotone (≤) ord (λx. f x (eSuc x))"
  and ord: "⋀x. ord bot (f x (eSuc x))"
  and bot: "ord bot bot"
  shows "monotone (≤) ord (λx. case x of 0 ⇒ bot | eSuc x' ⇒ f x' x)"
proof -
  have "monotone (≤) ord (λx. if x ≤ 0 then bot else f (epred x) x)"
  proof(rule monotone_if_bot)
    fix x y :: enat
    assume "x ≤ y" "¬ x ≤ 0"
    thus "ord (f (epred x) x) (f (epred y) y)"
      by(cases x y rule: co.enat.exhaust[case_product co.enat.exhaust])(auto intro: monotoneD[OF mono])
  next
    fix x :: enat
    assume "¬ x ≤ 0"
    thus "ord bot (f (epred x) x)"
      by(cases x rule: co.enat.exhaust)(auto intro: ord)
  qed(rule bot)
  also have "(λx. if x ≤ 0 then bot else f (epred x) x) = (λx. case x of 0 ⇒ bot | eSuc x' ⇒ f x' x)"
    by(auto simp add: fun_eq_iff split: co.enat.split)
  finally show ?thesis .
qed

lemma mcont_enat_le_case:
  fixes bot
  assumes ccpo: "class.ccpo lub ord (mk_less ord)"
  and mcont: "mcont Sup (≤) lub ord (λx. f x (eSuc x))"
  and ord: "⋀x. ord bot (f x (eSuc x))"
  shows "mcont Sup (≤) lub ord (λx. case x of 0 ⇒ bot | eSuc x' ⇒ f x' x)"
proof -
  from ccpo
  have "mcont Sup (≤) lub ord (λx. if x ≤ 0 then bot else f (epred x) x)"
  proof(rule mcont_if_bot)
    fix x y :: enat
    assume "x ≤ y" "¬ x ≤ 0"
    thus "ord (f (epred x) x) (f (epred y) y)"
      by(cases x y rule: co.enat.exhaust[case_product co.enat.exhaust])(auto intro: mcont_monoD[OF mcont])
  next
    fix Y :: "enat set"
    assume chain: "Complete_Partial_Order.chain (≤) Y"
      and Y: "Y ≠ {}" "⋀x. x ∈ Y ⟹ ¬ x ≤ 0"
    from Y have Y': "Y ∩ {x. x ≠ 0} ≠ {}" by auto
    from Y(2) have eq: "Y = eSuc ` (epred ` (Y ∩ {x. x ≠ 0}))"
      by(fastforce intro: rev_image_eqI)
    let ?Y = "epred ` (Y ∩ {x. x ≠ 0})"
    from chain_epredI [OF chain] Y'
    have "f (⨆?Y) (eSuc (⨆?Y)) = lub ((λx. f x (eSuc x)) ` ?Y)"
      using mcont [THEN mcont_contD] by blast
    moreover from chain_epredI [OF chain] Y'
      have "⨆(eSuc ` ?Y) = eSuc (⨆?Y)"
      using mcont_eSuc [THEN mcont_contD, symmetric] by blast
    ultimately show "f (epred (Sup Y)) (Sup Y) = lub ((λx. f (epred x) x) ` Y)"
      by (subst (1 2 3) eq) (simp add: image_image)
  next
    fix x :: enat
    assume "¬ x ≤ 0"
    thus "ord bot (f (epred x) x)"
      by(cases x rule: co.enat.exhaust)(auto intro: ord)
  qed
  also have "(λx. if x ≤ 0 then bot else f (epred x) x) = (λx. case x of 0 ⇒ bot | eSuc x' ⇒ f x' x)"
    by(auto simp add: fun_eq_iff split: co.enat.split)
  finally show ?thesis .
qed


subsection ‹Misc.›

lemma enat_add_mono [simp]:
  "enat x + y < enat x + z ⟷ y < z"
by(cases y)(case_tac [!] z, simp_all)

lemma enat_add1_eq [simp]: "enat x + y = enat x + z ⟷ y = z"
by (metis enat_add_mono add.commute neq_iff)

lemma enat_add2_eq [simp]: "y + enat x = z + enat x ⟷ y = z"
by (metis enat_add1_eq add.commute)

lemma enat_less_enat_plusI: "x < y ⟹ enat x < enat y + z"
by(cases z) simp_all

lemma enat_less_enat_plusI2:
  "enat y < z ⟹ enat (x + y) < enat x + z"
by (metis enat_add_mono plus_enat_simps(1))

lemma min_enat1_conv_enat: "⋀a b. min (enat a) b = enat (case b of enat b' ⇒ min a b' | ∞ ⇒ a)"
  and min_enat2_conv_enat: "⋀a b. min a (enat b) = enat (case a of enat a' ⇒ min a' b | ∞ ⇒ b)"
by(simp_all split: enat.split)

lemma eSuc_le_iff: "eSuc x ≤ y ⟷ (∃y'. y = eSuc y' ∧ x ≤ y')"
by(cases y rule: co.enat.exhaust) simp_all

lemma eSuc_eq_infinity_iff: "eSuc n = ∞ ⟷ n = ∞"
by(cases n)(simp_all add: zero_enat_def eSuc_enat)

lemma infinity_eq_eSuc_iff: "∞ = eSuc n ⟷ n = ∞"
by(cases n)(simp_all add: zero_enat_def eSuc_enat)

lemma enat_cocase_inf: "(case ∞ of 0 ⇒ a | eSuc b ⇒ f b) = f ∞"
by(auto split: co.enat.split simp add: infinity_eq_eSuc_iff)

lemma eSuc_Inf: "eSuc (Inf A) = Inf (eSuc ` A)"
proof -
  { assume "A ≠ {}"
    then obtain a where "a ∈ A" by blast
    then have "eSuc (LEAST a. a ∈ A) = (LEAST a. a ∈ eSuc ` A)"
    proof (rule LeastI2_wellorder)
      fix a assume "a ∈ A" and b: "∀b. b ∈ A ⟶ a ≤ b"
      then have a: "eSuc a ∈ eSuc ` A"
        by auto
      then show "eSuc a = (LEAST a. a ∈ eSuc ` A)"
        by (rule LeastI2_wellorder) (metis (full_types) b a antisym eSuc_le_iff imageE)
    qed }
  then show ?thesis
    by (simp add: Inf_enat_def)
qed

end