--- a/src/HOL/HOL.thy Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/HOL.thy Wed Feb 11 13:47:28 2009 +0100
@@ -932,7 +932,7 @@
structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
-structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "Theorems blacklisted for ATP");
+structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP");
*}
text {*ResBlacklist holds theorems blacklisted to sledgehammer.
@@ -1701,6 +1701,29 @@
*}
+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"
+)
+structure Nitpick_Ind_Intro_Thms = NamedThmsFun
+(
+ val name = "nitpick_ind_intro"
+ val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
+)
+*}
+setup {* Nitpick_Const_Simp_Thms.setup
+ #> Nitpick_Const_Psimp_Thms.setup
+ #> Nitpick_Ind_Intro_Thms.setup *}
+
subsection {* Legacy tactics and ML bindings *}
ML {*
--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Feb 11 13:47:28 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 Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Feb 11 13:47:28 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 Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/function_package/size.ML Wed Feb 11 13:47:28 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/inductive_package.ML Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/inductive_package.ML Wed Feb 11 13:47:28 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_Intro_Thms.add)])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), ctxt2) =
ctxt1 |>
--- a/src/HOL/Tools/old_primrec_package.ML Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/old_primrec_package.ML Wed Feb 11 13:47:28 2009 +0100
@@ -283,7 +283,8 @@
val simps'' = maps snd simps';
in
thy''
- |> note (("simps", [Simplifier.simp_add, Code.add_default_eqn_attribute]), simps'')
+ |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+ Code.add_default_eqn_attribute]), simps'')
|> snd
|> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
|> snd
--- a/src/HOL/Tools/primrec_package.ML Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/primrec_package.ML Wed Feb 11 13:47:28 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
--- a/src/HOL/Tools/recdef_package.ML Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/recdef_package.ML Wed Feb 11 13:47:28 2009 +0100
@@ -207,7 +207,8 @@
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, Code.add_default_eqn_attribute] else [];
+ val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+ Code.add_default_eqn_attribute] else [];
val ((simps' :: rules', [induct']), thy) =
thy
--- a/src/HOL/Tools/record_package.ML Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/record_package.ML Wed Feb 11 13:47:28 2009 +0100
@@ -2188,7 +2188,8 @@
val final_thy =
thms_thy
|> (snd oo PureThy.add_thmss)
- [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
+ [((Binding.name "simps", sel_upd_simps),
+ [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
((Binding.name "iffs", iffs), [iff_add])]
|> put_record name (make_record_info args parent fields extension induct_scheme')
|> put_sel_upd (names @ [full_moreN]) sel_upd_simps
--- a/src/HOL/Tools/sat_solver.ML Wed Feb 11 23:07:50 2009 +1100
+++ b/src/HOL/Tools/sat_solver.ML Wed Feb 11 13:47:28 2009 +0100
@@ -569,9 +569,10 @@
fun minisat_with_proofs fm =
let
val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
- val proofpath = File.tmp_path (Path.explode "result.prf")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
+ val proofpath = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
@@ -754,8 +755,9 @@
fun minisat fm =
let
val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
@@ -916,8 +918,9 @@
(getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
(* both versions of zChaff appear to have the same interface, so we do *)
(* not actually need to distinguish between them in the following code *)
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
@@ -941,8 +944,9 @@
fun berkmin fm =
let
val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!")
@@ -966,8 +970,9 @@
fun jerusat fm =
let
val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")