Theory DeclSemAsDenot

subsection "Declarative semantics as a denotational semantics"    

theory DeclSemAsDenot
  imports Lambda Values
begin

fun E :: "exp ⇒ env ⇒ val set" where
  Enat: "E (ENat n) ρ = { v. v = VNat n }" |
  Evar: "E (EVar x) ρ = { v. ∃ v'. lookup ρ x = Some v' ∧ v ⊑ v' }" |
  Elam: "E (ELam x e) ρ = { v. ∃ f. v = VFun f ∧ (∀ v1 v2. (v1, v2) ∈ set f 
    ⟶ v2 ∈ E e ((x,v1)#ρ)) }" |
  Eapp: "E (EApp e1 e2) ρ = { v3. ∃ f v2 v2' v3'. 
      VFun f ∈ E e1 ρ ∧ v2 ∈ E e2 ρ ∧ (v2', v3') ∈ set f ∧ v2' ⊑ v2 ∧ v3 ⊑ v3' }" |
  Eprim: "E (EPrim f e1 e2) ρ = { v. ∃ n1 n2. VNat n1 ∈ E e1 ρ 
          ∧ VNat n2 ∈ E e2 ρ ∧ v = VNat (f n1 n2) }" |
  Eif: "E (EIf e1 e2 e3) ρ = { v. ∃ n. VNat n ∈ E e1 ρ
         ∧ (n = 0 ⟶ v ∈ E e3 ρ) ∧ (n ≠ 0 ⟶ v ∈ E e2 ρ) }"

end