--- a/Quot/Nominal/Terms.thy	Wed Feb 24 14:09:34 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 14:37:51 2010 +0100
@@ -173,44 +173,32 @@
 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)
+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"