theory Terms
imports Nominal "../QuotMain" "../QuotList"
begin

atom_decl name

(*** lets with binding patterns ***)
datatype trm1 =
  Vr1 "name"
| Ap1 "trm1" "trm1"
| Lm1 "name" "trm1"
| Lt1 "bp" "trm1" "trm1"
and bp =
  BUnit
| BVr "name"
| BPr "bp" "bp"

(* to be given by the user *)
fun 
  bv1
where
  "bv1 (BUnit) = {}"
| "bv1 (BVr x) = {x}"
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"

(*** lets with single assignments ***)
datatype trm2 =
  Vr2 "name"
| Ap2 "trm2" "trm2"
| Lm2 "name" "trm2"
| Lt2 "assign" "trm2"
and assign =
  As "name" "trm2"

(* to be given by the user *)
fun 
  bv2
where
  "bv2 (As x t) = {x}"


(*** lets with many assignments ***)
datatype trm3 =
  Vr3 "name"
| Ap3 "trm3" "trm3"
| Lm3 "name" "trm3"
| Lt3 "assign" "trm3"
and assigns =
  ANil
| ACons "name" "trm3" "assigns"

(* to be given by the user *)
fun 
  bv3
where
  "bv3 ANil = {}"
| "bv3 (ACons x t as) = {x} \<union> (bv3 as)"

end