theory Termsimports Nominal "../QuotMain" "../QuotList"beginatom_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 bv1where "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 bv2where "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 bv3where "bv3 ANil = {}"| "bv3 (ACons x t as) = {x} \<union> (bv3 as)"end