# HG changeset patch
# User blanchet
# Date 1256139275 -7200
# Node ID 791a4655cae3a7519f93c38ca22d29db9aa0446a
# Parent  5a733f325939f63d0bcbbe2c7e0c4be7dec4c4fe
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"

diff -r 5a733f325939 -r 791a4655cae3 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/HOL.thy	Wed Oct 21 17:34:35 2009 +0200
@@ -2049,33 +2049,33 @@
 text {* This will be relocated once Nitpick is moved to HOL. *}
 
 ML {*
-structure Nitpick_Const_Defs = Named_Thms
+structure Nitpick_Defs = Named_Thms
 (
-  val name = "nitpick_const_def"
+  val name = "nitpick_def"
   val description = "alternative definitions of constants as needed by Nitpick"
 )
-structure Nitpick_Const_Simps = Named_Thms
+structure Nitpick_Simps = Named_Thms
 (
-  val name = "nitpick_const_simp"
+  val name = "nitpick_simp"
   val description = "equational specification of constants as needed by Nitpick"
 )
-structure Nitpick_Const_Psimps = Named_Thms
+structure Nitpick_Psimps = Named_Thms
 (
-  val name = "nitpick_const_psimp"
+  val name = "nitpick_psimp"
   val description = "partial equational specification of constants as needed by Nitpick"
 )
-structure Nitpick_Ind_Intros = Named_Thms
+structure Nitpick_Intros = Named_Thms
 (
-  val name = "nitpick_ind_intro"
+  val name = "nitpick_intro"
   val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
 )
 *}
 
 setup {*
-  Nitpick_Const_Defs.setup
-  #> Nitpick_Const_Simps.setup
-  #> Nitpick_Const_Psimps.setup
-  #> Nitpick_Ind_Intros.setup
+  Nitpick_Defs.setup
+  #> Nitpick_Simps.setup
+  #> Nitpick_Psimps.setup
+  #> Nitpick_Intros.setup
 *}
 
 
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Induct/LList.thy	Wed Oct 21 17:34:35 2009 +0200
@@ -665,7 +665,7 @@
 apply (subst LList_corec, force)
 done
 
-lemma llist_corec [nitpick_const_simp]: 
+lemma llist_corec [nitpick_simp]: 
     "llist_corec a f =   
      (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
 apply (unfold llist_corec_def LNil_def LCons_def)
@@ -774,10 +774,10 @@
 
 subsection{* The functional @{text lmap} *}
 
-lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
+lemma lmap_LNil [simp, nitpick_simp]: "lmap f LNil = LNil"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
-lemma lmap_LCons [simp, nitpick_const_simp]:
+lemma lmap_LCons [simp, nitpick_simp]:
 "lmap f (LCons M N) = LCons (f M) (lmap f N)"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
@@ -793,7 +793,7 @@
 
 subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
 
-lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
+lemma iterates [nitpick_simp]: "iterates f x = LCons x (iterates f (f x))"
 by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
 
 lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
@@ -848,18 +848,18 @@
 
 subsection{* @{text lappend} -- its two arguments cause some complications! *}
 
-lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
+lemma lappend_LNil_LNil [simp, nitpick_simp]: "lappend LNil LNil = LNil"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
 done
 
-lemma lappend_LNil_LCons [simp, nitpick_const_simp]: 
+lemma lappend_LNil_LCons [simp, nitpick_simp]: 
     "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
 done
 
-lemma lappend_LCons [simp, nitpick_const_simp]: 
+lemma lappend_LCons [simp, nitpick_simp]: 
     "lappend (LCons l l') N = LCons l (lappend l' N)"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Int.thy	Wed Oct 21 17:34:35 2009 +0200
@@ -1614,7 +1614,7 @@
 context ring_1
 begin
 
-lemma of_int_of_nat [nitpick_const_simp]:
+lemma of_int_of_nat [nitpick_simp]:
   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
 proof (cases "k < 0")
   case True then have "0 \<le> - k" by simp
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Wed Oct 21 17:34:35 2009 +0200
@@ -260,7 +260,7 @@
   qed
 qed
 
-lemma llist_corec [code, nitpick_const_simp]:
+lemma llist_corec [code, nitpick_simp]:
   "llist_corec a f =
     (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
 proof (cases "f a")
@@ -656,8 +656,8 @@
   qed
 qed
 
-lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
-  and lmap_LCons [simp, nitpick_const_simp]:
+lemma lmap_LNil [simp, nitpick_simp]: "lmap f LNil = LNil"
+  and lmap_LCons [simp, nitpick_simp]:
   "lmap f (LCons M N) = LCons (f M) (lmap f N)"
   by (simp_all add: lmap_def llist_corec)
 
@@ -729,9 +729,9 @@
   qed
 qed
 
-lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
-  and lappend_LNil_LCons [simp, nitpick_const_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
-  and lappend_LCons [simp, nitpick_const_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
+lemma lappend_LNil_LNil [simp, nitpick_simp]: "lappend LNil LNil = LNil"
+  and lappend_LNil_LCons [simp, nitpick_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
+  and lappend_LCons [simp, nitpick_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
   by (simp_all add: lappend_def llist_corec)
 
 lemma lappend_LNil1 [simp]: "lappend LNil l = l"
@@ -755,7 +755,7 @@
   iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
 
-lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
+lemma iterates [nitpick_simp]: "iterates f x = LCons x (iterates f (f x))"
   apply (unfold iterates_def)
   apply (subst llist_corec)
   apply simp
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -372,8 +372,7 @@
          in
            lthy''
            |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
-                map (Attrib.internal o K)
-                    [Simplifier.simp_add, Nitpick_Const_Simps.add]),
+                map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
                 maps snd simps')
            |> snd
          end)
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -262,8 +262,7 @@
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
-    |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
-         [Nitpick_Const_Simps.add])]
+    |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
     ||> Sign.parent_path
     ||> Theory.checkpoint
     |-> (fn thms => pair (reccomb_names, flat thms))
@@ -335,7 +334,7 @@
           (DatatypeProp.make_cases new_type_names descr sorts thy2)
   in
     thy2
-    |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms
+    |> Context.the_theory o fold (fold Nitpick_Simps.add_thm) case_thms
        o Context.Theory
     |> Sign.parent_path
     |> store_thmss "cases" new_type_names case_thms
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/Function/fundef.ML
--- a/src/HOL/Tools/Function/fundef.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/Function/fundef.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -37,12 +37,12 @@
 val simp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
      Code.add_default_eqn_attribute,
-     Nitpick_Const_Simps.add,
+     Nitpick_Simps.add,
      Quickcheck_RecFun_Simps.add]
 
 val psimp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
-     Nitpick_Const_Psimps.add]
+     Nitpick_Psimps.add]
 
 fun note_theorem ((name, atts), ths) =
   LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -209,7 +209,7 @@
 
     val ([size_thms], thy'') =  PureThy.add_thmss
       [((Binding.name "size", size_eqns),
-        [Simplifier.simp_add, Nitpick_Const_Simps.add,
+        [Simplifier.simp_add, Nitpick_Simps.add,
          Thm.declaration_attribute
              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
 
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -157,7 +157,7 @@
 
 fun make_const_spec_table thy =
   fold store_thm (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
-  |> (fn thy => fold store_thm (Nitpick_Const_Simps.get (ProofContext.init thy)) thy)
+  |> (fn thy => fold store_thm (Nitpick_Simps.get (ProofContext.init thy)) thy)
 *)
 fun make_const_spec_table thy =
   let
@@ -168,8 +168,8 @@
   in
     table   
     |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
-    |> store ignore_consts Nitpick_Const_Simps.get
-    |> store ignore_consts Nitpick_Ind_Intros.get
+    |> store ignore_consts Nitpick_Simps.get
+    |> store ignore_consts Nitpick_Intros.get
   end
   (*
 fun get_specification thy constname =
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -703,7 +703,7 @@
       LocalTheory.notes kind
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
            [Attrib.internal (K (ContextRules.intro_query NONE)),
-            Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>>
+            Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -284,7 +284,7 @@
   in
     thy''
     |> note (("simps",
-        [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'')
+        [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
     |> snd
     |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
     |> snd
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/primrec.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -272,7 +272,7 @@
       (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
     fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
       map (Attrib.internal o K)
-        [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]);
+        [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]);
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -214,7 +214,7 @@
     |-> (fn proto_simps => prove_simps proto_simps)
     |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
            Code.add_default_eqn_attrib :: map (Attrib.internal o K)
-          [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]),
+          [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]),
             simps))
     |> snd
   end
diff -r 5a733f325939 -r 791a4655cae3 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/recdef.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -202,7 +202,7 @@
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
-    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simps.add,
+    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Simps.add,
       Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
 
     val ((simps' :: rules', [induct']), thy) =