--- a/Nominal/Fv.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -385,6 +385,7 @@
   val nr_bns = non_rec_binds bindsall;
   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 fvbns = map snd bn_fv_bns;
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
@@ -548,9 +549,11 @@
      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names)
      (alpha_types @ alpha_bn_types)) []
      (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
+  val ordered_fvs = fv_frees @ fvbns;
+  val exported_fvs = map (Morphism.term (ProofContext.export_morphism lthy''' lthy)) ordered_fvs;
   val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
 in
-  ((all_fvs, alphas), lthy''')
+  (((all_fvs, ordered_fvs), alphas), lthy''')
 end
 *}
 
@@ -920,4 +923,76 @@
 end
 *}
 
+ML {*
+fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;
+
+fun mk_supp_neq arg (fv, alpha) =
+let
+  val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
+  val ty = fastype_of arg;
+  val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
+  val finite = @{term "finite :: atom set \<Rightarrow> bool"}
+  val rhs = collect $ Abs ("a", @{typ atom},
+    HOLogic.mk_not (finite $
+      (collect $ Abs ("b", @{typ atom},
+        HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))
+in
+  HOLogic.mk_eq (fv $ arg, rhs)
+end;
+
+fun supp_eq fv_alphas_lst =
+let
+  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (fv_ts, _) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) fv_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val args = map Free (names ~~ tys);
+  fun supp_eq_arg ((fv, arg), l) =
+    mk_conjl
+      ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::
+       (map (mk_supp_neq arg) l))
+  val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))
+in
+  (names, HOLogic.mk_Trueprop eqs)
 end
+*}
+
+ML {*
+fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =
+if length fv_ts_bn < length alpha_ts_bn then
+  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])
+else let
+  val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);
+  fun filter_fn i (x, j) = if j = i then SOME x else NONE;
+  val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;
+  val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;
+in
+  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all
+end
+*}
+
+lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+  apply (simp add: supp_Abs supp_Pair)
+  apply blast
+  done
+
+ML {*
+fun supp_eq_tac ind fv perm eqiff ctxt =
+  ind_tac ind THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
+*}
+
+end