--- a/Quot/Nominal/Terms.thy	Tue Feb 02 16:51:00 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 02 17:10:42 2010 +0100
@@ -104,6 +104,14 @@
   shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
   sorry
 
+(* Shouyld we derive it? But bv is given by the user? *)
+lemma bv1_eqvt[eqvt]:
+  shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
+  apply (induct x)
+apply (simp_all add: eqvts)
+apply (rule atom_eqvt)
+done
+
 lemma alpha1_eqvt:
   shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
   sorry
@@ -252,13 +260,41 @@
 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen])
 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)
+sorry
+
+
 lemma supp_fv:
   shows "supp t = fv_trm1 t"
 apply(induct t rule: trm1_bp_inducts(1))
-apply(simp_all add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp_all only: supp_at_base[simplified supp_def])
-apply(simp_all add: Collect_imp_eq Collect_neg_eq)
-sorry (* Lam & Let still to do *)
+apply(simp_all)
+apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
+apply(simp only: supp_at_base[simplified supp_def])
+apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
+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 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)
+apply(simp (no_asm) add: supp_def)
+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] bv1_eqvt)
+apply(simp add: Collect_imp_eq Collect_neg_eq)
+done