diff -r 2a878d7d631f -r ab8ed83d0188 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 24 17:42:52 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 18:38:49 2010 +0100
@@ -65,14 +65,14 @@
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
-  apply (simp_all add: atom_eqvt eqvts)
+  apply (simp_all add: eqvts atom_eqvt)
   done
 
 lemma fv_rtrm1_eqvt[eqvt]:
     "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
     "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
   apply (induct t and b)
-  apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
+  apply (simp_all add: eqvts atom_eqvt)
   done
 
 lemma alpha1_eqvt:
@@ -80,40 +80,12 @@
   "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"
   apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)
   apply (simp_all add:eqvts alpha1_inj)
-  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 Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
-  apply (erule exE)
-  apply (erule exE)
-  apply (rule conjI)
-  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: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
-  apply (rule_tac x="pi \<bullet> piaa" 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: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
+  apply (tactic {* 
+    ALLGOALS (
+      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})
+    ) *})
+  apply (simp_all only: eqvts atom_eqvt)
   done
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
@@ -453,45 +425,30 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}
 thm alpha5_inj
 
-lemma rbv5_eqvt:
+lemma rbv5_eqvt[eqvt]:
   "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
-sorry
+  apply (induct x)
+  apply (simp_all add: eqvts atom_eqvt)
+  done
 
-lemma fv_rtrm5_eqvt:
+lemma fv_rtrm5_rlts_eqvt[eqvt]:
   "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
-sorry
-
-lemma fv_rlts_eqvt:
-  "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)"
-sorry
+  "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
+  apply (induct x and l)
+  apply (simp_all add: eqvts atom_eqvt)
+  done
 
 lemma alpha5_eqvt:
   "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
   "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
-  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
+  apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)
   apply (simp_all add: alpha5_inj)
-  apply (erule exE)+
-  apply(unfold alpha_gen)
-  apply (erule conjE)+
-  apply (rule conjI)
-  apply (rule_tac x="x \<bullet> pi" in exI)
-  apply (rule conjI)
-  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
-  apply (subst permute_eqvt[symmetric])
-  apply (simp)
-  apply (rule_tac x="x \<bullet> pia" in exI)
-  apply (rule conjI)
-  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
-  apply (subst permute_eqvt[symmetric])
-  apply (simp)
+  apply (tactic {* 
+    ALLGOALS (
+      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})
+    ) *})
+  apply (simp_all only: eqvts atom_eqvt)
   done
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),