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.

abbreviation ESem_syn' ("⟦_⟧⇘_⇙"  [60,60] 60) where "⟦e⟧⇘ρ⇙ ≡ ESem e ⋅ ρ"
abbreviation EvalHeapSem_syn'  ("❙⟦ _ ❙⟧⇘_⇙"  [0,0] 110)  where "❙⟦Γ❙⟧⇘ρ⇙ ≡ evalHeap Γ (λ e. ⟦e⟧⇘ρ⇙)"
abbreviation AHSem_syn ("⦃_⦄_"  [60,60] 60) where "⦃Γ⦄ρ ≡ HSem Γ ⋅ ρ"
abbreviation AHSem_bot ("⦃_⦄"  [60] 60) where "⦃Γ⦄ ≡ ⦃Γ⦄⊥"

end
end