Adapted to changes in Finite_Set theory.
authorberghofe
Wed Feb 07 17:51:38 2007 +0100 (2007-02-07)
changeset 22274ce1459004c8d
parent 22273 9785397cc344
child 22275 51411098e49b
Adapted to changes in Finite_Set theory.
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/NumberTheory/BijectionRel.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/EvenOdd.thy
src/HOL/NumberTheory/Finite2.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Int2.thy
src/HOL/Real/ferrante_rackoff_proof.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Feb 07 17:46:03 2007 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Feb 07 17:51:38 2007 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  structure NominalAtoms : NOMINAL_ATOMS =
     1.5  struct
     1.6  
     1.7 -val Finites_emptyI = thm "Finites.emptyI";
     1.8 +val finite_emptyI = thm "finite.emptyI";
     1.9  val Collect_const = thm "Collect_const";
    1.10  
    1.11  
    1.12 @@ -67,8 +67,8 @@
    1.13        let 
    1.14      val name = ak_name ^ "_infinite"
    1.15          val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not
    1.16 -                    (HOLogic.mk_mem (HOLogic.mk_UNIV T,
    1.17 -                     Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))
    1.18 +                    (Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT) $
    1.19 +                       HOLogic.mk_UNIV T))
    1.20        in
    1.21          ((name, axiom), []) 
    1.22        end) ak_names_types) thy1;
    1.23 @@ -252,9 +252,9 @@
    1.24            val ty = TFree("'a",["HOL.type"]);
    1.25            val x   = Free ("x", ty);
    1.26            val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
    1.27 -          val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
    1.28 +          val cfinite  = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT)
    1.29            
    1.30 -          val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
    1.31 +          val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
    1.32  
    1.33         in  
    1.34          AxClass.define_class_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    1.35 @@ -481,7 +481,7 @@
    1.36                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
    1.37                  else
    1.38                    let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
    1.39 -                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites_emptyI];
    1.40 +                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
    1.41                    in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
    1.42          in
    1.43           AxClass.prove_arity (qu_name,[],[qu_class]) proof thy'
    1.44 @@ -618,7 +618,7 @@
    1.45  	     let
    1.46  	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
    1.47  	       val supp_def = thm "Nominal.supp_def";
    1.48 -               val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites_emptyI,defn];
    1.49 +               val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
    1.50                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
    1.51               in 
    1.52  	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Feb 07 17:46:03 2007 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Feb 07 17:51:38 2007 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4  structure NominalPackage : NOMINAL_PACKAGE =
     2.5  struct
     2.6  
     2.7 -val Finites_emptyI = thm "Finites.emptyI";
     2.8 +val finite_emptyI = thm "finite.emptyI";
     2.9  val finite_Diff = thm "finite_Diff";
    2.10  val finite_Un = thm "finite_Un";
    2.11  val Un_iff = thm "Un_iff";
    2.12 @@ -1016,7 +1016,7 @@
    2.13              (fn _ =>
    2.14                simp_tac (HOL_basic_ss addsimps (supp_def ::
    2.15                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
    2.16 -                 symmetric empty_def :: Finites_emptyI :: simp_thms @
    2.17 +                 symmetric empty_def :: finite_emptyI :: simp_thms @
    2.18                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
    2.19          in
    2.20            (supp_thm,
    2.21 @@ -1091,9 +1091,9 @@
    2.22        let val atomT = Type (atom, [])
    2.23        in map standard (List.take
    2.24          (split_conj_thm (Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop
    2.25 -           (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem
    2.26 -             (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
    2.27 -              Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT))))
    2.28 +           (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
    2.29 +             Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
    2.30 +               (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
    2.31                 (indnames ~~ recTs))))
    2.32             (fn _ => indtac dt_induct indnames 1 THEN
    2.33              ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
    2.34 @@ -1202,8 +1202,8 @@
    2.35  
    2.36      val ind_prems' =
    2.37        map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
    2.38 -        HOLogic.mk_Trueprop (HOLogic.mk_mem (f $ Free ("x", fsT'),
    2.39 -          Const ("Finite_Set.Finites", HOLogic.mk_setT (body_type T)))))) fresh_fs @
    2.40 +        HOLogic.mk_Trueprop (Const ("Finite_Set.finite", body_type T -->
    2.41 +          HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
    2.42        List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
    2.43          map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
    2.44            HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
    2.45 @@ -1480,8 +1480,8 @@
    2.46            HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
    2.47          val prems5 = mk_fresh3 (recs ~~ frees'') frees';
    2.48          val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
    2.49 -          (HOLogic.mk_mem (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y,
    2.50 -             Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT)))))
    2.51 +          (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
    2.52 +             (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
    2.53                 frees'') atomTs;
    2.54          val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
    2.55            (Const ("Nominal.fresh", T --> fsT' --> HOLogic.boolT) $
    2.56 @@ -1563,9 +1563,9 @@
    2.57          val name = Sign.base_name (fst (dest_Type aT));
    2.58          val fs_name = PureThy.get_thm thy11 (Name ("fs_" ^ name ^ "1"));
    2.59          val aset = HOLogic.mk_setT aT;
    2.60 -        val finites = Const ("Finite_Set.Finites", HOLogic.mk_setT aset);
    2.61 -        val fins = map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem
    2.62 -          (Const ("Nominal.supp", T --> aset) $ f, finites)))
    2.63 +        val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
    2.64 +        val fins = map (fn (f, T) => HOLogic.mk_Trueprop
    2.65 +          (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
    2.66              (rec_fns ~~ rec_fn_Ts)
    2.67        in
    2.68          map (fn th => standard (th RS mp)) (split_conj_thm
    2.69 @@ -1577,7 +1577,7 @@
    2.70                     val y = Free ("y" ^ string_of_int i, U)
    2.71                   in
    2.72                     HOLogic.mk_imp (R $ x $ y,
    2.73 -                     HOLogic.mk_mem (Const ("Nominal.supp", U --> aset) $ y, finites))
    2.74 +                     finite $ (Const ("Nominal.supp", U --> aset) $ y))
    2.75                   end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs)))))
    2.76              (fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
    2.77                 (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
    2.78 @@ -1597,9 +1597,9 @@
    2.79        end;
    2.80  
    2.81      val finite_premss = map (fn aT =>
    2.82 -      map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem
    2.83 -        (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f,
    2.84 -         Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT)))))
    2.85 +      map (fn (f, T) => HOLogic.mk_Trueprop
    2.86 +        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
    2.87 +           (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
    2.88             (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
    2.89  
    2.90      val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
    2.91 @@ -1715,9 +1715,9 @@
    2.92        in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
    2.93  
    2.94      val finite_ctxt_prems = map (fn aT =>
    2.95 -      HOLogic.mk_Trueprop (HOLogic.mk_mem
    2.96 -        (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt,
    2.97 -         Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT))))) dt_atomTs;
    2.98 +      HOLogic.mk_Trueprop
    2.99 +        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
   2.100 +           (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
   2.101  
   2.102      val rec_unique_thms = split_conj_thm (Goal.prove
   2.103        (ProofContext.init thy11) (map fst rec_unique_frees)
     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Feb 07 17:46:03 2007 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Feb 07 17:51:38 2007 +0100
     3.3 @@ -48,7 +48,7 @@
     3.4  structure NominalPermeq : NOMINAL_PERMEQ =
     3.5  struct
     3.6  
     3.7 -val Finites_emptyI = thm "Finites.emptyI";
     3.8 +val finite_emptyI = thm "finite.emptyI";
     3.9  val finite_Un = thm "finite_Un";
    3.10  
    3.11  (* pulls out dynamically a thm via the proof state *)
    3.12 @@ -264,8 +264,7 @@
    3.13      let val goal = List.nth(cprems_of st, i-1)
    3.14      in
    3.15        case Logic.strip_assums_concl (term_of goal) of
    3.16 -          _ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $
    3.17 -            Const ("Finite_Set.Finites", _)) =>
    3.18 +          _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
    3.19            let
    3.20              val cert = Thm.cterm_of (sign_of_thm st);
    3.21              val ps = Logic.strip_params (term_of goal);
    3.22 @@ -281,7 +280,7 @@
    3.23                Logic.strip_assums_concl (hd (prems_of supports_rule'));
    3.24              val supports_rule'' = Drule.cterm_instantiate
    3.25                [(cert (head_of S), cert s')] supports_rule'
    3.26 -            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites_emptyI]
    3.27 +            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, finite_emptyI]
    3.28            in
    3.29              (tactical ("guessing of the right supports-set",
    3.30                        EVERY [compose_tac (false, supports_rule'', 2) i,
    3.31 @@ -319,7 +318,7 @@
    3.32              val supports_fresh_rule'' = Drule.cterm_instantiate
    3.33                [(cert (head_of S), cert s')] supports_fresh_rule'
    3.34  	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
    3.35 -            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites_emptyI]
    3.36 +            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI]
    3.37              (* FIXME sometimes these rewrite rules are already in the ss, *)
    3.38              (* which produces a warning                                   *)
    3.39            in
     4.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Wed Feb 07 17:46:03 2007 +0100
     4.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Wed Feb 07 17:51:38 2007 +0100
     4.3 @@ -71,7 +71,7 @@
     4.4        "!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
     4.5    shows "P F"
     4.6    using major subs
     4.7 -  apply (induct set: Finites)
     4.8 +  apply (induct set: finite)
     4.9     apply (blast intro: cases)+
    4.10    done
    4.11  
     5.1 --- a/src/HOL/NumberTheory/Euler.thy	Wed Feb 07 17:46:03 2007 +0100
     5.2 +++ b/src/HOL/NumberTheory/Euler.thy	Wed Feb 07 17:51:38 2007 +0100
     5.3 @@ -118,7 +118,7 @@
     5.4  
     5.5  lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
     5.6      \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
     5.7 -  by (induct set: Finites) auto
     5.8 +  by (induct set: finite) auto
     5.9  
    5.10  lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> 
    5.11                    int(card(SetS a p)) = (p - 1) div 2"
     6.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Wed Feb 07 17:46:03 2007 +0100
     6.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Wed Feb 07 17:51:38 2007 +0100
     6.3 @@ -242,7 +242,7 @@
     6.4  
     6.5  lemma neg_one_special: "finite A ==>
     6.6      ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
     6.7 -  by (induct set: Finites) auto
     6.8 +  by (induct set: finite) auto
     6.9  
    6.10  lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
    6.11    by (induct n) auto
     7.1 --- a/src/HOL/NumberTheory/Finite2.thy	Wed Feb 07 17:46:03 2007 +0100
     7.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Wed Feb 07 17:51:38 2007 +0100
     7.3 @@ -38,19 +38,19 @@
     7.4  qed
     7.5  
     7.6  lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
     7.7 -  apply (induct set: Finites)
     7.8 +  apply (induct set: finite)
     7.9    apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
    7.10    done
    7.11  
    7.12  lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
    7.13      int(c) * int(card X)"
    7.14 -  apply (induct set: Finites)
    7.15 +  apply (induct set: finite)
    7.16    apply (auto simp add: zadd_zmult_distrib2)
    7.17    done
    7.18  
    7.19  lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
    7.20      c * setsum f A"
    7.21 -  by (induct set: Finites) (auto simp add: zadd_zmult_distrib2)
    7.22 +  by (induct set: finite) (auto simp add: zadd_zmult_distrib2)
    7.23  
    7.24  
    7.25  subsection {* Cardinality of explicit finite sets *}
     8.1 --- a/src/HOL/NumberTheory/Gauss.thy	Wed Feb 07 17:46:03 2007 +0100
     8.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Wed Feb 07 17:51:38 2007 +0100
     8.3 @@ -444,7 +444,7 @@
     8.4                                 "setprod uminus E"], auto)
     8.5      done
     8.6    also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
     8.7 -    using finite_E by (induct set: Finites) auto
     8.8 +    using finite_E by (induct set: finite) auto
     8.9    then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
    8.10      by (simp add: zmult_commute)
    8.11    with two show ?thesis
    8.12 @@ -484,7 +484,7 @@
    8.13      by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
    8.14    moreover have "setprod (%x. x * a) A =
    8.15      setprod (%x. a) A * setprod id A"
    8.16 -    using finite_A by (induct set: Finites) auto
    8.17 +    using finite_A by (induct set: finite) auto
    8.18    ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
    8.19      setprod id A))] (mod p)"
    8.20      by simp
     9.1 --- a/src/HOL/NumberTheory/Int2.thy	Wed Feb 07 17:46:03 2007 +0100
     9.2 +++ b/src/HOL/NumberTheory/Int2.thy	Wed Feb 07 17:51:38 2007 +0100
     9.3 @@ -175,7 +175,7 @@
     9.4  
     9.5  lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
     9.6      ==> zgcd (setprod id A,y) = 1"
     9.7 -  by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult)
     9.8 +  by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
     9.9  
    9.10  
    9.11  subsection {* Some properties of MultInv *}
    10.1 --- a/src/HOL/Real/ferrante_rackoff_proof.ML	Wed Feb 07 17:46:03 2007 +0100
    10.2 +++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Wed Feb 07 17:51:38 2007 +0100
    10.3 @@ -47,7 +47,7 @@
    10.4          fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
    10.5          val ss = simpset_of sg
    10.6          fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
    10.7 -        val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
    10.8 +        val uf = prove_bysimp sg ss (Const ("Finite_Set.finite", rsT --> HOLogic.boolT) $ hU)
    10.9      in (U,cterm_of sg hU,map proveinU U,uf)
   10.10      end;
   10.11