theory "Abstract-Denotational-Props"
imports "AbstractDenotational" Substitution
begin
context semantic_domain
begin
subsubsection {* The semantics ignores fresh variables *}
lemma ESem_considers_fv': "\ e \\<^bsub>\\<^esub> = \ e \\<^bsub>\ f|` (fv e)\<^esub>"
proof (induct e arbitrary: \ rule:exp_induct)
case (Var b x)
show ?case by (cases b) simp_all
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 (Let as e)
have "\e\\<^bsub>\as\\\<^esub> = \e\\<^bsub>(\as\\) f|` (fv as \ fv e)\<^esub>"
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 default (rule fv_supp_exp, rule ESem_considers_fv')
subsubsection {* Nicer equations for ESem, without freshness requirements *}
lemma ESem_Lam[simp]: "\ Lam [x]. e \\<^bsub>\\<^esub> = tick \ (Fn \ (\ v. \ e \\<^bsub>\(x := v)\<^esub>))"
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 \\<^bsub>\\<^esub> = \ Lam [x]. e \\<^bsub>env_delete x \\<^esub>"
by (rule ESem_fresh_cong) simp
also have "\ = tick \ (Fn \ (\ v. \ e \\<^bsub>(\ f|` (fv e - {x}))(x := v)\<^esub>))"
by simp
also have "\ = tick \ (Fn \ (\ v. \ e \\<^bsub>((\ f|` (fv e - {x}))(x := v)) f|` fv e\<^esub>))"
by (subst ESem_considers_fv, rule)
also have "\ = tick \ (Fn \ (\ v. \ e \\<^bsub>\(x := v) f|` fv e\<^esub>))"
unfolding *..
also have "\ = tick \ (Fn \ (\ v. \ e \\<^bsub>\(x := v)\<^esub>))"
unfolding ESem_considers_fv[symmetric]..
finally show ?thesis.
qed
declare ESem.simps(1)[simp del]
lemma ESem_Let[simp]: "\Let as body\\<^bsub>\\<^esub> = tick \ (\body\\<^bsub>\as\\\<^esub>)"
proof-
have "\ Let as body \\<^bsub>\\<^esub> = tick \ (\body\\<^bsub>\as\(\ f|` fv (Let as body))\<^esub>)"
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\\<^bsub>\\<^esub> = \body\\<^bsub>\as\\\<^esub>"
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 \\<^bsub>\\<^esub> = \ e[x::= y] \\<^bsub>\\<^esub>"
and
"\ x = \ y \ (\<^bold>\ as \<^bold>\\<^bsub>\\<^esub>) = \<^bold>\ as[x::h=y] \<^bold>\\<^bsub>\\<^esub>"
proof (nominal_induct e and as avoiding: x y arbitrary: \ and \ rule:exp_heap_strong_induct)
case (Var b var x y)
thus ?case by (cases b) 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\\<^bsub>\as\\\<^esub> = \exp[x::=y]\\<^bsub>\as\\\<^esub>"
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\\<^bsub>\(var := v)\<^esub> = \exp[x::=y]\\<^bsub>\(var := v)\<^esub>"
by (rule Lam)
thus ?case using Lam(1,2) 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:
assumes "x \ y"
shows "\ e \\<^bsub>\(x := \ y)\<^esub> = \ e[x::= y] \\<^bsub>\\<^esub>"
proof-
have [simp]: "x \ fv e[x::=y]" using assms by (auto simp add: fv_def supp_subst supp_at_base dest: set_mp[OF supp_subst])
have "\ e \\<^bsub>\(x := \ y)\<^esub> = \ e[x::= y] \\<^bsub>\(x := \ y)\<^esub>"
using assms(1)
by (auto intro: ESem_subst_same simp add: Rep_cfun_inverse)
also have "\ = \ e[x::= y] \\<^bsub>\\<^esub>"
by (rule ESem_fresh_cong) simp
finally
show ?thesis.
qed
end
end