Theory RelationalSemFSet

section "Declarative semantics as a relational semantics"

theory RelationalSemFSet
  imports Lambda ValuesFSet
begin
  
inductive rel_sem :: "env ⇒ exp ⇒ val ⇒ bool" ("_ ⊢ _ ⇒ _" [52,52,52] 51) where
  rnat[intro!]: "ρ ⊢ ENat n ⇒ VNat n" |
  rprim[intro!]: "⟦ ρ ⊢ e1 ⇒ VNat n1; ρ ⊢ e2 ⇒ VNat n2 ⟧ ⟹ ρ ⊢ EPrim f e1 e2 ⇒ VNat (f n1 n2)" |
  rvar[intro!]: "⟦ lookup ρ x = Some v'; v ⊑ v' ⟧ ⟹ ρ ⊢ EVar x ⇒ v" |
  rlam[intro!]: "⟦ ∀ v v'. (v,v') ∈ fset t ⟶ (x,v)#ρ ⊢ e ⇒ v' ⟧
    ⟹ ρ ⊢ ELam x e ⇒ VFun t" |
  rapp[intro!]: "⟦ ρ ⊢ e1 ⇒ VFun t; ρ ⊢ e2 ⇒ v2; (v3,v3') ∈ fset t; v3 ⊑ v2; v ⊑ v3'⟧
    ⟹ ρ ⊢ EApp e1 e2 ⇒ v" |
  rifnz[intro!]: "⟦ ρ ⊢ e1 ⇒ VNat n; n ≠ 0; ρ ⊢ e2 ⇒ v ⟧ ⟹ ρ ⊢ EIf e1 e2 e3 ⇒ v" |
  rifz[intro!]: "⟦ ρ ⊢ e1 ⇒ VNat n; n = 0; ρ ⊢ e3 ⇒ v ⟧ ⟹ ρ ⊢ EIf e1 e2 e3 ⇒ v"
  
end