diff -r 95e587907728 -r 3d28e437581b Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Thu Feb 11 14:23:26 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 11 15:08:45 2010 +0100
@@ -1190,6 +1190,76 @@
   apply (rule refl)
 done
 
+datatype rfoo8 =
+  Foo0 "name"
+| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
+and rbar8 =
+  Bar0 "name"
+| Bar1 "name" "name" "rbar8" --"bind second name in b"
+
+primrec
+  rbv8
+where
+  "rbv8 (Bar0 x) = {}"
+| "rbv8 (Bar1 v x b) = {atom v}"
+
+primrec 
+  rfv_foo8 and rfv_bar8
+where
+  "rfv_foo8 (Foo0 x) = {atom x}"
+| "rfv_foo8 (Foo1 b t) = (rfv_foo8 t - rbv8 b) \<union> (rfv_bar8 b)"
+| "rfv_bar8 (Bar0 x) = {atom x}"
+| "rfv_bar8 (Bar1 v x t) = {atom v} \<union> (rfv_bar8 t - {atom x})"
+
+instantiation
+  rfoo8 and rbar8 :: pt
+begin
+
+primrec
+  permute_rfoo8 and permute_rbar8
+where
+  "permute_rfoo8 pi (Foo0 a) = Foo0 (pi \<bullet> a)"
+| "permute_rfoo8 pi (Foo1 b t) = Foo1 (permute_rbar8 pi b) (permute_rfoo8 pi t)"
+| "permute_rbar8 pi (Bar0 a) = Bar0 (pi \<bullet> a)"
+| "permute_rbar8 pi (Bar1 v x t) = Bar1 (pi \<bullet> v) (pi \<bullet> x) (permute_rbar8 pi t)"
+
+instance sorry
+
+end
+
+inductive
+  alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
+and
+  alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
+| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
+| a3: "(\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f rfv_foo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
+| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b rfv_bar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
+
+lemma "(alpha8b ===> op =) rbv8 rbv8"
+  apply simp apply clarify
+  apply (erule alpha8f_alpha8b.inducts(2))
+  apply (simp_all)
+done
+
+lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8"
+  apply simp apply clarify
+  apply (erule alpha8f_alpha8b.inducts(2))
+  apply (simp_all add:alpha_gen)
+done
+
+lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8"
+  apply simp apply clarify
+  apply (erule alpha8f_alpha8b.inducts(1))
+  apply (simp_all add:alpha_gen)
+  apply (clarify)
+sorry (* ??? *)
+
+
+
+
+
 
 text {* type schemes *} 
 datatype ty =