Theory Env

theory Env
  imports Main "HOLCF-Join-Classes"
begin

default_sort type

text {*
Our type for environments is a function with a pcpo as the co-domain; this theory collects
related definitions.
*}

subsubsection {* The domain of a pcpo-valued function *}

definition edom :: "('key ⇒ 'value::pcpo) ⇒ 'key set"
  where "edom m = {x. m x ≠ ⊥}"

lemma bot_edom[simp]: "edom ⊥ = {}" by (simp add: edom_def)

lemma bot_edom2[simp]: "edom (λ_ . ⊥) = {}" by (simp add: edom_def)

lemma edomIff: "(a ∈ edom m) = (m a ≠ ⊥)" by (simp add: edom_def)
lemma edom_iff2: "(m a = ⊥) ⟷ (a ∉ edom m)" by (simp add: edom_def)

lemma edom_empty_iff_bot: "edom m = {} ⟷ m = ⊥"
  by (metis below_bottom_iff bot_edom edomIff empty_iff fun_belowI)

lemma lookup_not_edom: "x ∉ edom m ⟹ m x = ⊥"  by (auto iff:edomIff)

lemma lookup_edom[simp]: "m x ≠ ⊥ ⟹ x ∈ edom m"  by (auto iff:edomIff)

lemma edom_mono: "x ⊑ y ⟹ edom x ⊆ edom y"
  unfolding edom_def
  by auto (metis below_bottom_iff fun_belowD)
  

lemma edom_subset_adm[simp]:
  "adm (λae'. edom ae' ⊆ S)"
  apply (rule admI)
  apply rule
  apply (subst (asm) edom_def) back
  apply simp
  apply (subst (asm) lub_fun) apply assumption
  apply (subst (asm) lub_eq_bottom_iff)
  apply (erule ch2ch_fun)
  unfolding not_all
  apply (erule exE)
  apply (rule set_mp)
  apply (rule allE) apply assumption apply assumption
  unfolding edom_def
  apply simp
  done

subsubsection {* Updates *}

lemma edom_fun_upd_subset: "edom (h (x := v)) ⊆ insert x (edom h)"
  by (auto simp add: edom_def)

declare fun_upd_same[simp] fun_upd_other[simp]

subsubsection {* Restriction *}

definition env_restr :: "'a set ⇒ ('a ⇒ 'b::pcpo) ⇒ ('a ⇒ 'b)"
  where "env_restr S m = (λ x. if x ∈ S then m x else ⊥)"

abbreviation env_restr_rev  (infixl "f|`"  110)
  where "env_restr_rev m S ≡ env_restr S m"

notation (latex output) env_restr_rev ("_|⇘_⇙")

lemma env_restr_empty_iff[simp]: "m f|` S = ⊥ ⟷ edom m ∩ S = {}"
  apply (auto simp add: edom_def env_restr_def lambda_strict[symmetric]  split:if_splits)
  apply metis
  apply (fastforce simp add: edom_def env_restr_def lambda_strict[symmetric]  split:if_splits)
  done
lemmas env_restr_empty = iffD2[OF env_restr_empty_iff, simp]

lemma lookup_env_restr[simp]: "x ∈ S ⟹ (m f|` S) x = m x"
  by (fastforce simp add: env_restr_def)

lemma lookup_env_restr_not_there[simp]: "x ∉ S ⟹ (env_restr S m) x = ⊥"
  by (fastforce simp add: env_restr_def)

lemma lookup_env_restr_eq: "(m f|` S) x = (if x ∈ S then m x else ⊥)"
  by simp

lemma env_restr_eqI: "(⋀x. x ∈ S ⟹ m⇩1 x = m⇩2 x) ⟹ m⇩1 f|` S = m⇩2 f|` S"
  by (auto simp add: lookup_env_restr_eq)

lemma env_restr_eqD: "m⇩1 f|` S = m⇩2 f|` S ⟹ x ∈ S ⟹ m⇩1 x = m⇩2 x"
  by (auto dest!: fun_cong[where x = x])

lemma env_restr_belowI: "(⋀x. x ∈ S ⟹ m⇩1 x ⊑ m⇩2 x) ⟹ m⇩1 f|` S ⊑ m⇩2 f|` S"
  by (auto intro: fun_belowI simp add: lookup_env_restr_eq)

lemma env_restr_belowD: "m⇩1 f|` S ⊑ m⇩2 f|` S ⟹ x ∈ S ⟹ m⇩1 x ⊑ m⇩2 x"
  by (auto dest!: fun_belowD[where x = x])

lemma env_restr_env_restr[simp]:
 "x f|` d2 f|` d1 = x f|` (d1 ∩ d2)"
  by (fastforce simp add: env_restr_def)

lemma env_restr_env_restr_subset:
 "d1 ⊆ d2 ⟹ x f|` d2 f|` d1 = x f|` d1"
 by (metis Int_absorb2 env_restr_env_restr)

lemma env_restr_useless: "edom m ⊆ S ⟹ m f|` S = m"
  by (rule ext) (auto simp add: lookup_env_restr_eq dest!: set_mp)

lemma env_restr_UNIV[simp]: "m f|` UNIV = m"
  by (rule env_restr_useless) simp

lemma env_restr_fun_upd[simp]: "x ∈ S ⟹ m1(x := v) f|` S = (m1 f|` S)(x := v)"
  apply (rule ext)
  apply (case_tac "xa = x")
  apply (auto simp add: lookup_env_restr_eq)
  done

lemma env_restr_fun_upd_other[simp]: "x ∉ S ⟹ m1(x := v) f|` S = m1 f|` S"
  apply (rule ext)
  apply (case_tac "xa = x")
  apply (auto simp add: lookup_env_restr_eq)
  done

lemma env_restr_eq_subset:
  assumes "S ⊆ S'"
  and "m1 f|` S' = m2 f|` S'"
  shows "m1 f|` S = m2 f|` S"
using assms
by (metis env_restr_env_restr le_iff_inf)

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 edom_env[simp]:
  "edom (m f|` S) = edom m ∩ S"
  unfolding edom_def env_restr_def by auto

lemma env_restr_below_self: "f f|` S ⊑ f"
  by (rule fun_belowI) (auto simp add: env_restr_def)

lemma env_restr_below_trans:
  "m1 f|` S1 ⊑ m2 f|` S1 ⟹ m2 f|` S2 ⊑ m3 f|` S2 ⟹ m1 f|` (S1 ∩ S2) ⊑ m3 f|` (S1 ∩ S2)"
by (auto intro!: env_restr_belowI dest!: env_restr_belowD elim: below_trans)

lemma env_restr_cont: "cont (env_restr S)"
  apply (rule cont2cont_lambda)
  unfolding env_restr_def
  apply (intro cont2cont cont_fun)
  done

lemma env_restr_mono: "m1 ⊑ m2 ⟹  m1 f|` S ⊑ m2 f|` S"
  by (metis env_restr_belowI fun_belowD)

lemma env_restr_mono2: "S2 ⊆ S1  ⟹ m f|` S2 ⊑ m f|` S1"
  by (metis env_restr_below_self env_restr_env_restr_subset)

lemmas cont_compose[OF env_restr_cont, cont2cont, simp]

lemma env_restr_cong: "(⋀x. edom m ⊆ S ∩ S' ∪ -S ∩ -S')  ⟹ m f|` S = m f|` S'"
  by (rule ext)(auto simp add: lookup_env_restr_eq edom_def)

subsubsection {* Deleting *}

definition env_delete :: "'a ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b::pcpo)"
  where "env_delete x m = m(x := ⊥)"

lemma lookup_env_delete[simp]:
  "x' ≠ x ⟹ env_delete x m x' = m x'"
  by (simp add: env_delete_def)

lemma lookup_env_delete_None[simp]:
  "env_delete x m x = ⊥"
  by (simp add: env_delete_def)

lemma edom_env_delete[simp]:
  "edom (env_delete x m) = edom m - {x}"
  by (auto simp add: env_delete_def edom_def)

lemma edom_env_delete_subset:
  "edom (env_delete x m) ⊆ edom m" by auto

lemma env_delete_fun_upd[simp]:
  "env_delete x (m(x := v)) = env_delete x m"
  by (auto simp add: env_delete_def)

lemma env_delete_fun_upd2[simp]:
  "(env_delete x m)(x := v) = m(x := v)"
  by (auto simp add: env_delete_def)

lemma env_delete_fun_upd3[simp]:
  "x ≠ y ⟹ env_delete x (m(y := v)) = (env_delete x m)(y := v)"
  by (auto simp add: env_delete_def)

lemma env_delete_noop[simp]:
  "x ∉ edom m ⟹ env_delete x m = m"
  by (auto simp add: env_delete_def edom_def)

lemma fun_upd_env_delete[simp]: "x ∈ edom Γ ⟹ (env_delete x Γ)(x := Γ x) = Γ"
  by (auto)

lemma env_restr_env_delete_other[simp]: "x ∉ S ⟹ env_delete x m f|` S = m f|` S"
  apply (rule ext)
  apply (auto simp add: lookup_env_restr_eq)
  by (metis lookup_env_delete)

lemma env_delete_restr: "env_delete x m = m f|` (-{x})"
  by (auto simp add: lookup_env_restr_eq)

lemma below_env_deleteI: "f x = ⊥ ⟹ f ⊑ g ⟹ f ⊑ env_delete x g"
  by (metis env_delete_def env_delete_restr env_restr_mono fun_upd_triv)

lemma env_delete_below_cong[intro]:
  assumes "x ≠ v ⟹ e1 x ⊑ e2 x"
  shows "env_delete v e1 x ⊑ env_delete v e2 x"
  using assms unfolding env_delete_def by auto

lemma env_delete_env_restr_swap:
  "env_delete x (env_restr S e) = env_restr S (env_delete x e)"
  by (metis (erased, hide_lams) env_delete_def env_restr_fun_upd env_restr_fun_upd_other fun_upd_triv lookup_env_restr_eq)

lemma env_delete_mono:
  "m ⊑ m' ⟹ env_delete x m ⊑ env_delete x m'"
  unfolding env_delete_restr
  by (rule env_restr_mono)
  
lemma env_delete_below_arg:
  "env_delete x m ⊑ m"
  unfolding env_delete_restr
  by (rule env_restr_below_self)

subsubsection {* Merging of two functions *}

text {*
We'd like to have some nice syntax for @{term "override_on"}.
*}

abbreviation override_on_syn ("_ ++⇘_⇙ _" [100, 0, 100] 100) where "f1 ++⇘S⇙ f2 ≡ override_on f1 f2 S"

lemma override_on_bot[simp]:
  "⊥ ++⇘S⇙ m = m f|` S" 
  "m ++⇘S⇙ ⊥ = m f|` (-S)" 
  by (auto simp add: override_on_def env_restr_def)

lemma edom_override_on[simp]: "edom (m1 ++⇘S⇙ m2) = (edom m1 - S) ∪ (edom m2 ∩ S)"
  by (auto simp add: override_on_def edom_def)

lemma lookup_override_on_eq: "(m1 ++⇘S⇙ m2) x = (if x ∈ S then m2 x else m1 x)"
  by (cases "x ∉ S") simp_all

lemma override_on_upd_swap: 
  "x ∉ S ⟹ ρ(x := z) ++⇘S⇙ ρ' = (ρ ++⇘S⇙ ρ')(x := z)"
  by (auto simp add: override_on_def  edom_def)

lemma override_on_upd: 
  "x ∈ S ⟹ ρ ++⇘S⇙ (ρ'(x := z)) = (ρ ++⇘S - {x}⇙ ρ')(x := z)"
  by (auto simp add: override_on_def  edom_def)

lemma env_restr_add: "(m1 ++⇘S2⇙ m2) f|` S = m1 f|` S ++⇘S2⇙ m2 f|` S"
  by (auto simp add: override_on_def  edom_def env_restr_def)

lemma env_delete_add: "env_delete x (m1 ++⇘S⇙ m2) = env_delete x m1 ++⇘S - {x}⇙ env_delete x m2"
  by (auto simp add: override_on_def  edom_def env_restr_def env_delete_def)

subsubsection {* Environments with binary joins *}

lemma edom_join[simp]: "edom (f ⊔ (g::('a::type ⇒ 'b::{Finite_Join_cpo,pcpo}))) = edom f ∪ edom g"
  unfolding edom_def by auto

lemma env_delete_join[simp]: "env_delete x (f ⊔ (g::('a::type ⇒ 'b::{Finite_Join_cpo,pcpo}))) = env_delete x f ⊔ env_delete x g"
  by (metis env_delete_def fun_upd_meet_simp)

lemma env_restr_join:
  fixes m1 m2 :: "'a::type ⇒ 'b::{Finite_Join_cpo,pcpo}"
  shows "(m1 ⊔ m2) f|` S = (m1 f|` S) ⊔ (m2 f|` S )"
  by (auto simp add: env_restr_def)

lemma env_restr_join2:
  fixes m :: "'a::type ⇒ 'b::{Finite_Join_cpo,pcpo}"
  shows "m f|` S ⊔ m f|` S' = m f|` (S ∪ S')"
  by (auto simp add: env_restr_def)

lemma join_env_restr_UNIV:
  fixes m :: "'a::type ⇒ 'b::{Finite_Join_cpo,pcpo}"
  shows "S1 ∪ S2 = UNIV ⟹ (m f|` S1) ⊔ (m f|` S2) = m"
  by (fastforce simp add: env_restr_def)

lemma env_restr_split:
  fixes m :: "'a::type ⇒ 'b::{Finite_Join_cpo,pcpo}"
  shows "m = m f|` S ⊔ m f|` (- S)"
by (simp add: env_restr_join2 Compl_partition)

lemma env_restr_below_split:
  "m f|` S ⊑ m' ⟹ m f|` (- S) ⊑ m' ⟹ m ⊑ m'"
  by (metis ComplI fun_below_iff lookup_env_restr)

subsubsection {* Singleton environments *}

definition esing :: "'a ⇒ 'b::{pcpo} → ('a ⇒ 'b)"
  where "esing x = (Λ a. (λ y . (if x = y then a else ⊥)))"

lemma esing_bot[simp]: "esing x ⋅ ⊥ = ⊥"
  by (rule ext)(simp add: esing_def)

lemma esing_simps[simp]:
  "(esing x ⋅ n) x = n"
  "x' ≠ x ⟹ (esing x ⋅ n) x' = ⊥"
  by (simp_all add: esing_def)

lemma esing_eq_up_iff[simp]: "(esing x⋅(up⋅a)) y = up⋅a' ⟷ (x = y ∧ a = a')"
  by (auto simp add: fun_below_iff esing_def)

lemma esing_below_iff[simp]: "esing x ⋅ a ⊑ ae  ⟷ a ⊑ ae x"
  by (auto simp add: fun_below_iff esing_def)

lemma edom_esing_subset: "edom (esing x⋅n) ⊆ {x}"
  unfolding edom_def esing_def by auto

lemma edom_esing_up[simp]: "edom (esing x ⋅ (up ⋅ n)) = {x}"
  unfolding edom_def esing_def by auto

lemma env_delete_esing[simp]: "env_delete x (esing x ⋅ n) = ⊥"
  unfolding env_delete_def esing_def
  by auto

lemma env_restr_esing[simp]:
  "x∈ S ⟹ esing x⋅v f|` S = esing x⋅v" 
  by (auto intro: env_restr_useless dest: set_mp[OF edom_esing_subset])

lemma env_restr_esing2[simp]:
  "x ∉ S ⟹ esing x⋅v f|` S = ⊥" 
  by (auto  dest: set_mp[OF edom_esing_subset])

lemma esing_eq_iff[simp]:
  "esing x⋅v = esing x⋅v' ⟷ v = v'"
  by (metis esing_simps(1))


end