theory CorrectnessResourced
imports "ResourcedDenotational" Launchbury
begin
theorem correctness:
assumes "\ : e \\<^bsub>L\<^esub> \ : z"
and "fv (\, e) - domA \ \ set L"
shows "\\e\\<^bsub>\\\\\\<^esub> \ \\z\\<^bsub>\\\\\\<^esub>" and "(\\\\\) f|` domA \ \ (\\\\\) f|` domA \"
using assms
proof(nominal_induct arbitrary: \ rule:reds.strong_induct)
case Lambda
case 1 show ?case..
case 2 show ?case..
next
case (Application y \ e x L \ \ z e')
hence "y \ x" by (simp_all add: fresh_at_base)
have Gamma_subset: "domA \ \ domA \"
by (rule reds_doesnt_forget[OF Application.hyps(8)])
case 1
hence prem1: "fv (\, e) - domA \ \ set (x#L)" by auto
from 1 Gamma_subset have *: "x \ set L \ x \ domA \" by auto
have "fv (\, e'[y::=x]) - domA \ \ (fv (\, Lam [y]. e') - domA \) \ {x}"
by (auto dest!: set_mp[OF fv_subst_subset])
also have "\ \ (fv (\, e) - domA \) \ {x}"
using new_free_vars_on_heap[OF Application.hyps(8)] by auto
also have "\ \ set L \ {x}" using prem1 by auto
finally have "fv (\, e'[y::=x]) - domA \ \ set L \ {x}".
with *
have prem2: "fv (\, e'[y::=x]) - domA \ \ set L" by auto
have *: "(\\\\\) x \ (\\\\\) x"
proof(cases "x \ domA \")
case True
thus ?thesis
using fun_belowD[OF Application.hyps(10)[OF prem1], where \1 = \ and x = x]
by simp
next
case False
from False reds_avoids_live[OF Application.hyps(8)]
show ?thesis by (simp add: lookup_HSem_other)
qed
{
fix r
have "(\\ App e x \\<^bsub>\\\\\\<^esub>)\r \ ((\\ e \\<^bsub>\\\\\\<^esub>)\r \CFn (\\\\\) x)\r"
by (rule CEApp_no_restr)
also have "((\\ e \\<^bsub>\\\\\\<^esub>)) \ ((\\ Lam [y]. e' \\<^bsub>\\\\\\<^esub>))"
using Application.hyps(9)[OF prem1].
also note `((\\\\\) x) \ (\\\\\) x`
also have "(\\ Lam [y]. e' \\<^bsub>\\\\\\<^esub>)\r \ (CFn\(\ v. (\\ e' \\<^bsub>(\\\\\)(y := v)\<^esub>)))"
by (rule CELam_no_restr)
also have "CFn\(\ v. (\\ e' \\<^bsub>(\\\\\)(y := v)\<^esub>)) \CFn ((\\\\\) x) = (\\ e' \\<^bsub>(\\\\\)(y := (\\\\\) x)\<^esub>)"
by simp
also have "\ = (\\ e'[y ::= x] \\<^bsub>(\\\\\)\<^esub>)"
unfolding ESem_subst[OF `y \ x`]..
also have "\ \ \\ z \\<^bsub>\\\\\\<^esub>"
using Application.hyps(12)[OF prem2].
finally
have "(\\ App e x \\<^bsub>\\\\\\<^esub>)\r \ (\\ z \\<^bsub>\\\\\\<^esub>)\r" by this (intro cont2cont)+
}
thus ?case by (rule cfun_belowI)
show "(\\\\\) f|` (domA \) \ (\\\\\) f|` (domA \)"
using Application.hyps(10)[OF prem1]
env_restr_below_subset[OF Gamma_subset Application.hyps(13)[OF prem2]]
by (rule below_trans)
next
case (Variable \ x e L \ z)
hence [simp]:"x \ domA \"
by (metis domA_from_set map_of_is_SomeD)
case 2
have "x \ domA \"
by (rule reds_avoids_live[OF Variable.hyps(2)], simp_all)
have subset: "domA (delete x \) \ domA \"
by (rule reds_doesnt_forget[OF Variable.hyps(2)])
have "fv (delete x \, e) \ {x} \ fv (\, Var x)"
by (rule fv_delete_heap[OF `map_of \