# HG changeset patch
# User huffman
# Date 1329937146 -3600
# Node ID 9517cc2883ebdffcce1f870afc423243811c73d5
# Parent  f11f332b964f60e71a64c45efcb33632855f94ce# Parent  d5d49bd4a7b452f515a9f3acf91f0c94441db0e5
merged

diff -r f11f332b964f -r 9517cc2883eb NEWS
--- 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'.
diff -r f11f332b964f -r 9517cc2883eb doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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}
 *}
 
diff -r f11f332b964f -r 9517cc2883eb doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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%
diff -r f11f332b964f -r 9517cc2883eb etc/isar-keywords.el
--- 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"
diff -r f11f332b964f -r 9517cc2883eb src/HOL/IsaMakefile
--- 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
diff -r f11f332b964f -r 9517cc2883eb src/HOL/Quickcheck_Examples/Find_Unused_Assms_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
diff -r f11f332b964f -r 9517cc2883eb src/HOL/Quickcheck_Examples/ROOT.ML
--- 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"
 ];
diff -r f11f332b964f -r 9517cc2883eb src/HOL/Quickcheck_Narrowing.thy
--- 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
diff -r f11f332b964f -r 9517cc2883eb src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- /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;