# HG changeset patch
# User berghofe
# Date 1130940322 -3600
# Node ID d1e47ee130705e63734655104e73ba53e4e31676
# Parent  16608ab6ed84c26e21535e3834d0842542eb1a6c
Added code for proving that new datatype has finite support.

diff -r 16608ab6ed84 -r d1e47ee13070 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Nov 02 14:48:55 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Nov 02 15:05:22 2005 +0100
@@ -1895,6 +1895,29 @@
 
     val case_names_induct = mk_case_names_induct (List.concat descr');
 
+    (**** prove that new datatypes have finite support ****)
+
+    val indnames = DatatypeProp.make_tnames recTs;
+
+    val abs_supp = PureThy.get_thms thy8 (Name "abs_supp");
+    val supp_at = PureThy.get_thms thy8 (Name "supp_at");
+
+    val finite_supp_thms = map (fn atom =>
+      let val atomT = Type (atom, [])
+      in map standard (List.take
+        (split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop
+           (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem
+             (Const ("nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
+              Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT))))
+               (indnames ~~ recTs))))
+           (fn _ => indtac dt_induct indnames 1 THEN
+            ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
+              (abs_supp @ supp_at @
+               PureThy.get_thms thy8 (Name ("fs_" ^ Sign.base_name atom ^ "1")) @
+               List.concat supp_thms))))),
+         length new_type_names))
+      end) atoms;
+
     val (thy9, _) = thy8 |>
       Theory.add_path big_name |>
       PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
@@ -1904,7 +1927,14 @@
       DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
       DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
       DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
-      DatatypeAux.store_thmss "fresh" new_type_names fresh_thms;
+      DatatypeAux.store_thmss "fresh" new_type_names fresh_thms |>>
+      fold (fn (atom, ths) => fn thy =>
+        let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
+        in fold (fn T => AxClass.add_inst_arity_i
+            (fst (dest_Type T),
+              replicate (length sorts) [class], [class])
+            (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
+        end) (atoms ~~ finite_supp_thms);
 
   in
     (thy9, perm_eq_thms)