--- a/Quot/Nominal/Terms.thy	Wed Feb 17 17:51:35 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 08:37:45 2010 +0100
@@ -25,7 +25,7 @@
 where
   "bv1 (BUnit) = {}"
 | "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
+| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
 local_setup {* define_raw_fv "Terms.rtrm1"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
@@ -58,7 +58,7 @@
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
-apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
+apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts)
 done
 
 lemma fv_rtrm1_eqvt[eqvt]:

--- a/Quot/Nominal/Terms2.thy	Wed Feb 17 17:51:35 2010 +0100
+++ b/Quot/Nominal/Terms2.thy	Thu Feb 18 08:37:45 2010 +0100
@@ -25,7 +25,7 @@
 where
   "bv1 (BUnit) = {}"
 | "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
+| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
 local_setup {* define_raw_fv "Terms.rtrm1"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
@@ -58,7 +58,7 @@
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
-apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
+apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts)
 done
 
 lemma fv_rtrm1_eqvt[eqvt]:
@@ -225,6 +225,11 @@
 apply(simp add: supp_Pair supp_atom bp_supp)
 done
 
+lemma fv_eq_bv: "fv_bp bp = bv1 bp"
+apply(induct bp rule: trm1_bp_inducts(2))
+apply(simp_all)
+done
+
 lemma supp_fv:
   shows "supp t = fv_trm1 t"
 apply(induct t rule: trm1_bp_inducts(1))
@@ -240,23 +245,22 @@
 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(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 add: alpha1_INJ)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq)
-done*)
-sorry
+done
 
 lemma trm1_supp:
   "supp (Vr1 x) = {atom x}"
   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
   "supp (Lm1 x t) = (supp t) - {atom x}"
   "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
-sorry (*  by (simp_all only: supp_fv fv_trm1)
+by (simp_all add: supp_fv fv_trm1 fv_eq_bv)
 
 lemma trm1_induct_strong:
   assumes "\<And>name b. P b (Vr1 name)"
@@ -264,7 +268,7 @@
   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
   and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
   shows   "P a rtrma"
-sorry *)
+sorry
 
 section {*** lets with single assignments ***}
 
@@ -891,11 +895,6 @@
 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
 
-lemma bvfv7: "rbv7 x = fv_rtrm7 x"
-  apply induct
-  apply simp_all
-sorry (*done*)
-
 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
   apply simp
   apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
@@ -960,7 +959,10 @@
   apply simp apply clarify
   apply (erule alpha8f_alpha8b.inducts(1))
   apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
-sorry (*done*)
+  apply clarify
+  apply (erule alpha8f_alpha8b.inducts(2))
+  apply (simp_all)
+done