Session Launchbury

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 [] = {}"
  by (auto simp add: domA_def)

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

lemma finite_domA[simp]:
  "finite (domA Γ)"
  by (auto simp add: domA_def)

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

lemma map_add_domA[simp]: 
  "x  domA Γ  (map_of Δ ++ map_of Γ) x = map_of Γ x"
  "x  domA Γ  (map_of Δ ++ map_of Γ) x = map_of Δ x"
    apply (metis dom_map_of_conv_domA map_add_dom_app_simps(1))
    apply (metis dom_map_of_conv_domA map_add_dom_app_simps(3))
    done

lemma set_delete_subset: "set (delete k al)  set al"
  by (auto simp add: delete_eq)

lemma dom_delete_subset: "snd ` set (delete k al)  snd ` set al"
  by (auto simp add: delete_eq)

(*
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 | kv  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 | kvm} = {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))"
  by (auto simp add: mapCollect_def)

lemma image_mapCollect[simp]: 
  "g ` {f k v | k  v  m} = { g (f k v) | k  v  m}"
  by (auto simp add: mapCollect_def)

lemma mapCollect_map_upd[simp]:
  "mapCollect f (m(kv)) = 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 | kv  m . P }" == "CONST mapCollectFilter (λk v. (P,e)) m"

lemma mapCollectFilter_const_False[simp]:
  "{e | kv  m . False } = {}"
  unfolding mapCollect_def mapCollectFilter_def by simp

lemma mapCollectFilter_const_True[simp]:
  "{e | kv  m . True } = {e | kv  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)

lemma compatible_adm2:
  shows "adm (λ y. compatible x y)"
proof(rule admI)
  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 compatible_adm1: "adm (λ x. compatible x y)"
  by (subst compatible_sym_iff, rule compatible_adm2)

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))"
    by (rule join_cont1[OF ‹chain Y admD[OF compatible_adm2 ‹chain Z compat]])
  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_joinfg) 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_joinxy"  by (auto simp add: fun_below_iff)
    show "y  fun_joinxy"  by (auto simp add: fun_below_iff)
    fix z
    assume "x  z" and "y  z"
    thus "fun_joinxy  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_joinfgx = (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_joinxy"  by (auto simp add: cfun_below_iff)
    show "y  cfun_joinxy"  by (auto simp add: cfun_below_iff)
    fix z
    assume "x  z" and "y  z"
    thus "cfun_joinxy  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 (upx) (upy)  compatible x y"
proof
  assume "compatible (upx) (upy)"
  then obtain z' where z': "{upx,upy} <<| z'" unfolding compatible_def by auto
  then obtain z where  "{upx,upy} <<| upz" 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  "{upx,upy} <<| upz"  unfolding is_lub_def
    apply auto
    by (metis not_up_less_UU upE up_below)
  thus "compatible (upx) (upy)"  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)
  apply (simp add: all_compatible)
  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 (simp add: all_compatible)
  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 "fx  fy  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)
  

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

subsubsection ‹Updates›

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

declare fun_upd_same[simp] fun_upd_other[simp]

subsubsection ‹Restriction›

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

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

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

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

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

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

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

lemma env_restr_eqI: "(x. x  S  m1 x = m2 x)  m1 f|` S = m2 f|` S"
  by (auto simp add: lookup_env_restr_eq)

lemma env_restr_eqD: "m1 f|` S = m2 f|` S  x  S  m1 x = m2 x"
  by (auto dest!: fun_cong[where x = x])

lemma env_restr_belowI: "(x. x  S  m1 x  m2 x)  m1 f|` S  m2 f|` S"
  by (auto intro: fun_belowI simp add: lookup_env_restr_eq)

lemma env_restr_belowD: "m1 f|` S  m2 f|` S  x  S  m1 x  m2 x"
  by (auto dest!: fun_belowD[where x = x])

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

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

lemma env_restr_useless: "edom m  S  m f|` S = m"
  by (rule ext) (auto simp add: lookup_env_restr_eq dest!: 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")
  apply (auto simp add: lookup_env_restr_eq)
  done

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

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

lemma env_restr_below_subset:
  assumes "S  S'"
  and "m1 f|` S'  m2 f|` S'"
  shows "m1 f|` S  m2 f|` S"
using assms
by (auto intro!: env_restr_belowI dest!: env_restr_belowD)

lemma edom_env[simp]:
  "edom (m f|` S) = edom m  S"
  unfolding edom_def env_restr_def by auto

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

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

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

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

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

lemmas cont_compose[OF env_restr_cont, cont2cont, simp]

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

subsubsection ‹Deleting›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsubsection ‹Merging of two functions›

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

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

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

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

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

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

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

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

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

subsubsection ‹Environments with binary joins›

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

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

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

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

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

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

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

subsubsection ‹Singleton environments›

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

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

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

lemma esing_eq_up_iff[simp]: "(esing x(upa)) y = upa'  (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 xn)  {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 xv f|` S = esing xv" 
  by (auto intro: env_restr_useless dest: subsetD[OF edom_esing_subset])

lemma env_restr_esing2[simp]:
  "x  S  esing xv f|` S = " 
  by (auto  dest: subsetD[OF edom_esing_subset])

lemma esing_eq_iff[simp]:
  "esing xv = esing xv'  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)])

lemma pointwise_adm:
  fixes P :: "'a::pcpo  'b::pcpo  bool"
  assumes "adm (λ x. P (fst x) (snd x))"
  shows "adm (λ m. pointwise P (fst m) (snd m))"
proof (rule admI, goal_cases)
  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"
  assumes "adm P"
  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 (upx) = 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) = upa"

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))"
  apply (rule admI)
  apply (simp add:
      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. fx)  ρ)"

lemma [simp]: "cfun_compf(ρ(x := v)) = (cfun_compfρ)(x := fv)"
  unfolding cfun_comp_def by auto

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

lemma fix_eq_fix:
  "f(fixg)  fixg  g(fixf)  fixf  fixf = fixg"
  by (metis fix_least_below below_antisym)

subsubsection ‹Additional transitivity rules›

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"
  by (simp add: env_restr_evalHeap_noop)

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")
 apply (auto simp add: lookupEvalHeap)
 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 Γ")
    apply (auto simp add: lookupEvalHeap)
    done
qed

lemma evalHeap_reorder_head:
  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])

lemma evalHeap_reorder_head_append:
  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"
  by (simp add: assms)

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 (auto simp add: eqvt_def)
    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 (auto simp add: eqvt_def)
    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)

subsubsection ‹Additional simplification rules›

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

lemma fresh_star_singleton: "{ x } ♯* e  x  e"
  by (simp add: fresh_star_def)

subsubsection ‹Additional equivariance lemmas›

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)

lemma map_add_eqvt[eqvt]:
  "π  (m1 ++ m2) = (π  m1) ++ (π  m2)"
  unfolding map_add_def
  by (perm_simp, rule)

lemma map_of_eqvt[eqvt]:
  "π  map_of l = map_of (π  l)"
  apply (induct l)
  apply (simp add: permute_fun_def)
  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 v1 v2 = tranclp (π  P) (π  v1) (π  v2)" 
  unfolding tranclp_def by perm_simp rule

lemma rtranclp_eqvt[eqvt]: "π  rtranclp P v1 v2 = rtranclp (π  P) (π  v1) (π  v2)" 
  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
  apply (simp add: permute_self)
  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
by(induct Γ)(auto simp add: fresh_Cons)

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)"
  by (simp add: fresh_star_def pure_fresh)

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
  by (auto simp add: supp_finite_set_at_base)

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))"
  by rule (simp add: permute_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 = "()"])
  apply (auto simp add: fresh_star_def)
  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
by(induct Γ)(auto simp add: fresh_Cons)

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 (π  Γ)"
  by (simp add: domA_def)

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
      by (simp add: fresh_star_def fresh_def)
  }
  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)"
  by (simp add: fresh_def)

lemma bot_fresh_star[simp]: "a ♯* ( :: 'a :: pcpo_pt)"
  by (simp add: fresh_star_def)

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
  apply (simp add: permute_cfun_def eta_cfun)
  apply (simp add: permute_cfun_def cfun_eqI minus_add)
  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
  apply (simp add: Abs_cfun_eqvt)
  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
apply (rule parallel_fix_ind[OF adm_subst2])
apply (auto simp add: permute_self)
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)
  apply (simp add: permute_u_def)
  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
  apply (simp add: permute_self)
  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)"
  by (simp add: permute_lift_def)

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)
     (simp add: assms env_restr_def)


lemma env_restr_below_itself:
  shows "m f|` S  m"
  apply (rule fun_belowI)
  apply (case_tac "x  S")
  apply auto
  done  

lemma env_restr_cont:  "cont (env_restr S)"
  apply (rule cont2cont_lambda)
  apply (case_tac "y  S")
  apply auto
  done

lemma env_restr_belowD:
  assumes "m1 f|` S  m2 f|` S"
  assumes "x  S"
  shows "m1 x  m2 x"
  using fun_belowD[OF assms(1), where x = x] assms(2) by simp

lemma env_restr_eqD:
  assumes "m1 f|` S = m2 f|` S"
  assumes "x  S"
  shows "m1 x = m2  x"
  by (metis assms(1) assms(2) lookup_env_restr)

lemma env_restr_below_subset:
  assumes "S  S'"
  and "m1 f|` S'  m2 f|` S'"
  shows "m1 f|` S  m2 f|` S"
using assms
by (auto intro!: env_restr_belowI dest: env_restr_belowD)



lemma  override_on_below_restrI:
  assumes " x f|` (-S)  z f|` (-S)"
  and "y f|` S  z f|` S"
  shows  "x ++S y  z"
using assms
by (auto intro: override_on_belowI dest:env_restr_belowD)

lemma  fmap_below_add_restrI:
  assumes "x f|` (-S)  y f|` (-S)"
  and     "x f|` S  z f|` S"
  shows  "x  y ++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)"
  by (simp add: edom_def)

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)"
  by (auto simp add: env_restr_def)

lemma env_delete_eqvt[eqvt]:
  fixes m :: "'a::pt  'b::{cont_pt,pcpo}"
  shows "π  env_delete x m = env_delete (π  x) (π  m)"
  by (auto simp add: env_delete_def)

lemma esing_eqvt[eqvt]: "π  (esing x) = esing (π  x)"
  unfolding esing_def
  apply perm_simp
  apply (simp add: Abs_cfun_eqvt)
  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 (simp add: permute_pure)
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 "adm P"
  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 "adm P"
  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 Γ1y) (ρ2 ++domA Γ2 Γ2z)"
  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 Γ")
  apply (auto simp add: lookup_HSem_other)
  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])
  by (simp add: assms)

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

lemma HSem_reorder_head:
  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      
    unfolding HSem_def evalHeap_reorder_head[OF assms]
    by (simp add: domA_def)
qed

lemma HSem_reorder_head_append:
  assumes "x  domA Γ"
  shows "(x,e)#Γ@Δρ = Γ @ ((x,e)#Δ)ρ"
proof-
  have "set ((x,e)#Γ@Δ) = set (Γ @ ((x,e)#Δ))" by auto
  thus ?thesis
    unfolding HSem_def  evalHeap_reorder_head_append[OF assms]
    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ρ'))"
    by (simp add: HSem_def')
  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"
    by (simp add: HSem_def')
  also have " = fix  L"
    by (rule iterative_override_on[symmetric])
  also have " = fix  R'"
    by (rule iterative_override_on')
  also have " = (μ ρ'. (ρ ++domA Γ (Γρ'))( x := eΓρ'))"
    by (simp add: HSem_def')
  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
  show ?case by (simp add: env_restr_add env_restr_evalHeap_noop)
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› 

lemma HSem_add_fresh':
  assumes fresh: "atom x  Γ"
  assumes "x  edom ρ"
  assumes step: "e ρ'. e  snd ` set Γ   eρ' =  eenv_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 Γ
    by (simp add: env_delete_add)
qed

lemma HSem_add_fresh:
  assumes "atom x  Γ"
  assumes "x  edom ρ"
  shows  "env_delete x ((x, e) # Γρ) = Γρ"
proof(rule HSem_add_fresh'[OF assms], goal_cases)
  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])
 qed (simp add: lookup_HSem_other lookup_env_restr_eq)

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"
        by (simp add: map_add_dom_app_simps dom_map_of_conv_domA)
    next
      case False
      thus "map_of (Δ @ Γ) x = map_of (Γ @ Δ) x"
        by (simp add: map_add_dom_app_simps dom_map_of_conv_domA)
    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 Γ)"
      by (simp add: env_restr_HSem)
    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)
   apply (simp add: Cfun_app_eqvt permute_Lam)
   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)
     (auto simp add: heapToAssn.simps)

lemma bn_heapToAssn: "bn (heapToAssn Γ) = map (λx. atom (fst x)) Γ"
  by (induct rule: heapToAssn.induct)
     (auto simp add: heapToAssn.simps exp_assn.bn_defs)

lemma set_bn_to_atom_domA:
  "set (bn as) = atom ` domA (asToHeap as)"
   by (induct as rule: asToHeap.induct)
      (auto simp add: exp_assn.bn_defs)

text ‹
They are inverse to each other.
›

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

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

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)
     (simp_all add: heapToAssn.simps)

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 :: "varexpexpexp" ("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 (simp add: bn_heapToAssn)
  apply (rule Abs_eq_cong)
  apply (simp_all add: supp_Pair supp_heapToAssn)
  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)"
  by (simp add: fresh_Cons fresh_Nil Abs1_eq_iff fresh_Pair add: fresh_at_base pure_fresh)

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 Δ"
  by (simp add: thunks_def)

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)
  apply (simp add: Abs_cfun_eqvt)
  apply (simp add: unpermute_def permute_pure)
  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))"
        by (simp add: permute_pure)
      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)))"
        by (simp add: pemute_minus_self)
      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" ("_[_