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

```