--- a/Nominal-General/nominal_library.ML	Sun Aug 29 00:36:47 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sun Aug 29 01:17:36 2010 +0800
@@ -37,6 +37,11 @@
   val mk_supports_ty: typ -> term -> term -> term
   val mk_supports: term -> term -> term
 
+  val finite_const: typ -> term
+  val mk_finite_ty: typ -> term -> term
+  val mk_finite: term -> term
+
+
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 
@@ -117,14 +122,19 @@
 
 
 fun supp_ty ty = ty --> @{typ "atom set"};
-fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty)
+fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
 fun mk_supp_ty ty t = supp_const ty $ t;
 fun mk_supp t = mk_supp_ty (fastype_of t) t;
 
-fun supports_const ty = Const (@{const_name "supports"}, [@{typ "atom set"}, ty] ---> @{typ bool});
+fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool});
 fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2;
 fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2;
 
+fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool})
+fun mk_finite_ty ty t = finite_const ty $ t
+fun mk_finite t = mk_finite_ty (fastype_of t) t
+
+
 fun mk_equiv r = r RS @{thm eq_reflection};
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 

--- a/Nominal/Ex/SingleLet.thy	Sun Aug 29 00:36:47 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 29 01:17:36 2010 +0800
@@ -33,42 +33,16 @@
 thm single_let.fv_bn_eqvt
 thm single_let.size_eqvt
 thm single_let.supports
+thm single_let.fsupp
 
-lemma test:
-  "finite (supp (t::trm)) \<and> finite (supp (a::assg))"
-apply(rule single_let.induct)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-done
+
 
 instantiation trm and assg :: fs
 begin
 
 instance
 apply(default)
-apply(simp_all add: test)
+apply(simp_all add: single_let.fsupp)
 done
 
 end

--- a/Nominal/Ex/TypeSchemes.thy	Sun Aug 29 00:36:47 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy	Sun Aug 29 01:17:36 2010 +0800
@@ -19,6 +19,15 @@
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
+instantiation ty2 :: fs
+begin
+
+instance 
+sorry
+
+end
+
+
 nominal_datatype tys2 =
   All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
 

--- a/Nominal/NewParser.thy	Sun Aug 29 00:36:47 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 29 01:17:36 2010 +0800
@@ -547,6 +547,11 @@
     then prove_supports lthyB qperm_simps qtrms
     else raise TEST lthyB
 
+  val qfsupp_thms =
+    if get_STEPS lthy > 29
+    then prove_fsupp lthyB qtys qinduct qsupports_thms
+    else raise TEST lthyB
+
 
   (* noting the theorems *)  
 
@@ -566,7 +571,7 @@
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
-     
+     ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)

--- 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 *)