# Theory CCPO_Extensions

```section ‹Chain-Complete Partial Orders›

theory CCPO_Extensions
imports
"HOL-Library.Complete_Partial_Order2"
ENat_Extensions
Set_Extensions
begin

lemma chain_split[dest]:
assumes "Complete_Partial_Order.chain ord C" "x ∈ C"
shows "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}"
proof -
have 1: "⋀ y. y ∈ C ⟹ ord x y ∨ ord y x" using chainD assms by this
show ?thesis using 1 by blast
qed

lemma infinite_chain_below[dest]:
assumes "Complete_Partial_Order.chain ord C" "infinite C" "x ∈ C"
assumes "finite {y ∈ C. ord x y}"
shows "infinite {y ∈ C. ord y x}"
proof -
have 1: "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" using assms(1, 3) by rule
show ?thesis using finite_Un assms(2, 4) 1 by (metis (poly_guards_query))
qed
lemma infinite_chain_above[dest]:
assumes "Complete_Partial_Order.chain ord C" "infinite C" "x ∈ C"
assumes "finite {y ∈ C. ord y x}"
shows "infinite {y ∈ C. ord x y}"
proof -
have 1: "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" using assms(1, 3) by rule
show ?thesis using finite_Un assms(2, 4) 1 by (metis (poly_guards_query))
qed

lemma (in ccpo) ccpo_Sup_upper_inv:
assumes "Complete_Partial_Order.chain less_eq C" "x > ⨆ C"
shows "x ∉ C"
using assms ccpo_Sup_upper by fastforce
lemma (in ccpo) ccpo_Sup_least_inv:
assumes "Complete_Partial_Order.chain less_eq C" "⨆ C > x"
obtains y
where "y ∈ C" "¬ y ≤ x"
using assms ccpo_Sup_least that by fastforce

lemma ccpo_Sup_least_inv':
fixes C :: "'a :: {ccpo, linorder} set"
assumes "Complete_Partial_Order.chain less_eq C" "⨆ C > x"
obtains y
where "y ∈ C" "y > x"
proof -
obtain y where 1: "y ∈ C" "¬ y ≤ x" using ccpo_Sup_least_inv assms by this
show ?thesis using that 1 by simp
qed

lemma mcont2mcont_lessThan[THEN lfp.mcont2mcont, simp, cont_intro]:
shows mcont_lessThan: "mcont Sup less_eq Sup less_eq
(lessThan :: 'a :: {ccpo, linorder} ⇒ 'a set)"
proof
show "monotone less_eq less_eq (lessThan :: 'a ⇒ 'a set)" by (rule, auto)
show "cont Sup less_eq Sup less_eq (lessThan :: 'a ⇒ 'a set)"
proof
fix C :: "'a set"
assume 1: "Complete_Partial_Order.chain less_eq C"
show "{..< ⨆ C} = ⋃ (lessThan ` C)"
proof (intro equalityI subsetI)
fix A
assume 2: "A ∈ {..< ⨆ C}"
obtain B where 3: "B ∈ C" "B > A" using ccpo_Sup_least_inv' 1 2 by blast
show "A ∈ ⋃ (lessThan ` C)" using 3 by auto
next
fix A
assume 2: "A ∈ ⋃ (lessThan ` C)"
show "A ∈ {..< ⨆ C}" using ccpo_Sup_upper 2 by force
qed
qed
qed

class esize =
fixes esize :: "'a ⇒ enat"

class esize_order = esize + order +
assumes esize_finite[dest]: "esize x ≠ ∞ ⟹ finite {y. y ≤ x}"
assumes esize_mono[intro]: "x ≤ y ⟹ esize x ≤ esize y"
assumes esize_strict_mono[intro]: "esize x ≠ ∞ ⟹ x < y ⟹ esize x < esize y"
begin

lemma infinite_chain_eSuc_esize[dest]:
assumes "Complete_Partial_Order.chain less_eq C" "infinite C" "x ∈ C"
obtains y
where "y ∈ C" "esize y ≥ eSuc (esize x)"
proof (cases "esize x")
case (enat k)
have 1: "finite {y ∈ C. y ≤ x}" using esize_finite enat by simp
have 2: "infinite {y ∈ C. y ≥ x}" using assms 1 by rule
have 3: "{y ∈ C. y > x} = {y ∈ C. y ≥ x} - {x}" by auto
have 4: "infinite {y ∈ C. y > x}" using 2 unfolding 3 by simp
obtain y where 5: "y ∈ C" "y > x" using 4 by auto
have 6: "esize y > esize x" using esize_strict_mono enat 5(2) by blast
show ?thesis using that 5(1) 6 ileI1 by simp
next
case (infinity)
show ?thesis using that infinity assms(3) by simp
qed

lemma infinite_chain_arbitrary_esize[dest]:
assumes "Complete_Partial_Order.chain less_eq C" "infinite C"
obtains x
where "x ∈ C" "esize x ≥ enat n"
proof (induct n arbitrary: thesis)
case 0
show ?case using assms(2) 0 by force
next
case (Suc n)
obtain x where 1: "x ∈ C" "esize x ≥ enat n" using Suc(1) by blast
obtain y where 2: "y ∈ C" "esize y ≥ eSuc (esize x)" using assms 1(1) by rule
show ?case using gfp.leq_trans Suc(2) 1(2) 2 by fastforce
qed

end

class esize_ccpo = esize_order + ccpo
begin

lemma esize_cont[dest]:
assumes "Complete_Partial_Order.chain less_eq C" "C ≠ {}"
shows "esize (⨆ C) = ⨆ (esize ` C)"
proof (cases "finite C")
case False
have 1: "esize (⨆ C) = ∞"
proof
fix n
obtain A where 1: "A ∈ C" "esize A ≥ enat n" using assms(1) False by rule
have 2: "A ≤ ⨆ C" using ccpo_Sup_upper assms(1) 1(1) by this
have "enat n ≤ esize A" using 1(2) by this
also have "… ≤ esize (⨆ C)" using 2 by rule
finally show "enat n ≤ esize (⨆ C)" by this
qed
have 2: "(⨆ A ∈ C. esize A) = ∞"
proof
fix n
obtain A where 1: "A ∈ C" "esize A ≥ enat n" using assms(1) False by rule
show "enat n ≤ (⨆ A ∈ C. esize A)" using SUP_upper2 1 by this
qed
show ?thesis using 1 2 by simp
next
case True
have 1: "esize (⨆ C) = (⨆ x ∈ C. esize x)"
proof (intro order_class.order.antisym SUP_upper SUP_least esize_mono)
show "⨆ C ∈ C" using in_chain_finite assms(1) True assms(2) by this
show "⋀ x. x ∈ C ⟹ x ≤ ⨆ C" using ccpo_Sup_upper assms(1) by this
qed
show ?thesis using 1 by simp
qed

lemma esize_mcont: "mcont Sup less_eq Sup less_eq esize"
by (blast intro: mcontI monotoneI contI)

lemmas mcont2mcont_esize = esize_mcont[THEN lfp.mcont2mcont, simp, cont_intro]

end

end
```