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