theory AbstractDenotational
imports "HeapSemantics" Terms
begin
subsubsection {* The denotational semantics for expressions *}
text {*
Because we need to define two semantics later on, we are abstract in the actual domain.
*}
locale semantic_domain =
fixes Fn :: "('Value \ 'Value) \ ('Value::{pcpo_pt,pure})"
fixes Fn_project :: "'Value \ ('Value \ 'Value)"
fixes tick :: "'Value \ 'Value"
begin
nominal_function
ESem :: "exp \ (var \ 'Value) \ 'Value"
where
(* Restrict \ to avoid having to demand atom x \ \ *)
"ESem (Lam [x]. e) = (\ \. tick \ (Fn \ (\ v. ESem e \ ((\ f|` fv (Lam [x]. e))(x := v)))))"
(* Do not use \\ Var x \\<^bsub>\\<^esub> in the rule for App; it costs an additional
resource and makes the adequacy proof difficult. *)
| "ESem (App e x) = (\ \. tick \ (Fn_project \ (ESem e \ \) \ (\ x)))"
| "ESem (Var x) = (\ \. tick \ (\ x))"
| "ESem (Let as body) = (\ \. tick \ (ESem body \ (has_ESem.HSem ESem as \ (\ f|` fv (Let as body)))))"
| "ESem (Bool b) = \"
| "ESem (scrut ? e1 : e2) = \"
proof-
txt {* The following proofs discharge technical obligations generated by the Nominal package. *}
case goal1 thus ?case
unfolding eqvt_def ESem_graph_aux_def
apply rule
apply (perm_simp)
apply (simp add: Abs_cfun_eqvt)
done
next
case (goal3 P x)
thus ?case by (metis (poly_guards_query) exp_strong_exhaust)
next
case (goal4 x e x' e')
from goal4(5)
show ?case
proof (rule eqvt_lam_case)
fix \ :: perm
assume *: "supp (-\) \* (fv (Lam [x]. e) :: var set)"
{ fix \ v
have "ESem_sumC (\ \ e)\((\ f|` fv (Lam [x]. e))((\ \ x) := v)) = - \ \ ESem_sumC (\ \ e)\((\ f|` fv (Lam [x]. e))((\ \ x) := v))"
by (simp add: permute_pure)
also have "\ = ESem_sumC e\((- \ \ (\ f|` fv (Lam [x]. e)))(x := v))" by (simp add: pemute_minus_self eqvt_at_apply[OF goal4(1)])
also have "- \ \ (\ f|` fv (Lam [x]. e)) = (\ f|` fv (Lam [x]. e))" by (rule env_restr_perm'[OF *]) auto
finally have "ESem_sumC (\ \ e)\((\ f|` fv (Lam [x]. e))((\ \ x) := v)) = ESem_sumC e\((\ f|` fv (Lam [x]. e))(x := v))".
}
thus " (\ \. tick\(Fn\(\ v. ESem_sumC (\ \ e)\((\ f|` fv (Lam [x]. e))(\ \ x := v))))) = (\ \. tick\(Fn\(\ v. ESem_sumC e\((\ f|` fv (Lam [x]. e))(x := v)))))" by simp
qed
next
case (goal19 as body as' body')
from goal19(9)
show ?case
proof (rule eqvt_let_case)
fix \ :: perm
assume *: "supp (-\) \* (fv (Terms.Let as body) :: var set)"
{ fix \
have "ESem_sumC (\ \ body)\(has_ESem.HSem ESem_sumC (\ \ as)\(\ f|` fv (Terms.Let as body)))
= - \ \ ESem_sumC (\ \ body)\(has_ESem.HSem ESem_sumC (\ \ as)\(\ f|` fv (Terms.Let as body)))"
by (rule permute_pure[symmetric])
also have "\ = (- \ \ ESem_sumC) body\(has_ESem.HSem (- \ \ ESem_sumC) as\(- \ \ \ f|` fv (Terms.Let as body)))"
by (simp add: pemute_minus_self)
also have "(- \ \ ESem_sumC) body = ESem_sumC body"
by (rule eqvt_at_apply[OF `eqvt_at ESem_sumC body`])
also have "has_ESem.HSem (- \ \ ESem_sumC) as = has_ESem.HSem ESem_sumC as"
by (rule HSem_cong[OF eqvt_at_apply[OF goal19(2)] refl])
also have "- \ \ \ f|` fv (Let as body) = \ f|` fv (Let as body)"
by (rule env_restr_perm'[OF *], simp)
finally have "ESem_sumC (\ \ body)\(has_ESem.HSem ESem_sumC (\ \ as)\(\ f|` fv (Let as body))) = ESem_sumC body\(has_ESem.HSem ESem_sumC as\(\ f|` fv (Let as body)))".
}
thus "(\ \. tick\(ESem_sumC (\ \ body)\(has_ESem.HSem ESem_sumC (\ \ as)\(\ f|` fv (Let as body))))) =
(\ \. tick\(ESem_sumC body\(has_ESem.HSem ESem_sumC as\(\ f|` fv (Let as body)))))" by (simp only:)
qed
qed auto
(* [eqvt] attributes do not survive instantiation, so we pass (no_eqvt) here. We don't need it
anyways\ *)
nominal_termination (in semantic_domain) (no_eqvt) by lexicographic_order
sublocale has_ESem ESem.
abbreviation ESem_syn' ("\_\\<^bsub>_\<^esub>" [60,60] 60) where "\e\\<^bsub>\\<^esub> \ ESem e \ \"
abbreviation EvalHeapSem_syn' ("\<^bold>\ _ \<^bold>\\<^bsub>_\<^esub>" [0,0] 110) where "\<^bold>\\\<^bold>\\<^bsub>\\<^esub> \ evalHeap \ (\ e. \e\\<^bsub>\\<^esub>)"
abbreviation AHSem_syn ("\_\_" [60,60] 60) where "\\\\ \ HSem \ \ \"
abbreviation AHSem_bot ("\_\" [60] 60) where "\\\ \ \\\\"
end
end