Theory HOLCF-Utils

theory "HOLCF-Utils"
  imports  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