diff -r 2bf82fa871e7 -r 9bbf56cdeb88 Nominal/Test.thy
--- a/Nominal/Test.thy	Mon Mar 08 15:28:25 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 08 16:11:42 2010 +0100
@@ -30,6 +30,11 @@
 where
   "bi (BP x t) = {atom x}"
 
+(* compat should be
+compat (BP x t) pi (BP x' t')
+  \<equiv> alpha_trm t t' \<and> pi o x = x'
+*)
+
 typ lam_raw
 term VAR_raw
 term APP_raw
@@ -64,6 +69,12 @@
 | "f (PS x) = {atom x}"
 | "f (PD x y) = {atom x, atom y}"
 
+(* compat should be
+compat (PN) pi (PN) \<equiv> TRue
+compat (PS x) pi (PS x') \<equiv> pi o x = x'
+compat (PD p1 p2) pi (PD p1' p2') \<equiv> compat p1 pi p1' \<and> compat p2 pi p2'
+*)
+
 
 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
@@ -148,7 +159,17 @@
 where
   "bv2 (As x t) = {atom x}"
 
-(* example 3 from Terms.thy *)
+(* compat should be
+compat (As x t) pi (As x' t') \<equiv> pi o x = x' \<and> alpha t t'
+*)
+
+
+thm fv_trm2_raw_fv_assign_raw.simps[no_vars]
+thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars]
+
+
+
+text {* example 3 from Terms.thy *}
 
 nominal_datatype trm3 =
   Vr3 "name"
@@ -164,6 +185,12 @@
   "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
 
+
+(* compat should be
+compat (ANil) pi (PNil) \<equiv> TRue
+compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts'
+*)
+
 (* example 4 from Terms.thy *)
 
 (* fv_eqvt does not work, we need to repaire defined permute functions