# HG changeset patch # User blanchet # Date 1234356448 -3600 # Node ID 7c301075eef101623c0a57829b7d3fdb96b32f93 # Parent d203e9d4675bb49c2d7dccf6bf7c1d875990adbb# Parent 14e208d607af10fa228c838bb14ac736732708ba merged diff -r d203e9d4675b -r 7c301075eef1 src/HOL/HOL.thy --- 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 {* diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/datatype_abs_proofs.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)) diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/function_package/fundef_package.ML --- 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 diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/function_package/size.ML --- 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; diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/inductive_package.ML --- 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 |> diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/old_primrec_package.ML --- 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 diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/primrec_package.ML --- 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 diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/recdef_package.ML --- 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 diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/record_package.ML --- 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 diff -r d203e9d4675b -r 7c301075eef1 src/HOL/Tools/sat_solver.ML --- 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")