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⇙ ❙⟦Γ⇩1❙⟧⇘y⇙) (ρ⇩2 ++⇘domA Γ⇩2⇙ ❙⟦Γ⇩2❙⟧⇘z⇙)"
  shows "P (⦃Γ⇩1⦄ρ⇩1) (⦃Γ⇩2⦄ρ⇩2)"
  unfolding HSem_def'
  apply (rule parallel_fix_ind[OF assms(1), OF assms(2)])
  using step by simp

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

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

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

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

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

lemma 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 ⟧⇘ρ'⇙ = ⟦ e ⟧⇘env_delete x ρ'⇙"
  shows  "env_delete x (⦃(x, e) # Γ⦄ρ) = ⦃Γ⦄ρ"
proof (rule parallel_HSem_ind, goal_cases)
  case 1 show ?case by simp
next
  case 2 show ?case by auto
next
  case prems: (3 y z)
  have "env_delete x ρ = ρ" using `x ∉ edom ρ` by (rule env_delete_noop)
  moreover
  from fresh have "x ∉ domA Γ" by (metis domA_not_fresh)
  hence "env_delete x (❙⟦ (x, e) # Γ ❙⟧⇘y⇙) = ❙⟦ Γ ❙⟧⇘y⇙"
    by (auto intro: env_delete_noop dest:  set_mp[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