Theory Values

section "Declarative semantics with tables as lists"

  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
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)"