--- a/src/HOL/HOL.thy Fri Feb 06 15:15:46 2009 +0100
+++ b/src/HOL/HOL.thy Fri Feb 06 16:00:05 2009 +0100
@@ -1701,6 +1701,23 @@
*}
+subsection {* Nitpick theorem store *}
+
+ML {*
+structure Nitpick_Const_Simps_Thms = NamedThmsFun
+(
+ val name = "nitpick_const_simps"
+ val description = "Equational specification of constants as needed by Nitpick"
+)
+structure Nitpick_Ind_Intros_Thms = NamedThmsFun
+(
+ val name = "nitpick_ind_intros"
+ val description = "Introduction rules for inductive predicate as needed by Nitpick"
+)
+*}
+setup {* Nitpick_Const_Simps_Thms.setup
+ o Nitpick_Ind_Intros_Thms.setup *}
+
subsection {* Legacy tactics and ML bindings *}
ML {*
--- a/src/HOL/Tools/function_package/fundef_package.ML Fri Feb 06 15:15:46 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Fri Feb 06 16:00:05 2009 +0100
@@ -42,7 +42,8 @@
fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
let
- val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
+ val atts = Attrib.internal (K Simplifier.simp_add) ::
+ Attrib.internal (K Nitpick_Const_Simps_Thms.add) :: moreatts
val spec = post simps
|> map (apfst (apsnd (append atts)))
|> map (apfst (apfst extra_qualify))
--- a/src/HOL/Tools/function_package/size.ML Fri Feb 06 15:15:46 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Fri Feb 06 16:00:05 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_Simps_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))
--- a/src/HOL/Tools/inductive_package.ML Fri Feb 06 15:15:46 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Feb 06 16:00:05 2009 +0100
@@ -691,7 +691,8 @@
ctxt |>
LocalTheory.notes kind
(map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
- [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
+ [Attrib.internal (K (ContextRules.intro_query NONE)),
+ Attrib.internal (K Nitpick_Ind_Intros_Thms.add)])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), ctxt2) =
ctxt1 |>
--- a/src/HOL/Tools/primrec_package.ML Fri Feb 06 15:15:46 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Fri Feb 06 16:00:05 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_Simps_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