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