--- a/Nominal/Terms.thy	Thu Feb 25 07:48:33 2010 +0100
+++ b/Nominal/Terms.thy	Thu Feb 25 07:48:57 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}, []),
@@ -150,18 +122,8 @@
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
 
-instantiation trm1 and bp :: pt
-begin
-
-quotient_definition
-  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
-  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
-
-instance by default 
-  (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted])
-
-end
+setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
+  @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}
 
 lemmas
     permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
@@ -463,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}, []),