# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263567366 -3600
# Node ID 693aecde755df3a06e6726eaede984c5101eba86
# Parent  0f920b62fb7b27d28f64b298c20860f1700c9436
added free_variable function (do not know about the algorithm yet)

diff -r 0f920b62fb7b -r 693aecde755d Quot/Examples/Terms.thy
--- a/Quot/Examples/Terms.thy	Fri Jan 15 12:17:30 2010 +0100
+++ b/Quot/Examples/Terms.thy	Fri Jan 15 15:56:06 2010 +0100
@@ -4,12 +4,12 @@
 
 atom_decl name
 
-(*** lets with binding patterns ***)
+text {*** lets with binding patterns ***}
 datatype trm1 =
   Vr1 "name"
 | Ap1 "trm1" "trm1"
-| Lm1 "name" "trm1"
-| Lt1 "bp" "trm1" "trm1"
+| Lm1 "name" "trm1"        --"name is bound in trm1"
+| Lt1 "bp" "trm1" "trm1"   --"all variables in bp are bound in the 2nd trm1"
 and bp =
   BUnit
 | BVr "name"
@@ -23,7 +23,19 @@
 | "bv1 (BVr x) = {x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
 
-(*** lets with single assignments ***)
+(* 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 ***}
 datatype trm2 =
   Vr2 "name"
 | Ap2 "trm2" "trm2"
@@ -38,13 +50,23 @@
 where
   "bv2 (As x t) = {x}"
 
+(* 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)"
 
-(*** lets with many assignments ***)
+
+text {*** lets with many assignments ***}
 datatype trm3 =
   Vr3 "name"
 | Ap3 "trm3" "trm3"
 | Lm3 "name" "trm3"
-| Lt3 "assign" "trm3"
+| Lt3 "assigns" "trm3"
 and assigns =
   ANil
 | ACons "name" "trm3" "assigns"
@@ -56,4 +78,14 @@
   "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)"
 
+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)"
+
 end
\ No newline at end of file