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+ −