theory "Abstract-Denotational-Props" imports "AbstractDenotational" Substitution begin context semantic_domain begin subsubsection {* The semantics ignores fresh variables *} lemma ESem_considers_fv': "⟦ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ f|` (fv e)⇙" proof (induct e arbitrary: ρ rule:exp_induct) case Var show ?case by simp next have [simp]: "⋀ S x. S ∩ insert x S = S" by auto case App show ?case by (simp, subst (1 2) App, simp) next case (Lam x e) show ?case by simp next case (IfThenElse scrut e⇩1 e⇩2) have [simp]: "(fv scrut ∩ (fv scrut ∪ fv e⇩1 ∪ fv e⇩2)) = fv scrut" by auto have [simp]: "(fv e⇩1 ∩ (fv scrut ∪ fv e⇩1 ∪ fv e⇩2)) = fv e⇩1" by auto have [simp]: "(fv e⇩2 ∩ (fv scrut ∪ fv e⇩1 ∪ fv e⇩2)) = fv e⇩2" by auto show ?case apply simp apply (subst (1 2) IfThenElse(1)) apply (subst (1 2) IfThenElse(2)) apply (subst (1 2) IfThenElse(3)) apply (simp) done next case (Let as e) have "⟦e⟧⇘⦃as⦄ρ⇙ = ⟦e⟧⇘(⦃as⦄ρ) f|` (fv as ∪ fv e)⇙" apply (subst (1 2) Let(2)) apply simp apply (metis inf_sup_absorb sup_commute) done also have "fv as ⊆ fv as ∪ fv e" by (rule inf_sup_ord(3)) hence "(⦃as⦄ρ) f|` (fv as ∪ fv e) = ⦃as⦄(ρ f|` (fv as ∪ fv e))" by (rule HSem_ignores_fresh_restr'[OF _ Let(1)]) also have "⦃as⦄(ρ f|` (fv as ∪ fv e)) = ⦃as⦄ρ f|` (fv as ∪ fv e - domA as)" by (rule HSem_restr_cong) (auto simp add: lookup_env_restr_eq) finally show ?case by simp qed auto sublocale has_ignore_fresh_ESem ESem by standard (rule fv_supp_exp, rule ESem_considers_fv') subsubsection {* Nicer equations for ESem, without freshness requirements *} lemma ESem_Lam[simp]: "⟦ Lam [x]. e ⟧⇘ρ⇙ = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘ρ(x := v)⇙))" proof- have *: "⋀ v. ((ρ f|` (fv e - {x}))(x := v)) f|` fv e = (ρ(x := v)) f|` fv e" by (rule ext) (auto simp add: lookup_env_restr_eq) have "⟦ Lam [x]. e ⟧⇘ρ⇙ = ⟦ Lam [x]. e ⟧⇘env_delete x ρ⇙" by (rule ESem_fresh_cong) simp also have "… = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘(ρ f|` (fv e - {x}))(x := v)⇙))" by simp also have "… = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘((ρ f|` (fv e - {x}))(x := v)) f|` fv e⇙))" by (subst ESem_considers_fv, rule) also have "… = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘ρ(x := v) f|` fv e⇙))" unfolding *.. also have "… = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘ρ(x := v)⇙))" unfolding ESem_considers_fv[symmetric].. finally show ?thesis. qed declare ESem.simps(1)[simp del] lemma ESem_Let[simp]: "⟦Let as body⟧⇘ρ⇙ = tick ⋅ (⟦body⟧⇘⦃as⦄ρ⇙)" proof- have "⟦ Let as body ⟧⇘ρ⇙ = tick ⋅ (⟦body⟧⇘⦃as⦄(ρ f|` fv (Let as body))⇙)" by simp also have "⦃as⦄(ρ f|` fv(Let as body)) = ⦃as⦄(ρ f|` (fv as ∪ fv body))" by (rule HSem_restr_cong) (auto simp add: lookup_env_restr_eq) also have "… = (⦃as⦄ρ) f|` (fv as ∪ fv body)" by (rule HSem_ignores_fresh_restr'[symmetric, OF _ ESem_considers_fv]) simp also have "⟦body⟧⇘…⇙ = ⟦body⟧⇘⦃as⦄ρ⇙" by (rule ESem_fresh_cong) (auto simp add: lookup_env_restr_eq) finally show ?thesis. qed declare ESem.simps(4)[simp del] subsubsection {* Denotation of Substitution *} lemma ESem_subst_same: "ρ x = ρ y ⟹ ⟦ e ⟧⇘ρ⇙ = ⟦ e[x::= y] ⟧⇘ρ⇙" and "ρ x = ρ y ⟹ (❙⟦ as ❙⟧⇘ρ⇙) = ❙⟦ as[x::h=y] ❙⟧⇘ρ⇙" proof (nominal_induct e and as avoiding: x y arbitrary: ρ and ρ rule:exp_heap_strong_induct) case Var thus ?case by auto next case App from App(1)[OF App(2)] App(2) show ?case by auto next case (Let as exp x y ρ) from `atom \` domA as ♯* x` `atom \` domA as ♯* y` have "x ∉ domA as" "y ∉ domA as" by (metis fresh_star_at_base imageI)+ hence [simp]:"domA (as[x::h=y]) = domA as" by (metis bn_subst) from `ρ x = ρ y` have "(⦃as⦄ρ) x = (⦃as⦄ρ) y" using `x ∉ domA as` `y ∉ domA as` by (simp add: lookup_HSem_other) hence "⟦exp⟧⇘⦃as⦄ρ⇙ = ⟦exp[x::=y]⟧⇘⦃as⦄ρ⇙" by (rule Let) moreover from `ρ x = ρ y` have "⦃as⦄ρ = ⦃as[x::h=y]⦄ρ" and "(⦃as⦄ρ) x = (⦃as[x::h=y]⦄ρ) y" apply (induction rule: parallel_HSem_ind) apply (intro adm_lemmas cont2cont cont2cont_fun) apply simp apply simp apply simp apply (erule arg_cong[OF Let(3)]) using `x ∉ domA as` `y ∉ domA as` apply simp done ultimately show ?case using Let(1,2,3) by (simp add: fresh_star_Pair) next case (Lam var exp x y ρ) from `ρ x = ρ y` have "⋀v. (ρ(var := v)) x = (ρ(var := v)) y" using Lam(1,2) by (simp add: fresh_at_base) hence "⋀ v. ⟦exp⟧⇘ρ(var := v)⇙ = ⟦exp[x::=y]⟧⇘ρ(var := v)⇙" by (rule Lam) thus ?case using Lam(1,2) by simp next case IfThenElse from IfThenElse(1)[OF IfThenElse(4)] IfThenElse(2)[OF IfThenElse(4)] IfThenElse(3)[OF IfThenElse(4)] show ?case by simp next case Nil thus ?case by auto next case Cons from Cons(1,2)[OF Cons(3)] Cons(3) show ?case by auto qed auto lemma ESem_subst: shows "⟦ e ⟧⇘σ(x := σ y)⇙ = ⟦ e[x::= y] ⟧⇘σ⇙" proof(cases "x = y") case False hence [simp]: "x ∉ fv e[x::=y]" by (auto simp add: fv_def supp_subst supp_at_base dest: set_mp[OF supp_subst]) have "⟦ e ⟧⇘σ(x := σ y)⇙ = ⟦ e[x::= y] ⟧⇘σ(x := σ y)⇙" by (rule ESem_subst_same) simp also have "… = ⟦ e[x::= y] ⟧⇘σ⇙" by (rule ESem_fresh_cong) simp finally show ?thesis. next case True thus ?thesis by simp qed end end