diff -r 26f15c2dc131 -r 7e691b3c2414 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 09 16:10:08 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 09 16:44:06 2010 +0100
@@ -925,6 +925,138 @@
 apply (simp add: distinct_helper2)
 done
 
+
+
+
+
+
+
+datatype rtrm6 =
+  rVr6 "name"
+| rAp6 "rtrm6" "rtrm6"
+| rFo6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
+
+primrec
+  rbv6
+where
+  "rbv6 (rVr6 x) = {atom x}"
+| "rbv6 (rAp6 l r) = rbv6 l \<union> rbv6 r"
+| "rbv6 (rFo6 l r) = rbv6 l - rbv6 r"
+
+primrec
+  rfv_trm6
+where
+  "rfv_trm6 (rVr6 n) = {atom n}"
+| "rfv_trm6 (rAp6 t s) = (rfv_trm6 t) \<union> (rfv_trm6 s)"
+| "rfv_trm6 (rFo6 l r) = (rfv_trm6 r - rbv6 l) \<union> (rfv_trm6 l)"
+
+instantiation
+  rtrm6 :: pt
+begin
+
+primrec
+  permute_rtrm6
+where
+  "permute_rtrm6 pi (rVr6 a) = rVr6 (pi \<bullet> a)"
+| "permute_rtrm6 pi (rAp6 t1 t2) = rAp6 (permute_rtrm6 pi t1) (permute_rtrm6 pi t2)"
+| "permute_rtrm6 pi (rFo6 l r) = rFo6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"
+
+lemma pt_rtrm6_zero:
+  fixes t::rtrm6
+  shows "0 \<bullet> t = t"
+apply(induct t)
+apply(simp_all)
+done
+
+lemma pt_rtrm6_plus:
+  fixes t::rtrm6
+  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+apply(induct t)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_rtrm6_zero pt_rtrm6_plus)
+done
+
+end
+
+inductive
+  alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)"
+| a2: "\<lbrakk>t1 \<approx>6 t2; s1 \<approx>6 s2\<rbrakk> \<Longrightarrow> rAp6 t1 s1 \<approx>6 rAp6 t2 s2"
+| a3: "\<lbrakk>\<exists>pi. ((rbv6 l1, r1) \<approx>gen alpha6 rfv_trm6 pi (rbv6 l2, r2))\<rbrakk>
+        \<Longrightarrow> rFo6 l1 r1 \<approx>6 rFo6 l2 r2"
+
+lemma alpha6_equivps:
+  shows "equivp alpha6"
+sorry
+
+quotient_type
+  trm6 = rtrm6 / alpha6
+  by (auto intro: alpha6_equivps)
+
+quotient_definition
+  "Vr6 :: name \<Rightarrow> trm6"
+as
+  "rVr6"
+
+quotient_definition
+  "Ap6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
+as
+  "rAp6"
+
+quotient_definition
+  "Fo6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
+as
+  "rFo6"
+
+quotient_definition
+   "fv_trm6 :: trm6 \<Rightarrow> atom set"
+as
+  "rfv_trm6"
+
+quotient_definition
+   "bv6 :: trm6 \<Rightarrow> atom set"
+as
+  "rbv6"
+
+
+
+lemma [quot_respect]:
+ "(op = ===> alpha6) rVr6 rVr6"
+ "(alpha6 ===> alpha6 ===> alpha6) rAp6 rAp6"
+ "(alpha6 ===> alpha6 ===> alpha6) rFo6 rFo6"
+apply (simp_all add: a1 a2)
+apply clarify
+apply (rule a3)
+apply (rule_tac x="0::perm" in exI)
+apply (simp add: alpha_gen)
+(* needs rbv6_rsp *)
+sorry
+
+instantiation trm6 :: pt begin
+
+instance
+sorry
+end
+
+lemma "\<lbrakk>\<exists>pi. ((bv6 l1, r1) \<approx>gen (op =) fv_trm6 pi (bv6 l2, r2))\<rbrakk>
+        \<Longrightarrow> Fo6 l1 r1 = Fo6 l2 r2"
+apply (unfold alpha_gen)
+apply (lifting a3[unfolded alpha_gen])
+apply injection
+
+
+
+sorry
+
+
+
+
+
 text {* type schemes *} 
 datatype ty = 
   Var "name"