--- a/Nominal/Term5.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -43,6 +43,7 @@
 lemma fv_rtrm5_rlts_eqvt[eqvt]:
   "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
   "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
+  "pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)"
   apply (induct x and l)
   apply (simp_all add: eqvts atom_eqvt)
   done
@@ -57,8 +58,6 @@
 lemma alpha5_reflp:
 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"
 apply (rule rtrm5_rlts.induct)
-thm rtrm5_rlts.induct
- alpha_rtrm5_alpha_rlts_alpha_rbv5.induct
 apply (simp_all add: alpha5_inj)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
@@ -69,8 +68,6 @@
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)"
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct
-thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
 apply (simp_all add: alpha5_inj)
 sorry
 
@@ -95,6 +92,7 @@
  |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
  |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5}))
  |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
  |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
 *}
@@ -102,14 +100,14 @@
 
 lemma alpha5_rfv:
   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
-  "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m))"
-  "(alpha_rbv5 a b c \<Longrightarrow> True)"
+  "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))"
+  "(alpha_rbv5 0 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"
   apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
-  apply(simp_all)
+  apply(simp_all add: eqvts)
   apply(simp add: alpha_gen)
   apply(clarify)
-  apply(simp_all)
-  sorry (* works for non-rec *)
+  apply(simp)
+  sorry
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
@@ -121,6 +119,7 @@
 
 lemma [quot_respect]:
   "(alpha_rlts ===> op =) fv_rlts fv_rlts"
+  "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5"
   "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
   "(alpha_rlts ===> op =) rbv5 rbv5"
   "(op = ===> alpha_rtrm5) rVr5 rVr5"
@@ -173,12 +172,14 @@
 
 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
 lemmas bv5[simp] = rbv5.simps[quot_lifted]
-lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
+lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted]
+lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted]
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (simp add: alpha5_INJ)
+thm alpha5_INJ
+apply (simp only: alpha5_INJ)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)