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