text {*** lets with binding patterns ***}

| Lm1 "name" "trm1"        --"name is bound in trm1"

| Lt1 "bp" "trm1" "trm1"   --"all variables in bp are bound in the 2nd trm1"

(* needs to be calculated by the package *)

fun 

  fv_trm1 and fv_bp

where

  "fv_trm1 (Vr1 x) = {x}"

| "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)"

| "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}"

| "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)"

| "fv_bp (BUnit) = {}"

| "fv_bp (BVr x) = {x}"

| "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)"

text {*** lets with single assignments ***}

(* needs to be calculated by the package *)

fun 

  fv_trm2 and fv_assign

where

  "fv_trm2 (Vr2 x) = {x}"

| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"

| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}"

| "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"

| "fv_assign (As x t) = (fv_trm2 t)"

text {*** lets with many assignments ***}

| Lt3 "assigns" "trm3"

fun 

  fv_trm3 and fv_assigns

where

  "fv_trm3 (Vr3 x) = {x}"

| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"

| "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}"

| "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)"

| "fv_assigns (ANil) = {}"

| "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)"