# Theory AList-Utils

theory "AList-Utils"
imports Main "HOL-Library.AList"
begin
declare implies_True_equals [simp] False_implies_equals[simp]
text ‹We want to have ‹delete› and ‹update› back in the namespace.›

abbreviation delete where "delete ≡ AList.delete"
abbreviation update where "update ≡ AList.update"
abbreviation restrictA where "restrictA ≡ AList.restrict"
abbreviation clearjunk where "clearjunk ≡ AList.clearjunk"

lemmas restrict_eq = AList.restrict_eq
and delete_eq = AList.delete_eq

lemma restrictA_append: "restrictA S (a@b) = restrictA S a @ restrictA S b"
unfolding restrict_eq by (rule filter_append)

lemma length_restrictA_le: "length (restrictA S a) ≤ length a"
by (metis length_filter_le restrict_eq)

subsubsection ‹The domain of an associative list›

definition domA
where "domA h = fst  set h"

lemma domA_append[simp]:"domA (a @ b) = domA a ∪ domA b"
and [simp]:"domA ((v,e) # h) = insert v (domA h)"
and [simp]:"domA (p # h) = insert (fst p) (domA h)"
and [simp]:"domA [] = {}"

lemma domA_from_set:
"(x, e) ∈ set h ⟹ x ∈ domA h"
by (induct h, auto)

lemma finite_domA[simp]:
"finite (domA Γ)"

lemma domA_delete[simp]:
"domA (delete x Γ) = domA Γ - {x}"
by (induct Γ) auto

lemma domA_restrictA[simp]:
"domA (restrictA S Γ) = domA Γ ∩ S"
by (induct Γ) auto

lemma delete_not_domA[simp]:
"x ∉ domA Γ ⟹  delete x Γ = Γ"
by (induct Γ) auto

lemma deleted_not_domA: "x ∉ domA (delete x Γ)"
by (induct Γ) auto

lemma dom_map_of_conv_domA:
"dom (map_of Γ) = domA Γ"
by (induct Γ) (auto simp add: dom_if)

lemma domA_map_of_Some_the:
"x ∈ domA Γ ⟹ map_of Γ x = Some (the (map_of Γ x))"
by (induct Γ) (auto simp add: dom_if)

lemma domA_clearjunk[simp]: "domA (clearjunk Γ) = domA Γ"
unfolding domA_def using dom_clearjunk.

lemma the_map_option_domA[simp]: "x ∈ domA Γ ⟹ the (map_option f (map_of Γ x)) = f (the (map_of Γ x))"
by (induction Γ) auto

lemma map_of_domAD: "map_of Γ x = Some e ⟹ x ∈ domA Γ"
using dom_map_of_conv_domA by fastforce

lemma restrictA_noop: "domA Γ ⊆ S ⟹ restrictA S Γ = Γ"
unfolding restrict_eq by (induction Γ) auto

lemma restrictA_cong:
"(⋀x. x ∈ domA m1 ⟹ x ∈ V ⟷ x ∈ V') ⟹ m1 = m2 ⟹ restrictA V m1 = restrictA V' m2"
unfolding restrict_eq by (induction m1 arbitrary: m2) auto

subsubsection ‹Other lemmas about associative lists›

lemma delete_set_none: "(map_of l)(x := None) = map_of (delete x l)"
proof (induct l)
case Nil thus ?case by simp
case (Cons l ls)
from this[symmetric]
show ?case
by (cases "fst l = x") auto
qed

lemma list_size_delete[simp]: "size_list size (delete x l) < Suc (size_list size l)"
by (induct l) auto

lemma delete_append[simp]: "delete x (l1 @ l2) = delete x l1 @ delete x l2"
unfolding AList.delete_eq by simp

lemma map_of_delete_insert:
assumes "map_of Γ x = Some e"
shows "map_of ((x,e) # delete x Γ) = map_of Γ"
using assms by (induct Γ) (auto split:prod.split)

lemma map_of_delete_iff[simp]: "map_of (delete x Γ) xa = Some e ⟷ (map_of Γ xa = Some e) ∧ xa ≠ x"
by (metis delete_conv fun_upd_same map_of_delete option.distinct(1))

"x ∈ domA Γ ⟹ (map_of Δ ++ map_of Γ) x = map_of Γ x"
"x ∉ domA Γ ⟹ (map_of Δ ++ map_of Γ) x = map_of Δ x"
done

lemma set_delete_subset: "set (delete k al) ⊆ set al"

lemma dom_delete_subset: "snd  set (delete k al) ⊆ snd  set al"

(*
lemma ran_map_cong[fundef_cong]:
"⟦ list_all2 (λ x y. fst x = fst y ∧ f1 (fst x) (snd x) = f2 (fst y) (snd y)) m1 m2 ⟧
⟹ map_ran f1 m1 = map_ran f2 m2"
by (induction rule: list_all2_induct) auto
*)
lemma map_ran_cong[fundef_cong]:
"⟦ ⋀ x . x ∈ set m1 ⟹ f1 (fst x) (snd x) = f2 (fst x) (snd x) ; m1 = m2 ⟧
⟹ map_ran f1 m1 = map_ran f2 m2"
by (induction m1 arbitrary: m2) auto

lemma domA_map_ran[simp]: "domA (map_ran f m) = domA m"
unfolding domA_def by (rule dom_map_ran)

lemma map_ran_delete:
"map_ran f (delete x Γ) = delete x (map_ran f Γ)"
by (induction Γ)  auto

lemma map_ran_restrictA:
"map_ran f (restrictA V Γ) = restrictA V (map_ran f Γ)"
by (induction Γ)  auto

lemma map_ran_append:
"map_ran f (Γ@Δ) = map_ran f Γ @ map_ran f Δ"
by (induction Γ)  auto

subsubsection ‹Syntax for map comprehensions›

definition mapCollect :: "('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇀ 'b) ⇒ 'c set"
where "mapCollect f m = {f k v | k v . m k = Some v}"

syntax
"_MapCollect" :: "'c ⇒ pttrn => pttrn ⇒ 'a ⇀ 'b => 'c set"    ("(1{_ |/_/↦/_/∈/_/})")
translations
"{e | k↦v ∈ m}" == "CONST mapCollect (λk v. e) m"

lemma mapCollect_empty[simp]: "{f k v | k ↦ v ∈ Map.empty} = {}"
unfolding mapCollect_def by simp

lemma mapCollect_const[simp]:
"m ≠ Map.empty ⟹ {e | k↦v∈m} = {e}"
unfolding mapCollect_def by auto

lemma mapCollect_cong[fundef_cong]:
"(⋀ k v. m1 k = Some v ⟹ f1 k v = f2 k v) ⟹ m1 = m2 ⟹ mapCollect f1 m1 = mapCollect f2 m2"
unfolding mapCollect_def by force

lemma mapCollectE[elim!]:
assumes "x ∈ {f k v | k ↦ v ∈ m}"
obtains k v where "m k = Some v" and "x = f k v"
using assms by (auto simp add: mapCollect_def)

lemma mapCollectI[intro]:
assumes  "m k = Some v"
shows "f k v ∈ {f k v | k ↦ v ∈ m}"
using assms by (auto simp add: mapCollect_def)

lemma ball_mapCollect[simp]:
"(∀ x ∈ {f k v | k ↦ v ∈ m}. P x) ⟷ (∀ k v. m k = Some v ⟶ P (f k v))"

lemma image_mapCollect[simp]:
"g  {f k v | k ↦ v ∈ m} = { g (f k v) | k ↦ v ∈ m}"

lemma mapCollect_map_upd[simp]:
"mapCollect f (m(k↦v)) = insert (f k v) (mapCollect f (m(k := None)))"
unfolding mapCollect_def by auto

definition mapCollectFilter :: "('a ⇒ 'b ⇒ (bool × 'c)) ⇒ ('a ⇀ 'b) ⇒ 'c set"
where "mapCollectFilter f m = {snd (f k v) | k v . m k = Some v ∧ fst (f k v)}"

syntax
"_MapCollectFilter" :: "'c ⇒ pttrn ⇒ pttrn ⇒ ('a ⇀ 'b) ⇒ bool ⇒ 'c set"    ("(1{_ |/_/↦/_/∈/_/./ _})")
translations
"{e | k↦v ∈ m . P }" == "CONST mapCollectFilter (λk v. (P,e)) m"

lemma mapCollectFilter_const_False[simp]:
"{e | k↦v ∈ m . False } = {}"
unfolding mapCollect_def mapCollectFilter_def by simp

lemma mapCollectFilter_const_True[simp]:
"{e | k↦v ∈ m . True } = {e | k↦v ∈ m}"
unfolding mapCollect_def mapCollectFilter_def by simp

end


# Theory HOLCF-Join

theory "HOLCF-Join"
imports HOLCF
begin

subsubsection ‹Binary Joins and compatibility›

context cpo
begin
definition join :: "'a => 'a => 'a" (infixl "⊔" 80) where
"x ⊔ y = (if ∃ z. {x, y} <<| z then lub {x, y} else x)"

definition compatible :: "'a ⇒ 'a ⇒ bool"
where "compatible x y = (∃ z. {x, y} <<| z)"

lemma compatibleI:
assumes "x ⊑ z"
assumes "y ⊑ z"
assumes "⋀ a. ⟦ x ⊑ a ; y ⊑ a ⟧ ⟹ z ⊑ a"
shows "compatible x y"
proof-
from assms
have "{x,y} <<| z"
by (auto intro: is_lubI)
thus ?thesis unfolding compatible_def by (metis)
qed

lemma is_joinI:
assumes "x ⊑ z"
assumes "y ⊑ z"
assumes "⋀ a. ⟦ x ⊑ a ; y ⊑ a ⟧ ⟹ z ⊑ a"
shows "x ⊔ y = z"
proof-
from assms
have "{x,y} <<| z"
by (auto intro: is_lubI)
thus ?thesis unfolding join_def by (metis lub_eqI)
qed

lemma is_join_and_compatible:
assumes "x ⊑ z"
assumes "y ⊑ z"
assumes "⋀ a. ⟦ x ⊑ a ; y ⊑ a ⟧ ⟹ z ⊑ a"
shows "compatible x y ∧ x ⊔ y = z"
by (metis compatibleI is_joinI assms)

lemma compatible_sym: "compatible x y ⟹ compatible y x"
unfolding compatible_def by (metis insert_commute)

lemma compatible_sym_iff: "compatible x y ⟷ compatible y x"
unfolding compatible_def by (metis insert_commute)

lemma join_above1: "compatible x y ⟹ x ⊑ x ⊔ y"
unfolding compatible_def join_def
apply auto
by (metis is_lubD1 is_ub_insert lub_eqI)

lemma join_above2: "compatible x y ⟹ y ⊑ x ⊔ y"
unfolding compatible_def join_def
apply auto
by (metis is_lubD1 is_ub_insert lub_eqI)

lemma larger_is_join1: "y ⊑ x ⟹ x ⊔ y = x"
unfolding join_def
by (metis doubleton_eq_iff lub_bin)

lemma larger_is_join2: "x ⊑ y ⟹ x ⊔ y = y"
unfolding join_def
by (metis is_lub_bin lub_bin)

lemma join_self[simp]: "x ⊔ x = x"
unfolding join_def  by auto
end

lemma join_commute:  "compatible x y ⟹ x ⊔ y = y ⊔ x"
unfolding compatible_def unfolding join_def by (metis insert_commute)

lemma lub_is_join:
"{x, y} <<| z ⟹ x ⊔ y = z"
unfolding join_def by (metis lub_eqI)

lemma compatible_refl[simp]: "compatible x x"
by (rule compatibleI[OF below_refl below_refl])

lemma join_mono:
assumes "compatible a b"
and "compatible c d"
and "a ⊑ c"
and "b ⊑ d"
shows "a ⊔ b ⊑ c ⊔ d"
proof-
from assms obtain x y where "{a, b} <<| x" "{c, d} <<| y" unfolding compatible_def by auto
with assms have "a ⊑ y" "b ⊑ y" by (metis below.r_trans is_lubD1 is_ub_insert)+
with ‹{a, b} <<| x› have "x ⊑ y" by (metis is_lub_below_iff is_lub_singleton is_ub_insert)
moreover
from ‹{a, b} <<| x› ‹{c, d} <<| y› have "a ⊔ b = x" "c ⊔ d = y" by (metis lub_is_join)+
ultimately
show ?thesis by simp
qed

lemma
assumes "compatible x y"
shows join_above1: "x ⊑ x ⊔ y" and join_above2: "y ⊑ x ⊔ y"
proof-
from assms obtain z where "{x,y} <<| z" unfolding compatible_def by auto
hence  "x ⊔ y = z" and "x ⊑ z" and "y ⊑ z" apply (auto intro: lub_is_join) by (metis is_lubD1 is_ub_insert)+
thus "x ⊑ x ⊔ y" and "y ⊑ x ⊔ y" by simp_all
qed

lemma
assumes "compatible x y"
shows compatible_above1: "compatible x (x ⊔ y)" and compatible_above2: "compatible y (x ⊔ y)"
proof-
from assms obtain z where "{x,y} <<| z" unfolding compatible_def by auto
hence  "x ⊔ y = z" and "x ⊑ z" and "y ⊑ z" apply (auto intro: lub_is_join) by (metis is_lubD1 is_ub_insert)+
thus  "compatible x (x ⊔ y)" and  "compatible y (x ⊔ y)" by (metis below.r_refl compatibleI)+
qed

lemma join_below:
assumes "compatible x y"
and "x ⊑ a" and "y ⊑ a"
shows "x ⊔ y ⊑ a"
proof-
from assms obtain z where z: "{x,y} <<| z" unfolding compatible_def by auto
with assms have "z ⊑ a" by (metis is_lub_below_iff is_ub_empty is_ub_insert)
moreover
from z have "x ⊔ y = z" by (rule lub_is_join)
ultimately show ?thesis by simp
qed

lemma join_below_iff:
assumes "compatible x y"
shows "x ⊔ y ⊑ a ⟷ (x ⊑ a ∧ y ⊑ a)"
by (metis assms below_trans cpo_class.join_above1 cpo_class.join_above2 join_below)

lemma join_assoc:
assumes "compatible x y"
assumes "compatible x (y ⊔ z)"
assumes "compatible y z"
shows "(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)"
apply (rule is_joinI)
apply (rule join_mono[OF assms(1) assms(2) below_refl join_above1[OF assms(3)]])
apply (rule below_trans[OF join_above2[OF assms(3)] join_above2[OF assms(2)]])
apply (rule join_below[OF assms(2)])
apply (erule rev_below_trans)
apply (rule join_above1[OF assms(1)])
apply (rule join_below[OF assms(3)])
apply (erule rev_below_trans)
apply (rule join_above2[OF assms(1)])
apply assumption
done

lemma join_idem[simp]: "compatible x y ⟹ x ⊔ (x ⊔ y) = x ⊔ y"
apply (subst join_assoc[symmetric])
apply (rule compatible_refl)
apply (erule compatible_above1)
apply assumption
apply (subst join_self)
apply rule
done

lemma join_bottom[simp]: "x ⊔ ⊥ = x" "⊥ ⊔ x = x"
by (auto intro: is_joinI)

shows "adm (λ y. compatible x y)"
fix Y
assume c: "chain Y" and "∀i.  compatible x (Y i)"
hence a: "⋀ i. compatible x (Y i)" by auto
show "compatible x (⨆ i. Y i)"
proof(rule compatibleI)
have c2: "chain (λi. x ⊔ Y i)"
apply (rule chainI)
apply (rule join_mono[OF a a below_refl chainE[OF ‹chain Y›]])
done
show "x ⊑ (⨆ i. x ⊔ Y i)"
by (auto intro: admD[OF _ c2] join_above1[OF a])
show "(⨆ i. Y i) ⊑ (⨆ i. x ⊔ Y i)"
by (auto intro: admD[OF _ c] below_lub[OF c2 join_above2[OF a]])
fix a
assume "x ⊑ a" and "(⨆ i. Y i) ⊑ a"
show "(⨆ i. x ⊔ Y i) ⊑ a"
apply (rule lub_below[OF c2])
apply (rule join_below[OF a ‹x ⊑ a›])
apply (rule below_trans[OF is_ub_thelub[OF c] ‹(⨆ i. Y i) ⊑ a›])
done
qed
qed

lemma join_cont1:
assumes "chain Y"
assumes compat: "⋀ i. compatible (Y i) y"
shows "(⨆i. Y i) ⊔ y = (⨆ i. Y i ⊔ y)"
proof-
have c: "chain (λi. Y i ⊔ y)"
apply (rule chainI)
apply (rule join_mono[OF compat compat chainE[OF ‹chain Y›] below_refl])
done

show ?thesis
apply (rule is_joinI)
apply (rule lub_mono[OF ‹chain Y› c join_above1[OF compat]])
apply (rule below_lub[OF c join_above2[OF compat]])
apply (rule lub_below[OF c])
apply (rule join_below[OF compat])
apply (metis lub_below_iff[OF ‹chain Y›])
apply assumption
done
qed

lemma join_cont2:
assumes "chain Y"
assumes compat: "⋀ i. compatible x (Y i)"
shows "x ⊔ (⨆i. Y i) = (⨆ i. x ⊔ Y i)"
proof-
have c: "chain (λi. x ⊔ Y i)"
apply (rule chainI)
apply (rule join_mono[OF compat compat below_refl chainE[OF ‹chain Y›]])
done

show ?thesis
apply (rule is_joinI)
apply (rule below_lub[OF c join_above1[OF compat]])
apply (rule lub_mono[OF ‹chain Y› c join_above2[OF compat]])
apply (rule lub_below[OF c])
apply (rule join_below[OF compat])
apply assumption
apply (metis lub_below_iff[OF ‹chain Y›])
done
qed

lemma join_cont12:
assumes "chain Y" and "chain Z"
assumes compat: "⋀ i j. compatible (Y i) (Z j)"
shows "(⨆i. Y i) ⊔ (⨆i. Z i) = (⨆ i. Y i  ⊔ Z i)"
proof-
have "(⨆i. Y i) ⊔ (⨆i. Z i) = (⨆i. Y i ⊔ (⨆j. Z j))"
also have "... = (⨆i j. Y i ⊔ Z j)"
by (subst join_cont2[OF ‹chain Z› compat], rule)
also have "... = (⨆i. Y i ⊔ Z i)"
apply (rule diag_lub)
apply (rule chainI, rule join_mono[OF compat compat chainE[OF ‹chain Y›] below_refl])
apply (rule chainI, rule join_mono[OF compat compat below_refl chainE[OF ‹chain Z›]])
done
finally show ?thesis.
qed

context pcpo
begin
lemma bot_compatible[simp]:
"compatible x ⊥" "compatible ⊥ x"
unfolding compatible_def by (metis insert_commute is_lub_bin minimal)+
end

end


# Theory HOLCF-Join-Classes

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

class Finite_Join_cpo = cpo +
assumes all_compatible: "compatible x y"

lemmas join_mono = join_mono[OF all_compatible all_compatible ]
lemmas join_above1[simp] = all_compatible[THEN join_above1]
lemmas join_above2[simp] = all_compatible[THEN join_above2]
lemmas join_below[simp] = all_compatible[THEN join_below]
lemmas join_below_iff = all_compatible[THEN join_below_iff]
lemmas join_assoc[simp] = join_assoc[OF all_compatible all_compatible all_compatible]
lemmas join_comm[simp] = all_compatible[THEN join_commute]

lemma join_lc[simp]: "x ⊔ (y ⊔ z) = y ⊔ (x ⊔ (z::'a::Finite_Join_cpo))"
by (metis join_assoc join_comm)

lemma join_cont': "chain Y ⟹ (⨆ i. Y i) ⊔ y = (⨆ i. Y i ⊔ (y::'a::Finite_Join_cpo))"
by (metis all_compatible join_cont1)

lemma join_cont1:
fixes y :: "'a :: Finite_Join_cpo"
shows "cont (λx. (x ⊔ y))"
apply (rule contI2)
apply (rule monofunI)
apply (metis below_refl join_mono)
apply (rule eq_imp_below)
apply (rule join_cont')
apply assumption
done

lemma join_cont2:
fixes x :: "'a :: Finite_Join_cpo"
shows "cont (λy. (x ⊔ y))"
by (simp only: join_comm) (rule join_cont1)

lemma join_cont[cont2cont,simp]:"cont f ⟹ cont g ⟹ cont (λx. (f x ⊔ (g x::'a::Finite_Join_cpo)))"
apply (rule cont2cont_case_prod[where g = "λ x. (f x, g x)" and f = "λ p x y . x ⊔ y", simplified])
apply (rule join_cont2)
apply (metis cont2cont_Pair)
done

instantiation "fun" :: (type, Finite_Join_cpo) Finite_Join_cpo
begin
definition fun_join :: "('a ⇒ 'b) → ('a ⇒ 'b) → ('a ⇒ 'b)"
where "fun_join = (Λ f g . (λ x. (f x) ⊔ (g x)))"
lemma [simp]: "(fun_join⋅f⋅g) x = (f x) ⊔ (g x)"
unfolding fun_join_def
apply (subst beta_cfun, intro cont2cont cont2cont_lambda cont2cont_fun)+
..
instance
apply standard
proof(intro compatibleI exI conjI strip)
fix x y
show "x ⊑ fun_join⋅x⋅y"  by (auto simp add: fun_below_iff)
show "y ⊑ fun_join⋅x⋅y"  by (auto simp add: fun_below_iff)
fix z
assume "x ⊑ z" and "y ⊑ z"
thus "fun_join⋅x⋅y ⊑ z" by (auto simp add: fun_below_iff)
qed
end

instantiation "cfun" :: (cpo, Finite_Join_cpo) Finite_Join_cpo
begin
definition cfun_join :: "('a → 'b) → ('a → 'b) → ('a → 'b)"
where "cfun_join = (Λ f g  x. (f ⋅ x) ⊔ (g ⋅ x))"
lemma [simp]: "cfun_join⋅f⋅g⋅x = (f ⋅ x) ⊔ (g ⋅ x)"
unfolding cfun_join_def
apply (subst beta_cfun, intro cont2cont cont2cont_lambda cont2cont_fun)+
..
instance
apply standard
proof(intro compatibleI exI conjI strip)
fix x y
show "x ⊑ cfun_join⋅x⋅y"  by (auto simp add: cfun_below_iff)
show "y ⊑ cfun_join⋅x⋅y"  by (auto simp add: cfun_below_iff)
fix z
assume "x ⊑ z" and "y ⊑ z"
thus "cfun_join⋅x⋅y ⊑ z" by (auto simp add: cfun_below_iff)
qed
end

lemma bot_lub[simp]: "S <<| ⊥ ⟷  S ⊆ {⊥}"
by (auto dest!: is_lubD1 is_ubD intro: is_lubI is_ubI)

lemma compatible_up[simp]: "compatible (up⋅x) (up⋅y) ⟷ compatible x y"
proof
assume "compatible (up⋅x) (up⋅y)"
then obtain z' where z': "{up⋅x,up⋅y} <<| z'" unfolding compatible_def by auto
then obtain z where  "{up⋅x,up⋅y} <<| up⋅z" by (cases z') auto
hence "{x,y} <<| z"
unfolding is_lub_def
apply auto
by (metis up_below)
thus "compatible x y"  unfolding compatible_def..
next
assume "compatible x y"
then obtain z where z: "{x,y} <<| z" unfolding compatible_def by auto
hence  "{up⋅x,up⋅y} <<| up⋅z"  unfolding is_lub_def
apply auto
by (metis not_up_less_UU upE up_below)
thus "compatible (up⋅x) (up⋅y)"  unfolding compatible_def..
qed

instance u :: (Finite_Join_cpo) Finite_Join_cpo
proof
fix x y :: "'a⇩⊥"
show "compatible x y"
apply (cases x, simp)
apply (cases y, simp)
done
qed

class is_unit = fixes unit assumes is_unit: "⋀ x. x = unit"

instantiation unit :: is_unit
begin

definition "unit ≡ ()"

instance
by standard auto

end

instance lift :: (is_unit) Finite_Join_cpo
proof
fix x y :: "'a lift"
show "compatible x y"
apply (cases x, simp)
apply (cases y, simp)
apply (subst is_unit)
apply (subst is_unit) back
apply simp
done
qed

instance prod :: (Finite_Join_cpo, Finite_Join_cpo) Finite_Join_cpo
proof
fix x y :: "('a × 'b)"
let ?z = "(fst x ⊔ fst y, snd x ⊔ snd y)"
show "compatible x y"
proof(rule compatibleI)
show "x ⊑ ?z" by (cases x, auto)
show "y ⊑ ?z" by (cases y, auto)
fix z'
assume "x ⊑ z'" and "y ⊑ z'" thus "?z ⊑ z'"
by (cases z', cases x, cases y, auto)
qed
qed

lemma prod_join:
fixes x y :: "'a::Finite_Join_cpo × 'b::Finite_Join_cpo"
shows "x ⊔ y = (fst x ⊔ fst y, snd x ⊔ snd y)"
apply (rule is_joinI)
apply (cases x, auto)[1]
apply (cases y, auto)[1]
apply (cases x, cases y, case_tac a, auto)[1]
done

lemma
fixes x y :: "'a::Finite_Join_cpo × 'b::Finite_Join_cpo"
shows fst_join[simp]: "fst (x ⊔ y) = fst x ⊔ fst y"
and snd_join[simp]: "snd (x ⊔ y) = snd x ⊔ snd y"
unfolding prod_join by simp_all

lemma fun_meet_simp[simp]: "(f ⊔ g) x = f x ⊔ (g x::'a::Finite_Join_cpo)"
proof-
have "f ⊔ g = (λ x. f x ⊔ g x)"
by (rule is_joinI)(auto simp add: fun_below_iff)
thus ?thesis by simp
qed

lemma fun_upd_meet_simp[simp]: "(f ⊔ g) (x := y) = f (x := y)  ⊔ g (x := y::'a::Finite_Join_cpo)"
by auto

lemma cfun_meet_simp[simp]: "(f ⊔ g) ⋅ x = f ⋅ x ⊔ (g ⋅ x::'a::Finite_Join_cpo)"
proof-
have "f ⊔ g = (Λ x. f ⋅ x ⊔ g ⋅ x)"
by (rule is_joinI)(auto simp add: cfun_below_iff)
thus ?thesis by simp
qed

lemma cfun_join_below:
fixes f :: "('a::Finite_Join_cpo) → ('b::Finite_Join_cpo)"
shows "f⋅x ⊔ f⋅y ⊑ f⋅(x ⊔ y)"
by (intro join_below monofun_cfun_arg join_above1 join_above2)

lemma join_self_below[iff]:
"x = x ⊔ y ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"x = y ⊔ x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"x ⊔ y = x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"y ⊔ x = x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"x ⊔ y ⊑ x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
"y ⊔ x ⊑ x ⟷ y ⊑ (x::'a::Finite_Join_cpo)"
apply (metis join_above2 larger_is_join1)
apply (metis join_above1 larger_is_join2)
apply (metis join_above2 larger_is_join1)
apply (metis join_above1 larger_is_join2)
apply (metis join_above1 join_above2 below_antisym larger_is_join1)
apply (metis join_above2 join_above1 below_antisym larger_is_join2)
done

lemma join_bottom_iff[iff]:
"x ⊔ y = ⊥ ⟷ x = ⊥ ∧ (y::'a::{Finite_Join_cpo,pcpo}) = ⊥"
by (metis all_compatible join_bottom(2) join_comm join_idem)

class Join_cpo = cpo +
assumes exists_lub: "∃u. S <<| u"

context Join_cpo
begin
subclass Finite_Join_cpo
apply standard
unfolding compatible_def
apply (rule exists_lub)
done
end

lemma below_lubI[intro, simp]:
fixes x :: "'a :: Join_cpo"
shows  "x ∈ S ⟹ x ⊑ lub S"
by (metis exists_lub is_ub_thelub_ex)

lemma lub_belowI[intro, simp]:
fixes x :: "'a :: Join_cpo"
shows  "(⋀ y. y ∈ S ⟹ y ⊑ x) ⟹ lub S ⊑ x"
by (metis exists_lub is_lub_thelub_ex is_ub_def)

(* subclass (in Join_cpo)  pcpo *)
instance Join_cpo ⊆ pcpo
apply standard
apply (rule exI[where x = "lub {}"])
apply auto
done

lemma lub_empty_set[simp]:
"lub {} = (⊥::'a::Join_cpo)"
by (rule lub_eqI) simp

lemma lub_insert[simp]:
fixes x :: "'a :: Join_cpo"
shows "lub (insert x S) = x ⊔ lub S"
by (rule lub_eqI) (auto intro: below_trans[OF _ join_above2] simp add: join_below_iff is_ub_def is_lub_def)

end


# 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)

"adm (λae'. edom ae' ⊆ S)"
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 subsetD)
apply (rule allE) apply assumption apply assumption
unfolding edom_def
apply simp
done

lemma edom_fun_upd_subset: "edom (h (x := v)) ⊆ insert x (edom h)"

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"

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

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"

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)"

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!: subsetD)

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")
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")
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'"

lemma lookup_env_delete_None[simp]:
"env_delete x m x = ⊥"

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"

lemma env_delete_fun_upd2[simp]:
"(env_delete x m)(x := v) = m(x := v)"

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

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)
by (metis lookup_env_delete)

lemma env_delete_restr: "env_delete x m = m f| (-{x})"

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 )"

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

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"

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

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 ⋅ ⊥ = ⊥"

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

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: subsetD[OF edom_esing_subset])

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

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

end


# Theory Pointwise

theory Pointwise imports Main begin

text ‹
Lifting a relation to a function.
›

definition pointwise where "pointwise P m m' = (∀ x. P (m x) (m' x))"

lemma pointwiseI[intro]: "(⋀ x. P (m x) (m' x)) ⟹ pointwise P m m'" unfolding pointwise_def by blast

end


# Theory HOLCF-Utils

theory "HOLCF-Utils"
imports  HOLCF Pointwise
begin

default_sort type

lemmas cont_fun[simp]
lemmas cont2cont_fun[simp]

lemma cont_compose2:
assumes "⋀ y. cont (λ x. c x y)"
assumes "⋀ x. cont (λ y. c x y)"
assumes "cont f"
assumes "cont g"
shows "cont (λx. c (f x) (g x))"
by (intro cont_apply[OF assms(4) assms(2)]
cont2cont_fun[OF cont_compose[OF _ assms(3)]]
cont2cont_lambda[OF assms(1)])

fixes P :: "'a::pcpo ⇒ 'b::pcpo ⇒ bool"
assumes "adm (λ x. P (fst x) (snd x))"
shows "adm (λ m. pointwise P (fst m) (snd m))"
case prems: (1 Y)
show ?case
apply (rule pointwiseI)
apply (rule admD[OF adm_subst[where t = "λp . (fst p x, snd p x)" for x, OF _ assms, simplified] ‹chain Y›])
using prems(2) unfolding pointwise_def apply auto
done
qed

lemma cfun_beta_Pair:
assumes "cont (λ p. f (fst p) (snd p))"
shows "csplit⋅(Λ a b . f a b)⋅(x, y) = f x y"
apply simp
apply (subst beta_cfun)
apply (rule cont2cont_LAM')
apply (rule assms)
apply (rule beta_cfun)
apply (rule cont2cont_fun)
using assms
unfolding prod_cont_iff
apply auto
done

lemma fun_upd_mono:
"ρ1 ⊑ ρ2 ⟹ v1 ⊑ v2 ⟹ ρ1(x := v1) ⊑ ρ2(x := v2)"
apply (rule fun_belowI)
apply (case_tac "xa = x")
apply simp
apply (auto elim:fun_belowD)
done

lemma fun_upd_cont[simp,cont2cont]:
assumes "cont f" and "cont h"
shows "cont (λ x. (f x)(v := h x) :: 'a ⇒ 'b::pcpo)"
by (rule cont2cont_lambda)(auto simp add: assms)

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

lemma cont_if_else_above:
assumes "cont f"
assumes "cont g"
assumes "⋀ x. f x ⊑ g x"
assumes "⋀ x y. x ⊑ y ⟹ P y ⟹ P x"
shows "cont (λx. if P x then f x else g x)" (is "cont ?I")
proof(intro contI2 monofunI)
fix x y :: 'a
assume "x ⊑ y"
with assms(4)[OF this]
show "?I x ⊑ ?I y"
apply (auto)
apply (rule cont2monofunE[OF assms(1)], assumption)
apply (rule below_trans[OF cont2monofunE[OF assms(1)] assms(3)], assumption)
apply (rule cont2monofunE[OF assms(2)], assumption)
done
next
fix Y :: "nat ⇒ 'a"
assume "chain Y"
assume "chain (λi . ?I (Y i))"

have ch_f: "f (⨆ i. Y i) ⊑ (⨆ i. f (Y i))" by (metis ‹chain Y› assms(1) below_refl cont2contlubE)

show "?I (⨆ i. Y i) ⊑ (⨆ i. ?I (Y i))"
proof(cases "∀ i. P (Y i)")
case True hence "P (⨆ i. Y i)" by (metis ‹chain Y› adm_def assms(5))
with True ch_f show ?thesis by auto
next
case False
then obtain j where "¬ P (Y j)" by auto
hence *:  "∀ i ≥ j. ¬ P (Y i)" "¬ P (⨆ i. Y i)"
apply (auto)
apply (metis assms(4) chain_mono[OF ‹chain Y›])
apply (metis assms(4) is_ub_thelub[OF ‹chain Y›])
done

have "?I (⨆ i. Y i) = g (⨆ i. Y i)" using * by simp
also have "… = g (⨆ i. Y (i + j))" by (metis lub_range_shift[OF ‹chain Y›])
also have "… = (⨆ i. (g (Y (i + j))))" by (rule cont2contlubE[OF assms(2) chain_shift[OF ‹chain Y›]] )
also have "… = (⨆ i. (?I (Y (i + j))))" using * by auto
also have "… = (⨆ i. (?I (Y i)))" by (metis lub_range_shift[OF ‹chain (λi . ?I (Y i))›])
finally show ?thesis by simp
qed
qed

fun up2option :: "'a::cpo⇩⊥ ⇒ 'a option"
where "up2option Ibottom = None"
|     "up2option (Iup a) = Some a"

lemma up2option_simps[simp]:
"up2option ⊥ = None"
"up2option (up⋅x) = Some x"
unfolding up_def by (simp_all add: cont_Iup inst_up_pcpo)

fun option2up :: "'a option ⇒ 'a::cpo⇩⊥"
where "option2up None = ⊥"
|     "option2up (Some a) = up⋅a"

lemma option2up_up2option[simp]:
"option2up (up2option x) = x"
by (cases x) auto
lemma up2option_option2up[simp]:
"up2option (option2up x) = x"
by (cases x) auto

lemma adm_subst2: "cont f ⟹ cont g ⟹ adm (λx. f (fst x) = g (snd x))"
cont2contlubE[where f = f]  cont2contlubE[where f = g]
cont2contlubE[where f = snd]  cont2contlubE[where f = fst]
)
done

subsubsection ‹Composition of fun and cfun›

lemma cont2cont_comp [simp, cont2cont]:
assumes "cont f"
assumes "⋀ x. cont (f x)"
assumes "cont g"
shows "cont (λ x. (f x) ∘ (g x))"
unfolding comp_def
by (rule cont2cont_lambda)
(intro cont2cont  ‹cont g› ‹cont f› cont_compose2[OF cont2cont_fun[OF assms(1)] assms(2)] cont2cont_fun)

definition cfun_comp :: "('a::pcpo → 'b::pcpo) → ('c::type ⇒ 'a) → ('c::type ⇒ 'b)"
where  "cfun_comp = (Λ f ρ. (λ x. f⋅x) ∘ ρ)"

lemma [simp]: "cfun_comp⋅f⋅(ρ(x := v)) = (cfun_comp⋅f⋅ρ)(x := f⋅v)"
unfolding cfun_comp_def by auto

lemma cfun_comp_app[simp]: "(cfun_comp⋅f⋅ρ) x = f⋅(ρ x)"
unfolding cfun_comp_def by auto

lemma fix_eq_fix:
"f⋅(fix⋅g) ⊑ fix⋅g ⟹ g⋅(fix⋅f) ⊑ fix⋅f ⟹ fix⋅f = fix⋅g"
by (metis fix_least_below below_antisym)

text ‹
These collect side-conditions of the form @{term "cont f"}, so the usual way to discharge them
is to write @{text[source] "by this (intro cont2cont)+"} at the end.
›

lemma below_trans_cong[trans]:
"a ⊑ f x ⟹ x ⊑ y ⟹ cont f ⟹ a ⊑ f y "
by (metis below_trans cont2monofunE)

lemma not_bot_below_trans[trans]:
"a ≠ ⊥ ⟹ a ⊑ b ⟹ b ≠ ⊥"
by (metis below_bottom_iff)

lemma not_bot_below_trans_cong[trans]:
"f a ≠ ⊥ ⟹ a ⊑ b ⟹ cont f ⟹ f b ≠ ⊥"
by (metis below_bottom_iff cont2monofunE)

end


# Theory EvalHeap

theory "EvalHeap"
imports "AList-Utils" Env Nominal2.Nominal2 "HOLCF-Utils"
begin

subsubsection ‹Conversion from heaps to environments›

fun
evalHeap :: "('var × 'exp) list ⇒ ('exp ⇒ 'value::{pure,pcpo}) ⇒ 'var ⇒ 'value"
where
"evalHeap [] _ = ⊥"
| "evalHeap ((x,e)#h) eval = (evalHeap h eval) (x := eval e)"

lemma cont2cont_evalHeap[simp, cont2cont]:
"(⋀ e . e ∈ snd  set h ⟹ cont (λρ. eval ρ e)) ⟹ cont (λ ρ. evalHeap h (eval ρ))"
by(induct h, auto)

lemma evalHeap_eqvt[eqvt]:
"π ∙ evalHeap h eval = evalHeap (π ∙ h) (π ∙ eval)"
by (induct h) (auto simp add:fun_upd_eqvt  simp del: fun_upd_apply)

lemma edom_evalHeap_subset:"edom (evalHeap h eval) ⊆ domA h"
by (induct h eval rule:evalHeap.induct) (auto dest:subsetD[OF edom_fun_upd_subset] simp del: fun_upd_apply)

lemma evalHeap_cong[fundef_cong]:
"⟦ heap1 = heap2 ;  (⋀ e. e ∈ snd  set heap2 ⟹ eval1 e = eval2 e) ⟧
⟹  evalHeap heap1 eval1 = evalHeap heap2 eval2"
by (induct heap2 eval2 arbitrary:heap1 rule:evalHeap.induct, auto)

lemma lookupEvalHeap:
assumes "v ∈ domA h"
shows "(evalHeap h f) v = f (the (map_of h v))"
using assms
by (induct h f rule: evalHeap.induct) auto

lemma lookupEvalHeap':
assumes "map_of Γ v = Some e"
shows "(evalHeap Γ f) v = f e"
using assms
by (induct Γ f rule: evalHeap.induct) auto

lemma lookupEvalHeap_other[simp]:
assumes "v ∉ domA Γ"
shows "(evalHeap Γ f) v = ⊥"
using assms
by (induct Γ f rule: evalHeap.induct) auto

lemma env_restr_evalHeap_noop:
"domA h ⊆ S ⟹ env_restr S (evalHeap h eval) = evalHeap h eval"
apply (rule ext)
apply (case_tac "x ∈ S")
apply (auto simp add: lookupEvalHeap intro: lookupEvalHeap_other)
done

lemma env_restr_evalHeap_same[simp]:
"env_restr (domA h) (evalHeap h eval) = evalHeap h eval"

lemma evalHeap_cong':
"⟦ (⋀ x. x ∈ domA heap ⟹ eval1 (the (map_of heap x)) = eval2 (the (map_of heap x))) ⟧
⟹  evalHeap heap eval1 = evalHeap heap eval2"
apply (rule ext)
apply (case_tac "x ∈ domA heap")
done

lemma lookupEvalHeapNotAppend[simp]:
assumes "x ∉ domA Γ"
shows "(evalHeap (Γ@h) f) x = evalHeap h f x"
using assms by (induct Γ, auto)

lemma evalHeap_delete[simp]: "evalHeap (delete x Γ) eval = env_delete x (evalHeap Γ eval)"
by (induct Γ) auto

lemma evalHeap_mono:
"x ∉ domA Γ ⟹
evalHeap Γ eval ⊑ evalHeap ((x, e) # Γ) eval"
apply simp
apply (rule fun_belowI)
apply (case_tac "xa ∈ domA Γ")
apply (case_tac "xa = x")
apply auto
done

subsubsection ‹Reordering lemmas›

lemma evalHeap_reorder:
assumes "map_of Γ = map_of Δ"
shows "evalHeap Γ h = evalHeap Δ h"
proof (rule ext)
from assms
have *: "domA Γ = domA Δ" by (metis dom_map_of_conv_domA)

fix x
show "evalHeap Γ h x = evalHeap Δ h x"
using assms(1) *
apply (cases "x ∈ domA Γ")
done
qed

assumes "x ≠ y"
shows "evalHeap ((x,e1)#(y,e2)#Γ) eval = evalHeap ((y,e2)#(x,e1)#Γ) eval"
by (rule evalHeap_reorder) (simp add: fun_upd_twist[OF assms])

assumes "x ∉ domA Γ"
shows "evalHeap ((x,e)#Γ@Δ) eval = evalHeap (Γ @ ((x,e)#Δ)) eval"
by (rule evalHeap_reorder) (simp, metis assms dom_map_of_conv_domA map_add_upd_left)

lemma evalHeap_subst_exp:
assumes "eval e = eval e'"
shows "evalHeap ((x,e)#Γ) eval = evalHeap ((x,e')#Γ) eval"

end


# Theory Nominal-Utils

theory "Nominal-Utils"
imports Nominal2.Nominal2 "HOL-Library.AList"
begin

subsubsection ‹Lemmas helping with equivariance proofs›

lemma perm_rel_lemma:
assumes "⋀ π x y. r (π ∙ x) (π ∙ y) ⟹ r x y"
shows "r (π ∙ x) (π ∙ y) ⟷ r x y" (is "?l ⟷ ?r")
by (metis (full_types) assms permute_minus_cancel(2))

lemma perm_rel_lemma2:
assumes "⋀ π x y. r x y ⟹ r (π ∙ x) (π ∙ y)"
shows "r x y ⟷ r (π ∙ x) (π ∙ y)" (is "?l ⟷ ?r")
by (metis (full_types) assms permute_minus_cancel(2))

lemma fun_eqvtI:
assumes f_eqvt[eqvt]: "(⋀ p x. p ∙ (f x) = f (p ∙ x))"
shows "p ∙ f = f" by perm_simp rule

lemma eqvt_at_apply:
assumes "eqvt_at f x"
shows "(p ∙ f) x = f x"
by (metis (hide_lams, no_types) assms eqvt_at_def permute_fun_def permute_minus_cancel(1))

lemma eqvt_at_apply':
assumes "eqvt_at f x"
shows "p ∙ f x = f (p ∙ x)"
by (metis (hide_lams, no_types) assms eqvt_at_def)

lemma eqvt_at_apply'':
assumes "eqvt_at f x"
shows "(p ∙ f) (p ∙ x) = f (p ∙ x)"
by (metis (hide_lams, no_types) assms eqvt_at_def permute_fun_def permute_minus_cancel(1))

lemma size_list_eqvt[eqvt]: "p ∙ size_list f x = size_list (p ∙ f) (p ∙ x)"
proof (induction x)
case (Cons x xs)
have "f x = p ∙ (f x)" by (simp add: permute_pure)
also have "... = (p ∙ f) (p ∙ x)" by simp
with Cons
show ?case by (auto simp add: permute_pure)
qed simp

subsubsection ‹Freshness via equivariance›

lemma eqvt_fresh_cong1: "(⋀p x. p ∙ (f x) = f (p ∙ x)) ⟹ a ♯ x ⟹ a ♯ f x "
apply (rule fresh_fun_eqvt_app[of f])
apply (rule eqvtI)
apply (rule eq_reflection)
apply (rule ext)
apply (metis permute_fun_def permute_minus_cancel(1))
apply assumption
done

lemma eqvt_fresh_cong2:
assumes eqvt: "(⋀p x y. p ∙ (f x y) = f (p ∙ x) (p ∙ y))"
and fresh1: "a ♯ x" and fresh2: "a ♯ y"
shows "a ♯ f x y"
proof-
have "eqvt (λ (x,y). f x y)"
using eqvt
apply -
apply (rule ext)
apply auto
by (metis permute_minus_cancel(1))
moreover
have "a ♯ (x, y)" using fresh1 fresh2 by auto
ultimately
have "a ♯ (λ (x,y). f x y) (x, y)" by (rule fresh_fun_eqvt_app)
thus ?thesis by simp
qed

lemma eqvt_fresh_star_cong1:
assumes eqvt: "(⋀p x. p ∙ (f x) = f (p ∙ x))"
and fresh1: "a ♯* x"
shows "a ♯* f x"
by (metis fresh_star_def eqvt_fresh_cong1 assms)

lemma eqvt_fresh_star_cong2:
assumes eqvt: "(⋀p x y. p ∙ (f x y) = f (p ∙ x) (p ∙ y))"
and fresh1: "a ♯* x" and fresh2: "a ♯* y"
shows "a ♯* f x y"
by (metis fresh_star_def eqvt_fresh_cong2 assms)

lemma eqvt_fresh_cong3:
assumes eqvt: "(⋀p x y z. p ∙ (f x y z) = f (p ∙ x) (p ∙ y) (p ∙ z))"
and fresh1: "a ♯ x" and fresh2: "a ♯ y" and fresh3: "a ♯ z"
shows "a ♯ f x y z"
proof-
have "eqvt (λ (x,y,z). f x y z)"
using eqvt
apply -
apply (rule ext)
apply auto
by (metis permute_minus_cancel(1))
moreover
have "a ♯ (x, y, z)" using fresh1 fresh2 fresh3 by auto
ultimately
have "a ♯ (λ (x,y,z). f x y z) (x, y, z)" by (rule fresh_fun_eqvt_app)
thus ?thesis by simp
qed

lemma eqvt_fresh_star_cong3:
assumes eqvt: "(⋀p x y z. p ∙ (f x y z) = f (p ∙ x) (p ∙ y) (p ∙ z))"
and fresh1: "a ♯* x" and fresh2: "a ♯* y" and fresh3: "a ♯* z"
shows "a ♯* f x y z"
by (metis fresh_star_def eqvt_fresh_cong3 assms)

lemma not_self_fresh[simp]: "atom x ♯ x ⟷ False"
by (metis fresh_at_base(2))

lemma fresh_star_singleton: "{ x } ♯* e ⟷ x ♯ e"

lemma eqvt_cases:
fixes f x π
assumes eqvt: "⋀x. π ∙ f x = f (π ∙ x)"
obtains "f x" "f (π ∙ x)" | "¬ f x " " ¬ f (π ∙ x)"
using assms[symmetric]
by (cases "f x") auto

lemma range_eqvt: "π ∙ range Y = range (π ∙ Y)"
unfolding image_eqvt UNIV_eqvt ..

lemma case_option_eqvt[eqvt]:
"π ∙ case_option d f x = case_option (π ∙ d) (π ∙ f) (π ∙ x)"
by(cases x)(simp_all)

lemma supp_option_eqvt:
"supp (case_option d f x) ⊆ supp d ∪ supp f ∪ supp x"
apply (cases x)
apply (auto simp add: supp_Some )
apply (metis (mono_tags) Un_iff subsetCE supp_fun_app)
done

lemma funpow_eqvt[simp,eqvt]:
"π ∙ ((f :: 'a ⇒ 'a::pt) ^^ n) = (π ∙ f) ^^ (π ∙ n)"
apply (induct n)
apply simp
apply (rule ext)
apply simp
apply perm_simp
apply simp
done

lemma delete_eqvt[eqvt]:
"π ∙ AList.delete x Γ = AList.delete (π ∙ x) (π ∙ Γ)"
by (induct Γ, auto)

lemma restrict_eqvt[eqvt]:
"π ∙ AList.restrict S Γ = AList.restrict (π ∙ S) (π ∙ Γ)"
unfolding AList.restrict_eq by perm_simp rule

lemma supp_restrict:
"supp (AList.restrict S Γ) ⊆ supp Γ"
by (induction Γ) (auto simp add: supp_Pair supp_Cons)

lemma clearjunk_eqvt[eqvt]:
"π ∙ AList.clearjunk Γ = AList.clearjunk (π ∙ Γ)"
by (induction Γ rule: clearjunk.induct) auto

lemma map_ran_eqvt[eqvt]:
"π ∙ map_ran f Γ = map_ran (π ∙ f) (π ∙ Γ)"
by (induct Γ, auto)

lemma dom_perm:
"dom (π ∙ f) = π ∙ (dom f)"
unfolding dom_def by (perm_simp) (simp)

lemmas dom_perm_rev[simp,eqvt] = dom_perm[symmetric]

lemma ran_perm[simp]:
"π ∙ (ran f) = ran (π ∙ f)"
unfolding ran_def by (perm_simp) (simp)

"π ∙ (m1 ++ m2) = (π ∙ m1) ++ (π ∙ m2)"
by (perm_simp, rule)

lemma map_of_eqvt[eqvt]:
"π ∙ map_of l = map_of (π ∙ l)"
apply (induct l)
apply simp
apply perm_simp
apply auto
done

lemma concat_eqvt[eqvt]: "π ∙ concat l = concat (π ∙ l)"
by (induction l)(auto simp add: append_eqvt)

lemma tranclp_eqvt[eqvt]: "π ∙ tranclp P v⇩1 v⇩2 = tranclp (π ∙ P) (π ∙ v⇩1) (π ∙ v⇩2)"
unfolding tranclp_def by perm_simp rule

lemma rtranclp_eqvt[eqvt]: "π ∙ rtranclp P v⇩1 v⇩2 = rtranclp (π ∙ P) (π ∙ v⇩1) (π ∙ v⇩2)"
unfolding rtranclp_def by perm_simp rule

lemma Set_filter_eqvt[eqvt]: "π ∙ Set.filter P S = Set.filter (π ∙ P) (π ∙ S)"
unfolding Set.filter_def
by perm_simp rule

lemma Sigma_eqvt'[eqvt]: "π ∙ Sigma = Sigma"
apply (rule ext)
apply (rule ext)
apply (subst permute_fun_def)
apply (subst permute_fun_def)
unfolding Sigma_def
apply perm_simp
done

lemma override_on_eqvt[eqvt]:
"π ∙ (override_on m1 m2 S) = override_on (π ∙ m1) (π ∙ m2) (π ∙ S)"
by (auto simp add: override_on_def )

lemma card_eqvt[eqvt]:
"π ∙ (card S) = card (π ∙ S)"
by (cases "finite S", induct rule: finite_induct) (auto simp add: card_insert_if mem_permute_iff permute_pure)

(* Helper lemmas provided by Christian Urban *)

lemma Projl_permute:
assumes a: "∃y. f = Inl y"
shows "(p ∙ (Sum_Type.projl f)) = Sum_Type.projl (p ∙ f)"
using a by auto

lemma Projr_permute:
assumes a: "∃y. f = Inr y"
shows "(p ∙ (Sum_Type.projr f)) = Sum_Type.projr (p ∙ f)"
using a by auto

subsubsection ‹Freshness lemmas›

lemma fresh_list_elem:
assumes "a ♯ Γ"
and "e ∈ set Γ"
shows "a ♯ e"
using assms

lemma set_not_fresh:
"x ∈ set L ⟹ ¬(atom x ♯ L)"
by (metis fresh_list_elem not_self_fresh)

lemma pure_fresh_star[simp]: "a ♯* (x :: 'a :: pure)"

lemma supp_set_mem: "x ∈ set L ⟹ supp x ⊆ supp L"
by (induct L) (auto simp add: supp_Cons)

lemma set_supp_mono: "set L ⊆ set L2 ⟹ supp L ⊆ supp L2"
by (induct L)(auto simp add: supp_Cons supp_Nil dest:supp_set_mem)

lemma fresh_star_at_base:
fixes x :: "'a :: at_base"
shows "S ♯* x ⟷ atom x ∉ S"
by (metis fresh_at_base(2) fresh_star_def)

subsubsection ‹Freshness and support for subsets of variables›

lemma supp_mono: "finite (B::'a::fs set) ⟹ A ⊆ B ⟹ supp A ⊆ supp B"
by (metis infinite_super subset_Un_eq supp_of_finite_union)

lemma fresh_subset:
"finite B ⟹ x ♯ (B :: 'a::at_base set) ⟹ A ⊆ B ⟹ x ♯ A"
by (auto dest:supp_mono simp add: fresh_def)

lemma fresh_star_subset:
"finite B ⟹ x ♯* (B :: 'a::at_base set) ⟹ A ⊆ B ⟹ x ♯* A"
by (metis fresh_star_def fresh_subset)

lemma fresh_star_set_subset:
"x ♯* (B :: 'a::at_base list) ⟹ set A ⊆ set B ⟹ x ♯* A"
by (metis fresh_star_set fresh_star_subset[OF finite_set])

subsubsection ‹The set of free variables of an expression›

definition fv :: "'a::pt ⇒ 'b::at_base set"
where "fv e = {v. atom v ∈ supp e}"

lemma fv_eqvt[simp,eqvt]: "π ∙ (fv e) = fv (π ∙ e)"
unfolding fv_def by simp

lemma fv_Nil[simp]: "fv [] = {}"
by (auto simp add: fv_def supp_Nil)
lemma fv_Cons[simp]: "fv (x # xs) = fv x ∪ fv xs"
by (auto simp add: fv_def supp_Cons)
lemma fv_Pair[simp]: "fv (x, y) = fv x ∪ fv y"
by (auto simp add: fv_def supp_Pair)
lemma fv_append[simp]: "fv (x @ y) = fv x ∪ fv y"
by (auto simp add: fv_def supp_append)
lemma fv_at_base[simp]: "fv a = {a::'a::at_base}"
by (auto simp add: fv_def supp_at_base)
lemma fv_pure[simp]: "fv (a::'a::pure) = {}"
by (auto simp add: fv_def pure_supp)

lemma fv_set_at_base[simp]: "fv (l :: ('a :: at_base) list) = set l"
by (induction l) auto

lemma flip_not_fv: "a ∉ fv x ⟹ b ∉ fv x ⟹ (a ↔ b) ∙ x = x"
by (metis flip_def fresh_def fv_def mem_Collect_eq swap_fresh_fresh)

lemma fv_not_fresh: "atom x ♯ e ⟷ x ∉ fv e"
unfolding fv_def fresh_def by blast

lemma fresh_fv: "finite (fv e :: 'a set) ⟹  atom (x :: ('a::at_base)) ♯ (fv e :: 'a set) ⟷ atom x ♯ e"
unfolding fv_def fresh_def

lemma finite_fv[simp]: "finite (fv (e::'a::fs) :: ('b::at_base) set)"
proof-
have "finite (supp e)" by (metis finite_supp)
hence "finite (atom - supp e :: 'b set)"
apply (rule finite_vimageI)
apply (rule inj_onI)
apply (simp)
done
moreover
have "(atom - supp e  :: 'b set) = fv e"   unfolding fv_def by auto
ultimately
show ?thesis by simp
qed

definition fv_list :: "'a::fs ⇒ 'b::at_base list"
where "fv_list e = (SOME l. set l = fv e)"

lemma set_fv_list[simp]: "set (fv_list e) = (fv e :: ('b::at_base) set)"
proof-
have "finite (fv e :: 'b set)" by (rule finite_fv)
from finite_list[OF finite_fv]
obtain l where "set l = (fv e :: 'b set)"..
thus ?thesis
unfolding fv_list_def by (rule someI)
qed

lemma fresh_fv_list[simp]:
"a ♯ (fv_list e :: 'b::at_base list) ⟷ a ♯ (fv e :: 'b::at_base set)"
proof-
have "a ♯ (fv_list e :: 'b::at_base list) ⟷ a ♯ set (fv_list e :: 'b::at_base list)"
by (rule fresh_set[symmetric])
also have "… ⟷ a ♯ (fv e :: 'b::at_base set)" by simp
finally show ?thesis.
qed

subsubsection ‹Other useful lemmas›

lemma pure_permute_id: "permute p = (λ x. (x::'a::pure))"

lemma supp_set_elem_finite:
assumes "finite S"
and "(m::'a::fs) ∈ S"
and "y ∈ supp m"
shows "y ∈ supp S"
using assms supp_of_finite_sets
by auto

lemmas fresh_star_Cons = fresh_star_list(2)

lemma mem_permute_set:
shows "x ∈ p ∙ S ⟷ (- p ∙ x) ∈ S"
by (metis mem_permute_iff permute_minus_cancel(2))

lemma flip_set_both_not_in:
assumes "x ∉ S" and "x' ∉ S"
shows "((x' ↔ x) ∙ S) = S"
unfolding permute_set_def
by (auto) (metis assms flip_at_base_simps(3))+

lemma inj_atom: "inj atom" by (metis atom_eq_iff injI)

lemmas image_Int[OF inj_atom, simp]

lemma eqvt_uncurry: "eqvt f ⟹ eqvt (case_prod f)"
unfolding eqvt_def
by perm_simp simp

lemma supp_fun_app_eqvt2:
assumes a: "eqvt f"
shows "supp (f x y) ⊆ supp x ∪ supp y"
proof-
from supp_fun_app_eqvt[OF eqvt_uncurry [OF a]]
have "supp (case_prod f (x,y)) ⊆ supp (x,y)".
thus ?thesis by (simp add: supp_Pair)
qed

lemma supp_fun_app_eqvt3:
assumes a: "eqvt f"
shows "supp (f x y z) ⊆ supp x ∪ supp y ∪ supp z"
proof-
from supp_fun_app_eqvt2[OF eqvt_uncurry [OF a]]
have "supp (case_prod f (x,y) z) ⊆ supp (x,y) ∪ supp z".
thus ?thesis by (simp add: supp_Pair)
qed

(* Fighting eta-contraction *)
lemma permute_0[simp]: "permute 0 = (λ x. x)"
by auto
lemma permute_comp[simp]: "permute x ∘ permute y = permute (x + y)" by auto

lemma map_permute: "map (permute p) = permute p"
apply rule
apply (induct_tac x)
apply auto
done

lemma fresh_star_restrictA[intro]: "a ♯* Γ ⟹ a ♯* AList.restrict V Γ"
by (induction Γ) (auto simp add: fresh_star_Cons)

(* Unused. Still submit? *)
lemma Abs_lst_Nil_eq[simp]: "[[]]lst. (x::'a::fs) = [xs]lst. x' ⟷ (([],x) = (xs, x'))"
apply rule
apply (frule Abs_lst_fcb2[where f = "λ x y _ . (x,y)" and as = "[]" and bs = "xs" and c = "()"])
done

(* Unused. Still submit? *)
lemma Abs_lst_Nil_eq2[simp]: "[xs]lst. (x::'a::fs) = [[]]lst. x' ⟷ ((xs,x) = ([], x'))"
by (subst eq_commute) auto

end


# Theory AList-Utils-Nominal

theory "AList-Utils-Nominal"
imports "AList-Utils" "Nominal-Utils"
begin

subsubsection ‹Freshness lemmas related to associative lists›

lemma domA_not_fresh:
"x ∈ domA Γ ⟹ ¬(atom x ♯ Γ)"
by (induct Γ, auto simp add: fresh_Cons fresh_Pair)

lemma fresh_delete:
assumes "a ♯ Γ"
shows "a ♯ delete v Γ"
using assms

lemma fresh_star_delete:
assumes "S ♯* Γ"
shows "S ♯* delete v Γ"
using assms fresh_delete unfolding fresh_star_def by fastforce

lemma fv_delete_subset:
"fv (delete v Γ) ⊆ fv Γ"
using fresh_delete unfolding fresh_def fv_def by auto

lemma fresh_heap_expr:
assumes "a ♯ Γ"
and "(x,e) ∈ set Γ"
shows "a ♯ e"
using assms
by (metis fresh_list_elem fresh_Pair)

lemma fresh_heap_expr':
assumes "a ♯ Γ"
and "e ∈ snd  set Γ"
shows "a ♯ e"
using assms
by (induct Γ, auto simp add: fresh_Cons fresh_Pair)

lemma fresh_star_heap_expr':
assumes "S ♯* Γ"
and "e ∈ snd  set Γ"
shows "S ♯* e"
using assms
by (metis fresh_star_def fresh_heap_expr')

lemma fresh_map_of:
assumes "x ∈ domA Γ"
assumes "a ♯ Γ"
shows "a ♯ the (map_of Γ x)"
using assms
by (induct Γ)(auto simp add: fresh_Cons fresh_Pair)

lemma fresh_star_map_of:
assumes "x ∈ domA Γ"
assumes "a ♯* Γ"
shows "a ♯* the (map_of Γ x)"
using assms by (simp add: fresh_star_def fresh_map_of)

lemma domA_fv_subset: "domA Γ ⊆ fv Γ"
by (induction Γ) auto

lemma map_of_fv_subset: "x ∈ domA Γ ⟹ fv (the (map_of Γ x)) ⊆ fv Γ"
by (induction Γ) auto

lemma map_of_Some_fv_subset: "map_of Γ x = Some e ⟹ fv e ⊆ fv Γ"
by (metis domA_from_set map_of_fv_subset map_of_SomeD option.sel)

subsubsection ‹Equivariance lemmas›

lemma domA[eqvt]:
"π ∙ domA Γ = domA (π ∙ Γ)"

lemma mapCollect[eqvt]:
"π ∙ mapCollect f m = mapCollect (π ∙ f) (π ∙ m)"
unfolding mapCollect_def
by perm_simp rule

subsubsection ‹Freshness and distinctness›

lemma fresh_distinct:
assumes "atom  S ♯* Γ"
shows "S ∩ domA Γ = {}"
proof-
{ fix x
assume "x ∈ S"
moreover
assume "x ∈ domA Γ"
hence "atom x ∈ supp Γ"
by (induct Γ)(auto simp add: supp_Cons domA_def supp_Pair supp_at_base)
ultimately
have False
using assms
}
thus "S ∩ domA Γ = {}" by auto
qed

lemma fresh_distinct_list:
assumes "atom  S ♯* l"
shows "S ∩ set l = {}"
using assms
by (metis disjoint_iff_not_equal fresh_list_elem fresh_star_def image_eqI not_self_fresh)

lemma fresh_distinct_fv:
assumes "atom  S ♯* l"
shows "S ∩ fv l = {}"
using assms
by (metis disjoint_iff_not_equal fresh_star_def fv_not_fresh image_eqI)

subsubsection ‹Pure codomains›

lemma domA_fv_pure:
fixes Γ :: "('a::at_base × 'b::pure) list"
shows  "fv Γ = domA Γ"
apply (induct Γ)
apply simp
apply (case_tac a)
apply (simp)
done

lemma domA_fresh_pure:
fixes Γ :: "('a::at_base × 'b::pure) list"
shows  "x ∈ domA Γ ⟷ ¬(atom x ♯ Γ)"
unfolding domA_fv_pure[symmetric]
by (auto simp add: fv_def fresh_def)

end


# Theory Nominal-HOLCF

theory "Nominal-HOLCF"
imports
"Nominal-Utils" "HOLCF-Utils"
begin

subsubsection ‹Type class of continuous permutations and variations thereof›

class cont_pt =
cpo +
pt +
assumes perm_cont: "⋀p. cont ((permute p) :: 'a::{cpo,pt} ⇒ 'a)"

class discr_pt =
discrete_cpo +
pt

class pcpo_pt =
cont_pt +
pcpo

instance pcpo_pt ⊆ cont_pt
by standard (auto intro: perm_cont)

instance discr_pt ⊆ cont_pt
by standard auto

lemma (in cont_pt) perm_cont_simp[simp]: "π ∙ x ⊑ π ∙ y ⟷ x ⊑ y"
apply rule
apply (drule cont2monofunE[OF perm_cont, of _ _ "-π"], simp)[1]
apply (erule cont2monofunE[OF perm_cont, of _ _ "π"])
done

lemma (in cont_pt) perm_below_to_right: "π ∙ x ⊑ y ⟷ x ⊑ - π ∙  y"
by (metis perm_cont_simp pt_class.permute_minus_cancel(2))

lemma perm_is_ub_simp[simp]: "π ∙ S <| π ∙ (x::'a::cont_pt) ⟷ S <| x"
by (auto simp add: is_ub_def permute_set_def)

lemma perm_is_ub_eqvt[simp,eqvt]: "S <| (x::'a::cont_pt) ⟹ π ∙ S <| π ∙ x"
by simp

lemma perm_is_lub_simp[simp]: "π ∙ S <<| π ∙ (x::'a::cont_pt) ⟷ S <<| x"
apply (rule perm_rel_lemma)
by (metis is_lubI is_lubD1 is_lubD2 perm_cont_simp perm_is_ub_simp)

lemma perm_is_lub_eqvt[simp,eqvt]: "S <<| (x::'a::cont_pt) ==> π ∙ S <<| π ∙ x"
by simp

lemmas perm_cont2cont[simp,cont2cont] = cont_compose[OF perm_cont]

lemma perm_still_cont: "cont (π ∙ f) = cont (f :: ('a :: cont_pt) ⇒ ('b :: cont_pt))"
proof
have imp:"⋀ (f :: 'a ⇒ 'b) π. cont f ⟹ cont (π ∙ f)"
unfolding permute_fun_def
by (metis cont_compose perm_cont)
show "cont f ⟹ cont (π ∙ f)" using imp[of "f" "π"].
show "cont (π ∙ f) ⟹ cont (f)" using imp[of "π ∙ f" "-π"] by simp
qed

lemma perm_bottom[simp,eqvt]: "π ∙ ⊥ = (⊥::'a::{cont_pt,pcpo})"
proof-
have "⊥ ⊑ -π ∙ (⊥::'a::{cont_pt,pcpo})" by simp
hence "π ∙ ⊥ ⊑ π ∙ (-π ∙ (⊥::'a::{cont_pt,pcpo}))" by(rule cont2monofunE[OF perm_cont])
hence "π ∙ ⊥ ⊑ (⊥::'a::{cont_pt,pcpo})" by simp
thus "π ∙ ⊥ = (⊥::'a::{cont_pt,pcpo})" by simp
qed

lemma bot_supp[simp]: "supp (⊥ :: 'a :: pcpo_pt) = {}"
by (rule supp_fun_eqvt) (simp add: eqvt_def)

lemma bot_fresh[simp]: "a ♯ (⊥ :: 'a :: pcpo_pt)"

lemma bot_fresh_star[simp]: "a ♯* (⊥ :: 'a :: pcpo_pt)"

lemma below_eqvt [eqvt]:
"π ∙ (x ⊑ y) = (π ∙ x ⊑ π ∙ (y::'a::cont_pt))" by (auto simp add: permute_pure)

lemma lub_eqvt[simp]:
"(∃ z. S <<| (z::'a::{cont_pt})) ⟹ π ∙ lub S = lub (π ∙ S)"
by (metis lub_eqI perm_is_lub_simp)

lemma chain_eqvt[eqvt]:
fixes F :: "nat ⇒ 'a::cont_pt"
shows "chain F ⟹ chain (π ∙ F)"
apply (rule chainI)
apply (drule_tac i = i in chainE)
apply (subst (asm) perm_cont_simp[symmetric, where π = π])
by (metis permute_fun_app_eq permute_pure)

subsubsection ‹Instance for @{type cfun}›

instantiation "cfun" :: (cont_pt, cont_pt) pt
begin
definition "p ∙ (f :: 'a  → 'b) = (Λ x. p ∙ (f ⋅ (- p ∙ x)))"

instance
apply standard
done
end

lemma permute_cfun_eq: "permute p = (λ f. (Abs_cfun (permute p)) oo f oo (Abs_cfun (permute (-p))))"
by (rule, rule cfun_eqI, auto simp add: permute_cfun_def)

lemma Cfun_app_eqvt[eqvt]:
"π ∙ (f ⋅ x) = (π ∙ f) ⋅ (π ∙ x)"
unfolding permute_cfun_def
by auto

lemma permute_Lam: "cont f ⟹ p ∙ (Λ x. f x) = (Λ x. (p ∙ f) x)"
apply (rule cfun_eqI)
unfolding permute_cfun_def
by (metis Abs_cfun_inverse2 eqvt_lambda unpermute_def )

lemma Abs_cfun_eqvt: "cont f ⟹ (p ∙ Abs_cfun) f = Abs_cfun f"
apply (subst permute_fun_def)
by (metis permute_Lam perm_still_cont permute_minus_cancel(1))

lemma cfun_eqvtI: "(⋀x. p ∙ (f ⋅ x) = f' ⋅ (p ∙ x)) ⟹ p ∙ f = f'"
by (metis Cfun_app_eqvt cfun_eqI permute_minus_cancel(1))

lemma ID_eqvt[eqvt]: "π ∙ ID = ID"
unfolding ID_def
apply perm_simp
done

instance "cfun" :: (cont_pt, cont_pt) cont_pt
by standard (subst permute_cfun_eq, auto)

instance "cfun" :: ("{pure,cont_pt}", "{pure,cont_pt}") pure
by standard (auto  simp add: permute_cfun_def permute_pure Cfun.cfun.Rep_cfun_inverse)

instance "cfun" :: (cont_pt, pcpo_pt) pcpo_pt
by standard

subsubsection ‹Instance for @{type fun}›

lemma permute_fun_eq: "permute p = (λ f. (permute p) ∘ f ∘ (permute (-p)))"
by (rule, rule, metis comp_apply eqvt_lambda unpermute_def)

instance "fun" :: (pt, cont_pt) cont_pt
apply standard
apply (rule cont2cont_lambda)
apply (subst permute_fun_def)
apply (rule perm_cont2cont)
apply (rule cont_fun)
done

lemma fix_eqvt[eqvt]:
"π ∙ fix = (fix :: ('a → 'a) → 'a::{cont_pt,pcpo})"
apply (rule cfun_eqI)
apply (subst permute_cfun_def)
apply simp
done

subsubsection ‹Instance for @{type u}›

(* Everything very pure. Does this work?
instantiation u :: (cpo) pt
begin
definition "p ∙ (x :: 'a u) = x"
instance by standard (auto simp add: permute_u_def)
end
instance u :: (cpo) pure by standard (simp add: permute_u_def)
instance u :: (cpo) cont_pt by standard (simp add: pure_permute_id)
instance u :: (cpo) pcpo_pt ..
*)

instantiation u :: (cont_pt) pt
begin
definition "p ∙ (x :: 'a u) = fup⋅(Λ x. up⋅(p ∙ x))⋅x"
instance
apply standard
apply (case_tac x) apply (auto simp add: permute_u_def)
apply (case_tac x) apply (auto simp add: permute_u_def)
done
end

instance u :: (cont_pt) cont_pt
proof
fix p
(* Fighting eta contraction... *)
have "permute p = (λ x. fup⋅(Λ x. up⋅(p ∙ x))⋅(x:: 'a u))"
by (rule ext, rule permute_u_def)
moreover have "cont (λ x. fup⋅(Λ x. up⋅(p ∙ x))⋅(x:: 'a u))" by simp
ultimately show "cont (permute p :: 'a u ⇒ 'a u)" by simp
qed

instance u :: (cont_pt) pcpo_pt ..

class pure_cont_pt = pure + cont_pt

instance u :: (pure_cont_pt) pure
apply standard
apply (case_tac x)
apply (auto simp add: permute_u_def permute_pure)
done

lemma up_eqvt[eqvt]: "π ∙ up = up"
apply (rule cfun_eqI)
apply (subst permute_cfun_def, simp)
done

lemma fup_eqvt[eqvt]: "π ∙ fup = fup"
apply (rule cfun_eqI)
apply (rule cfun_eqI)
apply (subst permute_cfun_def, simp)
apply (subst permute_cfun_def, simp)
apply (case_tac xa)
apply simp
done

subsubsection ‹Instance for @{type lift}›

instantiation lift :: (pt) pt
begin
definition "p ∙ (x :: 'a lift) = case_lift ⊥ (λ x. Def (p ∙ x)) x"
instance
apply standard
apply (case_tac x) apply (auto simp add: permute_lift_def)
apply (case_tac x) apply (auto simp add: permute_lift_def)
done
end

instance lift :: (pt) cont_pt
proof
fix p
(* Fighting eta contraction... *)
have "permute p = (λ x. case_lift ⊥ (λ x. Def (p ∙ x)) (x::'a lift))"
by (rule ext, rule permute_lift_def)
moreover have "cont (λ x. case_lift ⊥ (λ x. Def (p ∙ x)) (x::'a lift))" by simp
ultimately show "cont (permute p :: 'a lift ⇒ 'a lift)" by simp
qed

instance lift :: (pt) pcpo_pt ..

instance lift :: (pure) pure
apply standard
apply (case_tac x)
apply (auto simp add: permute_lift_def permute_pure)
done

lemma Def_eqvt[eqvt]: "π ∙ (Def x) = Def (π ∙ x)"

lemma case_lift_eqvt[eqvt]: "π ∙ case_lift d f x = case_lift (π ∙ d) (π ∙ f) (π ∙ x)"
by (cases x) (auto simp add: permute_self)

subsubsection ‹Instance for @{type prod}›

instance prod :: (cont_pt, cont_pt) cont_pt
proof
fix p
(* Fighting eta contraction... *)
have "permute p = (λ (x :: ('a, 'b) prod). (p ∙ fst x, p ∙ snd x))"  by auto
moreover have "cont ..." by (intro cont2cont)
ultimately show "cont (permute p :: ('a,'b) prod  ⇒ ('a,'b) prod)" by simp
qed

end


# 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)

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)

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


# Theory HasESem

theory HasESem
imports "Nominal-HOLCF" "Env-HOLCF"
begin

text ‹
A local to work abstract in the expression type and semantics.
›

locale has_ESem =
fixes ESem :: "'exp::pt ⇒ ('var::at_base ⇒ 'value) → 'value::{pure,pcpo}"
begin
abbreviation ESem_syn ("⟦ _ ⟧⇘_⇙"  [0,0] 110) where "⟦e⟧⇘ρ⇙ ≡ ESem e ⋅ ρ"
end

locale has_ignore_fresh_ESem = has_ESem +
assumes fv_supp: "supp e = atom  (fv e :: 'b set)"
assumes ESem_considers_fv: "⟦ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ f| (fv e)⇙"

end


# Theory Iterative

theory Iterative
imports "Env-HOLCF"
begin

text ‹
A setup for defining a fixed point of mutual recursive environments iteratively
›

locale iterative =
fixes ρ :: "'a::type ⇒ 'b::pcpo"
and e1 :: "('a ⇒ 'b) → ('a ⇒ 'b)"
and e2 :: "('a ⇒ 'b) → 'b"
and S :: "'a set" and x :: 'a
assumes ne:"x ∉ S"
begin
abbreviation "L == (Λ ρ'. (ρ ++⇘S⇙ e1 ⋅ ρ')(x := e2 ⋅ ρ'))"
abbreviation "H == (λ ρ'. Λ ρ''. ρ' ++⇘S⇙ e1 ⋅ ρ'')"
abbreviation "R == (Λ ρ'. (ρ ++⇘S⇙ (fix ⋅ (H ρ')))(x := e2 ⋅ ρ'))"
abbreviation "R' == (Λ ρ'. (ρ ++⇘S⇙ (fix ⋅ (H ρ')))(x := e2 ⋅ (fix ⋅ (H ρ'))))"

lemma split_x:
fixes y
obtains "y = x" and "y ∉ S" | "y ∈ S" and "y ≠ x" | "y ∉ S" and "y ≠ x" using ne by blast
lemmas below = fun_belowI[OF split_x, where y1 = "λx. x"]
lemmas eq = ext[OF split_x, where y1 = "λx. x"]

lemma lookup_fix[simp]:
fixes y and F :: "('a ⇒ 'b) → ('a ⇒ 'b)"
shows "(fix ⋅ F) y = (F ⋅ (fix ⋅ F)) y"
by (subst fix_eq, rule)

lemma R_S: "⋀ y. y ∈ S ⟹ (fix ⋅ R) y = (e1 ⋅ (fix ⋅ (H (fix ⋅ R)))) y"
by (case_tac y rule: split_x) simp_all

lemma R'_S: "⋀ y. y ∈ S ⟹ (fix ⋅ R') y = (e1 ⋅ (fix ⋅ (H (fix ⋅ R')))) y"
by (case_tac y rule: split_x) simp_all

lemma HR_is_R[simp]: "fix⋅(H (fix ⋅ R)) = fix ⋅ R"
by (rule eq) simp_all

lemma HR'_is_R'[simp]: "fix ⋅ (H (fix ⋅ R')) = fix ⋅ R'"
by (rule eq) simp_all

lemma H_noop:
fixes ρ' ρ''
assumes "⋀ y. y ∈ S ⟹ y ≠ x ⟹ (e1 ⋅ ρ'') y ⊑ ρ' y"
shows "H ρ' ⋅ ρ'' ⊑ ρ'"
using assms
by -(rule below, simp_all)

lemma HL_is_L[simp]: "fix ⋅ (H (fix ⋅ L)) = fix ⋅ L"
proof (rule below_antisym)
show "fix ⋅ (H (fix ⋅ L)) ⊑ fix ⋅ L"
by (rule fix_least_below[OF H_noop]) simp
hence *: "e2 ⋅ (fix ⋅ (H (fix ⋅ L))) ⊑ e2 ⋅ (fix ⋅ L)" by (rule monofun_cfun_arg)

show "fix ⋅ L ⊑ fix ⋅ (H (fix ⋅ L))"
by (rule fix_least_below[OF below]) (simp_all add: ne *)
qed

lemma iterative_override_on:
shows "fix ⋅ L = fix ⋅ R"
proof(rule below_antisym)
show "fix ⋅ R ⊑ fix ⋅ L"
by (rule fix_least_below[OF below]) simp_all

show "fix ⋅ L ⊑ fix ⋅ R"
apply (rule fix_least_below[OF below])
apply simp
apply (simp del: lookup_fix add: R_S)
apply simp
done
qed

lemma iterative_override_on':
shows "fix ⋅ L = fix ⋅  R'"
proof(rule below_antisym)
show "fix ⋅ R' ⊑ fix ⋅ L"
by (rule fix_least_below[OF below]) simp_all

show "fix ⋅ L ⊑ fix ⋅ R'"
apply (rule fix_least_below[OF below])
apply simp
apply (simp del: lookup_fix add: R'_S)
apply simp
done
qed
end

end


# Theory Env-Nominal

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

subsubsection ‹Equivariance lemmas›

lemma edom_perm:
fixes f :: "'a::pt ⇒ 'b::{pcpo_pt}"
shows "edom (π ∙ f) = π ∙ (edom f)"

lemmas edom_perm_rev[simp,eqvt] = edom_perm[symmetric]

lemma mem_edom_perm[simp]:
fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt}"
shows "xa ∈ edom (p ∙ ρ) ⟷ - p ∙ xa ∈ edom ρ"
by (metis (mono_tags) edom_perm_rev mem_Collect_eq permute_set_eq)

lemma env_restr_eqvt[eqvt]:
fixes m :: "'a::pt ⇒ 'b::{cont_pt,pcpo}"
shows "π ∙ m f| d = (π ∙ m) f| (π ∙ d)"

lemma env_delete_eqvt[eqvt]:
fixes m :: "'a::pt ⇒ 'b::{cont_pt,pcpo}"
shows "π ∙ env_delete x m = env_delete (π ∙ x) (π ∙ m)"

lemma esing_eqvt[eqvt]: "π ∙ (esing x) = esing (π ∙ x)"
unfolding esing_def
apply perm_simp
done

subsubsection ‹Permutation and restriction›

lemma env_restr_perm:
fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt,pure}"
assumes "supp p ♯* S" and [simp]: "finite S"
shows "(p ∙ ρ) f| S = ρ f| S"
using assms
apply -
apply (rule ext)
apply (case_tac "x ∈ S")
apply (simp)
apply (subst permute_fun_def)
apply (subst perm_supp_eq)
apply (auto simp add:perm_supp_eq supp_minus_perm fresh_star_def fresh_def supp_set_elem_finite)
done

lemma env_restr_perm':
fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt,pure}"
assumes "supp p ♯* S" and [simp]: "finite S"
shows "p ∙ (ρ f| S) = ρ f| S"
by (simp add: perm_supp_eq[OF assms(1)]  env_restr_perm[OF assms])

lemma env_restr_flip:
fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt,pure}"
assumes "x ∉ S" and "x' ∉ S"
shows "((x' ↔ x) ∙ ρ) f| S = ρ f| S"
using assms
apply -
apply rule
apply (auto  simp add: permute_flip_at env_restr_def split:if_splits)
by (metis eqvt_lambda flip_at_base_simps(3) minus_flip permute_pure unpermute_def)

lemma env_restr_flip':
fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt,pure}"
assumes "x ∉ S" and "x' ∉ S"
shows "(x' ↔ x) ∙ (ρ f| S) = ρ f| S"
by (simp add: flip_set_both_not_in[OF assms]  env_restr_flip[OF assms])

subsubsection ‹Pure codomains›
(*
lemma edom_fv_pure:
fixes f :: "('a::at_base ⇒ 'b::{pcpo,pure})"
assumes "finite (edom f)"
shows  "fv f = edom f"
using assms
proof (induction "edom f" arbitrary: f)
case empty
hence "f = ⊥" unfolding edom_def by auto
thus ?case by (auto simp add: fv_def fresh_def supp_def)
next
case (insert x S)
have "f = (env_delete x f)(x := f x)" by auto

from insert x S = edom f  and x ∉ S
have "S = edom (env_delete x f)" by auto
hence "fv (env_delete x f) = edom (env_delete x f)" by (rule insert)
*)

lemma edom_fv_pure:
fixes f :: "('a::at_base ⇒ 'b::{pcpo,pure})"
assumes "finite (edom f)"
shows  "fv f ⊆ edom f"
using assms
proof (induction "edom f" arbitrary: f)
case empty
hence "f = ⊥" unfolding edom_def by auto
thus ?case by (auto simp add: fv_def fresh_def supp_def)
next
case (insert x S)
have "f = (env_delete x f)(x := f x)" by auto
hence "fv f ⊆ fv (env_delete x f) ∪ fv x ∪ fv (f x)"
using eqvt_fresh_cong3[where f = fun_upd and x = "env_delete x f" and y = x and z = "f x", OF fun_upd_eqvt]
apply (auto simp add: fv_def fresh_def)
by (metis fresh_def pure_fresh)
also

from ‹insert x S = edom f›  and ‹x ∉ S›
have "S = edom (env_delete x f)" by auto
hence "fv (env_delete x f) ⊆ edom (env_delete x f)" by (rule insert)
also
have "fv (f x) = {}" by (rule fv_pure)
also
from ‹insert x S = edom f› have "x ∈ edom f" by auto
hence "edom (env_delete x f) ∪ fv x ∪ {} ⊆ edom f" by auto
finally
show ?case by this (intro Un_mono subset_refl)
qed

(*
lemma domA_fresh_pure:
fixes Γ :: "('a::at_base × 'b::pure) list"
shows  "x ∈ domA Γ ⟷ ¬(atom x ♯ Γ)"
unfolding domA_fv_pure[symmetric]
by (auto simp add: fv_def fresh_def)
*)

end


# Theory HeapSemantics

theory HeapSemantics
imports EvalHeap "AList-Utils-Nominal" HasESem Iterative "Env-Nominal"
begin

subsubsection ‹A locale for heap semantics, abstract in the expression semantics›

context has_ESem
begin

abbreviation EvalHeapSem_syn  ("❙⟦ _ ❙⟧⇘_⇙"  [0,0] 110)
where "EvalHeapSem_syn Γ ρ ≡ evalHeap Γ (λ e. ⟦e⟧⇘ρ⇙)"

definition
HSem :: "('var × 'exp) list ⇒ ('var ⇒ 'value) → ('var ⇒ 'value)"
where "HSem Γ = (Λ ρ . (μ ρ'. ρ ++⇘domA Γ⇙ ❙⟦Γ❙⟧⇘ρ'⇙))"

abbreviation HSem_syn ("⦃ _ ⦄_"  [0,60] 60)
where "⦃Γ⦄ρ ≡ HSem Γ ⋅ ρ"

lemma HSem_def': "⦃Γ⦄ρ = (μ ρ'. ρ ++⇘domA Γ⇙ ❙⟦Γ❙⟧⇘ρ'⇙)"
unfolding HSem_def by simp

subsubsection ‹Induction and other lemmas about @{term HSem}›

lemma HSem_ind:
assumes "P ⊥"
assumes step: "⋀ ρ'. P ρ' ⟹  P (ρ ++⇘domA Γ⇙ ❙⟦Γ❙⟧⇘ρ'⇙)"
shows "P (⦃Γ⦄ρ)"
unfolding HSem_def'
apply (rule fix_ind[OF assms(1), OF assms(2)])
using step by simp

lemma HSem_below:
assumes rho: "⋀x. x ∉ domA h ⟹ ρ x ⊑ r x"
assumes h: "⋀x. x ∈ domA h ⟹ ⟦the (map_of h x)⟧⇘r⇙ ⊑ r x"
shows "⦃h⦄ρ ⊑ r"
proof (rule HSem_ind, goal_cases)
case 1 show ?case by (auto)
next
case 2 show ?case by (rule minimal)
next
case (3 ρ')
show ?case
by (rule override_on_belowI)
(auto simp add: lookupEvalHeap  below_trans[OF monofun_cfun_arg[OF ‹ρ' ⊑ r›] h] rho)
qed

lemma HSem_bot_below:
assumes h: "⋀x. x ∈ domA h ⟹ ⟦the (map_of h x)⟧⇘r⇙ ⊑ r x"
shows "⦃h⦄⊥ ⊑ r"
using assms
by (metis HSem_below fun_belowD minimal)

lemma HSem_bot_ind:
assumes "P ⊥"
assumes step: "⋀ ρ'. P ρ' ⟹ P (❙⟦ Γ ❙⟧⇘ρ'⇙)"
shows "P (⦃Γ⦄⊥)"
apply (rule HSem_ind[OF assms(1,2)])
apply (drule assms(3))
apply simp
done

lemma parallel_HSem_ind:
assumes "adm (λρ'. P (fst ρ') (snd ρ'))"
assumes "P ⊥ ⊥"
assumes step: "⋀y z. P y z ⟹
P (ρ⇩1 ++⇘domA Γ⇩1⇙ ❙⟦Γ⇩1❙⟧⇘y⇙) (ρ⇩2 ++⇘domA Γ⇩2⇙ ❙⟦Γ⇩2❙⟧⇘z⇙)"
shows "P (⦃Γ⇩1⦄ρ⇩1) (⦃Γ⇩2⦄ρ⇩2)"
unfolding HSem_def'
apply (rule parallel_fix_ind[OF assms(1), OF assms(2)])
using step by simp

lemma HSem_eq:
shows "⦃Γ⦄ρ = ρ ++⇘domA Γ⇙ ❙⟦Γ❙⟧⇘⦃Γ⦄ρ⇙"
unfolding HSem_def'
by (subst fix_eq) simp

lemma HSem_bot_eq:
shows "⦃Γ⦄⊥ = ❙⟦Γ❙⟧⇘⦃Γ⦄⊥⇙"
by (subst HSem_eq) simp

lemma lookup_HSem_other:
assumes "y ∉ domA h"
shows "(⦃h⦄ρ) y = ρ y"
apply (subst HSem_eq)
using assms by simp

lemma lookup_HSem_heap:
assumes "y ∈ domA h"
shows "(⦃h⦄ρ) y = ⟦ the (map_of h y) ⟧⇘⦃h⦄ρ⇙"
apply (subst HSem_eq)
using assms by (simp add: lookupEvalHeap)

lemma HSem_edom_subset:  "edom (⦃Γ⦄ρ) ⊆ edom ρ ∪ domA Γ"
apply rule
unfolding edomIff
apply (case_tac "x ∈ domA Γ")
done

lemma (in -) env_restr_override_onI:"-S2 ⊆ S ⟹ env_restr S ρ1 ++⇘S2⇙ ρ2 = ρ1 ++⇘S2⇙ ρ2"
by (rule ext) (auto simp add: lookup_override_on_eq )

lemma HSem_restr:
"⦃h⦄(ρ f| (- domA h)) = ⦃h⦄ρ"
apply (rule parallel_HSem_ind)
apply simp
apply auto[1]
apply (subst env_restr_override_onI)
apply simp_all
done

lemma HSem_restr_cong:
assumes "ρ f| (- domA h) = ρ' f| (- domA h)"
shows "⦃h⦄ρ = ⦃h⦄ρ'"
apply (subst (1 2) HSem_restr[symmetric])

lemma HSem_restr_cong_below:
assumes "ρ f| (- domA h) ⊑ ρ' f| (- domA h)"
shows "⦃h⦄ρ ⊑ ⦃h⦄ρ'"
by (subst (1 2) HSem_restr[symmetric]) (rule monofun_cfun_arg[OF assms])

lemma HSem_reorder:
assumes "map_of Γ = map_of Δ"
shows "⦃Γ⦄ρ = ⦃Δ⦄ρ"
by (simp add: HSem_def' evalHeap_reorder[OF assms] assms dom_map_of_conv_domA[symmetric])

assumes "x ≠ y"
shows "⦃(x,e1)#(y,e2)#Γ⦄ρ = ⦃(y,e2)#(x,e1)#Γ⦄ρ"
proof-
have "set ((x,e1)#(y,e2)#Γ) = set ((y,e2)#(x,e1)#Γ)"
by auto
thus ?thesis
qed

assumes "x ∉ domA Γ"
shows "⦃(x,e)#Γ@Δ⦄ρ = ⦃Γ @ ((x,e)#Δ)⦄ρ"
proof-
have "set ((x,e)#Γ@Δ) = set (Γ @ ((x,e)#Δ))" by auto
thus ?thesis
by simp
qed

lemma env_restr_HSem:
assumes "domA Γ ∩ S = {}"
shows "(⦃ Γ ⦄ρ) f| S = ρ f| S"
proof (rule env_restr_eqI)
fix x
assume "x ∈ S"
hence "x ∉ domA Γ" using assms by auto
thus "(⦃ Γ ⦄ρ) x = ρ x"
by (rule lookup_HSem_other)
qed

lemma env_restr_HSem_noop:
assumes "domA Γ ∩ edom ρ = {}"
shows "(⦃ Γ ⦄ρ) f| edom ρ = ρ"
by (simp add: env_restr_HSem[OF assms] env_restr_useless)

lemma HSem_Nil[simp]: "⦃[]⦄ρ = ρ"
by (subst HSem_eq, simp)

subsubsection ‹Substitution›

lemma HSem_subst_exp:
assumes "⋀ρ'. ⟦ e ⟧⇘ρ'⇙ = ⟦ e' ⟧⇘ρ'⇙"
shows "⦃(x, e) # Γ⦄ρ = ⦃(x, e') # Γ⦄ρ"
by (rule parallel_HSem_ind) (auto simp add: assms evalHeap_subst_exp)

lemma HSem_subst_expr_below:
assumes below: "⟦ e1 ⟧⇘⦃(x, e2) # Γ⦄ρ⇙ ⊑ ⟦ e2 ⟧⇘⦃(x, e2) # Γ⦄ρ⇙"
shows "⦃(x, e1) # Γ⦄ρ ⊑ ⦃(x, e2) # Γ⦄ρ"
by (rule HSem_below) (auto simp add: lookup_HSem_heap below lookup_HSem_other)

lemma HSem_subst_expr:
assumes below1: "⟦ e1 ⟧⇘⦃(x, e2) # Γ⦄ρ⇙ ⊑ ⟦ e2 ⟧⇘⦃(x, e2) # Γ⦄ρ⇙"
assumes below2: "⟦ e2 ⟧⇘⦃(x, e1) # Γ⦄ρ⇙ ⊑ ⟦ e1 ⟧⇘⦃(x, e1) # Γ⦄ρ⇙"
shows "⦃(x, e1) # Γ⦄ρ = ⦃(x, e2) # Γ⦄ρ"
by (metis assms HSem_subst_expr_below below_antisym)

subsubsection ‹Re-calculating the semantics of the heap is idempotent›

lemma HSem_redo:
shows "⦃Γ⦄(⦃Γ @ Δ⦄ρ) f| (edom ρ ∪ domA Δ) = ⦃Γ @ Δ⦄ρ" (is "?LHS = ?RHS")
proof (rule below_antisym)
show "?LHS ⊑ ?RHS"
by (rule HSem_below)
(auto simp add: lookup_HSem_heap fun_belowD[OF env_restr_below_itself])

show "?RHS ⊑ ?LHS"
proof(rule HSem_below, goal_cases)
case (1 x)
thus ?case
by (cases "x ∉ edom ρ") (auto simp add: lookup_HSem_other dest:lookup_not_edom)
next
case prems: (2 x)
thus ?case
proof(cases "x ∈ domA Γ")
case True
thus ?thesis by (auto simp add: lookup_HSem_heap)
next
case False
hence delta: "x ∈ domA Δ" using prems by auto
with False ‹?LHS ⊑ ?RHS›
show ?thesis by (auto simp add: lookup_HSem_other lookup_HSem_heap monofun_cfun_arg)
qed
qed
qed

subsubsection ‹Iterative definition of the heap semantics›

lemma iterative_HSem:
assumes "x ∉ domA Γ"
shows "⦃(x,e) # Γ⦄ρ = (μ ρ'. (ρ ++⇘domA Γ⇙ (⦃Γ⦄ρ'))( x := ⟦e⟧⇘ρ'⇙))"
proof-
from assms
interpret iterative
where e1 =  "Λ ρ'. ❙⟦Γ❙⟧⇘ρ'⇙"
and e2 = "Λ ρ'. ⟦e⟧⇘ρ'⇙"
and S = "domA Γ"
and x = x by unfold_locales

have "⦃(x,e) # Γ⦄ρ = fix ⋅ L"
by (simp add: HSem_def' override_on_upd ne)
also have "… = fix ⋅ R"
by (rule iterative_override_on)
also have "… = (μ ρ'. (ρ ++⇘domA Γ⇙ (⦃Γ⦄ρ'))( x := ⟦e⟧⇘ρ'⇙))"
finally show ?thesis.
qed

lemma iterative_HSem':
assumes "x ∉ domA Γ"
shows "(μ ρ'. (ρ ++⇘domA Γ⇙ (⦃Γ⦄ρ'))( x := ⟦e⟧⇘ρ'⇙))
= (μ ρ'. (ρ ++⇘domA Γ⇙ (⦃Γ⦄ρ'))( x := ⟦e⟧⇘⦃Γ⦄ρ'⇙))"
proof-
from assms
interpret iterative
where e1 =  "Λ ρ'. ❙⟦Γ❙⟧⇘ρ'⇙"
and e2 = "Λ ρ'. ⟦e⟧⇘ρ'⇙"
and S = "domA Γ"
and x = x by unfold_locales

have "(μ ρ'. (ρ ++⇘domA Γ⇙ (⦃Γ⦄ρ'))( x := ⟦e⟧⇘ρ'⇙)) = fix ⋅ R"
also have "… = fix ⋅ L"
by (rule iterative_override_on[symmetric])
also have "… = fix ⋅ R'"
by (rule iterative_override_on')
also have "… = (μ ρ'. (ρ ++⇘domA Γ⇙ (⦃Γ⦄ρ'))( x := ⟦e⟧⇘⦃Γ⦄ρ'⇙))"
finally
show ?thesis.
qed

subsubsection ‹Fresh variables on the heap are irrelevant›

lemma HSem_ignores_fresh_restr':
assumes "fv Γ ⊆ S"
assumes "⋀ x ρ. x ∈ domA Γ ⟹ ⟦ the (map_of Γ x) ⟧⇘ρ⇙ = ⟦ the (map_of Γ x) ⟧⇘ρ f| (fv (the (map_of Γ x)))⇙"
shows "(⦃Γ⦄ρ) f| S = ⦃Γ⦄ρ f| S"
proof(induction rule: parallel_HSem_ind[case_names adm base step])
case adm thus ?case by simp
next
case base
show ?case by simp
next
case (step y z)
have "❙⟦ Γ ❙⟧⇘y⇙ = ❙⟦ Γ ❙⟧⇘z⇙"
proof(rule evalHeap_cong')
fix x
assume "x ∈ domA Γ"
hence "fv (the (map_of Γ x)) ⊆ fv Γ" by (rule map_of_fv_subset)
with assms(1)
have "fv (the (map_of Γ x)) ∩ S = fv (the (map_of Γ x))" by auto
with step
have "y f| fv (the (map_of Γ x)) = z f| fv (the (map_of Γ x))" by auto
with ‹x ∈ domA Γ›
show "⟦ the (map_of Γ x) ⟧⇘y⇙ = ⟦ the (map_of Γ x) ⟧⇘z⇙"
by (subst (1 2) assms(2)[OF ‹x ∈ domA Γ›]) simp
qed
moreover
have "domA Γ ⊆ S" using domA_fv_subset assms(1) by auto
ultimately
qed
end

subsubsection ‹Freshness›

context has_ignore_fresh_ESem begin

lemma ESem_fresh_cong:
assumes "ρ f| (fv e) = ρ' f| (fv e)"
shows "⟦ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ'⇙"
by (metis assms ESem_considers_fv)

lemma ESem_fresh_cong_subset:
assumes "fv e ⊆ S"
assumes "ρ f| S = ρ' f| S"
shows "⟦ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ'⇙"
by (rule ESem_fresh_cong[OF  env_restr_eq_subset[OF assms]])

lemma ESem_fresh_cong_below:
assumes "ρ f| (fv e) ⊑ ρ' f| (fv e)"
shows "⟦ e ⟧⇘ρ⇙ ⊑ ⟦ e ⟧⇘ρ'⇙"
by (metis assms ESem_considers_fv monofun_cfun_arg)

lemma ESem_fresh_cong_below_subset:
assumes "fv e ⊆ S"
assumes "ρ f| S ⊑ ρ' f| S"
shows "⟦ e ⟧⇘ρ⇙ ⊑ ⟦ e ⟧⇘ρ'⇙"
by (rule ESem_fresh_cong_below[OF  env_restr_below_subset[OF assms]])

lemma ESem_ignores_fresh_restr:
assumes "atom  S ♯* e"
shows "⟦ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ f| (- S)⇙"
proof-
have "fv e ∩ - S = fv e" using assms by (auto simp add: fresh_def fresh_star_def fv_supp)
thus ?thesis by (subst (1 2) ESem_considers_fv) simp
qed

lemma ESem_ignores_fresh_restr':
assumes "atom  (edom ρ - S) ♯* e"
shows "⟦ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ f| S⇙"
proof-
have "⟦ e ⟧⇘ρ⇙ =  ⟦ e ⟧⇘ρ f| (- (edom ρ - S))⇙"
by (rule ESem_ignores_fresh_restr[OF assms])
also have "ρ f| (- (edom ρ - S)) = ρ f| S"
by (rule ext) (auto simp add: lookup_env_restr_eq dest: lookup_not_edom)
finally show ?thesis.
qed

lemma HSem_ignores_fresh_restr'':
assumes "fv Γ ⊆ S"
shows "(⦃Γ⦄ρ) f| S = ⦃Γ⦄ρ f| S"
by (rule HSem_ignores_fresh_restr'[OF assms(1) ESem_considers_fv])

lemma HSem_ignores_fresh_restr:
assumes "atom  S ♯* Γ"
shows "(⦃Γ⦄ρ) f| (- S) = ⦃Γ⦄ρ f| (- S)"
proof-
from assms have "fv Γ ⊆ - S" by (auto simp add: fv_def fresh_star_def fresh_def)
thus ?thesis by (rule HSem_ignores_fresh_restr'')
qed

lemma HSem_fresh_cong_below:
assumes "ρ f| ((S ∪ fv Γ) - domA Γ) ⊑ ρ' f| ((S ∪ fv Γ) - domA Γ)"
shows "(⦃Γ⦄ρ) f| S ⊑ (⦃Γ⦄ρ') f| S"
proof-
from assms
have "⦃Γ⦄(ρ f| (S ∪ fv Γ)) ⊑ ⦃Γ⦄(ρ' f| (S ∪ fv Γ))"
by (auto intro: HSem_restr_cong_below simp add: Diff_eq inf_commute)
hence "(⦃Γ⦄ρ) f| (S ∪ fv Γ) ⊑ (⦃Γ⦄ρ') f| (S ∪ fv Γ)"
by (subst (1 2) HSem_ignores_fresh_restr'') simp_all
thus ?thesis
by (rule env_restr_below_subset[OF Un_upper1])
qed

lemma HSem_fresh_cong:
assumes "ρ f| ((S ∪ fv Γ) - domA Γ) = ρ' f| ((S ∪ fv Γ) - domA Γ)"
shows "(⦃Γ⦄ρ) f| S = (⦃Γ⦄ρ') f| S"
apply (rule below_antisym)
apply (rule HSem_fresh_cong_below[OF eq_imp_below[OF assms]])
apply (rule HSem_fresh_cong_below[OF eq_imp_below[OF assms[symmetric]]])
done

subsubsection ‹Adding a fresh variable to a heap does not affect its semantics›

assumes fresh: "atom x ♯ Γ"
assumes "x ∉ edom ρ"
assumes step: "⋀e ρ'. e ∈ snd  set Γ ⟹ ⟦ e ⟧⇘ρ'⇙ = ⟦ e ⟧⇘env_delete x ρ'⇙"
shows  "env_delete x (⦃(x, e) # Γ⦄ρ) = ⦃Γ⦄ρ"
proof (rule parallel_HSem_ind, goal_cases)
case 1 show ?case by simp
next
case 2 show ?case by auto
next
case prems: (3 y z)
have "env_delete x ρ = ρ" using ‹x ∉ edom ρ› by (rule env_delete_noop)
moreover
from fresh have "x ∉ domA Γ" by (metis domA_not_fresh)
hence "env_delete x (❙⟦ (x, e) # Γ ❙⟧⇘y⇙) = ❙⟦ Γ ❙⟧⇘y⇙"
by (auto intro: env_delete_noop dest:  subsetD[OF edom_evalHeap_subset])
moreover
have "… = ❙⟦ Γ ❙⟧⇘z⇙"
apply (rule evalHeap_cong[OF refl])
apply (subst (1) step, assumption)
using prems(1) apply auto
done
ultimately
show ?case using ‹x ∉ domA Γ›
qed

assumes "atom x ♯ Γ"
assumes "x ∉ edom ρ"
shows  "env_delete x (⦃(x, e) # Γ⦄ρ) = ⦃Γ⦄ρ"
case (1 e ρ')
assume "e ∈ snd  set Γ"
hence "atom x ♯ e" by (metis assms(1) fresh_heap_expr')
hence "x ∉ fv e" by (simp add: fv_def fresh_def)
thus ?case
by (rule ESem_fresh_cong[OF env_restr_env_delete_other[symmetric]])
qed

subsubsection ‹Mutual recursion with fresh variables›

lemma HSem_subset_below:
assumes fresh: "atom  domA Γ ♯* Δ"
shows "⦃Δ⦄(ρ f| (- domA Γ)) ⊑ (⦃Δ@Γ⦄ρ)  f| (- domA Γ)"
proof(rule HSem_below)
fix x
assume [simp]: "x ∈ domA Δ"
with assms have *: "atom  domA Γ ♯* the (map_of Δ x)" by (metis fresh_star_map_of)
hence [simp]: "x ∉ domA Γ" using fresh ‹x ∈ domA Δ› by (metis fresh_star_def domA_not_fresh image_eqI)
show "⟦ the (map_of Δ x) ⟧⇘(⦃Δ @ Γ⦄ρ) f| (- domA Γ)⇙ ⊑ ((⦃Δ @ Γ⦄ρ) f| (- domA Γ)) x"
by (simp add: lookup_HSem_heap ESem_ignores_fresh_restr[OF *, symmetric])

text ‹In the following lemma we show that the semantics of fresh variables can be be calculated
together with the presently bound variables, or separately.›

lemma HSem_merge:
assumes fresh: "atom  domA Γ ♯* Δ"
shows "⦃Γ⦄⦃Δ⦄ρ = ⦃Γ@Δ⦄ρ"
proof(rule below_antisym)
have map_of_eq: "map_of (Δ @ Γ) = map_of (Γ @ Δ)"
proof
fix x
show "map_of (Δ @ Γ) x = map_of (Γ @ Δ) x"
proof (cases "x ∈ domA Γ")
case True
hence "x ∉ domA Δ" by (metis fresh_distinct fresh IntI equals0D)
thus "map_of (Δ @ Γ) x = map_of (Γ @ Δ) x"
next
case False
thus "map_of (Δ @ Γ) x = map_of (Γ @ Δ) x"
qed
qed

show "⦃Γ⦄⦃Δ⦄ρ ⊑ ⦃Γ@Δ⦄ρ"
proof(rule HSem_below)
fix x
assume [simp]:"x ∉ domA Γ"

have "(⦃Δ⦄ρ) x = ((⦃Δ⦄ρ) f| (- domA Γ)) x" by simp
also have "… = (⦃Δ⦄(ρ f| (- domA Γ))) x"
by (rule arg_cong[OF HSem_ignores_fresh_restr[OF fresh]])
also have "… ⊑ ((⦃Δ@Γ⦄ρ)  f| (- domA Γ)) x"
by (rule fun_belowD[OF HSem_subset_below[OF fresh]] )
also have "… = (⦃Δ@Γ⦄ρ) x" by simp
also have "… = (⦃Γ @ Δ⦄ρ) x" by (rule arg_cong[OF HSem_reorder[OF map_of_eq]])
finally
show "(⦃Δ⦄ρ) x ⊑ (⦃Γ @ Δ⦄ρ) x".
qed (auto simp add: lookup_HSem_heap lookup_env_restr_eq)

have *: "⋀ x. x ∈ domA Δ ⟹ x ∉ domA Γ"
using fresh by (auto simp add: fresh_Pair fresh_star_def domA_not_fresh)

have foo: "edom ρ ∪ domA Δ ∪ domA Γ - (edom ρ ∪ domA Δ ∪ domA Γ) ∩ - domA Γ = domA Γ" by auto
have foo2:"(edom ρ ∪ domA Δ - (edom ρ ∪ domA Δ) ∩ - domA Γ) ⊆ domA Γ" by auto

{ fix x
assume "x ∈ domA Δ"
hence *: "atom  domA Γ ♯* the (map_of Δ x)"
by (rule  fresh_star_map_of[OF _ fresh])

have "⟦ the (map_of Δ x) ⟧⇘⦃Γ⦄⦃Δ⦄ρ⇙ = ⟦ the (map_of Δ x) ⟧⇘(⦃Γ⦄⦃Δ⦄ρ) f| (- domA Γ)⇙"
by (rule ESem_ignores_fresh_restr[OF *])
also have "(⦃Γ⦄⦃Δ⦄ρ) f| (- domA Γ) = (⦃Δ⦄ρ) f| (- domA Γ)"
also have "⟦ the (map_of Δ x) ⟧⇘…⇙ = ⟦ the (map_of Δ x) ⟧⇘⦃Δ⦄ρ⇙"
by (rule ESem_ignores_fresh_restr[symmetric, OF *])
finally
have "⟦ the (map_of Δ x) ⟧⇘⦃Γ⦄⦃Δ⦄ρ⇙ = ⟦ the (map_of Δ x) ⟧⇘⦃Δ⦄ρ⇙".
}
thus "⦃Γ@Δ⦄ρ ⊑ ⦃Γ⦄⦃Δ⦄ρ"
by -(rule HSem_below, auto simp add: lookup_HSem_other lookup_HSem_heap *)
qed
end

subsubsection ‹Parallel induction›

lemma parallel_HSem_ind_different_ESem:
assumes "adm (λρ'. P (fst ρ') (snd ρ'))"
assumes "P ⊥ ⊥"
assumes "⋀y z. P y z ⟹ P (ρ ++⇘domA h⇙ evalHeap h (λe. ESem1 e ⋅ y)) (ρ2 ++⇘domA h2⇙ evalHeap h2 (λe. ESem2 e ⋅ z))"
shows "P (has_ESem.HSem ESem1 h⋅ρ) (has_ESem.HSem ESem2 h2⋅ρ2)"
proof-
interpret HSem1: has_ESem ESem1.
interpret HSem2: has_ESem ESem2.

show ?thesis
unfolding HSem1.HSem_def' HSem2.HSem_def'
apply (rule parallel_fix_ind[OF assms(1)])
apply (rule assms(2))
apply simp
apply (erule assms(3))
done
qed

subsubsection ‹Congruence rule›

lemma HSem_cong[fundef_cong]:
"⟦ (⋀ e. e ∈ snd  set heap2 ⟹ ESem1 e = ESem2 e); heap1 = heap2  ⟧
⟹ has_ESem.HSem ESem1 heap1 = has_ESem.HSem ESem2 heap2"
unfolding has_ESem.HSem_def
by (auto cong:evalHeap_cong)

subsubsection ‹Equivariance of the heap semantics›

lemma HSem_eqvt[eqvt]:
"π ∙ has_ESem.HSem ESem Γ = has_ESem.HSem (π ∙ ESem) (π ∙ Γ)"
proof-
show ?thesis
unfolding has_ESem.HSem_def
apply (subst permute_Lam, simp)
apply (subst eqvt_lambda)
done
qed

end


# Theory Vars

theory Vars
imports Nominal2.Nominal2
begin

text ‹
The type of variables is abstract and provided by the Nominal package. All we know is that it is countable.
›

atom_decl var

end


# Theory Terms

theory Terms
imports "Nominal-Utils" Vars  "AList-Utils-Nominal"
begin

subsubsection ‹Expressions›

text ‹
This is the main data type of the development; our minimal lambda calculus with recursive let-bindings.
It is created using the nominal\_datatype command, which creates alpha-equivalence classes.

The package does not support nested recursion, so the bindings of the let cannot simply be of type
‹(var, exp) list›. Instead, the definition of lists have to be inlined here, as the custom type
‹assn›. Later we create conversion functions between these two types, define a properly typed ‹let›
and redo the various lemmas in terms of that, so that afterwards, the type ‹assn› is no longer
referenced.
›

nominal_datatype exp =
Var var
| App exp var
| LetA as::assn body::exp binds "bn as" in body as
| Lam x::var body::exp binds x in body  ("Lam [_]. _" [100, 100] 100)
| Bool bool
| IfThenElse exp exp exp  ("((_)/ ? (_)/ : (_))" [0, 0, 10] 10)
and assn =
ANil | ACons var exp assn
binder
bn :: "assn ⇒ atom list"
where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"

notation (latex output) Terms.Var ("_")
notation (latex output) Terms.App ("_ _")
notation (latex output) Terms.Lam ("λ_. _"  [100, 100] 100)

type_synonym heap = "(var × exp) list"

lemma exp_assn_size_eqvt[eqvt]: "p ∙ (size :: exp ⇒ nat) = size"
by (metis exp_assn.size_eqvt(1) fun_eqvtI permute_pure)

subsubsection ‹Rewriting in terms of heaps›

text ‹
We now work towards using @{type heap} instead of @{type assn}. All this
could be skipped if Nominal supported nested recursion.
›

text ‹
Conversion from @{typ assn} to @{typ heap}.
›

nominal_function asToHeap :: "assn ⇒ heap"
where ANilToHeap: "asToHeap ANil = []"
| AConsToHeap: "asToHeap (ACons v e as) = (v, e) # asToHeap as"
unfolding eqvt_def asToHeap_graph_aux_def
apply rule
apply simp
apply rule
apply(case_tac x rule: exp_assn.exhaust(2))
apply auto
done
nominal_termination(eqvt) by lexicographic_order

lemma asToHeap_eqvt: "eqvt asToHeap"
unfolding eqvt_def
by (auto simp add: permute_fun_def asToHeap.eqvt)

text ‹The other direction.›

fun heapToAssn :: "heap ⇒ assn"
where "heapToAssn [] = ANil"
| "heapToAssn ((v,e)#Γ) = ACons v e (heapToAssn Γ)"

declare heapToAssn.simps[simp del]

lemma heapToAssn_eqvt[simp,eqvt]: "p ∙ heapToAssn Γ =  heapToAssn (p ∙ Γ)"
by (induct Γ rule: heapToAssn.induct)

lemma bn_heapToAssn: "bn (heapToAssn Γ) = map (λx. atom (fst x)) Γ"
by (induct rule: heapToAssn.induct)

lemma set_bn_to_atom_domA:
"set (bn as) = atom  domA (asToHeap as)"
by (induct as rule: asToHeap.induct)

text ‹
They are inverse to each other.
›

lemma heapToAssn_asToHeap[simp]:
"heapToAssn (asToHeap as) = as"
by (induct  rule: exp_assn.inducts(2)[of "λ _ . True"])

lemma asToHeap_heapToAssn[simp]:
"asToHeap (heapToAssn as) = as"
by (induct rule: heapToAssn.induct)

lemma heapToAssn_inject[simp]:
"heapToAssn x = heapToAssn y ⟷ x = y"
by (metis asToHeap_heapToAssn)

text ‹
They are transparent to various notions from the Nominal package.
›

lemma supp_heapToAssn: "supp (heapToAssn Γ) = supp Γ"
by (induct rule: heapToAssn.induct)
(simp_all add: heapToAssn.simps  exp_assn.supp supp_Nil supp_Cons supp_Pair sup_assoc)

lemma supp_asToHeap: "supp (asToHeap as) = supp as"
by (induct as rule: asToHeap.induct)
(simp_all add:  exp_assn.supp supp_Nil supp_Cons supp_Pair sup_assoc)

lemma fv_asToHeap: "fv (asToHeap Γ) = fv Γ"
unfolding fv_def by (auto simp add: supp_asToHeap)

lemma fv_heapToAssn: "fv (heapToAssn Γ) = fv Γ"
unfolding fv_def by (auto simp add: supp_heapToAssn)

lemma [simp]: "size (heapToAssn Γ) = size_list (λ (v,e) . size e) Γ"
by (induct rule: heapToAssn.induct)

lemma Lam_eq_same_var[simp]: "Lam [y]. e = Lam [y]. e' ⟷  e = e'"
by auto (metis fresh_PairD(2) obtain_fresh)

text ‹Now we define the Let constructor in the form that we actually want.›

hide_const HOL.Let
definition Let :: "heap ⇒ exp ⇒ exp"
where "Let Γ e = LetA (heapToAssn Γ) e"

notation (latex output) Let ("\<^latex>‹\\textrm{\\textsf{let}}› _ \<^latex>‹\\textrm{\\textsf{in}}› _")

abbreviation
LetBe :: "var⇒exp⇒exp⇒exp" ("let _ be _ in _ " [100,100,100] 100)
where
"let x be t1 in t2 ≡ Let [(x,t1)] t2"

text ‹
We rewrite all (relevant) lemmas about @{term LetA} in terms of @{term Let}.
›

lemma size_Let[simp]: "size (Let Γ e) = size_list (λp. size (snd p)) Γ + size e + Suc 0"
unfolding Let_def by (auto simp add: split_beta')

lemma Let_distinct[simp]:
"Var v ≠ Let Γ e"
"Let Γ e ≠ Var v"
"App e v ≠ Let Γ e'"
"Lam [v]. e' ≠ Let Γ e"
"Let Γ e ≠ Lam [v]. e'"
"Let Γ e' ≠ App e v"
"Bool b ≠ Let Γ e"
"Let Γ e ≠ Bool b"
"(scrut ? e1 : e2) ≠ Let Γ e"
"Let Γ e ≠ (scrut ? e1 : e2)"
unfolding Let_def by simp_all

lemma Let_perm_simps[simp,eqvt]:
"p ∙ Let Γ e = Let (p ∙ Γ) (p ∙ e)"
unfolding Let_def by simp

lemma Let_supp:
"supp (Let Γ e) = (supp e ∪ supp Γ) - atom  (domA Γ)"
unfolding Let_def by (simp add: exp_assn.supp supp_heapToAssn bn_heapToAssn domA_def image_image)

lemma Let_fresh[simp]:
"a ♯ Let Γ e = (a ♯ e ∧ a ♯ Γ ∨ a ∈ atom  domA Γ)"
unfolding fresh_def by (auto simp add: Let_supp)

lemma Abs_eq_cong:
assumes "⋀ p. (p ∙ x = x') ⟷ (p ∙ y = y')"
assumes "supp y = supp x"
assumes "supp y' = supp x'"
shows "([a]lst. x = [a']lst. x') ⟷ ([a]lst. y = [a']lst. y')"
by (simp add: Abs_eq_iff alpha_lst assms)

lemma Let_eq_iff[simp]:
"(Let Γ e = Let Γ' e') = ([map (λx. atom (fst x)) Γ ]lst. (e, Γ) = [map (λx. atom (fst x)) Γ']lst. (e',Γ'))"
unfolding Let_def
apply (rule Abs_eq_cong)
done

lemma exp_strong_exhaust:
fixes c :: "'a :: fs"
assumes "⋀var. y = Var var ⟹ P"
assumes "⋀exp var. y = App exp var ⟹ P"
assumes "⋀Γ exp. atom  domA Γ ♯* c ⟹ y = Let Γ exp ⟹ P"
assumes "⋀var exp. {atom var} ♯* c ⟹ y = Lam [var]. exp ⟹ P"
assumes "⋀ b. (y = Bool b) ⟹ P"
assumes "⋀ scrut e1 e2. y = (scrut ? e1 : e2) ⟹ P"
shows P
apply (rule  exp_assn.strong_exhaust(1)[where y = y and c = c])
apply (metis assms(1))
apply (metis assms(2))
apply (metis assms(3) set_bn_to_atom_domA Let_def heapToAssn_asToHeap)
apply (metis assms(4))
apply (metis assms(5))
apply (metis assms(6))
done

text ‹
And finally the induction rules with @{term Let}.
›

lemma exp_heap_induct[case_names Var App Let Lam Bool IfThenElse Nil Cons]:
assumes "⋀b var. P1 (Var var)"
assumes "⋀exp var. P1 exp ⟹ P1 (App exp var)"
assumes "⋀Γ exp. P2 Γ ⟹ P1 exp ⟹ P1 (Let Γ exp)"
assumes "⋀var exp. P1 exp ⟹ P1 (Lam [var]. exp)"
assumes "⋀ b. P1 (Bool b)"
assumes "⋀ scrut e1 e2. P1 scrut ⟹ P1 e1 ⟹ P1 e2 ⟹ P1 (scrut ? e1 : e2)"
assumes "P2 []"
assumes "⋀var exp Γ. P1 exp ⟹ P2 Γ ⟹ P2 ((var, exp)#Γ)"
shows "P1 e" and "P2 Γ"
proof-
have "P1 e" and "P2 (asToHeap (heapToAssn Γ))"
apply (induct rule: exp_assn.inducts[of P1 "λ assn. P2 (asToHeap assn)"])
apply (metis assms(1))
apply (metis assms(2))
apply (metis assms(3) Let_def heapToAssn_asToHeap )
apply (metis assms(4))
apply (metis assms(5))
apply (metis assms(6))
apply (metis assms(7) asToHeap.simps(1))
apply (metis assms(8) asToHeap.simps(2))
done
thus "P1 e" and "P2 Γ" unfolding asToHeap_heapToAssn.
qed

lemma exp_heap_strong_induct[case_names Var App Let Lam Bool IfThenElse Nil Cons]:
assumes "⋀var c. P1 c (Var var)"
assumes "⋀exp var c. (⋀c. P1 c exp) ⟹ P1 c (App exp var)"
assumes "⋀Γ exp c. atom  domA Γ ♯* c ⟹ (⋀c. P2 c Γ) ⟹ (⋀c. P1 c exp) ⟹ P1 c (Let Γ exp)"
assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P1 c exp) ⟹ P1 c (Lam [var]. exp)"
assumes "⋀ b c. P1 c (Bool b)"
assumes "⋀ scrut e1 e2 c. (⋀ c. P1 c scrut) ⟹ (⋀ c. P1 c e1) ⟹ (⋀ c. P1 c e2) ⟹ P1 c (scrut ? e1 : e2)"
assumes "⋀c. P2 c []"
assumes "⋀var exp Γ c. (⋀c. P1 c exp) ⟹ (⋀c. P2 c Γ) ⟹ P2 c ((var,exp)#Γ)"
fixes c :: "'a :: fs"
shows "P1 c e" and "P2 c Γ"
proof-
have "P1 c e" and "P2 c (asToHeap (heapToAssn Γ))"
apply (induct rule: exp_assn.strong_induct[of P1 "λ c assn. P2 c (asToHeap assn)"])
apply (metis assms(1))
apply (metis assms(2))
apply (metis assms(3) set_bn_to_atom_domA Let_def heapToAssn_asToHeap )
apply (metis assms(4))
apply (metis assms(5))
apply (metis assms(6))
apply (metis assms(7) asToHeap.simps(1))
apply (metis assms(8) asToHeap.simps(2))
done
thus "P1 c e" and "P2 c Γ" unfolding asToHeap_heapToAssn.
qed

subsubsection ‹Nice induction rules›

text ‹
These rules can be used instead of the original induction rules, which require a separate
goal for @{typ assn}.
›

lemma exp_induct[case_names Var App Let Lam Bool IfThenElse]:
assumes "⋀var. P (Var var)"
assumes "⋀exp var. P exp ⟹ P (App exp var)"
assumes "⋀Γ exp. (⋀ x. x ∈ domA Γ ⟹  P (the (map_of Γ x))) ⟹ P exp ⟹ P (Let Γ exp)"
assumes "⋀var exp.  P exp ⟹ P (Lam [var]. exp)"
assumes "⋀ b. P (Bool b)"
assumes "⋀ scrut e1 e2. P scrut ⟹ P e1 ⟹ P e2 ⟹ P (scrut ? e1 : e2)"
shows "P exp"
apply (rule exp_heap_induct[of P "λ Γ. (∀x ∈ domA Γ. P (the (map_of Γ x)))"])
apply (metis assms(1))
apply (metis assms(2))
apply (metis assms(3))
apply (metis assms(4))
apply (metis assms(5))
apply (metis assms(6))
apply auto
done

lemma  exp_strong_induct_set[case_names Var App Let Lam Bool IfThenElse]:
assumes "⋀var c. P c (Var var)"
assumes "⋀exp var c. (⋀c. P c exp) ⟹ P c (App exp var)"
assumes "⋀Γ exp c.
atom  domA Γ ♯* c ⟹ (⋀c x e. (x,e) ∈ set Γ ⟹  P c e) ⟹ (⋀c. P c exp) ⟹ P c (Let Γ exp)"
assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P c exp) ⟹ P c (Lam [var]. exp)"
assumes "⋀b c. P c (Bool b)"
assumes "⋀scrut e1 e2 c. (⋀ c. P c scrut) ⟹ (⋀ c. P c e1) ⟹ (⋀ c. P c e2) ⟹ P c (scrut ? e1 : e2)"
shows "P (c::'a::fs) exp"
apply (rule exp_heap_strong_induct(1)[of P "λ c Γ. (∀(x,e) ∈ set Γ. P c e)"])
apply (metis assms(1))
apply (metis assms(2))
apply (metis assms(3) split_conv)
apply (metis assms(4))
apply (metis assms(5))
apply (metis assms(6))
apply auto
done

lemma  exp_strong_induct[case_names Var App Let Lam Bool IfThenElse]:
assumes "⋀var c. P c (Var var)"
assumes "⋀exp var c. (⋀c. P c exp) ⟹ P c (App exp var)"
assumes "⋀Γ exp c.
atom  domA Γ ♯* c ⟹ (⋀c x. x ∈ domA Γ ⟹  P c (the (map_of Γ x))) ⟹ (⋀c. P c exp) ⟹ P c (Let Γ exp)"
assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P c exp) ⟹ P c (Lam [var]. exp)"
assumes "⋀b c. P c (Bool b)"
assumes "⋀ scrut e1 e2 c. (⋀ c. P c scrut) ⟹ (⋀ c. P c e1) ⟹ (⋀ c. P c e2) ⟹ P c (scrut ? e1 : e2)"
shows "P (c::'a::fs) exp"
apply (rule exp_heap_strong_induct(1)[of P "λ c Γ. (∀x ∈ domA Γ. P c (the (map_of Γ x)))"])
apply (metis assms(1))
apply (metis assms(2))
apply (metis assms(3))
apply (metis assms(4))
apply (metis assms(5))
apply (metis assms(6))
apply auto
done

subsubsection ‹Testing alpha equivalence›

lemma alpha_test:
shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
by (simp add: Abs1_eq_iff fresh_at_base pure_fresh)

lemma alpha_test2:
shows "let x be (Var x) in (Var x) = let y be (Var y) in (Var y)"

lemma alpha_test3:
shows "
Let [(x, Var y), (y, Var x)] (Var x)
=
Let [(y, Var x), (x, Var y)] (Var y)" (is "Let ?la ?lb = _")
by (simp add: bn_heapToAssn Abs1_eq_iff fresh_Pair fresh_at_base
Abs_swap2[of "atom x" "(?lb, [(x, Var y), (y, Var x)])" "[atom x, atom y]" "atom y"])

subsubsection ‹Free variables›

lemma fv_supp_exp: "supp e = atom  (fv (e::exp) :: var set)" and fv_supp_as: "supp as = atom  (fv (as::assn) :: var set)"
by (induction e and as rule:exp_assn.inducts)
(auto simp add: fv_def exp_assn.supp supp_at_base pure_supp)

lemma fv_supp_heap: "supp (Γ::heap) = atom  (fv Γ :: var set)"
by (metis fv_def fv_supp_as supp_heapToAssn)

lemma fv_Lam[simp]: "fv (Lam [x]. e) = fv e - {x}"
unfolding fv_def by (auto simp add: exp_assn.supp)
lemma fv_Var[simp]: "fv (Var x) = {x}"
unfolding fv_def by (auto simp add: exp_assn.supp supp_at_base pure_supp)
lemma fv_App[simp]: "fv (App e x) = insert x (fv e)"
unfolding fv_def by (auto simp add: exp_assn.supp supp_at_base)
lemma fv_Let[simp]: "fv (Let Γ e) = (fv Γ ∪ fv e) - domA Γ"
unfolding fv_def by (auto simp add: Let_supp exp_assn.supp supp_at_base set_bn_to_atom_domA)
lemma fv_Bool[simp]: "fv (Bool b) = {}"
unfolding fv_def by (auto simp add: exp_assn.supp pure_supp)
lemma fv_IfThenElse[simp]: "fv (scrut ? e1 : e2)  = fv scrut ∪ fv e1 ∪ fv e2"
unfolding fv_def by (auto simp add: exp_assn.supp)

lemma fv_delete_heap:
assumes "map_of Γ x = Some e"
shows "fv (delete x Γ, e) ∪ {x} ⊆ (fv (Γ, Var x) :: var set)"
proof-
have "fv (delete x Γ) ⊆ fv Γ" by (metis fv_delete_subset)
moreover
have "(x,e) ∈ set Γ" by (metis assms map_of_SomeD)
hence "fv e ⊆ fv Γ" by (metis assms domA_from_set map_of_fv_subset option.sel)
moreover
have "x ∈ fv (Var x)" by simp
ultimately show ?thesis by auto
qed

subsubsection ‹Lemmas helping with nominal definitions›

lemma eqvt_lam_case:
assumes "Lam [x]. e = Lam [x']. e'"
assumes "⋀ π . supp (-π) ♯* (fv (Lam [x]. e) :: var set) ⟹
supp π ♯* (Lam [x]. e) ⟹
F (π ∙ e) (π ∙ x) (Lam [x]. e) = F e x (Lam [x]. e)"
shows "F e x (Lam [x]. e) = F e' x' (Lam [x']. e')"
proof-

from assms(1)
have "[[atom x]]lst. (e, x) = [[atom x']]lst. (e', x')" by auto
then obtain p
where "(supp (e, x) - {atom x}) ♯* p"
and [simp]: "p ∙ x = x'"
and [simp]: "p ∙ e = e'"
unfolding  Abs_eq_iff(3) alpha_lst.simps by auto

from ‹_ ♯* p›
have *: "supp (-p) ♯* (fv (Lam [x]. e) :: var set)"
by (auto simp add: fresh_star_def fresh_def supp_finite_set_at_base supp_Pair fv_supp_exp fv_supp_heap supp_minus_perm)

from ‹_ ♯* p›
have **: "supp p ♯* Lam [x]. e"
by (auto simp add: fresh_star_def fresh_def supp_Pair fv_supp_exp)

have "F e x (Lam [x]. e) =  F (p ∙ e) (p ∙ x) (Lam [x]. e)" by (rule assms(2)[OF * **, symmetric])
also have "… = F e' x' (Lam [x']. e')" by (simp add: assms(1))
finally show ?thesis.
qed

(* Nice idea, but doesn't work well with extra arguments to the function

lemma eqvt_lam_case_eqvt:
assumes "Lam [x]. e = Lam [x']. e'"
assumes F_eqvt: "⋀ π e'. π ∙ F e x e' = F (π ∙ e) (π ∙ x) (π ∙ e')"
assumes F_supp: "atom x ♯ F e x (Lam [x]. e)"
shows "F e x (Lam [x]. e) = F e' x' (Lam [x']. e')"
using assms(1)
proof(rule eqvt_lam_case)
have "eqvt F" unfolding eqvt_def by (rule, perm_simp, rule) so rry
hence "supp (F e x (Lam [x]. e)) ⊆ supp e ∪ supp x ∪ supp (Lam [x]. e)" by (rule supp_fun_app_eqvt3)
with F_supp[unfolded fresh_def]
have *: "supp (F e x (Lam [x]. e)) ⊆ supp (Lam [x]. e)" by (auto simp add: exp_assn.supp supp_at_base)

fix π :: perm
assume "supp π ♯* Lam [x]. e" with *
have "supp π ♯* F e x (Lam [x]. e)" by (auto simp add: fresh_star_def fresh_def)
hence "F e x (Lam [x]. e) = π ∙ (F e x (Lam [x]. e))" by (metis perm_supp_eq)
also have "… =  F (π ∙ e) (π ∙ x) (π ∙ (Lam [x]. e))" by (simp add: F_eqvt)
also have "π ∙ (Lam [x]. e) = (Lam [x]. e)" using supp π ♯* Lam [x]. e by (metis perm_supp_eq)
finally show "F (π ∙ e) (π ∙ x) (Lam [x]. e) = F e x (Lam [x]. e)"..
qed
*)

lemma eqvt_let_case:
assumes "Let as body = Let as' body'"
assumes "⋀ π .
supp (-π) ♯* (fv (Let as body) :: var set) ⟹
supp π ♯* Let as body ⟹
F (π ∙ as) (π ∙ body) (Let as body) = F as body (Let as body)"
shows "F as body (Let as body) = F as' body' (Let as' body')"
proof-
from assms(1)
have "[map (λ p. atom (fst p)) as]lst. (body, as) = [map (λ p. atom (fst p)) as']lst. (body', as')" by auto
then obtain p
where "(supp (body, as) - atom  domA as) ♯* p"
and [simp]: "p ∙ body = body'"
and [simp]: "p ∙ as = as'"
unfolding  Abs_eq_iff(3) alpha_lst.simps by (auto simp add: domA_def image_image)

from ‹_ ♯* p›
have *: "supp (-p) ♯* (fv (Terms.Let as body) :: var set)"
by (auto simp add: fresh_star_def fresh_def supp_finite_set_at_base supp_Pair fv_supp_exp fv_supp_heap supp_minus_perm)

from ‹_ ♯* p›
have **: "supp p ♯* Terms.Let as body"
by (auto simp add: fresh_star_def fresh_def supp_Pair fv_supp_exp fv_supp_heap )

have "F as body (Let as body) =  F (p ∙ as) (p ∙ body) (Let as body)" by (rule assms(2)[OF * **, symmetric])
also have "… = F as' body' (Let as' body')" by (simp add: assms(1))
finally show ?thesis.
qed

subsubsection ‹A smart constructor for lets›

text ‹
Certian program transformations might change the bound variables, possibly making it an empty list.
This smart constructor avoids the empty let in the resulting expression. Semantically, it should
not make a difference.
›

definition SmartLet :: "heap => exp => exp"
where "SmartLet Γ e = (if Γ = [] then e else Let Γ e)"

lemma SmartLet_eqvt[eqvt]: "π ∙ (SmartLet Γ e) = SmartLet (π ∙ Γ) (π ∙ e)"
unfolding SmartLet_def by perm_simp rule

lemma SmartLet_supp:
"supp (SmartLet Γ e) = (supp e ∪ supp Γ) - atom  (domA Γ)"
unfolding SmartLet_def using Let_supp by (auto simp add: supp_Nil)

lemma fv_SmartLet[simp]: "fv (SmartLet Γ e) = (fv Γ ∪ fv e) - domA Γ"
unfolding SmartLet_def by auto

subsubsection ‹A predicate for value expressions›

nominal_function isLam :: "exp ⇒ bool" where
"isLam (Var x) = False" |
"isLam (Lam [x]. e) = True" |
"isLam (App e x) = False" |
"isLam (Let as e) = False" |
"isLam (Bool b) = False" |
"isLam (scrut ? e1 : e2) = False"
unfolding isLam_graph_aux_def eqvt_def
apply simp
apply simp
apply (metis exp_strong_exhaust)
apply auto
done
nominal_termination (eqvt) by lexicographic_order

lemma isLam_Lam: "isLam (Lam [x]. e)" by simp

lemma isLam_obtain_fresh:
assumes "isLam z"
obtains y e'
where "z = (Lam [y]. e')" and "atom y ♯ (c::'a::fs)"
using assms by (nominal_induct z avoiding: c rule:exp_strong_induct) auto

nominal_function isVal :: "exp ⇒ bool" where
"isVal (Var x) = False" |
"isVal (Lam [x]. e) = True" |
"isVal (App e x) = False" |
"isVal (Let as e) = False" |
"isVal (Bool b) = True" |
"isVal (scrut ? e1 : e2) = False"
unfolding isVal_graph_aux_def eqvt_def
apply simp
apply simp
apply (metis exp_strong_exhaust)
apply auto
done
nominal_termination (eqvt) by lexicographic_order

lemma isVal_Lam: "isVal (Lam [x]. e)" by simp
lemma isVal_Bool: "isVal (Bool b)" by simp

subsubsection ‹The notion of thunks›
(*
fun thunks :: "heap ⇒ var set" where
"thunks [] = {}"
| "thunks ((x,e)#Γ) = (if isLam e then {} else {x}) ∪ thunks Γ"
*)

definition thunks :: "heap ⇒ var set" where
"thunks Γ = {x . case map_of Γ x of Some e ⇒ ¬ isVal e | None ⇒ False}"

lemma thunks_Nil[simp]: "thunks [] = {}" by (auto simp add: thunks_def)

lemma thunks_domA: "thunks Γ ⊆ domA Γ"
by (induction Γ ) (auto simp add: thunks_def)

lemma thunks_Cons: "thunks ((x,e)#Γ) = (if isVal e then thunks Γ - {x} else insert x (thunks Γ))"
by (auto simp add: thunks_def )

lemma thunks_append[simp]: "thunks (Δ@Γ) = thunks Δ ∪ (thunks Γ - domA Δ)"
by (induction Δ) (auto simp add: thunks_def )

lemma thunks_delete[simp]: "thunks (delete x Γ) = thunks Γ - {x}"
by (induction Γ) (auto simp add: thunks_def )

lemma thunksI[intro]: "map_of Γ x = Some e ⟹ ¬ isVal e ⟹ x ∈ thunks Γ"
by (induction Γ) (auto simp add: thunks_def )

lemma thunksE[intro]: "x ∈ thunks Γ ⟹ map_of Γ x = Some e ⟹ ¬ isVal e"
by (induction Γ) (auto simp add: thunks_def )

lemma thunks_cong: "map_of Γ = map_of Δ ⟹ thunks Γ = thunks Δ"

lemma thunks_eqvt[eqvt]:
"π ∙ thunks Γ = thunks (π ∙ Γ)"
unfolding thunks_def
by perm_simp rule

subsubsection ‹Non-recursive Let bindings›

definition nonrec :: "heap ⇒ bool" where
"nonrec Γ = (∃ x e. Γ = [(x,e)] ∧ x ∉ fv e)"

lemma nonrecE:
assumes "nonrec Γ"
obtains x e where "Γ = [(x,e)]" and "x ∉ fv e"
using assms
unfolding nonrec_def
by blast

lemma nonrec_eqvt[eqvt]:
"nonrec Γ ⟹ nonrec (π ∙ Γ)"
apply (erule nonrecE)
apply (auto simp add: nonrec_def fv_def fresh_def )
apply (metis fresh_at_base_permute_iff fresh_def)
done

lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
assumes "⋀var. P (Var var)"
assumes "⋀exp var. P exp ⟹ P (App exp var)"
assumes "⋀Γ exp. ¬ nonrec Γ ⟹ (⋀ x. x ∈ domA Γ ⟹  P (the (map_of Γ x))) ⟹ P exp ⟹ P (Let Γ exp)"
assumes "⋀x e exp. x ∉ fv e ⟹ P e ⟹ P exp ⟹ P (let x be e in exp)"
assumes "⋀var exp.  P exp ⟹ P (Lam [var]. exp)"
assumes "⋀b. P (Bool b)"
assumes "⋀ scrut e1 e2. P scrut ⟹ P e1 ⟹ P e2 ⟹ P (scrut ? e1 : e2)"
shows "P exp"
apply (rule exp_induct[of P])
apply (metis assms(1))
apply (metis assms(2))
apply (case_tac "nonrec Γ")
apply (erule nonrecE)
apply simp
apply (metis assms(4))
apply (metis assms(3))
apply (metis assms(5))
apply (metis assms(6))
apply (metis assms(7))
done

lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
assumes "⋀var c. P c (Var var)"
assumes "⋀exp var c. (⋀c. P c exp) ⟹ P c (App exp var)"
assumes "⋀Γ exp c.
atom  domA Γ ♯* c ⟹ ¬ nonrec Γ ⟹ (⋀c x. x ∈ domA Γ ⟹  P c (the (map_of Γ x))) ⟹ (⋀c. P c exp) ⟹ P c (Let Γ exp)"
assumes "⋀x e exp c. {atom x} ♯* c ⟹ x ∉ fv e ⟹ (⋀ c. P c e) ⟹ (⋀ c. P c exp) ⟹ P c (let x be e in exp)"
assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P c exp) ⟹ P c (Lam [var]. exp)"
assumes "⋀b c. P c (Bool b)"
assumes "⋀ scrut e1 e2 c. (⋀ c. P c scrut) ⟹ (⋀ c. P c e1) ⟹ (⋀ c. P c e2) ⟹ P c (scrut ? e1 : e2)"
shows "P (c::'a::fs) exp"
apply (rule exp_strong_induct[of P])
apply (metis assms(1))
apply (metis assms(2))
apply (case_tac "nonrec Γ")
apply (erule nonrecE)
apply simp
apply (metis assms(4))
apply (metis assms(3))
apply (metis assms(5))
apply (metis assms(6))
apply (metis assms(7))
done

lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
assumes "⋀var c. P c (Var var)"
assumes "⋀exp var c. (⋀c. P c exp) ⟹ P c (App exp var)"
assumes "⋀Γ exp c.
atom  domA Γ ♯* c ⟹ ¬ nonrec Γ ⟹ (⋀c x e. (x,e) ∈ set Γ ⟹  P c e) ⟹ (⋀c. P c exp) ⟹ P c (Let Γ exp)"
assumes "⋀x e exp c. {atom x} ♯* c ⟹ x ∉ fv e ⟹ (⋀ c. P c e) ⟹ (⋀ c. P c exp) ⟹ P c (let x be e in exp)"
assumes "⋀var exp c. {atom var} ♯* c ⟹ (⋀c. P c exp) ⟹ P c (Lam [var]. exp)"
assumes "⋀b c. P c (Bool b)"
assumes "⋀ scrut e1 e2 c. (⋀ c. P c scrut) ⟹ (⋀ c. P c e1) ⟹ (⋀ c. P c e2) ⟹ P c (scrut ? e1 : e2)"
shows "P (c::'a::fs) exp"
apply (rule exp_strong_induct_set(1)[of P])
apply (metis assms(1))
apply (metis assms(2))
apply (case_tac "nonrec Γ")
apply (erule nonrecE)
apply simp
apply (metis assms(4))
apply (metis assms(3))
apply (metis assms(5))
apply (metis assms(6))
apply (metis assms(7))
done

subsubsection ‹Renaming a lambda-bound variable›

lemma change_Lam_Variable:
assumes "y' ≠ y ⟹ atom y' ♯ (e,  y)"
shows   "Lam [y]. e =  Lam [y']. ((y ↔ y') ∙ e)"
proof(cases "y' = y")
case True thus ?thesis by simp
next
case False
from assms[OF this]
have "(y ↔ y') ∙ (Lam [y]. e) = Lam [y]. e"
by -(rule flip_fresh_fresh, (simp add: fresh_Pair)+)
moreover
have "(y ↔ y') ∙ (Lam [y]. e) = Lam [y']. ((y ↔ y') ∙ e)"
by simp
ultimately
show "Lam [y]. e =  Lam [y']. ((y ↔ y') ∙ e)" by (simp add: fresh_Pair)
qed

end


# Theory AbstractDenotational

theory AbstractDenotational
imports HeapSemantics Terms
begin

subsubsection ‹The denotational semantics for expressions›

text ‹
Because we need to define two semantics later on, we are abstract in the actual domain.
›

locale semantic_domain =
fixes Fn :: "('Value → 'Value) → ('Value::{pcpo_pt,pure})"
fixes Fn_project :: "'Value → ('Value → 'Value)"
fixes B :: "bool discr → 'Value"
fixes B_project :: "'Value → 'Value → 'Value → 'Value"
fixes tick :: "'Value → 'Value"
begin

nominal_function
ESem :: "exp ⇒ (var ⇒ 'Value) → 'Value"
where (*
Restrict ρ to avoid having to demand atom x ♯ ρ *)
"ESem (Lam [x]. e) = (Λ ρ. tick⋅(Fn⋅(Λ v. ESem e⋅((ρ f| fv (Lam [x]. e))(x := v)))))" (*
Do not use ⟦ Var x ⟧⇘ρ⇙  in the rule for App; it costs an additional
resource and makes the adequacy proof difficult. *)
| "ESem (App e x) = (Λ ρ. tick⋅(Fn_project⋅(ESem e⋅ρ)⋅(ρ x)))"
| "ESem (Var x) = (Λ ρ. tick⋅(ρ x))"
| "ESem (Let as body) = (Λ ρ. tick⋅(ESem body⋅(has_ESem.HSem ESem as⋅(ρ f| fv (Let as body)))))"
| "ESem (Bool b) = (Λ ρ. tick⋅(B⋅(Discr b)))"
| "ESem (scrut ? e1 : e2) = (Λ ρ. tick⋅((B_project⋅(ESem scrut⋅ρ))⋅(ESem e1⋅ρ)⋅(ESem e2⋅ρ)))"
proof goal_cases
txt ‹The following proofs discharge technical obligations generated by the Nominal package.›

case 1 thus ?case
unfolding eqvt_def ESem_graph_aux_def
apply rule
apply (perm_simp)
done
next
case (3 P x)
thus ?case by (metis (poly_guards_query) exp_strong_exhaust)
next

case prems: (4 x e x' e')
from prems(5)
show ?case
proof (rule eqvt_lam_case)
fix π :: perm
assume *: "supp (-π) ♯* (fv (Lam [x]. e) :: var set)"
{ fix ρ v
have "ESem_sumC (π ∙ e)⋅((ρ f| fv (Lam [x]. e))((π ∙ x) := v)) = - π ∙ ESem_sumC (π ∙ e)⋅((ρ f| fv (Lam [x]. e))((π ∙ x) := v))"
also have "… = ESem_sumC e⋅((- π ∙ (ρ f| fv (Lam [x]. e)))(x := v))" by (simp add: pemute_minus_self eqvt_at_apply[OF prems(1)])
also have "- π ∙ (ρ f| fv (Lam [x]. e)) = (ρ f| fv (Lam [x]. e))"  by (rule env_restr_perm'[OF *]) auto
finally have "ESem_sumC (π ∙ e)⋅((ρ f| fv (Lam [x]. e))((π ∙ x) := v)) = ESem_sumC e⋅((ρ f| fv (Lam [x]. e))(x := v))".
}
thus " (Λ ρ. tick⋅(Fn⋅(Λ v. ESem_sumC (π ∙ e)⋅((ρ f| fv (Lam [x]. e))(π ∙ x := v))))) = (Λ ρ. tick⋅(Fn⋅(Λ v. ESem_sumC e⋅((ρ f| fv (Lam [x]. e))(x := v)))))" by simp
qed
next

case prems: (19 as body as' body')
from prems(9)
show ?case
proof (rule eqvt_let_case)
fix π :: perm
assume *: "supp (-π) ♯* (fv (Terms.Let as body) :: var set)"

{ fix ρ
have "ESem_sumC (π ∙ body)⋅(has_ESem.HSem ESem_sumC (π ∙ as)⋅(ρ f| fv (Terms.Let as body)))
= - π ∙ ESem_sumC (π ∙ body)⋅(has_ESem.HSem ESem_sumC (π ∙ as)⋅(ρ f| fv (Terms.Let as body)))"
by (rule permute_pure[symmetric])
also have "… = (- π ∙ ESem_sumC) body⋅(has_ESem.HSem (- π ∙ ESem_sumC) as⋅(- π ∙ ρ f| fv (Terms.Let as body)))"
also have "(- π ∙ ESem_sumC) body = ESem_sumC body"
by (rule eqvt_at_apply[OF ‹eqvt_at ESem_sumC body›])
also have "has_ESem.HSem (- π ∙ ESem_sumC) as = has_ESem.HSem  ESem_sumC as"
by (rule HSem_cong[OF eqvt_at_apply[OF prems(2)] refl])
also have "- π ∙ ρ f| fv (Let as body) = ρ f| fv (Let as body)"
by (rule env_restr_perm'[OF *], simp)
finally have "ESem_sumC (π ∙ body)⋅(has_ESem.HSem ESem_sumC (π ∙ as)⋅(ρ f| fv (Let as body))) = ESem_sumC body⋅(has_ESem.HSem ESem_sumC as⋅(ρ f| fv (Let as body)))".
}
thus "(Λ ρ. tick⋅(ESem_sumC (π ∙ body)⋅(has_ESem.HSem ESem_sumC (π ∙ as)⋅(ρ f| fv (Let as body))))) =
(Λ ρ. tick⋅(ESem_sumC body⋅(has_ESem.HSem ESem_sumC as⋅(ρ f| fv (Let as body)))))" by (simp only:)
qed
qed auto
(* [eqvt] attributes do not survive instantiation, so we pass (no_eqvt) here. We don't need it
anyways… *)
nominal_termination (in semantic_domain) (no_eqvt) by lexicographic_order

sublocale has_ESem ESem.

notation ESem_syn ("⟦ _ ⟧⇘_⇙"  [60,60] 60)
notation EvalHeapSem_syn  ("❙⟦ _ ❙⟧⇘_⇙"  [0,0] 110)
notation HSem_syn ("⦃_⦄_"  [60,60] 60)
abbreviation AHSem_bot ("⦃_⦄"  [60] 60) where "⦃Γ⦄ ≡ ⦃Γ⦄⊥"

end
end



# Theory Substitution

theory Substitution
imports Terms
begin

text ‹Defining a substitution function on terms turned out to be slightly tricky.›

fun
subst_var :: "var ⇒ var ⇒ var ⇒ var" ("_[_::v=_]" [1000,100,100] 1000)
where "x[y ::v= z] = (if x = y then z else x)"

nominal_function  (default "case_sum (λx. Inl undefined) (λx. Inr undefined)",
invariant "λ a r . (∀ Γ y z . ((a = Inr (Γ, y, z) ∧ atom  domA Γ ♯* (y, z)) ⟶ map (λx . atom (fst x))  (Sum_Type.projr r) = map (λx . atom (fst x)) Γ))")
subst :: "exp ⇒ var ⇒ var ⇒ exp" ("_[_::=_]" [1000,100,100] 1000)
and
subst_heap :: "heap ⇒ var ⇒ var ⇒ heap" ("_[_`