Quelle  C.thy

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

default_sort cpo

text ‹
  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^\<infinity> = fix⋅C"

lemma C_Cinf[simp]: "C⋅C^\<infinity> = C^\<infinity>" unfolding Cinf_def by (rule fix_eq[symmetric])

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

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

lemma below_Cinf[simp]: "r ⊑ C^\<infinity>"
  apply (induct r)
  apply simp_all[2]
  apply (metis (full_types) C_Cinf monofun_cfun_arg)
  done

lemma C_eq_Cinf[simp]: "C ≠ C^\<infinity>"
  by (metis C_below_C Suc_n_not_le_n below_Cinf)

lemma Cinf_eq_C[simp]: "C^\<infinity> = C ⋅ r ⟷ C^\<infinity> = r"
  by (metis C.injects C_Cinf)

lemma C_eq_C[simp]: "(C = C) ⟷ 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" | "r = C^\<infinity>"
proof-
  { fix m
    have "∃ n. C_take m ⋅ r = C "
    proof (rule C.finite_induct)
      have "⊥ = C" by simp
      thus "∃n. ⊥ = C"..
    next
      fix r
      show "∃n. r = C ==> ∃n. C⋅r = C"
        by (auto simp del: iterate_Suc simp add: iterate_Suc[symmetric])
    qed
  }
  then obtain f where take: "∧ m. C_take m ⋅ r = C ^m" by metis
  have "chain (λ m. C ^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 ^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 ^m)"
      apply (rule max_in_chainI)
      apply simp
      apply (erule n)
      done
    hence "(⊔ m. C ^m) = C ⁿ" unfolding  maxinch_is_thelub[OF ‹chain _›].
    thus ?thesis using that unfolding r by blast
  next
    assume "∧m. ∃n. m ≤ f n"
    hence "∧ n. C ⊑ r" unfolding r by (fastforce intro: below_lub[OF ‹chain _›])
    hence "(⊔ n. C) ⊑ r" 
      by (rule lub_below[OF chain_iterate])
    hence "C^\<infinity> ⊑ r" unfolding Cinf_def fix_def2.
    hence "C^\<infinity> = 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^\<infinity> = f ⋅ C^\<infinity>"
  unfolding Cinf_def
  by (subst fix_eq) simp

end