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