--- a/NEWS Wed Feb 22 17:34:31 2012 +0100
+++ b/NEWS Wed Feb 22 19:59:06 2012 +0100
@@ -296,6 +296,9 @@
* Improved code generation of multisets.
+* New diagnostic command find_unused_assms to find potentially superfluous
+ assumptions in theorems using Quickcheck.
+
* Quickcheck:
- Quickcheck returns variable assignments as counterexamples, which
allows to reveal the underspecification of functions under test.
@@ -318,6 +321,8 @@
- Support for multisets.
+ - Added "use_subtype" options.
+
* Nitpick:
- Fixed infinite loop caused by the 'peephole_optim' option and
affecting 'rat' and 'real'.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 22 17:34:31 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 22 19:59:06 2012 +0100
@@ -1643,7 +1643,8 @@
@{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "refute_params"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"}
+ @{command_def (HOL) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "find_unused_assms"} & : & @{text "context \<rightarrow>"}
\end{matharray}
@{rail "
@@ -1660,10 +1661,14 @@
(@@{command (HOL) quickcheck_params} | @@{command (HOL) refute_params} |
@@{command (HOL) nitpick_params}) ( '[' args ']' )?
;
+
@@{command (HOL) quickcheck_generator} typeconstructor \\
'operations:' ( @{syntax term} +)
;
+ @@{command (HOL) find_unused_assms} theoryname?
+ ;
+
modes: '(' (@{syntax name} +) ')'
;
@@ -1743,6 +1748,10 @@
\item[@{text report}] if set quickcheck reports how many tests
fulfilled the preconditions.
+ \item[@{text use_subtype}] if set quickcheck automatically lifts
+ conjectures to registered subtypes if possible, and tests the
+ lifted conjecture.
+
\item[@{text quiet}] if set quickcheck does not output anything
while testing.
@@ -1806,6 +1815,13 @@
\item @{command (HOL) "nitpick_params"} changes @{command (HOL)
"nitpick"} configuration options persistently.
+ \item @{command (HOL) "find_unused_assms"} finds potentially superfluous
+ assumptions in theorems using quickcheck.
+ It takes the theory name to be checked for superfluous assumptions as
+ optional argument. If not provided, it checks the current theory.
+ Options to the internal quickcheck invocations can be changed with
+ common configuration declarations.
+
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 22 17:34:31 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 22 19:59:06 2012 +0100
@@ -2341,7 +2341,8 @@
\indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{refute\_params}\hypertarget{command.HOL.refute-params}{\hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{nitpick\_params}\hypertarget{command.HOL.nitpick-params}{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{quickcheck\_generator}\hypertarget{command.HOL.quickcheck-generator}{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
+ \indexdef{HOL}{command}{quickcheck\_generator}\hypertarget{command.HOL.quickcheck-generator}{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{HOL}{command}{find\_unused\_assms}\hypertarget{command.HOL.find-unused-assms}{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}
\end{matharray}
\begin{railoutput}
@@ -2415,6 +2416,13 @@
\rail@nextplus{3}
\rail@endplus
\rail@end
+\rail@begin{2}{}
+\rail@term{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{theoryname}}[]
+\rail@endbar
+\rail@end
\rail@begin{2}{\isa{modes}}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@plus
@@ -2504,6 +2512,10 @@
\item[\isa{report}] if set quickcheck reports how many tests
fulfilled the preconditions.
+ \item[\isa{use{\isaliteral{5F}{\isacharunderscore}}subtype}] if set quickcheck automatically lifts
+ conjectures to registered subtypes if possible, and tests the
+ lifted conjecture.
+
\item[\isa{quiet}] if set quickcheck does not output anything
while testing.
@@ -2562,6 +2574,13 @@
\item \hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}} changes \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} configuration options persistently.
+ \item \hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}} finds potentially superfluous
+ assumptions in theorems using quickcheck.
+ It takes the theory name to be checked for superfluous assumptions as
+ optional argument. If not provided, it checks the current theory.
+ Options to the internal quickcheck invocations can be changed with
+ common configuration declarations.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/etc/isar-keywords.el Wed Feb 22 17:34:31 2012 +0100
+++ b/etc/isar-keywords.el Wed Feb 22 19:59:06 2012 +0100
@@ -92,6 +92,7 @@
"finally"
"find_consts"
"find_theorems"
+ "find_unused_assms"
"fix"
"fixrec"
"from"
@@ -358,6 +359,7 @@
"export_code"
"find_consts"
"find_theorems"
+ "find_unused_assms"
"full_prf"
"header"
"help"
--- a/src/HOL/IsaMakefile Wed Feb 22 17:34:31 2012 +0100
+++ b/src/HOL/IsaMakefile Wed Feb 22 19:59:06 2012 +0100
@@ -1513,6 +1513,7 @@
HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz
$(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL \
+ Quickcheck_Examples/Find_Unused_Assms_Examples.thy \
Quickcheck_Examples/Quickcheck_Examples.thy \
Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \
Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy Wed Feb 22 19:59:06 2012 +0100
@@ -0,0 +1,27 @@
+theory Find_Unused_Assms_Examples
+imports Main
+begin
+
+section {* Arithmetics *}
+
+declare [[quickcheck_finite_types = false]]
+
+find_unused_assms Divides
+find_unused_assms GCD
+find_unused_assms MacLaurin
+
+section {* Set Theory *}
+
+declare [[quickcheck_finite_types = true]]
+
+find_unused_assms Fun
+find_unused_assms Relation
+find_unused_assms Set
+find_unused_assms Wellfounded
+
+section {* Datatypes *}
+
+find_unused_assms List
+find_unused_assms Map
+
+end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 17:34:31 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 19:59:06 2012 +0100
@@ -1,4 +1,5 @@
use_thys [
+ "Find_Unused_Assms_Examples",
"Quickcheck_Examples",
"Quickcheck_Lattice_Examples"
];
--- a/src/HOL/Quickcheck_Narrowing.thy Wed Feb 22 17:34:31 2012 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Wed Feb 22 19:59:06 2012 +0100
@@ -8,6 +8,7 @@
("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
("Tools/Quickcheck/Narrowing_Engine.hs")
("Tools/Quickcheck/narrowing_generators.ML")
+ ("Tools/Quickcheck/find_unused_assms.ML")
begin
subsection {* Counterexample generator *}
@@ -452,10 +453,15 @@
*)
+subsection {* The @{text find_unused_assms} command *}
+
+use "Tools/Quickcheck/find_unused_assms.ML"
+
+subsection {* Closing up *}
+
hide_type code_int narrowing_type narrowing_term cons property
hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero
hide_const (open) Var Ctr "apply" sum cons
hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Wed Feb 22 19:59:06 2012 +0100
@@ -0,0 +1,116 @@
+(* Title: HOL/Tools/Quickcheck/find_unused_assms.ML
+ Author: Lukas Bulwahn, TU Muenchen
+
+Finding unused assumptions in lemmas (using Quickcheck)
+*)
+
+signature FIND_UNUSED_ASSMS =
+sig
+ val find_unused_assms : Proof.context -> string -> (string * int list list option) list
+ val print_unused_assms : Proof.context -> string option -> unit
+end;
+
+structure Find_Unused_Assms : FIND_UNUSED_ASSMS =
+struct
+
+fun all_unconcealed_thms_of thy =
+ let
+ val facts = Global_Theory.facts_of thy
+ in
+ Facts.fold_static
+ (fn (s, ths) =>
+ if Facts.is_concealed facts s then I else append (map (`(Thm.get_name_hint)) ths))
+ facts []
+ end;
+
+fun thms_of thy thy_name = all_unconcealed_thms_of thy
+ |> filter (fn (_, th) => Context.theory_name (theory_of_thm th) = thy_name);
+
+fun do_while P f s = if P s then (let val s' = f s in (do_while P f s') o (cons s') end) else I
+
+fun drop_indexes is xs = fold_index (fn (i, x) => if member (op =) is i then I else cons x) xs []
+
+fun find_max_subsets [] = []
+ | find_max_subsets (ss :: sss) = ss ::
+ (find_max_subsets (map (filter_out (fn s => exists (fn s' => subset (op =) (s, s')) ss)) sss))
+
+(* main functionality *)
+
+fun find_unused_assms ctxt thy_name =
+ let
+ val ctxt' = ctxt
+ |> Config.put Quickcheck.abort_potential true
+ |> Config.put Quickcheck.quiet true
+ val all_thms = filter (fn (s, _) => length (space_explode "." s) = 2)
+ (thms_of (Proof_Context.theory_of ctxt) thy_name)
+ fun check_single conjecture =
+ case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
+ SOME (SOME _) => false
+ | SOME NONE => true
+ | NONE => false
+ fun build X Ss =
+ fold (fn S => fold
+ (fn x => if member (op =) S x then I
+ else insert (eq_set (op =)) (insert (op =) x S)) X) Ss []
+ fun check (s, th) =
+ case Logic.strip_horn (prop_of (Thm.unvarify_global th)) of
+ ([], _) => cons (s, NONE)
+ | (ts, t) =>
+ let
+ fun mk_conjecture is = (Logic.list_implies (drop_indexes is ts, t))
+ val singles = filter (check_single o mk_conjecture o single) (map_index fst ts)
+ val multiples = do_while (not o null)
+ (fn I => filter (check_single o mk_conjecture) (build singles I))
+ (map single singles) [(map single singles)]
+ val maximals = flat (find_max_subsets multiples)
+ in
+ cons (s, SOME maximals)
+ end
+ in
+ fold check all_thms []
+ end
+
+(* printing results *)
+
+fun pretty_indexes is =
+ Pretty.block (separate (Pretty.str " and ")
+ (map (fn x => Pretty.str (string_of_int (x + 1))) (sort int_ord is))
+ @ [Pretty.brk 1])
+
+fun pretty_thm (s, SOME set_of_indexes) =
+ Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 ::
+ Pretty.str "unnecessary assumption(s) " ::
+ separate (Pretty.str ", or ") (map pretty_indexes set_of_indexes))
+
+fun print_unused_assms ctxt opt_thy_name =
+ let
+ val start = Timing.start ()
+ val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
+ val results = find_unused_assms ctxt thy_name
+ val total = length results
+ val with_assumptions = length (filter (is_some o snd) results)
+ val with_superfluous_assumptions = filter_out (fn (_, r) => r = SOME [])
+ (filter (is_some o snd) results)
+
+ val msg = "Found " ^ string_of_int (length with_superfluous_assumptions)
+ ^ " theorem(s) with (potentially) superfluous assumptions"
+ val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
+ ^ " in the theory " ^ quote thy_name
+ ^ " with a total of " ^ string_of_int total ^ " theorem(s)"
+ ^ " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
+ in
+ ([Pretty.str (msg ^ ":"), Pretty.str ""] @
+ map pretty_thm with_superfluous_assumptions
+ @ [Pretty.str "", Pretty.str end_msg])
+ end |> Pretty.chunks |> Pretty.writeln;
+
+
+val _ =
+ Outer_Syntax.improper_command "find_unused_assms" "find theorems with superfluous assumptions"
+ Keyword.diag
+ (Scan.option Parse.name
+ >> (fn opt_thy_name =>
+ Toplevel.no_timing o Toplevel.keep (fn state =>
+ print_unused_assms (Toplevel.context_of state) opt_thy_name)));
+
+end;