diff -r b355cab42841 -r 4029105011ca Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 11 16:50:44 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 17:47:29 2010 +0100
@@ -119,7 +119,7 @@
     fold (fn a => fn b =>
       if a = @{term True} then b else
       if b = @{term True} then a else
-      HOLogic.mk_conj (a, b)) props @{term True};
+      HOLogic.mk_conj (a, b)) (rev props) @{term True};
   fun mk_diff a b =
     if b = noatoms then a else
     if b = a then noatoms else
@@ -718,17 +718,21 @@
 *}
 
 ML {*
-fun mk_supports_eq cnstr =
+fun mk_supp ty x =
+  Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
+*}
+
+ML {*
+fun mk_supports_eq thy 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)
+    if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
+    if is_atom_set thy 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})
@@ -738,4 +742,40 @@
 end
 *}
 
+ML {*
+fun prove_supports ctxt perms cnst =
+let
+  val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
+in
+  Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
 end
+*}
+
+ML {*
+fun mk_fs tys =
+let
+  val names = Datatype_Prop.make_tnames tys
+  val frees = map Free (names ~~ tys)
+  val supps = map2 mk_supp tys frees
+  val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps
+in
+  (names, HOLogic.mk_Trueprop (mk_conjl fin_supps))
+end
+*}
+
+ML {*
+fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
+  rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom finite_insert finite.emptyI finite_Un})
+*}
+
+ML {*
+fun prove_fs ctxt induct supports tys =
+let
+  val (names, eq) = mk_fs tys
+in
+  Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)
+end
+*}
+
+end