theory CorrectnessOriginal
imports "Denotational" "Launchbury"
begin
text {*
This is the main correctness theorem, Theorem 2 from \cite{launchbury}.
*}
(* Another possible invariant seems to be: "edom \ - domA \ \ set L" *)
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
from Application.hyps(10)[OF prem1, where \ = \]
have "((\\\\) f|` domA \) x = ((\\\\) f|` domA \) x" by simp
with True show ?thesis by simp
next
case False
from False reds_avoids_live[OF Application.hyps(8)]
show ?thesis by (simp add: lookup_HSem_other)
qed
have "\ App e x \\<^bsub>\\\\\<^esub> = (\ e \\<^bsub>\\\\\<^esub>) \Fn (\\\\) x"
by simp
also have "\ = (\ Lam [y]. e' \\<^bsub>\\\\\<^esub>) \Fn (\\\\) x"
using Application.hyps(9)[OF prem1] by simp
also have "\ = (\ Lam [y]. e' \\<^bsub>\\\\\<^esub>) \Fn (\\\\) x"
unfolding *..
also have "\ = (Fn \ (\ v. \ e' \\<^bsub>(\\\\)(y := v)\<^esub>)) \Fn (\\\\) x"
by simp
also have "\ = \ e' \\<^bsub>(\\\\)(y := (\\\\) x)\<^esub>"
by simp
also have "\ = \ e'[y ::= x] \\<^bsub>\\\\\<^esub>"
by (rule arg_cong[OF ESem_subst[OF `y \ x`]])
also have "\ = \ z \\<^bsub>\\\\\<^esub>"
by (rule Application.hyps(12)[OF prem2])
finally
show ?case.
show "(\\\\) f|` domA \ = (\\\\) f|` domA \"
using Application.hyps(10)[OF prem1]
env_restr_eq_subset[OF Gamma_subset Application.hyps(13)[OF prem2]]
by (rule trans)
next
case (Variable \ x e L \ z)
hence [simp]:"x \ domA \" by (metis domA_from_set map_of_is_SomeD)
let ?\ = "delete x \"
case 2
have "x \ domA \"
by (rule reds_avoids_live[OF Variable.hyps(2)], simp_all)
have subset: "domA ?\ \ domA \"
by (rule reds_doesnt_forget[OF Variable.hyps(2)])
have "fv (?\, e) \ {x} \ fv (\, Var x)"
by (rule fv_delete_heap[OF `map_of \ x = Some e`])
hence prem: "fv (?\, e) - domA ?\ \ set (x # L)" using 2 by auto
have fv_subset: "fv (?\, e) - domA ?\ \ - (domA \ - domA \)"
apply (rule subset_trans[OF prem])
apply (rule subset_trans[OF reds_avoids_live'[OF Variable.hyps(2)]])
by auto
let "?new" = "domA \ - domA \"
have "domA \ \ (-?new)" by auto
have "\\\\ = \(x,e) # ?\\\"
by (rule HSem_reorder[OF map_of_delete_insert[symmetric, OF Variable(1)]])
also have "\ = (\ \'. (\ ++\<^bsub>(domA ?\)\<^esub> (\?\\\'))( x := \ e \\<^bsub>\'\<^esub>))"
by (rule iterative_HSem, simp)
also have "\ = (\ \'. (\ ++\<^bsub>(domA ?\)\<^esub> (\?\\\'))( x := \ e \\<^bsub>\?\\\'\<^esub>))"
by (rule iterative_HSem', simp)
finally
have "(\\\\)f|` (- ?new) = (...) f|` (- ?new)" by simp
also have "\ = (\ \'. (\ ++\<^bsub>domA \\<^esub> (\\\\