--- a/Nominal/Fv.thy	Tue Mar 16 18:19:00 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 16 20:07:13 2010 +0100
@@ -154,16 +154,6 @@
 end
 *}
 
-ML {*
-fun all_binds l =
-let
-  fun is_non_rec (SOME (f, _), _, _) = SOME f
-    | is_non_rec _ = NONE
-in
-  distinct (op =) (map_filter is_non_rec (flat (flat l)))
-end
-*}
-
 (* We assume no bindings in the type on which bn is defined *)
 ML {*
 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =
@@ -266,9 +256,8 @@
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
-  val all_bns = all_binds bindsall;
   val nr_bns = non_rec_binds bindsall;
-  val rel_bns = filter (fn (bn, _, _) => bn mem all_bns) bns;
+  val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
   val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
@@ -307,21 +296,15 @@
             @{term "{} :: atom set"}
         | fv_bind args (SOME (f, _), i, _) = f $ (nth args i);
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
+      fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE
+        | find_nonrec_binder _ _ = NONE
       fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE
         | find_compound_binder _ _ = NONE
       fun fv_arg ((dt, x), arg_no) =
-        case get_first (find_compound_binder arg_no) bindcs of
-          SOME (f, is_rec) =>
+        case get_first (find_nonrec_binder arg_no) bindcs of
+          SOME f =>
             (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of
-                SOME fv_bn =>
-                  if is_rec then
-                    let
-                      val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
-                      val sub = fv_binds args relevant
-                    in
-                      mk_diff (fv_bn $ x) sub
-                    end
-                  else fv_bn $ x
+                SOME fv_bn => fv_bn $ x
               | NONE => error "bn specified in a non-rec binding but not in bn list")
         | NONE =>
             let

--- a/Nominal/Parser.thy	Tue Mar 16 18:19:00 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 16 20:07:13 2010 +0100
@@ -337,14 +337,22 @@
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
+  val _ = tracing "3";
   val fv_eqvt_tac =
     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
     else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
+  val _ = tracing "4";
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5;
-  val (fv_bn_eqvts, lthy6a) = fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
+  val _ = tracing "4a";
+  val (fv_bn_eqvts, lthy6a) = 
+    if fv_ts_loc_bn = [] then ([], lthy6) else
+    fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) 
+      (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
+  val _ = tracing "4b";
   val lthy6 = lthy6a;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
+  val _ = tracing "5";
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1

--- a/Nominal/Term5.thy	Tue Mar 16 18:19:00 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 20:07:13 2010 +0100
@@ -43,7 +43,6 @@
 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
@@ -134,7 +133,6 @@
  |> 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})))
 *}
@@ -142,14 +140,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 \<and> fv_rbv5 l = fv_rbv5 m))"
-  "(alpha_rbv5 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"
+  "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
+  "(alpha_rbv5 b c \<Longrightarrow> True)"
   apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
   apply(simp_all add: eqvts)
   apply(simp add: alpha_gen)
   apply(clarify)
   apply(simp)
-  sorry
+done
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
@@ -159,9 +157,38 @@
   apply simp
   done
 
+local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
+print_theorems
+
+
+lemma alpha_rbv_rsp_pre:
+  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z"
+  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply (case_tac [!] z)
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply auto
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
+
+lemma alpha_rbv_rsp_pre2:
+  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y"
+  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply (case_tac [!] z)
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply auto
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
+
 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"
@@ -176,15 +203,9 @@
   apply (rule_tac x="0" in exI)
   apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   apply clarify
-  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply simp_all
-  apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply simp_all
-  defer defer (* Both sides false, so equal when we have distinct *)
-  apply (erule conjE)+
-  apply clarify
-  apply (simp add: alpha5_inj)
-  sorry (* may be true? *)
+  apply (simp add: alpha_rbv_rsp_pre2)
+  apply (simp add: alpha_rbv_rsp_pre)
+done
 
 lemma
   shows "(alpha_rlts ===> op =) rbv5 rbv5"
@@ -212,9 +233,9 @@
 
 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
 lemmas bv5[simp] = rbv5.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 fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas alpha5_DIS = alpha_dis[quot_lifted]
 
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
@@ -235,7 +256,6 @@
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
-apply (metis flip_at_simps(1) supp_at_base supp_eqvt)
 done
 
 lemma lets_ok3:
@@ -252,27 +272,15 @@
    (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (simp add: alpha5_INJ alpha_gen)
 apply (simp add: permute_trm5_lts eqvts)
-apply (simp add: alpha5_INJ(5))
-apply (simp add: alpha5_INJ(1))
+apply (simp add: alpha5_INJ)
 done
 
-lemma distinct_helper:
-  shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
-  apply auto
-  apply (erule alpha_rtrm5.cases)
-  apply (simp_all only: rtrm5.distinct)
-  done
-
-lemma distinct_helper2:
-  shows "(Vr5 x) \<noteq> (Ap5 y z)"
-  by (lifting distinct_helper)
-
 lemma lets_nok:
   "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
    (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
    (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
-apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts)
+apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts)
 done
 
 end

--- a/Nominal/Term5n.thy	Tue Mar 16 18:19:00 2010 +0100
+++ b/Nominal/Term5n.thy	Tue Mar 16 20:07:13 2010 +0100
@@ -169,7 +169,6 @@
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
-apply (metis flip_at_simps(1) supp_at_base supp_eqvt)
 done
 
 lemma lets_ok3:
@@ -186,7 +185,6 @@
 apply (simp add: alpha5_INJ alpha_gen)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)
-apply auto
 done
 
 lemma distinct_helper: