Theory Environments

(*  Title:      Environments.thy
    Author:     Florian Kammuller and Henry Sudhof, 2008
*)

theory Environments imports Main begin 

subsection ‹Type Environments›
text‹Some basic properties of our variable environments.›

(* We use a wrapped map and an error element *)
datatype 'a environment = 
  Env "(string ⇀ 'a)"
| Malformed

(* Adding an entry to an environment. Overwriting an entry switches to the error state*)
primrec
  add :: "('a environment) ⇒ string ⇒ 'a ⇒ 'a environment"    
  (‹_⦇_:_⦈› [90, 0, 0] 91)
where
  add_def: "(Env e)⦇x:a⦈ = 
     (if (x ∉ dom e) then (Env (e(x ↦ a))) else Malformed)" 
| add_mal: "Malformed⦇x:a⦈ = Malformed"

(* domains of environments, i.e. the set of used variable names *)
primrec
  env_dom :: "('a environment) ⇒ string set"
where
  env_dom_def: "env_dom (Env e) = dom e" 
| env_dom_mal: "env_dom (Malformed) = {}" 

(* Retrieving an entry from an environment *)
primrec
  env_get :: "('a environment) ⇒ string  ⇒ 'a option" (‹_!_›)
where
  env_get_def: "env_get (Env e) x = e x " 
| env_get_mal: "env_get (Malformed) x = None " 

(* Environment well-formedness. For now weaker than usually recommended for LN; just finiteness and not being the error value *)
primrec ok::"('a environment) ⇒ bool"
where
  OK_Env [intro]: "ok (Env e) = (finite (dom e))"
| OK_Mal [intro]: "ok Malformed = False"

(* commutativity of add *)
lemma subst_add:
  fixes x y
  assumes "x ≠ y"
  shows "e⦇x:a⦈⦇y:b⦈ = e⦇y:b⦈⦇x:a⦈"
proof (cases e)
  case Malformed thus ?thesis by simp
next
  case (Env f) with assms show ?thesis
  proof (cases "x ∈ dom f", simp)
    case False with assms Env show ?thesis
    proof (cases "y ∈ dom f", simp_all, intro ext)
      fix xa :: string
      case False with assms show "(f(x ↦ a,y ↦ b)) xa = (f(y ↦ b,x ↦ a)) xa"
      proof (cases "xa = x", simp)
        case False with assms show ?thesis
          by (cases "xa = y", simp_all)
      qed
    qed
  qed
qed

(* A well-formed environment is finite *)
lemma ok_finite[simp]: "ok e ⟹ finite (env_dom e)"
  by (cases e, simp+)

(* A well-formed environment is not malformed *)
lemma ok_ok[simp]: "ok e ⟹ ∃x. e = (Env x)"
  by (cases e, simp+)

(* If something is in the set of variable names, then it has a value assigned to it *)
lemma env_defined:
  fixes x :: string and e :: "'a environment"
  assumes "x ∈ env_dom e"
  shows "∃T . e!x = Some T"
proof (cases e)
  case Malformed with assms show ?thesis by simp (* contradiction *)
next
  case Env with assms show ?thesis by (simp, force)
qed

(* adding of new elements does not remove elements *)
lemma env_bigger: "⟦ a ∉ env_dom e; x ∈ (env_dom e) ⟧ ⟹ x ∈ env_dom (e⦇a:X⦈)"
  by (cases e, simp_all)

(* Added for convenience *)
lemma env_bigger2: 
  "⟦ a ∉ env_dom e; b ∉ (env_dom e); x ∈ (env_dom e); a ≠ b ⟧ 
  ⟹ x ∈ env_dom (e⦇a:X⦈⦇b:Y⦈)"
  by (cases e, simp_all)

(* If there is an entry, then the environment is sane. *)
lemma not_malformed: "x ∈ (env_dom e) ⟹ ∃fun. e = Env fun"
  by (cases e, simp_all)

(* Smaller environments are well formed. *)
lemma not_malformed_smaller: 
  fixes e :: "'a environment" and a :: string and X :: 'a
  assumes "ok (e⦇a:X⦈)"
  shows "ok e"
proof (cases e)
  case Malformed with assms show ?thesis by simp (* contradiction *)
next
  case (Env f) with ok_finite[OF assms] assms show ?thesis
    by (cases "a ∉ dom f", simp_all)
qed

(* Elements not in a bigger environment are not in a smaller one either *)
lemma not_in_smaller:
  fixes e :: "'a environment" and a :: string and X :: 'a
  assumes "ok (e⦇a:X⦈)"
  shows "a ∉ env_dom e"
proof (cases e)
  case Malformed thus ?thesis by simp
next
  case (Env f) with assms show ?thesis
    by (cases "a ∉ dom f", simp_all)
qed

(* A variable that got added is in the environment *)
lemma in_add:
  fixes e :: "'a environment" and a :: string and X :: 'a
  assumes "ok (e⦇a:X⦈)"
  shows "a ∈ env_dom (e⦇a:X⦈)"
proof (cases e)
  case Malformed with assms show ?thesis by simp (* contradiction *)
next
  case (Env f) with assms show ?thesis 
    by (cases "a ∉ dom f", simp_all)
qed

(* Similar to subst_add, but using a more convenient premise *)
lemma ok_add_reverse:
  fixes 
  e :: "'a environment" and a :: string and X :: 'a and 
  b :: string and Y :: 'a
  assumes "ok (e⦇a:X⦈⦇b:Y⦈)"
  shows "(e⦇b:Y⦈⦇a:X⦈) = (e⦇a:X⦈⦇b:Y⦈)"
proof (cases e)
  case Malformed with assms show ?thesis by simp (* contradiction *)
next
  case (Env f) 
  with 
    not_in_smaller[OF ‹ok (e⦇a:X⦈⦇b:Y⦈)›] in_add[OF assms]
    not_in_smaller[OF not_malformed_smaller[OF assms]] 
    in_add[OF not_malformed_smaller[OF assms]]
  show ?thesis
    by (simp, intro conjI impI, elim conjE, auto simp: fun_upd_twist)
qed

lemma not_in_env_bigger: 
  fixes e :: "'a environment" and a :: string and X :: 'a and x :: string
  assumes "x ∉ (env_dom e)" and "x ≠ a"
  shows "x ∉ env_dom (e⦇a:X⦈)"
proof (cases e)
  case Malformed thus ?thesis by simp
next
  case (Env f) with assms show ?thesis 
    by (cases "a ∉ dom f", simp_all)
qed

lemma not_in_env_bigger_2: 
  fixes 
  e :: "'a environment" and a :: string and X :: 'a and 
  b :: string and Y :: 'a and x :: string
  assumes "x ∉ (env_dom e)" and "x ≠ a" and "x ≠ b"
  shows "x ∉ env_dom (e⦇a:X⦈⦇b:Y⦈)"
proof (cases e)
  case Malformed thus ?thesis by simp
next
  case (Env f) with assms show ?thesis 
    by (cases "a ∉ dom f", simp_all)
qed

lemma not_in_env_smaller: 
  fixes e :: "'a environment" and a :: string and X :: 'a and x :: string
  assumes "x ∉ (env_dom (e⦇a:X⦈))" and "x ≠ a" and "ok (e⦇a:X⦈)"
  shows "x ∉ env_dom e"
proof (cases e)
  case Malformed with assms(3) show ?thesis by simp (* contradiction *)
next
  case (Env f) with assms show ?thesis 
    by (cases "a ∉ dom f", simp_all)
qed

(* Conditions derivable from the well-formedness *)
lemma ok_add_2: 
  fixes 
  e :: "'a environment" and a :: string and X :: 'a and 
  b :: string and Y :: 'a
  assumes "ok (e⦇a:X⦈⦇b:Y⦈)"
  shows "ok e ∧ a ∉ env_dom e ∧ b ∉ env_dom e ∧ a ≠ b"
proof -
  {
    assume "ok (e⦇b:X⦈⦇b:Y⦈)" 
    from not_in_smaller[OF this] in_add[OF not_malformed_smaller[OF this]]
    have False by simp
  } with assms have "a ≠ b" by auto
  moreover
  from assms ok_add_reverse[OF assms] have "ok (e⦇b:Y⦈⦇a:X⦈)" by simp
  note not_in_smaller[OF not_malformed_smaller[OF this]]
  ultimately
  show ?thesis 
    using 
      not_malformed_smaller[OF not_malformed_smaller[OF assms]]
      not_in_smaller[OF not_malformed_smaller[OF assms]]
  by simp
qed

(* A variable that got added is in the environment *)
lemma in_add_2:
  fixes 
  e :: "'a environment" and a :: string and X :: 'a and 
  b :: string and Y :: 'a
  assumes "ok (e⦇a:X⦈⦇b:Y⦈)"
  shows "a ∈ env_dom (e⦇a:X⦈⦇b:Y⦈) ∧ b ∈ env_dom (e⦇a:X⦈⦇b:Y⦈)"
proof -
  from ok_add_2[OF assms] show ?thesis 
    by (elim conjE, intro conjI, (cases e, simp_all)+)
qed

(* Convenience version *)
lemma ok_add_3:
  fixes 
  e :: "'a environment" and a :: string and X :: 'a and 
  b :: string and Y :: 'a and c :: string and Z :: 'a
  assumes "ok (e⦇a:X⦈⦇b:Y⦈⦇c:Z⦈)"
  shows 
  "a ∉ env_dom e ∧ b ∉ env_dom e ∧ c ∉ env_dom e ∧ a ≠ b ∧ b ≠ c ∧ a ≠ c"
proof -
  {
    assume "ok (e⦇a:X⦈⦇c:Y⦈⦇c:Z⦈)" 
    from not_in_smaller[OF this] in_add[OF not_malformed_smaller[OF this]]
    have False by simp
  } with assms have "b ≠ c" by auto
  moreover
  from assms ok_add_reverse[OF assms] have "ok (e⦇a:X⦈⦇c:Z⦈⦇b:Y⦈)" by simp
  note ok_add_2[OF not_malformed_smaller[OF this]]
  ultimately
  show ?thesis using ok_add_2[OF not_malformed_smaller[OF assms]]
    by simp
qed

lemma in_env_smaller: 
  fixes e :: "'a environment" and a :: string and X :: 'a and x :: string 
  assumes "x ∈ (env_dom (e⦇a:X⦈))" and "x ≠ a"
  shows "x ∈ env_dom e"
proof -
  from not_malformed[OF assms(1)] obtain f where f: "e⦇a:X⦈ = Env f" by auto
  with assms show ?thesis
  proof (cases e)
    case Malformed with ‹e⦇a:X⦈ = Env f› 
    have False by simp
    then show ?thesis ..
  next
    case (Env f') with assms f show ?thesis
      by (simp, cases "a ∈ dom f'", simp_all, force)
  qed
qed

lemma in_env_smaller2:
  fixes 
  e :: "'a environment" and a :: string and X :: 'a and 
  b :: string and Y :: 'a and x :: string 
  assumes "x ∈ (env_dom (e⦇a:X⦈⦇b:Y⦈))" and "x ≠ a" and "x ≠ b"
  shows "x ∈ env_dom e"
  by (simp add: in_env_smaller[OF in_env_smaller[OF assms(1) assms(3)] assms(2)])

lemma get_env_bigger:
  fixes e :: "'a environment" and a :: string and X :: 'a and x :: string 
  assumes "x ∈ (env_dom (e⦇a:X⦈))" and "x ≠ a"
  shows "e!x = e⦇a:X⦈!x"
proof -
  from not_malformed[OF assms(1)] obtain f where f: "e⦇a:X⦈ = Env f" by auto
  thus ?thesis proof (cases e)
    case Malformed with ‹e⦇a:X⦈ = Env f›
    show ?thesis by simp (* contradiction *)
  next
    case (Env f') with assms f show ?thesis
      by (cases "a ∉ dom f'", auto)
  qed
qed

lemma get_env_bigger2: 
  fixes 
  e :: "'a environment" and a :: string and X :: 'a and 
  b :: string and Y :: 'a and x :: string 
  assumes "x ∈ (env_dom (e⦇a:X⦈⦇b:Y⦈))" and "x ≠ a" and "x ≠ b"
  shows "e!x = e⦇a:X⦈⦇b:Y⦈!x"
  by (simp add: get_env_bigger[OF assms(1) assms(3)]
                get_env_bigger[OF in_env_smaller[OF assms(1) assms(3)] assms(2)])

lemma get_env_smaller: "⟦ x ∈ env_dom e; a ∉ env_dom e ⟧ ⟹ e⦇a:X⦈!x = e!x"
  by (cases e, auto)

lemma get_env_smaller2: 
  "⟦ x ∈ env_dom e; a ∉ env_dom e; b ∉ env_dom e; a ≠ b ⟧ 
  ⟹ e⦇a:X⦈⦇b:Y⦈!x = e!x"
  by (cases e, auto)

lemma add_get_eq: "⟦ xa ∉ env_dom e; ok e; the e⦇xa:U⦈!xa = T ⟧ ⟹ U = T" 
  by (cases e, auto)

lemma add_get: "⟦ xa ∉ env_dom e; ok e ⟧ ⟹ the e⦇xa:U⦈!xa = U" 
  by (cases e, auto)

lemma add_get2_1: 
  fixes e :: "'a environment" and x :: string and A :: 'a and y :: string and B :: 'a
  assumes "ok (e⦇x:A⦈⦇y:B⦈)"
  shows "the e⦇x:A⦈⦇y:B⦈!x = A"
proof -
  from ok_add_2[OF assms] show ?thesis
    by (cases e, elim conjE, simp_all)
qed

lemma add_get2_2:
  fixes e :: "'a environment" and x :: string and A :: 'a and y :: string and B :: 'a
  assumes "ok (e⦇x:A⦈⦇y:B⦈)"
  shows "the e⦇x:A⦈⦇y:B⦈!y = B"
proof -
  from ok_add_2[OF assms] show ?thesis
    by (cases e, elim conjE, simp_all)
qed

lemma ok_add_ok: "⟦ ok e; x ∉ env_dom e ⟧ ⟹ ok (e⦇x:X⦈)" 
  by (cases e, auto)

lemma env_add_dom: 
  fixes e :: "'a environment" and x :: string
  assumes "ok e" and "x ∉ env_dom e" 
  shows "env_dom (e⦇x:X⦈) = env_dom e ∪ {x}"
proof (auto simp: in_add[OF ok_add_ok[OF assms]], rule ccontr)
  fix y assume "y ∈ env_dom (e⦇x:X⦈)" and "y ∉ env_dom e" and "y ≠ x"
  from in_env_smaller[OF this(1) this(3)] this(2) show False by simp
next
  fix y assume "y ∈ env_dom e"
  from env_bigger[OF not_in_smaller[OF ok_add_ok[OF assms]] this]
  show "y ∈ env_dom (e⦇x:X⦈)" by assumption
qed

lemma env_add_dom_2:
  fixes e :: "'a environment" and x :: string and y :: string
  assumes "ok e" and "x ∉ env_dom e" and "y ∉ env_dom e" and "x ≠ y"
  shows "env_dom (e⦇x:X⦈⦇y:Y⦈) = env_dom e ∪ {x,y}"
proof -
  from env_add_dom[OF assms(1-2)] assms(3-4)
  have "y ∉ env_dom (e⦇x:X⦈)" by simp
  from 
    env_add_dom[OF assms(1-2)] 
    env_add_dom[OF ok_add_ok[OF assms(1-2)] this]
  show ?thesis by auto
qed

fun
   env_app :: "('a environment) ⇒  ('a environment) ⇒ ('a environment)" (‹_+_›)
where
  "env_app (Env a) (Env b) = 
  (if (ok (Env a) ∧ ok (Env b) ∧ env_dom (Env b) ∩ env_dom (Env a) = {}) 
   then  Env (a ++ b) else Malformed )"

lemma env_app_dom:
  fixes e1 :: "'a environment" and e2 :: "'a environment"
  assumes "ok e1" and "env_dom e1 ∩ env_dom e2 = {}" and "ok e2"
  shows "env_dom (e1+e2) = env_dom e1 ∪ env_dom e2"
proof -
  from ok_ok[OF ‹ok e1›] ok_ok[OF ‹ok e2›]
  obtain f1 f2 where "e1 = Env f1" and "e2 = Env f2" by auto
  with assms(2) ok_finite[OF ‹ok e1›] ok_finite[OF ‹ok e2›]
  show ?thesis by auto
qed

lemma env_app_same[simp]: 
  fixes e1 :: "'a environment" and e2 :: "'a environment" and x :: string
  assumes 
  "ok e1" and "x ∈ env_dom e1" and 
  "env_dom e1 ∩ env_dom e2 = {}" and "ok e2"
  shows "the (e1+e2!x) = the e1!x"
proof -
  from ok_ok[OF ‹ok e1›] ok_ok[OF ‹ok e2›] 
  obtain f1 f2 where "e1 = Env f1" and "e2 = Env f2" by auto
  with assms(2-3) ok_finite[OF ‹ok e1›] ok_finite[OF ‹ok e2›]
  show ?thesis proof (auto) 
    fix y :: 'a assume "dom f1 ∩ dom f2 = {}" and "f1 x = Some y"
    from map_add_comm[OF this(1)] this(2) have "(f1 ++ f2) x = Some y"
      by (simp add: map_add_Some_iff)
    thus "the ((f1 ++ f2) x) = y" by auto
  qed
qed

lemma env_app_ok[simp]: 
  fixes e1 :: "'a environment" and e2 :: "'a environment"
  assumes "ok e1" and "env_dom e1 ∩ env_dom e2 = {}" and "ok e2"
  shows "ok (e1+e2)"
proof -
  from ok_ok[OF ‹ok e1›] ok_ok[OF ‹ok e2›] 
  obtain f1 f2 where "e1 = Env f1" and "e2 = Env f2" by auto
  with assms show ?thesis by (simp,force)
qed

lemma env_app_add[simp]:
  fixes e1 :: "'a environment" and e2 :: "'a environment" and x :: string
  assumes 
  "ok e1" and "env_dom e1 ∩ env_dom e2 = {}" and "ok e2" and 
  "x ∉ env_dom e1" and "x ∉ env_dom e2"
  shows "(e1+e2)⦇x:X⦈ = e1⦇x:X⦈+e2"
proof -
  from ok_ok[OF ‹ok e1›] ok_ok[OF ‹ok e2›] 
  obtain f1 f2 where "e1 = Env f1" and "e2 = Env f2" by auto
  with assms show ?thesis proof (clarify, simp, intro impI ext)
    fix xa :: string
    assume "x ∉ dom f1" and "x ∉ dom f2"
    thus "((f1 ++ f2)(x ↦ X)) xa = (f1(x ↦ X) ++ f2) xa"
    proof (cases "x = xa", simp_all)
      case False thus "(f1 ++ f2) xa = (f1(x ↦ X) ++ f2) xa" 
        by (simp add: map_add_def split: option.split)
    next
      case True with ‹x ∉ dom f1› ‹x ∉ dom f2› 
      have "(f1(xa ↦ X) ++ f2) xa = Some X"
        by (auto simp: map_add_Some_iff)
      thus "Some X = (f1(xa ↦ X) ++ f2) xa" by simp
    qed
  qed
qed

lemma env_app_add2[simp]:
  fixes 
  e1 :: "'a environment" and e2 :: "'a environment" and 
  x :: string and y :: string
  assumes 
  "ok e1" and "env_dom e1 ∩ env_dom e2 = {}" and "ok e2" and
  "x ∉ env_dom e1" and "x ∉ env_dom e2" and "y ∉ env_dom e1" and
  "y ∉ env_dom e2" and "x ≠ y"
  shows "(e1+e2)⦇x:X⦈⦇y:Y⦈ = e1⦇x:X⦈⦇y:Y⦈+e2"
proof -
  from ok_ok[OF ‹ok e1›] ok_ok[OF ‹ok e2›] 
  obtain f1 f2 where "e1 = Env f1" and "e2 = Env f2" by auto
  with assms show ?thesis proof (clarify, simp, intro impI ext)
    fix xa :: string
    assume "x ∉ dom f1" and "x ∉ dom f2" and "y ∉ dom f1" and "y ∉ dom f2"
    with ‹x ≠ y›
    show "((f1 ++ f2)(x ↦ X, y ↦ Y)) xa = (f1(x ↦ X, y ↦ Y) ++ f2) xa"
    proof (cases "x = xa", simp)
      case True 
      with ‹x ≠ y› ‹x ∉ dom f1› ‹x ∉ dom f2› ‹y ∉ dom f1› ‹y ∉ dom f2›
      have "(f1(xa ↦ X,y ↦ Y) ++ f2) xa = Some X"
        by (auto simp: map_add_Some_iff)
      thus "Some X = (f1(xa ↦ X,y ↦ Y) ++ f2) xa" by simp
    next
      case False thus ?thesis
      proof (cases "y = xa", simp_all)
        case False with ‹x ≠ xa› 
        show "(f1 ++ f2) xa = (f1(x ↦ X,y ↦ Y) ++ f2) xa" 
          by (simp add: map_add_def split: option.split)
      next
        case True 
        with ‹x ≠ y› ‹x ∉ dom f1› ‹x ∉ dom f2› ‹y ∉ dom f1› ‹y ∉ dom f2›
        have "(f1(x ↦ X,xa ↦ Y) ++ f2) xa = Some Y"
          by (auto simp: map_add_Some_iff)
        thus "Some Y = (f1(x ↦ X, xa ↦ Y) ++ f2) xa" by simp
      qed
    qed
  qed
qed

end