--- 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 {*
--- 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))
--- 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
--- 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;
--- 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