--- a/Nominal/Test.thy	Wed Mar 17 12:18:35 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 12:23:04 2010 +0100
@@ -107,6 +107,44 @@
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
+lemma supports_lam_bp:
+  "(supp (atom a)) supports (VAR a)"
+  "(supp t \<union> supp s) supports (APP t s)"
+  "(supp (atom a) \<union> supp t) supports (LAM a t)"
+  "(supp b \<union> supp t) supports (LET b t)"
+  "(supp (atom a) \<union> supp t) supports (BP a t)"
+apply -
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
+done
+
+lemma finite_supp_lam_bp:
+  fixes lam::"lam" 
+  and   bp::"bp"
+  shows "finite (supp lam)"
+  and   "finite (supp bp)"
+apply(induct lam and bp rule: lam_bp_inducts)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp add: supp_atom)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp add: supp_atom)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp)
+apply(rule supports_finite)
+apply(rule supports_lam_bp)
+apply(simp add: supp_atom)
+done
+
+
 ML {* val _ = recursive := true *}
 
 nominal_datatype lam' =
@@ -334,6 +372,23 @@
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
 
+lemma supports_subset:
+  fixes S1 S2 :: "atom set"
+  assumes  a: "S1 supports x"
+  and      b: "S1 \<subseteq> S2"
+  shows "S2 supports x"
+  using a b
+  by (auto simp add: supports_def)
+
+lemma finite_fv_t_tyS:
+  fixes T::"t"
+  and   S::"tyS"
+  shows "finite (fv_t T)" 
+  and   "finite (fv_tyS S)"
+apply(induct T and S rule: t_tyS_inducts)
+apply(simp_all add: t_tyS_fv)
+done
+
 lemma supp_fv_t_tyS:
   shows "supp T = fv_t T" 
   and   "supp S = fv_tyS S"
@@ -364,9 +419,11 @@
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
-oops
-(*apply(simp only: supp_Abs)
-done*)
+apply(rule trans)
+apply(rule finite_supp_Abs)
+apply(simp add: finite_fv_t_tyS)
+apply(simp)
+done
 
 (* example 1 from Terms.thy *)