# HG changeset patch
# User blanchet
# Date 1234172397 -3600
# Node ID 0abd89253a0fc123b880e13a15f6ac95d0d107c1
# Parent  409138c4de1208a6324214c2b0bc2fd723772da6# Parent  6e93ae65c678532ba4b6c279f37b1c0cff03aa09
merged

diff -r 409138c4de12 -r 0abd89253a0f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Feb 08 11:59:26 2009 +0100
+++ b/src/HOL/HOL.thy	Mon Feb 09 10:39:57 2009 +0100
@@ -1701,6 +1701,23 @@
 *}
 
 
+subsection {* Nitpick theorem store *}
+
+ML {*
+structure Nitpick_Const_Simp_Thms = NamedThmsFun
+(
+  val name = "nitpick_const_simp"
+  val description = "Equational specification of constants as needed by Nitpick"
+)
+structure Nitpick_Const_Psimp_Thms = NamedThmsFun
+(
+  val name = "nitpick_const_psimp"
+  val description = "Partial equational specification of constants as needed by Nitpick"
+)
+*}
+setup {* Nitpick_Const_Simp_Thms.setup
+         #> Nitpick_Const_Psimp_Thms.setup *}
+
 subsection {* Legacy tactics and ML bindings *}
 
 ML {*
diff -r 409138c4de12 -r 0abd89253a0f src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Feb 08 11:59:26 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 09 10:39:57 2009 +0100
@@ -333,9 +333,10 @@
     val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
       (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
           (DatatypeProp.make_cases new_type_names descr sorts thy2)
-
   in
     thy2
+    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
+       o Context.Theory
     |> parent_path flat_names
     |> store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
diff -r 409138c4de12 -r 0abd89253a0f src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sun Feb 08 11:59:26 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 09 10:39:57 2009 +0100
@@ -71,8 +71,9 @@
 
       val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
-            |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps
-            ||> fold_option (snd oo addsmps I "simps" []) trsimps
+            |> addsmps (NameSpace.qualified "partial") "psimps"
+                       [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
+            ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
             ||>> note_theorem ((qualify "pinduct",
                    [Attrib.internal (K (RuleCases.case_names cnames)),
                     Attrib.internal (K (RuleCases.consumes 1)),
@@ -127,7 +128,8 @@
       val tinduct = map remove_domain_condition pinducts
 
       val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
-      val allatts = if has_guards then [] else [Code.add_default_eqn_attrib]
+      val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
+        [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
 
       val qualify = NameSpace.qualified defname;
     in
diff -r 409138c4de12 -r 0abd89253a0f src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Sun Feb 08 11:59:26 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Mon Feb 09 10:39:57 2009 +0100
@@ -209,8 +209,9 @@
 
     val ([size_thms], thy'') =  PureThy.add_thmss
       [((Binding.name "size", size_eqns),
-        [Simplifier.simp_add, Thm.declaration_attribute
-              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
+        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+         Thm.declaration_attribute
+             (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
 
   in
     SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
@@ -238,4 +239,4 @@
 
 val setup = DatatypePackage.interpretation add_size_thms;
 
-end;
\ No newline at end of file
+end;
diff -r 409138c4de12 -r 0abd89253a0f src/HOL/Tools/inductive_package.ML
diff -r 409138c4de12 -r 0abd89253a0f src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Sun Feb 08 11:59:26 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Mon Feb 09 10:39:57 2009 +0100
@@ -251,7 +251,8 @@
     val qualify = Binding.qualify prefix;
     val spec' = (map o apfst)
       (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
-    val simp_att = (Attrib.internal o K) Simplifier.simp_add;
+    val simp_atts = map (Attrib.internal o K)
+      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
@@ -259,7 +260,7 @@
     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
     |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
     |-> (fn simps' => LocalTheory.note Thm.theoremK
-          ((qualify (Binding.name "simps"), [simp_att]), maps snd simps'))
+          ((qualify (Binding.name "simps"), simp_atts), maps snd simps'))
     |>> snd
   end handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn