Theory C

theory C
imports HOLCF "Mono-Nat-Fun"
begin

default_sort cpo

text ‹
The initial solution to the domain equation $C = C_\bot$, i.e. the completion of the natural numbers.
›

domain C = C (lazy "C")

lemma below_C: "x ⊑ C⋅x"
  by (induct x) auto

definition Cinf (‹C⇧∞›) where "C⇧∞ = fix⋅C"

lemma C_Cinf[simp]: "C⋅C⇧∞ = C⇧∞" unfolding Cinf_def by (rule fix_eq[symmetric])

abbreviation Cpow (‹C⇗_⇖›) where "C⇗n⇖ ≡ iterate n⋅C⋅⊥"

lemma C_below_C[simp]: "(C⇗i⇖ ⊑ C⇗j⇖) ⟷ i ≤ j"
  apply (induction i arbitrary: j)
  apply simp
  apply (case_tac j, auto)
  done

lemma below_Cinf[simp]: "r ⊑ C⇧∞"
  apply (induct r)
  apply simp_all[2]
  apply (metis (full_types) C_Cinf monofun_cfun_arg)
  done

lemma C_eq_Cinf[simp]: "C⇗i⇖ ≠ C⇧∞"
  by (metis C_below_C Suc_n_not_le_n below_Cinf)

lemma Cinf_eq_C[simp]: "C⇧∞ = C ⋅ r ⟷ C⇧∞ = r"
  by (metis C.injects C_Cinf)

lemma C_eq_C[simp]: "(C⇗i⇖ = C⇗j⇖) ⟷ i = j"
  by (metis C_below_C le_antisym le_refl)

lemma case_of_C_below: "(case r of C⋅y ⇒ x) ⊑ x"
  by (cases r) auto

lemma C_case_below: "C_case ⋅ f ⊑ f"
  by (metis cfun_belowI C.case_rews(2) below_C monofun_cfun_arg)

lemma C_case_bot[simp]: "C_case ⋅ ⊥ = ⊥"
  apply (subst eq_bottom_iff)
  apply (rule C_case_below)
  done

lemma C_case_cong:
  assumes "⋀ r'. r = C⋅r' ⟹ f⋅r' = g⋅r'"
  shows "C_case⋅f⋅r = C_case⋅g⋅r"
using assms by (cases r) auto


lemma C_cases:
  obtains n where "r = C⇗n⇖" | "r = C⇧∞"
proof-
  { fix m
    have "∃ n. C_take m ⋅ r = C⇗n⇖ "
    proof (rule C.finite_induct)
      have "⊥ = C⇗0⇖" by simp
      thus "∃n. ⊥ = C⇗n⇖"..
    next
      fix r
      show "∃n. r = C⇗n⇖ ⟹ ∃n. C⋅r = C⇗n⇖"
        by (auto simp del: iterate_Suc simp add: iterate_Suc[symmetric])
    qed
  }
  then obtain f where take: "⋀ m. C_take m ⋅ r = C⇗f m⇖" by metis
  have "chain (λ m. C⇗f m⇖)" using ch2ch_Rep_cfunL[OF C.chain_take, where x=r, unfolded take].
  hence "mono f" by (auto simp add: mono_iff_le_Suc chain_def elim!:chainE)
  have r: "r = (⨆ m. C⇗f m⇖)"  by (metis (lifting) take C.reach lub_eq)
  from ‹mono f›
  show thesis
  proof(rule nat_mono_characterization)
    fix n
    assume n: "⋀ m. n ≤ m ==> f n = f m"
    have "max_in_chain n (λ m. C⇗f m⇖)"
      apply (rule max_in_chainI)
      apply simp
      apply (erule n)
      done
    hence "(⨆ m. C⇗f m⇖) = C⇗f n⇖" unfolding  maxinch_is_thelub[OF ‹chain _›].
    thus ?thesis using that unfolding r by blast
  next
    assume "⋀m. ∃n. m ≤ f n"
    hence "⋀ n. C⇗n⇖ ⊑ r" unfolding r by (fastforce intro: below_lub[OF ‹chain _›])
    hence "(⨆ n. C⇗n⇖) ⊑ r" 
      by (rule lub_below[OF chain_iterate])
    hence "C⇧∞ ⊑ r" unfolding Cinf_def fix_def2.
    hence "C⇧∞ = r" using below_Cinf by (metis below_antisym)
    thus thesis using that by blast
  qed
qed


lemma C_case_Cinf[simp]: "C_case ⋅ f ⋅ C⇧∞ = f ⋅ C⇧∞"
  unfolding Cinf_def
  by (subst fix_eq) simp

end