theory "HOLCF-Utils" imports "~~/src/HOL/HOLCF/HOLCF" Pointwise begin default_sort type lemmas cont_fun[simp] lemmas cont2cont_fun[simp] lemma cont_compose2: assumes "⋀ y. cont (λ x. c x y)" assumes "⋀ x. cont (λ y. c x y)" assumes "cont f" assumes "cont g" shows "cont (λx. c (f x) (g x))" by (intro cont_apply[OF assms(4) assms(2)] cont2cont_fun[OF cont_compose[OF _ assms(3)]] cont2cont_lambda[OF assms(1)]) lemma pointwise_adm: fixes P :: "'a::pcpo ⇒ 'b::pcpo ⇒ bool" assumes "adm (λ x. P (fst x) (snd x))" shows "adm (λ m. pointwise P (fst m) (snd m))" proof (rule admI, goal_cases) case prems: (1 Y) show ?case apply (rule pointwiseI) apply (rule admD[OF adm_subst[where t = "λp . (fst p x, snd p x)" for x, OF _ assms, simplified] `chain Y`]) using prems(2) unfolding pointwise_def apply auto done qed lemma cfun_beta_Pair: assumes "cont (λ p. f (fst p) (snd p))" shows "csplit⋅(Λ a b . f a b)⋅(x, y) = f x y" apply simp apply (subst beta_cfun) apply (rule cont2cont_LAM') apply (rule assms) apply (rule beta_cfun) apply (rule cont2cont_fun) using assms unfolding prod_cont_iff apply auto done lemma fun_upd_mono: "ρ1 ⊑ ρ2 ⟹ v1 ⊑ v2 ⟹ ρ1(x := v1) ⊑ ρ2(x := v2)" apply (rule fun_belowI) apply (case_tac "xa = x") apply simp apply (auto elim:fun_belowD) done lemma fun_upd_cont[simp,cont2cont]: assumes "cont f" and "cont h" shows "cont (λ x. (f x)(v := h x) :: 'a ⇒ 'b::pcpo)" by (rule cont2cont_lambda)(auto simp add: assms) lemma fun_upd_belowI: assumes "⋀ z . z ≠ x ⟹ ρ z ⊑ ρ' z" assumes "y ⊑ ρ' x" shows "ρ(x := y) ⊑ ρ'" apply (rule fun_belowI) using assms apply (case_tac "xa = x") apply auto done lemma cont_if_else_above: assumes "cont f" assumes "cont g" assumes "⋀ x. f x ⊑ g x" assumes "⋀ x y. x ⊑ y ⟹ P y ⟹ P x" assumes "adm P" shows "cont (λx. if P x then f x else g x)" (is "cont ?I") proof(intro contI2 monofunI) fix x y :: 'a assume "x ⊑ y" with assms(4)[OF this] show "?I x ⊑ ?I y" apply (auto) apply (rule cont2monofunE[OF assms(1)], assumption) apply (rule below_trans[OF cont2monofunE[OF assms(1)] assms(3)], assumption) apply (rule cont2monofunE[OF assms(2)], assumption) done next fix Y :: "nat ⇒ 'a" assume "chain Y" assume "chain (λi . ?I (Y i))" have ch_f: "f (⨆ i. Y i) ⊑ (⨆ i. f (Y i))" by (metis `chain Y` assms(1) below_refl cont2contlubE) show "?I (⨆ i. Y i) ⊑ (⨆ i. ?I (Y i))" proof(cases "∀ i. P (Y i)") case True hence "P (⨆ i. Y i)" by (metis `chain Y` adm_def assms(5)) with True ch_f show ?thesis by auto next case False then obtain j where "¬ P (Y j)" by auto hence *: "∀ i ≥ j. ¬ P (Y i)" "¬ P (⨆ i. Y i)" apply (auto) apply (metis assms(4) chain_mono[OF `chain Y`]) apply (metis assms(4) is_ub_thelub[OF `chain Y`]) done have "?I (⨆ i. Y i) = g (⨆ i. Y i)" using * by simp also have "… = g (⨆ i. Y (i + j))" by (metis lub_range_shift[OF `chain Y`]) also have "… = (⨆ i. (g (Y (i + j))))" by (rule cont2contlubE[OF assms(2) chain_shift[OF `chain Y`]] ) also have "… = (⨆ i. (?I (Y (i + j))))" using * by auto also have "… = (⨆ i. (?I (Y i)))" by (metis lub_range_shift[OF `chain (λi . ?I (Y i))`]) finally show ?thesis by simp qed qed fun up2option :: "'a::cpo⇩⊥ ⇒ 'a option" where "up2option Ibottom = None" | "up2option (Iup a) = Some a" lemma up2option_simps[simp]: "up2option ⊥ = None" "up2option (up⋅x) = Some x" unfolding up_def by (simp_all add: cont_Iup inst_up_pcpo) fun option2up :: "'a option ⇒ 'a::cpo⇩⊥" where "option2up None = ⊥" | "option2up (Some a) = up⋅a" lemma option2up_up2option[simp]: "option2up (up2option x) = x" by (cases x) auto lemma up2option_option2up[simp]: "up2option (option2up x) = x" by (cases x) auto lemma adm_subst2: "cont f ⟹ cont g ⟹ adm (λx. f (fst x) = g (snd x))" apply (rule admI) apply (simp add: cont2contlubE[where f = f] cont2contlubE[where f = g] cont2contlubE[where f = snd] cont2contlubE[where f = fst] ) done subsubsection {* Composition of fun and cfun *} lemma cont2cont_comp [simp, cont2cont]: assumes "cont f" assumes "⋀ x. cont (f x)" assumes "cont g" shows "cont (λ x. (f x) ∘ (g x))" unfolding comp_def by (rule cont2cont_lambda) (intro cont2cont `cont g` `cont f` cont_compose2[OF cont2cont_fun[OF assms(1)] assms(2)] cont2cont_fun) definition cfun_comp :: "('a::pcpo → 'b::pcpo) → ('c::type ⇒ 'a) → ('c::type ⇒ 'b)" where "cfun_comp = (Λ f ρ. (λ x. f⋅x) ∘ ρ)" lemma [simp]: "cfun_comp⋅f⋅(ρ(x := v)) = (cfun_comp⋅f⋅ρ)(x := f⋅v)" unfolding cfun_comp_def by auto lemma cfun_comp_app[simp]: "(cfun_comp⋅f⋅ρ) x = f⋅(ρ x)" unfolding cfun_comp_def by auto lemma fix_eq_fix: "f⋅(fix⋅g) ⊑ fix⋅g ⟹ g⋅(fix⋅f) ⊑ fix⋅f ⟹ fix⋅f = fix⋅g" by (metis fix_least_below below_antisym) subsubsection {* Additional transitivity rules *} text {* These collect side-conditions of the form @{term "cont f"}, so the usual way to discharge them is to write @{text[source] "by this (intro cont2cont)+"} at the end. *} lemma below_trans_cong[trans]: "a ⊑ f x ⟹ x ⊑ y ⟹ cont f ⟹ a ⊑ f y " by (metis below_trans cont2monofunE) lemma not_bot_below_trans[trans]: "a ≠ ⊥ ⟹ a ⊑ b ⟹ b ≠ ⊥" by (metis below_bottom_iff) lemma not_bot_below_trans_cong[trans]: "f a ≠ ⊥ ⟹ a ⊑ b ⟹ cont f ⟹ f b ≠ ⊥" by (metis below_bottom_iff cont2monofunE) end