Theory Values

section "Declarative semantics with tables as lists"

text‹
  The semantics that represents function tables as lists is largely obsolete,
  being replaced by the finite set representation. However, the proof
  of equivalence to the intersection type system still uses the version
  based on lists.
›
  
subsection "Definition of values for declarative semantics" 

theory Values
  imports Main Lambda
begin
  
datatype val = VNat nat | VFun "(val × val) list"

type_synonym func = "(val × val) list"

inductive val_le :: "val ⇒ val ⇒ bool" (infix "⊑" 52) 
  and fun_le :: "func ⇒ func ⇒ bool" (infix "≲" 52) where
  vnat_le[intro!]: "(VNat n) ⊑ (VNat n)" |
  vfun_le[intro!]: "t1 ≲ t2 ⟹ (VFun t1) ⊑ (VFun t2)" |
  fun_le[intro!]: "(∀ v1 v2. (v1,v2) ∈ set t1 ⟶ 
                       (∃ v3 v4. (v3,v4) ∈ set t2 
                        ∧ v1 ⊑ v3 ∧ v3 ⊑ v1 ∧ v2 ⊑ v4 ∧ v4 ⊑ v2))
                   ⟹ t1 ≲ t2"

type_synonym env = "((name × val) list)"

definition env_le :: "env ⇒ env ⇒ bool" (infix "⊑" 52) where 
  "ρ ⊑ ρ' ≡ ∀ x v. lookup ρ x = Some v ⟶ (∃ v'. lookup ρ' x = Some v' ∧ v ⊑ v')" 

definition env_eq :: "env ⇒ env ⇒ bool" (infix "≈" 50) where
  "ρ ≈ ρ' ≡ (∀ x. lookup ρ x = lookup ρ' x)"

end