--- a/Quot/Nominal/Terms.thy	Thu Feb 11 16:54:04 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 11 17:58:06 2010 +0100
@@ -1194,14 +1194,12 @@
 
 
 
-atom_decl name2
-
 datatype rfoo8 =
   Foo0 "name"
 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
 and rbar8 =
-  Bar0 "name2"
-| Bar1 "name" "name2" "rbar8" --"bind second name in b"
+  Bar0 "name"
+| Bar1 "name" "name" "rbar8" --"bind second name in b"
 
 primrec
   rbv8
@@ -1268,6 +1266,115 @@
 
 
 
+
+datatype rlam9 =
+  Var9 "name"
+| Lam9 "name" "rlam9" --"bind name in rlam"
+and rbla9 =
+  Bla9 "rlam9" "rlam9" --"bind bv(first) in second"
+
+primrec
+  rbv9
+where
+  "rbv9 (Var9 x) = {}"
+| "rbv9 (Lam9 x b) = {atom x}"
+
+primrec 
+  rfv_lam9 and rfv_bla9
+where
+  "rfv_lam9 (Var9 x) = {atom x}"
+| "rfv_lam9 (Lam9 b t) = (rfv_lam9 t - {atom b})"
+| "rfv_bla9 (Bla9 l r) = (rfv_lam9 r - rbv9 l) \<union> rfv_lam9 l"
+
+instantiation
+  rlam9 and rbla9 :: pt
+begin
+
+primrec
+  permute_rlam9 and permute_rbla9
+where
+  "permute_rlam9 pi (Var9 a) = Var9 (pi \<bullet> a)"
+| "permute_rlam9 pi (Lam9 b t) = Lam9 (pi \<bullet> b) (permute_rlam9 pi t)"
+| "permute_rbla9 pi (Bla9 l r) = Bla9 (permute_rlam9 pi l) (permute_rlam9 pi r)"
+
+instance sorry
+
+end
+
+inductive
+  alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
+and
+  alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"
+| a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l rfv_lam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
+| a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l rfv_lam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2"
+
+quotient_type
+  lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
+sorry
+
+quotient_definition
+  "qVar9 :: name \<Rightarrow> lam9"
+as
+  "Var9"
+
+quotient_definition
+  "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9"
+as
+  "Lam9"
+
+quotient_definition
+  "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9"
+as
+  "Bla9"
+
+quotient_definition
+  "fv_lam9 :: lam9 \<Rightarrow> atom set"
+as
+  "rfv_lam9"
+
+quotient_definition
+  "fv_bla9 :: bla9 \<Rightarrow> atom set"
+as
+  "rfv_bla9"
+
+quotient_definition
+  "bv9 :: lam9 \<Rightarrow> atom set"
+as
+  "rbv9"
+
+instantiation lam9 and bla9 :: pt
+begin
+
+quotient_definition
+  "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"
+as
+  "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
+
+quotient_definition
+  "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
+as
+  "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
+
+instance
+sorry
+
+end
+
+lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk>
+ \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"
+apply (lifting a3[unfolded alpha_gen])
+apply injection
+sorry
+
+
+
+
+
+
+
+
 text {* type schemes *} 
 datatype ty = 
   Var "name"