# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265190624 -3600
# Node ID dce45db1606340f9cce269ededd4b4a5c2d1771e
# Parent  135bf399c036aca00ff34c492cebf8cc95fbd763
Some cleaning and eqvt proof

diff -r 135bf399c036 -r dce45db16063 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 09:25:21 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 10:50:24 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