--- a/Nominal/nominal_dt_supp.ML	Sun Aug 29 00:36:47 2010 +0800
+++ b/Nominal/nominal_dt_supp.ML	Sun Aug 29 01:17:36 2010 +0800
@@ -8,14 +8,14 @@
 signature NOMINAL_DT_SUPP =
 sig
   val prove_supports: Proof.context -> thm list -> term list -> thm list  
-
+  val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
 struct
 
 
-(* supports lemmas *)
+(* supports lemmas for constructors *)
 
 fun mk_supports_goal ctxt qtrm =
 let  
@@ -52,7 +52,28 @@
   map (prove_supports_single ctxt perm_simps) qtrms
 
 
+(* finite supp lemmas for qtypes *)
 
+fun prove_fsupp ctxt qtys qinduct qsupports_thms =
+let
+  val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt
+  val goals = vs ~~ qtys
+    |> map Free
+    |> map (mk_finite o mk_supp)
+    |> foldr1 (HOLogic.mk_conj)
+    |> HOLogic.mk_Trueprop
+
+  val tac = 
+    EVERY' [ rtac @{thm supports_finite},
+             resolve_tac qsupports_thms,
+             asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ]
+in
+  Goal.prove ctxt' [] [] goals
+    (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
+  |> singleton (ProofContext.export ctxt' ctxt)
+  |> Datatype_Aux.split_conj_thm
+  |> map zero_var_indexes
+end
 
 end (* structure *)