--- a/Nominal/Fv.thy	Thu Mar 11 16:16:15 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 16:50:44 2010 +0100
@@ -706,4 +706,36 @@
 end
 *}
 
+lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
+by auto
+
+ML {*
+fun supports_tac perm =
+  simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
+    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
+    asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
+      swap_fresh_fresh fresh_atom swap_at_base_simps(3)}))
+*}
+
+ML {*
+fun mk_supports_eq cnstr =
+let
+  val (tys, ty) = (strip_type o fastype_of) cnstr
+  val names = Datatype_Prop.make_tnames tys
+  val frees = map Free (names ~~ tys)
+  val rhs = list_comb (cnstr, frees)
+  fun mk_supp ty x =
+    Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
+  fun mk_supp_arg (x, ty) =
+    if is_atom @{theory} ty then mk_supp @{typ atom} (mk_atom ty $ x) else
+    if is_atom_set @{theory} ty then mk_supp @{typ "atom set"} (mk_atoms x)
+    else mk_supp ty x
+  val lhss = map mk_supp_arg (frees ~~ tys)
+  val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
+  val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
+in
+  (names, eq)
 end
+*}
+
+end