Up to index of Isabelle/HOL/Locally-Nameless-Sigma
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, 50, 0] 91)
where
add_def: "(Env e)<x:a> =
(if (x ∉ dom e) then (Env (e(x \<mapsto> a))) else Malformed)"
| add_mal: "Malformed<x:a> = Malformed"
syntax (xsymbols)
add :: "('a environment) => string => 'a => (string ~=> 'a)"
("_(|_:_|))," [90, 0, 0] 91)
(* 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 \<mapsto> a,y \<mapsto> b)) xa = (f(y \<mapsto> b,x \<mapsto> 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 \<mapsto> X)) xa = (f1(x \<mapsto> X) ++ f2) xa"
proof (cases "x = xa", simp_all)
case False thus "(f1 ++ f2) xa = (f1(x \<mapsto> 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 \<mapsto> X) ++ f2) xa = Some X"
by (auto simp: map_add_Some_iff)
thus "Some X = (f1(xa \<mapsto> 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 \<mapsto> X, y \<mapsto> Y)) xa = (f1(x \<mapsto> X, y \<mapsto> 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 \<mapsto> X,y \<mapsto> Y) ++ f2) xa = Some X"
by (auto simp: map_add_Some_iff)
thus "Some X = (f1(xa \<mapsto> X,y \<mapsto> 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 \<mapsto> X,y \<mapsto> 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 \<mapsto> X,xa \<mapsto> Y) ++ f2) xa = Some Y"
by (auto simp: map_add_Some_iff)
thus "Some Y = (f1(x \<mapsto> X, xa \<mapsto> Y) ++ f2) xa" by simp
qed
qed
qed
qed
end