--- a/Quot/Nominal/Terms.thy	Wed Feb 24 15:36:07 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 15:39:17 2010 +0100
@@ -158,18 +158,14 @@
 is
   "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
 
-lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
-
-instance
-apply default
-apply(induct_tac [!] x rule: trm1_bp_inducts(1))
-apply(simp_all)
-done
+instance by default 
+  (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted])
 
 end
 
 lemmas
-    fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
+    permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
+and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
@@ -181,7 +177,7 @@
   "{} supports BUnit"
   "(supp (atom x)) supports (BVr x)"
   "(supp a \<union> supp b) supports (BPr a b)"
-apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh)
+apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1)
 apply(rule_tac [!] allI)+
 apply(rule_tac [!] impI)
 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
@@ -223,14 +219,14 @@
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
 apply(simp add: supp_Abs fv_trm1)
-apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
+apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
 apply(simp add: alpha1_INJ)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen.simps)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
 apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
-apply(simp (no_asm) add: supp_def)
+apply(simp (no_asm) add: supp_def permute_trm1)
 apply(simp add: alpha1_INJ alpha_bp_eq)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
@@ -579,35 +575,16 @@
 is
   "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
 
-lemma trm5_lts_zero:
-  "0 \<bullet> (x\<Colon>trm5) = x"
-  "0 \<bullet> (y\<Colon>lts) = y"
-  apply(induct x and y rule: trm5_lts_inducts)
-  apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
-  done
-
-lemma trm5_lts_plus:
-  "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
-  "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
-  apply(induct x and y rule: trm5_lts_inducts)
-  apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
-  done
-
-instance
-  apply default
-  apply (simp_all add: trm5_lts_zero trm5_lts_plus)
-  done
+instance by default
+  (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])
 
 end
 
-lemmas 
-  permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
-and
-  alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-and
-  bv5[simp] = rbv5.simps[quot_lifted]
-and
-  fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
+lemmas
+    permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
+and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+and bv5[simp] = rbv5.simps[quot_lifted]
+and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"