Adapted to changes in Finite_Set theory.

--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Feb 07 17:51:38 2007 +0100
@@ -16,7 +16,7 @@
 structure NominalAtoms : NOMINAL_ATOMS =
 struct
 
-val Finites_emptyI = thm "Finites.emptyI";
+val finite_emptyI = thm "finite.emptyI";
 val Collect_const = thm "Collect_const";
 
 
@@ -67,8 +67,8 @@
       let 
     val name = ak_name ^ "_infinite"
         val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not
-                    (HOLogic.mk_mem (HOLogic.mk_UNIV T,
-                     Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))
+                    (Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT) $
+                       HOLogic.mk_UNIV T))
       in
         ((name, axiom), []) 
       end) ak_names_types) thy1;
@@ -252,9 +252,9 @@
           val ty = TFree("'a",["HOL.type"]);
           val x   = Free ("x", ty);
           val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
-          val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
+          val cfinite  = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT)
           
-          val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
+          val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
 
        in  
         AxClass.define_class_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
@@ -481,7 +481,7 @@
                              rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
                 else
                   let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
-                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites_emptyI];
+                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
                   in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
         in
          AxClass.prove_arity (qu_name,[],[qu_class]) proof thy'
@@ -618,7 +618,7 @@
 	     let
 	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
 	       val supp_def = thm "Nominal.supp_def";
-               val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites_emptyI,defn];
+               val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
              in 
 	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy

--- a/src/HOL/Nominal/nominal_package.ML	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Feb 07 17:51:38 2007 +0100
@@ -18,7 +18,7 @@
 structure NominalPackage : NOMINAL_PACKAGE =
 struct
 
-val Finites_emptyI = thm "Finites.emptyI";
+val finite_emptyI = thm "finite.emptyI";
 val finite_Diff = thm "finite_Diff";
 val finite_Un = thm "finite_Un";
 val Un_iff = thm "Un_iff";
@@ -1016,7 +1016,7 @@
             (fn _ =>
               simp_tac (HOL_basic_ss addsimps (supp_def ::
                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
-                 symmetric empty_def :: Finites_emptyI :: simp_thms @
+                 symmetric empty_def :: finite_emptyI :: simp_thms @
                  abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
         in
           (supp_thm,
@@ -1091,9 +1091,9 @@
       let val atomT = Type (atom, [])
       in map standard (List.take
         (split_conj_thm (Goal.prove_global 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))))
+           (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
+             Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
+               (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
                (indnames ~~ recTs))))
            (fn _ => indtac dt_induct indnames 1 THEN
             ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
@@ -1202,8 +1202,8 @@
 
     val ind_prems' =
       map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
-        HOLogic.mk_Trueprop (HOLogic.mk_mem (f $ Free ("x", fsT'),
-          Const ("Finite_Set.Finites", HOLogic.mk_setT (body_type T)))))) fresh_fs @
+        HOLogic.mk_Trueprop (Const ("Finite_Set.finite", body_type T -->
+          HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
       List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
         map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
           HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
@@ -1480,8 +1480,8 @@
           HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
         val prems5 = mk_fresh3 (recs ~~ frees'') frees';
         val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
-          (HOLogic.mk_mem (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y,
-             Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT)))))
+          (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
+             (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
                frees'') atomTs;
         val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
           (Const ("Nominal.fresh", T --> fsT' --> HOLogic.boolT) $
@@ -1563,9 +1563,9 @@
         val name = Sign.base_name (fst (dest_Type aT));
         val fs_name = PureThy.get_thm thy11 (Name ("fs_" ^ name ^ "1"));
         val aset = HOLogic.mk_setT aT;
-        val finites = Const ("Finite_Set.Finites", HOLogic.mk_setT aset);
-        val fins = map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem
-          (Const ("Nominal.supp", T --> aset) $ f, finites)))
+        val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
+        val fins = map (fn (f, T) => HOLogic.mk_Trueprop
+          (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
             (rec_fns ~~ rec_fn_Ts)
       in
         map (fn th => standard (th RS mp)) (split_conj_thm
@@ -1577,7 +1577,7 @@
                    val y = Free ("y" ^ string_of_int i, U)
                  in
                    HOLogic.mk_imp (R $ x $ y,
-                     HOLogic.mk_mem (Const ("Nominal.supp", U --> aset) $ y, finites))
+                     finite $ (Const ("Nominal.supp", U --> aset) $ y))
                  end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs)))))
             (fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
                (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
@@ -1597,9 +1597,9 @@
       end;
 
     val finite_premss = map (fn aT =>
-      map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem
-        (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f,
-         Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT)))))
+      map (fn (f, T) => HOLogic.mk_Trueprop
+        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
+           (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
            (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
 
     val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
@@ -1715,9 +1715,9 @@
       in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
 
     val finite_ctxt_prems = map (fn aT =>
-      HOLogic.mk_Trueprop (HOLogic.mk_mem
-        (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt,
-         Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT))))) dt_atomTs;
+      HOLogic.mk_Trueprop
+        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
+           (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
 
     val rec_unique_thms = split_conj_thm (Goal.prove
       (ProofContext.init thy11) (map fst rec_unique_frees)

--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Feb 07 17:51:38 2007 +0100
@@ -48,7 +48,7 @@
 structure NominalPermeq : NOMINAL_PERMEQ =
 struct
 
-val Finites_emptyI = thm "Finites.emptyI";
+val finite_emptyI = thm "finite.emptyI";
 val finite_Un = thm "finite_Un";
 
 (* pulls out dynamically a thm via the proof state *)
@@ -264,8 +264,7 @@
     let val goal = List.nth(cprems_of st, i-1)
     in
       case Logic.strip_assums_concl (term_of goal) of
-          _ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $
-            Const ("Finite_Set.Finites", _)) =>
+          _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
           let
             val cert = Thm.cterm_of (sign_of_thm st);
             val ps = Logic.strip_params (term_of goal);
@@ -281,7 +280,7 @@
               Logic.strip_assums_concl (hd (prems_of supports_rule'));
             val supports_rule'' = Drule.cterm_instantiate
               [(cert (head_of S), cert s')] supports_rule'
-            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites_emptyI]
+            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, finite_emptyI]
           in
             (tactical ("guessing of the right supports-set",
                       EVERY [compose_tac (false, supports_rule'', 2) i,
@@ -319,7 +318,7 @@
             val supports_fresh_rule'' = Drule.cterm_instantiate
               [(cert (head_of S), cert s')] supports_fresh_rule'
 	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
-            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites_emptyI]
+            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI]
             (* FIXME sometimes these rewrite rules are already in the ss, *)
             (* which produces a warning                                   *)
           in

--- a/src/HOL/NumberTheory/BijectionRel.thy	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/NumberTheory/BijectionRel.thy	Wed Feb 07 17:51:38 2007 +0100
@@ -71,7 +71,7 @@
       "!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
   shows "P F"
   using major subs
-  apply (induct set: Finites)
+  apply (induct set: finite)
    apply (blast intro: cases)+
   done
 

--- a/src/HOL/NumberTheory/Euler.thy	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/NumberTheory/Euler.thy	Wed Feb 07 17:51:38 2007 +0100
@@ -118,7 +118,7 @@
 
 lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
     \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
-  by (induct set: Finites) auto
+  by (induct set: finite) auto
 
 lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> 
                   int(card(SetS a p)) = (p - 1) div 2"

--- a/src/HOL/NumberTheory/EvenOdd.thy	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/NumberTheory/EvenOdd.thy	Wed Feb 07 17:51:38 2007 +0100
@@ -242,7 +242,7 @@
 
 lemma neg_one_special: "finite A ==>
     ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
-  by (induct set: Finites) auto
+  by (induct set: finite) auto
 
 lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
   by (induct n) auto

--- a/src/HOL/NumberTheory/Finite2.thy	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy	Wed Feb 07 17:51:38 2007 +0100
@@ -38,19 +38,19 @@
 qed
 
 lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
-  apply (induct set: Finites)
+  apply (induct set: finite)
   apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
   done
 
 lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
     int(c) * int(card X)"
-  apply (induct set: Finites)
+  apply (induct set: finite)
   apply (auto simp add: zadd_zmult_distrib2)
   done
 
 lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
     c * setsum f A"
-  by (induct set: Finites) (auto simp add: zadd_zmult_distrib2)
+  by (induct set: finite) (auto simp add: zadd_zmult_distrib2)
 
 
 subsection {* Cardinality of explicit finite sets *}

--- a/src/HOL/NumberTheory/Gauss.thy	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy	Wed Feb 07 17:51:38 2007 +0100
@@ -444,7 +444,7 @@
                                "setprod uminus E"], auto)
     done
   also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
-    using finite_E by (induct set: Finites) auto
+    using finite_E by (induct set: finite) auto
   then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
     by (simp add: zmult_commute)
   with two show ?thesis
@@ -484,7 +484,7 @@
     by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
   moreover have "setprod (%x. x * a) A =
     setprod (%x. a) A * setprod id A"
-    using finite_A by (induct set: Finites) auto
+    using finite_A by (induct set: finite) auto
   ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
     setprod id A))] (mod p)"
     by simp

--- a/src/HOL/NumberTheory/Int2.thy	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/NumberTheory/Int2.thy	Wed Feb 07 17:51:38 2007 +0100
@@ -175,7 +175,7 @@
 
 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
     ==> zgcd (setprod id A,y) = 1"
-  by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult)
+  by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
 
 
 subsection {* Some properties of MultInv *}

--- a/src/HOL/Real/ferrante_rackoff_proof.ML	Wed Feb 07 17:46:03 2007 +0100
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Wed Feb 07 17:51:38 2007 +0100
@@ -47,7 +47,7 @@
         fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
         val ss = simpset_of sg
         fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
-        val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
+        val uf = prove_bysimp sg ss (Const ("Finite_Set.finite", rsT --> HOLogic.boolT) $ hU)
     in (U,cterm_of sg hU,map proveinU U,uf)
     end;