--- a/Quot/Nominal/Terms.thy	Wed Feb 03 12:06:10 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 12:13:22 2010 +0100
@@ -121,7 +121,29 @@
   shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
   apply (induct t s rule: alpha1.inducts)
   apply (simp_all add:eqvts alpha1_inj)
-  sorry
+  apply (erule exE)
+  apply (rule_tac x="pi \<bullet> pia" in exI)
+  apply (simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+  apply(simp add: atom_eqvt eqvts)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+  apply(simp add: eqvts atom_eqvt)
+  apply(simp add: permute_eqvt[symmetric])
+  apply (erule exE)
+  apply (rule_tac x="pi \<bullet> pia" in exI)
+  apply (simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+  apply(simp add: atom_eqvt eqvts)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+  apply(simp add: eqvts atom_eqvt)
+  apply(simp add: permute_eqvt[symmetric])
+  done
 
 lemma alpha1_equivp: "equivp alpha1" 
   sorry
@@ -331,7 +353,7 @@
 apply(simp (no_asm) add: supp_def)
 apply(simp add: alpha1_INJ)
 apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen.simps)
+apply(simp add: alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done
@@ -349,7 +371,7 @@
   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
   and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
   shows   "P a rtrma"
-
+sorry
 
 section {*** lets with single assignments ***}
 
@@ -628,4 +650,85 @@
 
 
 
+
+
+
+
+
+datatype rtrm5 =
+  rVr5 "name"
+| rAp5 "rtrm5" "rtrm5"
+| rLt5 "rlts" "rtrm5"
+and rlts =
+  rLnil
+| rLcons "name" "rtrm5" "rlts"
+
+primrec
+  bv5
+where
+  "bv5 rLnil = {}"
+| "bv5 (rLcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+
+primrec
+  rfv_trm5 and rfv_lts
+where
+  "rfv_trm5 (rVr5 n) = {atom n}"
+| "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
+| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - bv5 lts) \<union> (rfv_lts lts - bv5 lts)"
+| "rfv_lts (rLnil) = {}"
+| "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
+
+instantiation
+  rtrm5 and rlts :: pt
+begin
+
+primrec
+  permute_rtrm5 and permute_rlts
+where
+  "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
+| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
+| "permute_rtrm5 pi (rLt5 as t) = rLt5 (permute_rlts pi as) (permute_rtrm5 pi t)"
+| "permute_rlts pi (rLnil) = rLnil"
+| "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
+
+lemma pt_rtrm5_zero:
+  fixes t::rtrm5
+  and   l::rlts
+  shows "0 \<bullet> t = t"
+  and   "0 \<bullet> l = l"
+apply(induct t and l rule: rtrm5_rlts.inducts)
+apply(simp_all)
+done
+
+lemma pt_rtrm5_plus:
+  fixes t::rtrm5
+  and   l::rlts
+  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+  and   "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
+apply(induct t and l rule: rtrm5_rlts.inducts)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
+done
+
 end
+
+inductive
+  alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
+and
+  alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
+| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
+| a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and>
+             (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and>
+              (pi \<bullet> (bv5 l1) = bv5 l2))
+        \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
+| a4: "rLnil \<approx>l rLnil"
+| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+
+thm a3[simplified alpha_gen]
+end