# Theory Coinductive_Nat

theory Coinductive_Nat
imports Extended_Nat Complete_Partial_Order2
```(*  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"

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

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"

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"

lemma the_enat_eSuc: "n ≠ ∞ ⟹ the_enat (eSuc n) = Suc (the_enat n)"

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)"

lemma case_enat_0 [simp]: "case_enat f i 0 = f 0"

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)"

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)"

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)"

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

"co.case_enat a f ((numeral v) + n) = (let pv = epred_numeral v in f (pv + n))"

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"

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

lemma enat_unfold_eq_0 [simp]:
"enat_unfold stop next a = 0 ⟷ stop a"

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

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])
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
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
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''
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
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)"
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

assumes "Y ≠ {}"
shows "Sup ((λy :: enat. y+x) ` Y) = Sup Y + x"
proof(cases "finite Y")
case True
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

"Y ≠ {} ⟹ Sup ((λy :: enat. x + y) ` Y) = x + Sup Y"

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"

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)

shows monotone_eadd: "monotone (rel_prod (≤) (≤)) (≤) (λ(x, y). x + y :: enat)"

lemma mcont_eadd2: "mcont Sup (≤) Sup (≤) (λy. x + y :: enat)"

lemma mcont_eadd1: "mcont Sup (≤) Sup (≤) (λx. x + y :: enat)"

"⟦ mcont lub ord Sup (≤) (λx. f x);
mcont lub ord Sup (≤) (λx. g x) ⟧
⟹ mcont lub ord Sup (≤) (λx. f x + g x :: enat)"

"⟦ monotone (fun_ord (≤)) (≤) f; monotone (fun_ord (≤)) (≤) g ⟧
⟹ monotone (fun_ord (≤)) (≤) (λx. f x + g x :: enat)"

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)"

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 finite_subset[rotated]) auto
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}"
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.›

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

lemma enat_add2_eq [simp]: "y + enat x = z + enat x ⟷ y = z"

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"

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 = ∞"

lemma infinity_eq_eSuc_iff: "∞ = eSuc n ⟷ n = ∞"

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