Theory Env-HOLCF

theory "Env-HOLCF"
  imports Env "HOLCF-Utils"
begin

subsubsection ‹Continuity and pcpo-valued functions›

lemma  override_on_belowI:
  assumes "⋀ a. a ∈ S ⟹ y a ⊑ z a"
  and "⋀ a. a ∉ S ⟹ x a ⊑ z a"
  shows  "x ++⇘S⇙ y ⊑ z"
  using assms 
  apply -
  apply (rule fun_belowI)
  apply (case_tac "xa ∈ S")
  apply auto
  done

lemma override_on_cont1: "cont (λ x. x ++⇘S⇙ m)"
  by (rule cont2cont_lambda) (auto simp add: override_on_def)

lemma override_on_cont2: "cont (λ x. m ++⇘S⇙ x)"
  by (rule cont2cont_lambda) (auto simp add: override_on_def)

lemma override_on_cont2cont[simp, cont2cont]:
  assumes "cont f"
  assumes "cont g"
  shows "cont (λ x. f x ++⇘S⇙ g x)"
by (rule cont_apply[OF assms(1) override_on_cont1 cont_compose[OF override_on_cont2 assms(2)]])

lemma override_on_mono:
  assumes "x1 ⊑ (x2 :: 'a::type ⇒ 'b::cpo)"
  assumes "y1 ⊑ y2"
  shows "x1 ++⇘S⇙ y1 ⊑ x2 ++⇘S⇙ y2"
by (rule below_trans[OF cont2monofunE[OF override_on_cont1 assms(1)] cont2monofunE[OF override_on_cont2 assms(2)]])

lemma fun_upd_below_env_deleteI:
  assumes "env_delete x ρ ⊑ env_delete x ρ'" 
  assumes "y ⊑ ρ' x"
  shows  "ρ(x := y) ⊑ ρ'"
  using assms
  apply (auto intro!: fun_upd_belowI   simp add: env_delete_def)
  by (metis fun_belowD fun_upd_other)

lemma fun_upd_belowI2:
  assumes "⋀ z . z ≠ x ⟹ ρ z ⊑ ρ' z" 
  assumes "ρ x ⊑ y"
  shows  "ρ ⊑ ρ'(x := y)"
  apply (rule fun_belowI)
  using assms by auto

lemma env_restr_belowI:
  assumes  "⋀ x. x ∈ S ⟹ (m1 f|` S) x ⊑ (m2 f|` S) x"
  shows "m1 f|` S ⊑ m2 f|` S"
  apply (rule fun_belowI)
  by (metis assms below_bottom_iff lookup_env_restr_not_there)

lemma env_restr_belowI2:
  assumes  "⋀ x. x ∈ S ⟹ m1 x ⊑ m2 x"
  shows "m1 f|` S ⊑ m2"
  by (rule fun_belowI)
     (simp add: assms env_restr_def)


lemma env_restr_below_itself:
  shows "m f|` S ⊑ m"
  apply (rule fun_belowI)
  apply (case_tac "x ∈ S")
  apply auto
  done  

lemma env_restr_cont:  "cont (env_restr S)"
  apply (rule cont2cont_lambda)
  apply (case_tac "y ∈ S")
  apply auto
  done

lemma env_restr_belowD:
  assumes "m1 f|` S ⊑ m2 f|` S"
  assumes "x ∈ S"
  shows "m1 x ⊑ m2 x"
  using fun_belowD[OF assms(1), where x = x] assms(2) by simp

lemma env_restr_eqD:
  assumes "m1 f|` S = m2 f|` S"
  assumes "x ∈ S"
  shows "m1 x = m2  x"
  by (metis assms(1) assms(2) lookup_env_restr)

lemma env_restr_below_subset:
  assumes "S ⊆ S'"
  and "m1 f|` S' ⊑ m2 f|` S'"
  shows "m1 f|` S ⊑ m2 f|` S"
using assms
by (auto intro!: env_restr_belowI dest: env_restr_belowD)



lemma  override_on_below_restrI:
  assumes " x f|` (-S) ⊑ z f|` (-S)"
  and "y f|` S ⊑ z f|` S"
  shows  "x ++⇘S⇙ y ⊑ z"
using assms
by (auto intro: override_on_belowI dest:env_restr_belowD)

lemma  fmap_below_add_restrI:
  assumes "x f|` (-S) ⊑ y f|` (-S)"
  and     "x f|` S ⊑ z f|` S"
  shows  "x ⊑ y ++⇘S⇙ z"
using assms
by (auto intro!: fun_belowI dest:env_restr_belowD simp add: lookup_override_on_eq)

lemmas env_restr_cont2cont[simp,cont2cont] = cont_compose[OF env_restr_cont]

lemma env_delete_cont:  "cont (env_delete x)"
  apply (rule cont2cont_lambda)
  apply (case_tac "y = x")
  apply auto
  done
lemmas env_delete_cont2cont[simp,cont2cont] = cont_compose[OF env_delete_cont]


end