theory C imports "~~/src/HOL/HOLCF/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