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