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