# HG changeset patch
# User bulwahn
# Date 1311142599 -7200
# Node ID 64819f353c5336ef8ef48997040c8be836fbb1a5
# Parent  003f8c5f3e379f5c8a9241887067ebc639cae673
updating documentation about quickcheck; adding information about try

diff -r 003f8c5f3e37 -r 64819f353c53 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 20 08:16:38 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 20 08:16:39 2011 +0200
@@ -1382,6 +1382,11 @@
     @{text "elim:"}, and @{text "dest:"} are passed to the appropriate proof
     methods.
 
+  \item @{command (HOL) "try"} attempts to prove or disprove a subgoal
+    using a combination of provers and disprovers (@{text "solve_direct"},
+    @{text "quickcheck"}, @{text "try_methods"}, @{text "sledgehammer"},
+    @{text "nitpick"}).
+
   \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
     automatic provers (resolution provers and SMT solvers). See the Sledgehammer
     manual \cite{isabelle-sledgehammer} for details.
@@ -1448,17 +1453,24 @@
     free variables; by default the first subgoal is tested, an other
     can be selected explicitly using an optional goal index.
     Assignments can be chosen exhausting the search space upto a given
-    size or using a fixed number of random assignments in the search space.
+    size, or using a fixed number of random assignments in the search space,
+    or exploring the search space symbolically using narrowing.
     By default, quickcheck uses exhaustive testing.
     A number of configuration options are supported for
     @{command (HOL) "quickcheck"}, notably:
 
     \begin{description}
 
-    \item[@{text tester}] specifies how to explore the search space
-      (e.g. exhaustive or random).
+    \item[@{text tester}] specifies which testing approach to apply.
+      There are three testers, @{text exhaustive},
+      @{text random}, and @{text narrowing}.
       An unknown configuration option is treated as an argument to tester,
       making @{text "tester ="} optional.
+      When multiple testers are given, these are applied in parallel. 
+      If no tester is specified, quickcheck uses the testers that are
+      set active, i.e., configurations
+      @{text quickcheck_exhaustive_active}, @{text quickcheck_random_active},
+      @{text quickcheck_narrowing_active} are set to true.
     \item[@{text size}] specifies the maximum size of the search space
     for assignment values.
 
diff -r 003f8c5f3e37 -r 64819f353c53 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 20 08:16:38 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 20 08:16:39 2011 +0200
@@ -2013,6 +2013,11 @@
     \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof
     methods.
 
+  \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal
+    using a combination of provers and disprovers (\isa{{\isaliteral{22}{\isachardoublequote}}solve{\isaliteral{5F}{\isacharunderscore}}direct{\isaliteral{22}{\isachardoublequote}}},
+    \isa{{\isaliteral{22}{\isachardoublequote}}quickcheck{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}try{\isaliteral{5F}{\isacharunderscore}}methods{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}sledgehammer{\isaliteral{22}{\isachardoublequote}}},
+    \isa{{\isaliteral{22}{\isachardoublequote}}nitpick{\isaliteral{22}{\isachardoublequote}}}).
+
   \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external
     automatic provers (resolution provers and SMT solvers). See the Sledgehammer
     manual \cite{isabelle-sledgehammer} for details.
@@ -2131,17 +2136,24 @@
     free variables; by default the first subgoal is tested, an other
     can be selected explicitly using an optional goal index.
     Assignments can be chosen exhausting the search space upto a given
-    size or using a fixed number of random assignments in the search space.
+    size, or using a fixed number of random assignments in the search space,
+    or exploring the search space symbolically using narrowing.
     By default, quickcheck uses exhaustive testing.
     A number of configuration options are supported for
     \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
 
     \begin{description}
 
-    \item[\isa{tester}] specifies how to explore the search space
-      (e.g. exhaustive or random).
+    \item[\isa{tester}] specifies which testing approach to apply.
+      There are three testers, \isa{exhaustive},
+      \isa{random}, and \isa{narrowing}.
       An unknown configuration option is treated as an argument to tester,
       making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional.
+      When multiple testers are given, these are applied in parallel. 
+      If no tester is specified, quickcheck uses the testers that are
+      set active, i.e., configurations
+      \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}exhaustive{\isaliteral{5F}{\isacharunderscore}}active}, \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}random{\isaliteral{5F}{\isacharunderscore}}active},
+      \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}narrowing{\isaliteral{5F}{\isacharunderscore}}active} are set to true.
     \item[\isa{size}] specifies the maximum size of the search space
     for assignment values.