Theory Lambda

section "Syntax of the lambda calculus"

theory Lambda
imports Main
begin
  
type_synonym name = nat

datatype exp = EVar name | ENat nat | ELam name exp | EApp exp exp
  | EPrim "nat  nat  nat" exp exp | EIf exp exp exp
      
fun lookup :: "('a × 'b) list  'a  'b option" where
  "lookup [] x = None" |
  "lookup ((y,v)#ls) x = (if (x = y) then Some v else lookup ls x)"

fun FV :: "exp  nat set" where
  "FV (EVar x) = {x}" |
  "FV (ENat n) = {}" |
  "FV (ELam x e) = FV e - {x}" |
  "FV (EApp e1 e2) = FV e1  FV e2" |
  "FV (EPrim f e1 e2) = FV e1  FV e2" |
  "FV (EIf e1 e2 e3) = FV e1  FV e2  FV e3"

fun BV :: "exp  nat set" where
  "BV (EVar x) = {}" |
  "BV (ENat n) = {}" |
  "BV (ELam x e) = BV e  {x}" |
  "BV (EApp e1 e2) = BV e1  BV e2" |
  "BV (EPrim f e1 e2) = BV e1  BV e2" |
  "BV (EIf e1 e2 e3) = BV e1  BV e2  BV e3"

end