theory CorrectnessStacked
imports "Denotational" LaunchburyStacked
begin
subsubsection {* The semantics of let only adds new bindings *}
text {*
The following lemma is not as general as possible and specialized to @{text "\ = fempty"}, as that is
the only case required later on, and easier to prove.
*}
lemma HSem_unfold_let:
assumes distinct: "distinctVars ((x, body) # \)"
assumes fresh: "set (bn as) \* (x, Let as body, \)"
shows "\(x, Let as body) # \\ = (\(x, body) # asToHeap as @ \\)f|` (insert x (heapVars \))"
proof-
from fresh
have fresh_Gamma: "atom ` heapVars (asToHeap as) \* \"
by (metis fresh_star_Pair set_bn_to_atom_heapVars)
from fresh
have "set (bn as) \* ((x, Let as body) # \)"
by (auto simp add: fresh_star_def fresh_Pair fresh_Cons)
from fresh_assn_distinct[OF this]
have disjoint: "heapVars (asToHeap as) \ insert x (heapVars \) = {}"
by auto
hence x_not_as: "x \ heapVars (asToHeap as)"
by auto
{
fix x' e
assume "e \ snd ` set \"
have simp1: " fdom (\(x, body) # asToHeap as @ \\) \ insert x (heapVars \) = insert x (heapVars \)"
by auto
have simp2: "fdom (\(x, body) # asToHeap as @ \\) - insert x (heapVars \) = heapVars (asToHeap as)"
using disjoint
by auto
have fresh_e: "atom ` heapVars (asToHeap as) \* e"
by (rule fresh_star_heap_expr'[OF fresh_Gamma `_ \ snd\` set \`])
have "\ e \\<^bsub>fmap_restr (insert x (heapVars \)) (\(x, body) # asToHeap as @ \\)\<^esub> = \ e \\<^bsub>\(x, body) # asToHeap as @ \\\<^esub>"
apply (rule ESem_ignores_fresh_restr'[symmetric])
apply (subst simp2)
apply (rule fresh_e)
done
} note Gamma_eq = this
case goal1
have "\(x, Let as body) # \\ = fmap_restr (insert x (heapVars \)) (\(x, body) # asToHeap as @ \\)"
proof(rule below_antisym)
show "\(x, Let as body) # \\ \ fmap_restr (insert x (heapVars \)) (\(x, body) # asToHeap as @ \\)" (is "_ \ ?r")
proof (rule HSem_fempty_below)
fix x'
assume "x' \ heapVars ((x, Terms.Let as body) # \)"
hence x': "x' \ insert x (heapVars \)" by simp
hence x'_not_as:"x' \ heapVars (asToHeap as)"
using disjoint
by auto
show "\ the (map_of ((x, Terms.Let as body) # \) x') \\<^bsub>?r\<^esub> \ ?r f! x'"
proof(cases "x' = x")
case True
have "\ Terms.Let as body \\<^bsub>?r\<^esub> = \ body \\<^bsub>\asToHeap as\?r\<^esub>" by simp
also have "... = \ body \\<^bsub>\asToHeap as\(fmap_restr (insert x (heapVars \)) (\asToHeap as @ ((x, body) # \)\))\<^esub>"
by (rule arg_cong[OF HSem_reorder_head_append[OF x_not_as]])
also have "... = \ body \\<^bsub>\asToHeap as @ ((x, body) # \)\\<^esub>"
by (rule arg_cong[OF HSem_redo[where \ = "f\" and \ = "(x, body) # \", simplified]])
also have "... = \ body \\<^bsub>\(x, body) # asToHeap as @ \\\<^esub>"
by (rule arg_cong[OF HSem_reorder_head_append[OF x_not_as], symmetric])
finally
show ?thesis using True x' by (simp add: lookup_HSem_heap)
next
case False thus ?thesis
apply (subst (2) HSem_eq)
using x'
apply (simp add: lookupHeapToEnvNotAppend[OF x'_not_as] lookupHeapToEnv Gamma_eq[OF the_map_of_snd])
done
qed
qed auto
have "(\(x, body) # asToHeap as @ \\) \ \asToHeap as\\(x, Let as body) # \\" (is "_ \ ?r")
proof (rule HSem_fempty_below)
fix x'
assume "x' \ heapVars ((x, body) # asToHeap as @ \)"
hence x': "x' = x \ x' \ heapVars (asToHeap as) \ x' \ heapVars \" by simp
show "\ the (map_of ((x, body) # asToHeap as @ \) x') \\<^bsub>?r\<^esub> \ ?r f! x'"
proof(cases "x' = x")
assume "x' = x"
thus ?thesis
by (simp add: lookup_HSem_other[OF x_not_as] lookup_HSem_heap)
next
have merged_r: "?r = \asToHeap as @ ((x, Let as body) # \)\"
apply (rule HSem_merge)
using disjoint distinct apply (auto simp add: distinctVars_Cons distinctVars_append)[1]
using fresh apply (metis fresh_star_list(2) fresh_star_Pair set_bn_to_atom_heapVars)
done
assume "x' \ x"
hence map_of_reorder: "map_of ((x, body) # asToHeap as @ \) x' = map_of (asToHeap as @ ((x, Let as body) # \)) x'"
apply simp
apply (subst map_add_upd_left)
apply (metis dom_map_of_conv_heapVars x_not_as)
apply simp
done
show ?thesis
unfolding merged_r
apply (subst lookup_HSem_heap)
using x' apply simp[1]
unfolding map_of_reorder
apply (rule below_refl)
done
qed
qed auto
thus "fmap_restr (insert x (heapVars \)) (\(x, body) # asToHeap as @ \\) \ \(x, Let as body) # \\"
apply (rule below_trans[OF cont2monofunE[OF fmap_restr_cont] eq_imp_below])
apply (rule fmap_restr_HSem_noop[of _ "\(x, Terms.Let as body) # \\", simplified (no_asm)])
using disjoint apply auto
done
qed
thus ?case
by (rule subst[where s = "insert q Q", standard, rotated], auto)
qed
text {* This is the main correctness theorem for the stacked semantics. *}
theorem correctness:
assumes "\ : \' \ \ : \'"
and "distinctVars (\' @ \)"
shows "\\'@\\ \ \\'@\\"
using assms
proof(induct rule:reds_distinct_ind)
case (Lambda x y e \ \')
show ?case by simp
-- "The lambda-case is trival"
next
case (Application n \ \' \ \' x e y \ \' z e')
let "?restr \" = "fmap_restr (insert x (heapVars \' \ heapVars \)) (\::Env)"
let "?restr2 \" = "fmap_restr (insert x (heapVars \' \ heapVars \)) (\::Env)"
have "n \ z" using Application by (simp add: fresh_Pair fresh_at_base)
from stack_unchanged[OF distinct_redsD1[OF Application.hyps(8)]]
have "\' = \'" by simp
hence [simp]:"atom n \ \'" using Application by (simp add: fresh_Pair)+
have "atom n \ (\, e)" using Application by (simp add: fresh_Pair)
note reds_fresh[OF Application(8) this]
hence "atom n \ (\, Lam [z]. e')"
using Application(5)
by (metis (hide_lams, no_types) Application(1) fresh_Pair heapVars_not_fresh)
with `n \ z`
have [simp]: "atom n \ \" "atom n \ e'"
by (auto simp add: fresh_Pair)
note subset1 = reds_doesnt_forget'(1)[OF Application.hyps(8), unfolded append_Cons]
from reds_doesnt_forget'(2)[OF Application.hyps(8), unfolded append_Cons]
have subset2: "heapVars ((x, App (Var n) y) # \') \ heapVars ((x, App (Var n) y) # \')"
apply (rule distinctVars_Cons_subset)
apply (metis Application(4) distinctVars_appendD1)
apply (metis Application(5) distinctVars_appendD1)
done
have "n \ x"
by (metis Application(1) fresh_PairD(1) fresh_PairD(2) not_self_fresh)
have "\((x, App e y) # \') @ \\ = (\(x, App e y) # \' @ \\)"
by simp
also
have "... = ?restr (\(n, e) # (x, App e y) # \' @ \\)"
-- {* Adding a fresh variable *}
apply (subst HSem_add_fresh[of n "(x, App e y) # \' @ \" "f\" e , symmetric])
using Application(1) apply (simp add: fresh_Pair fresh_Cons fresh_append)
apply simp
apply simp
done
also have "... = ?restr (\(x, App e y) # (n, e) # \' @ \\)"
by (rule arg_cong[OF HSem_reorder_head[OF `n \ x`]])
also
have "... = ?restr (\(x, App (Var n) y) # (n, e) # \' @ \\)"
-- {* Substituting the variable *}
apply (rule arg_cong[OF HSem_subst_var_app[symmetric]])
using Application(1) apply (simp add: fresh_Pair)
apply simp
done
also
have "... = ?restr (\(n, e) # (x, App (Var n) y) # \' @ \\)"
by (simp add: HSem_reorder_head[OF `n \ x`])
also
have "... \ ?restr2 (\(n, Lam [z]. e') # (x, App (Var n) y) # \' @ \\)"
-- "Induction hypothesis"
apply (rule fmap_restr_le[OF Application.hyps(9)[simplified]])
using subset1 subset2 by auto
also
have "... \ ?restr2 (\(x, App (Var n) y) # (n, Lam [z]. e') # \' @ \\)"
by (simp add: HSem_reorder_head[OF `n \ x`])
also
have "... = ?restr2 (\(x, App (Lam [z]. e') y) # (n, Lam [z]. e') # \' @ \\)"
-- "Substituting the variable again"
apply (rule arg_cong[OF HSem_subst_var_app])
using Application(1) apply (simp add: fresh_Pair)
apply simp
done
also
have "... = ?restr2 (\(n, Lam [z]. e') # (x, App (Lam [z]. e') y) # \' @ \\)"
by (simp add: HSem_reorder_head[OF `n \ x`])
also
have "... = (\(x, App (Lam [z]. e') y) # \' @ \\)"
-- "Removing the fresh variable"
apply (subst HSem_add_fresh[of n "(x, App (Lam [z]. e') y) # \' @ \" fempty "Lam [z]. e'", symmetric])
using Application(1) apply (simp add: fresh_Pair fresh_Cons fresh_append)
apply simp
apply simp
done
also
have "... = \(x, e'[z::=y]) # \' @ \\"
-- "Semantics of application"
apply (rule HSem_subst_exp)
apply simp
apply (rule ESem_subst[simplified])
using Application(2)
apply (auto simp add: fresh_Pair heapVars_not_fresh)
done
also
have "... \ \\' @ \\"
-- "Induction hypothesis"
by (rule Application.hyps(11)[simplified])
finally
show "\((x, App e y) # \') @ \\ \ \