--- a/Nominal/Term5.thy	Mon Mar 22 18:38:59 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 23 07:39:10 2010 +0100
@@ -72,7 +72,12 @@
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
 apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
-(*
+done
+
+lemma alpha5_symp1:
+"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
+(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
+(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
 apply (simp_all add: alpha5_inj)
 apply (erule exE)
@@ -91,7 +96,50 @@
 apply (rotate_tac 6)
 apply simp
 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])
-apply (simp)*)
+apply (simp)
+done
+
+thm alpha_gen_sym[no_vars]
+thm alpha_gen_compose_sym[no_vars]
+
+lemma tt: 
+  "\<lbrakk>R (- p \<bullet> x) y \<Longrightarrow> R (p \<bullet> y) x; (bs, x) \<approx>gen R f (- p) (cs, y)\<rbrakk> \<Longrightarrow> (cs, y) \<approx>gen R f p (bs, x)"
+  unfolding alphas
+  unfolding fresh_star_def
+  by (auto simp add:  fresh_minus_perm)
+
+lemma alpha5_symp2:
+  shows "a \<approx>5 b \<Longrightarrow> b \<approx>5 a"
+  and   "x \<approx>l y \<Longrightarrow> y \<approx>l x"
+  and   "alpha_rbv5 x y \<Longrightarrow> alpha_rbv5 y x"
+apply(induct rule:  alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* binding case *)
+apply(simp add: alpha5_inj)
+apply(erule exE)
+apply(rule_tac x="- pi" in exI)
+apply(rule tt)
+apply(simp add: alphas)
+apply(erule conjE)+
+apply(drule_tac p="- pi" in alpha5_eqvt(2))
+apply(drule_tac p="- pi" in alpha5_eqvt(2))
+apply(drule_tac p="- pi" in alpha5_eqvt(1))
+apply(drule_tac p="- pi" in alpha5_eqvt(1))
+apply(simp)
+apply(simp add: alphas)
+apply(erule conjE)+
+apply metis
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
 done
 
 lemma alpha5_transp:
@@ -114,6 +162,10 @@
 apply (simp_all add: alpha5_inj)
 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
 (* HERE *)
+(*
+apply(rule alpha_gen_trans)
+thm alpha_gen_trans
+defer
 apply (simp add: alpha_gen)
 apply clarify
 apply(simp add: fresh_star_plus)
@@ -132,6 +184,8 @@
 apply (drule_tac p="pi" in alpha5_eqvt(1))
 apply simp
 done
+*)
+sorry
 
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"