theory Correctness
imports "CorrectnessStacked" "Launchbury-Unstack"
begin
text {* Fresh bindings can be added to the heap *}
lemma ESem_add_fresh:
assumes fresh: "atom x \ (\, e)"
and "x \ fdom \"
shows "\e\\<^bsub>\(x, e') # \\\\<^esub> = \e\\<^bsub>\\\\\<^esub>"
proof(rule ESem_ignores_fresh[symmetric])
have "\\\\ = fmap_restr (fdom \ \ heapVars \) (\(x, e') # \\\) "
apply (rule HSem_add_fresh[OF _ `x \ fdom \`, symmetric])
using fresh by (simp add: fresh_Pair)
thus "\\\\ \ \(x, e') # \\\"
by (auto simp add: fmap_less_restrict)
have "(insert x (fdom \ \ heapVars \) - (fdom \ \ heapVars \)) = {x}"
using fresh `x \ fdom \` by (auto simp add: fresh_Pair heapVars_not_fresh)
thus "atom ` (fdom (\(x, e') # \\\) - fdom (\\\\)) \* e"
using fresh
by (simp add: fresh_star_def fresh_Pair)
qed
text {*
As a corollary of the correctness of the stacked semantics and its equivalence to the original
semantics we obtaim Theorem 2 from \cite{launchbury}.
*}
theorem correctness:
assumes "\ : e \\<^bsub>L\<^esub> \ : z"
and [simp]:"distinctVars \"
shows "\e\\<^bsub>\\\\<^esub> = \z\\<^bsub>\\\\<^esub>" and "\\\ \ \\\"
proof-
obtain x :: var where fresh: "atom x \ (\,e,\,z)"
by (rule obtain_fresh)
have "\ : e \\<^bsub>x#L\<^esub> \ : z"
by (rule reds_add_var_L[OF assms(1) fresh], simp)
hence "\ : [(x, e)] \ \ : [(x, z)]"
by (rule add_stack, simp_all add: supp_Nil)
moreover
from fresh
have "x \ heapVars \"
by (metis heapVars_not_fresh fresh_Pair)
hence "distinctVars ([(x, e)] @ \)"
by (simp add: distinctVars_append distinctVars_Cons)
ultimately
have le: "\[(x, e)] @ \\ \ \[(x, z)] @ \\"
by (rule CorrectnessStacked.correctness)
have "\\\ = fmap_restr (heapVars \) (\(x, e) # \\)"
apply (rule HSem_add_fresh[where \ = "f\", simplified, symmetric])
using fresh apply (simp add: fresh_Pair)
done
also have "... \ fmap_restr (heapVars \) (\(x, z) # \\)"
by (rule fmap_restr_le[OF le Launchbury.reds_doesnt_forget[OF assms(1)], simplified])
also have "... = \\\"
apply (rule HSem_add_fresh[where \ = "f\", simplified])
using fresh by (simp add: fresh_Pair)
finally show "\\\ \ \\\".
have "\e\\<^bsub>\\\\<^esub> = \e\\<^bsub>\(x, e) # \\\<^esub>"
apply (rule ESem_add_fresh[where \ = "f\", symmetric, simplified])
using fresh by (simp add: fresh_Pair)
also have "... = \(x, e) # \\ f! x"
by (simp add: the_lookup_HSem_heap)
also have "... = \(x, z) # \\ f! x" by (simp add: fmap_less_eqD[OF le, simplified])
also have "... = \z\\<^bsub>\(x, z) # \\\<^esub>" by (simp add: the_lookup_HSem_heap)
also have "... = \z\\<^bsub>\\\\<^esub>"
apply (rule ESem_add_fresh[where \ = "f\", simplified])
using fresh by (simp add: fresh_Pair)
finally show "\ e \\<^bsub>\\\\<^esub> = \ z \\<^bsub>\\\\<^esub>".
qed
end