diff -r 11b8798dea5d -r 4b0563bc4b03 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 24 17:32:22 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 17:32:43 2010 +0100
@@ -158,59 +158,43 @@
 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]
 
-lemma lm1_supp_pre:
-  shows "(supp (atom x, t)) supports (Lm1 x t) "
-apply(simp add: supports_def)
-apply(fold fresh_def)
-apply(simp add: fresh_Pair swap_fresh_fresh)
-apply(clarify)
-apply(subst swap_at_base_simps(3))
+lemma supports:
+  "(supp (atom x)) supports (Vr1 x)"
+  "(supp t \<union> supp s) supports (Ap1 t s)"
+  "(supp (atom x) \<union> supp t) supports (Lm1 x t)"
+  "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
+  "{} 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 permute_trm1)
+apply(rule_tac [!] allI)+
+apply(rule_tac [!] impI)
+apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
 apply(simp_all add: fresh_atom)
 done
 
-lemma lt1_supp_pre:
-  shows "(supp (x, t, s)) supports (Lt1 t x s) "
-apply(simp add: supports_def)
-apply(fold fresh_def)
-apply(simp add: fresh_Pair swap_fresh_fresh)
-done
-
-lemma bp_supp: "finite (supp (bp :: bp))"
-  apply (induct bp)
-  apply(simp_all add: supp_def)
-  apply(simp add: supp_at_base supp_def[symmetric])
-  apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def)
+lemma rtrm1_bp_fs:
+  "finite (supp (x :: trm1))"
+  "finite (supp (b :: bp))"
+  apply (induct x and b rule: trm1_bp_inducts)
+  apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
+  apply(simp_all add: supp_atom)
   done
 
 instance trm1 :: fs
 apply default
-apply(induct_tac x rule: trm1_bp_inducts(1))
-apply(simp_all)
-apply(simp add: supp_def alpha1_INJ eqvts)
-apply(simp add: supp_def[symmetric] supp_at_base)
-apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
-apply(rule supports_finite)
-apply(rule lm1_supp_pre)
-apply(simp add: supp_Pair supp_atom)
-apply(rule supports_finite)
-apply(rule lt1_supp_pre)
-apply(simp add: supp_Pair supp_atom bp_supp)
+apply (rule rtrm1_bp_fs(1))
 done
 
 lemma fv_eq_bv: "fv_bp bp = bv1 bp"
@@ -235,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)
@@ -591,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))"