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 ++⇘Sy  z"
  using assms 
  apply -
  apply (rule fun_belowI)
  apply (case_tac "xa  S")
  apply auto
  done

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

lemma override_on_cont2: "cont (λ x. m ++⇘Sx)"
  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 ++⇘Sg 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 ++⇘Sy1  x2 ++⇘Sy2"
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 ++⇘Sy  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 ++⇘Sz"
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