Quelle  HOLCF-Utils.thy

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_\<bottom> ==> '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_\<bottom>"
  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 ‹
  collect side-conditions of the form @{term "cont f"}, so the usual way to discharge them
  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