Theory AbstractDenotational

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 B :: "bool discr  'Value"
  fixes B_project :: "'Value  '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 ⟧ρ  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) = (Λ ρ. tick(B(Discr b)))"
| "ESem (scrut ? e1 : e2) = (Λ ρ. tick((B_project(ESem scrutρ))(ESem e1ρ)(ESem e2ρ)))"
proof goal_cases
txt ‹The following proofs discharge technical obligations generated by the Nominal package.›

case 1 thus ?case
  unfolding eqvt_def ESem_graph_aux_def
  apply rule
  apply (perm_simp)
  apply (simp add: Abs_cfun_eqvt)
  apply (simp add: unpermute_def permute_pure)
  done
next
case (3 P x)
  thus ?case by (metis (poly_guards_query) exp_strong_exhaust)
next

case prems: (4 x e x' e')
  from prems(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 prems(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 prems: (19 as body as' body')
  from prems(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 prems(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.

notation ESem_syn (" _ ⟧⇘_"  [60,60] 60)
notation EvalHeapSem_syn  (" _ _"  [0,0] 110)
notation HSem_syn ("__"  [60,60] 60)
abbreviation AHSem_bot ("_"  [60] 60) where "Γ  Γ"

end
end