# HG changeset patch
# User kuncar
# Date 1323092821 -3600
# Node ID 97be233b32ed8e1e16a9bc9e8c52ea01b6e1f412
# Parent  fe2fd2f76f48642d5ca9b1be8180689f33c8013b# Parent  46046d8e96590de7d6149893c3a7e97a995b7029
merged

diff -r fe2fd2f76f48 -r 97be233b32ed NEWS
--- a/NEWS	Mon Dec 05 14:44:46 2011 +0100
+++ b/NEWS	Mon Dec 05 14:47:01 2011 +0100
@@ -145,6 +145,21 @@
 produces a rule which can be used to perform case distinction on both
 a list and a nat.
 
+* Quickcheck:
+  - Quickcheck returns variable assignments as counterexamples, which
+    allows to reveal the underspecification of functions under test.
+    For example, refuting "hd xs = x", it presents the variable
+    assignment xs = [] and x = a1 as a counterexample, assuming that
+    any property is false whenever "hd []" occurs in it.
+    These counterexample are marked as potentially spurious, as
+    Quickcheck also returns "xs = []" as a counterexample to the
+    obvious theorem "hd xs = hd xs".
+    After finding a potentially spurious counterexample, Quickcheck
+    continues searching for genuine ones.
+    By default, Quickcheck shows potentially spurious and genuine
+    counterexamples. The option "genuine_only" sets quickcheck to
+    only show genuine counterexamples.
+ 
 * Nitpick:
   - Fixed infinite loop caused by the 'peephole_optim' option and
     affecting 'rat' and 'real'.
diff -r fe2fd2f76f48 -r 97be233b32ed doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 05 14:44:46 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 05 14:47:01 2011 +0100
@@ -1592,6 +1592,10 @@
     \item[@{text size}] specifies the maximum size of the search space
     for assignment values.
 
+    \item[@{text genuine_only}] sets quickcheck only to return genuine
+      counterexample, but not potentially spurious counterexamples due
+      to underspecified functions.
+    
     \item[@{text eval}] takes a term or a list of terms and evaluates
       these terms under the variable assignment found by quickcheck.
 
@@ -1609,8 +1613,11 @@
     \item[@{text report}] if set quickcheck reports how many tests
     fulfilled the preconditions.
 
-    \item[@{text quiet}] if not set quickcheck informs about the
-    current size for assignment values.
+    \item[@{text quiet}] if set quickcheck does not output anything
+    while testing.
+    
+    \item[@{text verbose}] if set quickcheck informs about the
+    current size and cardinality while testing.
 
     \item[@{text expect}] can be used to check if the user's
     expectation was met (@{text no_expectation}, @{text
diff -r fe2fd2f76f48 -r 97be233b32ed doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 05 14:44:46 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 05 14:47:01 2011 +0100
@@ -2346,6 +2346,10 @@
     \item[\isa{size}] specifies the maximum size of the search space
     for assignment values.
 
+    \item[\isa{genuine{\isaliteral{5F}{\isacharunderscore}}only}] sets quickcheck only to return genuine
+      counterexample, but not potentially spurious counterexamples due
+      to underspecified functions.
+    
     \item[\isa{eval}] takes a term or a list of terms and evaluates
       these terms under the variable assignment found by quickcheck.
 
@@ -2363,8 +2367,11 @@
     \item[\isa{report}] if set quickcheck reports how many tests
     fulfilled the preconditions.
 
-    \item[\isa{quiet}] if not set quickcheck informs about the
-    current size for assignment values.
+    \item[\isa{quiet}] if set quickcheck does not output anything
+    while testing.
+    
+    \item[\isa{verbose}] if set quickcheck informs about the
+    current size and cardinality while testing.
 
     \item[\isa{expect}] can be used to check if the user's
     expectation was met (\isa{no{\isaliteral{5F}{\isacharunderscore}}expectation}, \isa{no{\isaliteral{5F}{\isacharunderscore}}counterexample}, or \isa{counterexample}).
diff -r fe2fd2f76f48 -r 97be233b32ed src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Dec 05 14:47:01 2011 +0100
@@ -38,9 +38,9 @@
        Left e -> throw e);
 
 answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b;
-answer potential a known unknown =
+answer genuine_only a known unknown =
   Control.Exception.catch (answeri a known unknown) 
-    (\ (PatternMatchFail _) -> known False (not potential));
+    (\ (PatternMatchFail _) -> known False genuine_only);
 
 -- Refute
 
@@ -52,14 +52,14 @@
   ", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
 
 eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
-eval potential p k u = answer potential p (\genuine p -> answer potential p k u) u;
+eval genuine_only p k u = answer genuine_only p k u;
 
 ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
-ref potential r xs = eval potential (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
-  (\p -> sumMapM (ref potential r) 1 (refineList xs p));
-          
+ref genuine_only r xs = eval genuine_only (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
+  (\p -> sumMapM (ref genuine_only r) 1 (refineList xs p));
+
 refute :: Bool -> Result -> IO Int;
-refute potential r = ref potential r (args r);
+refute genuine_only r = ref genuine_only r (args r);
 
 sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
 sumMapM f n [] = return n;
@@ -109,10 +109,10 @@
 -- Top-level interface
 
 depthCheck :: Testable a => Bool -> Int -> a -> IO ();
-depthCheck potential d p =
-  (refute potential $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
+depthCheck genuine_only d p =
+  (refute genuine_only $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
 
 smallCheck :: Testable a => Bool -> Int -> a -> IO ();
-smallCheck potential d p = mapM_ (\d -> depthCheck potential d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
+smallCheck genuine_only d p = mapM_ (\d -> depthCheck genuine_only d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
 
 }
diff -r fe2fd2f76f48 -r 97be233b32ed src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Dec 05 14:47:01 2011 +0100
@@ -57,9 +57,9 @@
        Left e -> throw e
 
 answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
-answer potential a known unknown =
+answer genuine_only a known unknown =
   Control.Exception.catch (answeri a known unknown) 
-    (\ (PatternMatchFail _) -> known (not potential))
+    (\ (PatternMatchFail _) -> known genuine_only)
 
 --  Proofs and Refutation
 
@@ -154,19 +154,19 @@
 -- refute
 
 refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
-refute exec potential d t = ref t
+refute exec genuine_only d t = ref t
   where
     ref t =
       let path = find t in
         do
-          t' <- answer potential (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
+          t' <- answer genuine_only (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
             (\p -> return (if length p < d then refineTree path p t else updateNode path unknown t));
           case evalOf t' of
             UnknownValue True -> ref t'
             _ -> return t'
 
 depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
-depthCheck potential d p = refute (checkOf p) potential d (treeOf 0 p) >>= (\t -> 
+depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t -> 
   case evalOf t of
    Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
    _ -> putStrLn ("NONE"))
diff -r fe2fd2f76f48 -r 97be233b32ed src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Dec 05 14:47:01 2011 +0100
@@ -7,10 +7,10 @@
 signature EXHAUSTIVE_GENERATORS =
 sig
   val compile_generator_expr:
-    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
   val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
   val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
-  val put_counterexample: (unit -> int -> int -> (bool * term list) option)
+  val put_counterexample: (unit -> int -> bool -> int -> (bool * term list) option)
     -> Proof.context -> Proof.context
   val put_counterexample_batch: (unit -> (int -> term list option) list)
     -> Proof.context -> Proof.context
@@ -289,7 +289,7 @@
   let
     fun mk_naive_test_term t =
       fold_rev mk_closure (map lookup (Term.add_free_names t []))
-        (mk_if (t, none_t, return))
+        (mk_if (t, none_t, return) true)
     fun mk_smart_test_term' concl bound_vars assms genuine =
       let
         fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
@@ -298,7 +298,7 @@
             | assm :: assms => (vars_of assm, (HOLogic.mk_not assm, none_t, 
                 mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms))
       in
-        fold_rev mk_closure (map lookup vars) (mk_if check)
+        fold_rev mk_closure (map lookup vars) (mk_if check genuine)
       end
     val mk_smart_test_term =
       Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true)
@@ -323,7 +323,7 @@
         fast_exhaustiveT T)
         $ lambda free t $ depth
     val none_t = @{term "()"}
-    fun mk_safe_if (cond, then_t, else_t) = mk_if (cond, then_t, else_t true)
+    fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if none_t return ctxt 
   in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
 
@@ -342,17 +342,19 @@
     val names = Term.add_free_names t []
     val frees = map Free (Term.add_frees t [])
     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
-    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+    val ([depth_name, genuine_only_name], ctxt'') =
+      Variable.variant_fixes ["depth", "genuine_only"] ctxt'
     val depth = Free (depth_name, @{typ code_numeral})
+    val genuine_only = Free (genuine_only_name, @{typ bool}) 
     val return = mk_return (HOLogic.mk_list @{typ "term"}
         (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
     fun mk_exhaustive_closure (free as Free (_, T)) t =
       Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
         $ lambda free t $ depth
     val none_t = Const (@{const_name "None"}, resultT)
-    val mk_if = Quickcheck_Common.mk_safe_if ctxt
+    val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
-  in lambda depth (mk_test_term t) end
+  in lambda genuine_only (lambda depth (mk_test_term t)) end
 
 fun mk_full_generator_expr ctxt (t, eval_terms) =
   let
@@ -360,9 +362,11 @@
     val ctxt' = Variable.auto_fixes t ctxt
     val names = Term.add_free_names t []
     val frees = map Free (Term.add_frees t [])
-    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+    val ([depth_name, genuine_only_name], ctxt'') =
+      Variable.variant_fixes ["depth", "genuine_only"] ctxt'
     val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
     val depth = Free (depth_name, @{typ code_numeral})
+    val genuine_only = Free (depth_name, @{typ bool})    
     val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
     fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
     val return = mk_return (HOLogic.mk_list @{typ term}
@@ -370,21 +374,22 @@
     fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
       if Sign.of_sort thy (T, @{sort enum}) then
         Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
-          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT) 
+          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
             $ lambda free (lambda term_var t))
       else
         Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
           $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
             $ lambda free (lambda term_var t)) $ depth
     val none_t = Const (@{const_name "None"}, resultT)
-    val mk_if = Quickcheck_Common.mk_safe_if ctxt
+    val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
-  in lambda depth (mk_test_term t) end
+  in lambda genuine_only (lambda depth (mk_test_term t)) end
 
 fun mk_parametric_generator_expr mk_generator_expr =
   Quickcheck_Common.gen_mk_parametric_generator_expr 
-    ((mk_generator_expr, absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT))),
-      @{typ "code_numeral"} --> resultT)
+    ((mk_generator_expr,
+      absdummy @{typ bool} (absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT)))),
+      @{typ bool} --> @{typ "code_numeral"} --> resultT)
 
 fun mk_validator_expr ctxt t =
   let
@@ -399,7 +404,7 @@
     fun mk_bounded_forall (Free (s, T)) t =
       Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
         $ lambda (Free (s, T)) t $ depth
-    fun mk_safe_if (cond, then_t, else_t) = mk_if (cond, then_t, else_t true)
+    fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
     val mk_test_term =
       mk_test_term lookup mk_bounded_forall mk_safe_if @{term True} (K @{term False}) ctxt
   in lambda depth (mk_test_term t) end
@@ -422,7 +427,7 @@
 
 structure Counterexample = Proof_Data
 (
-  type T = unit -> int -> int -> (bool * term list) option
+  type T = unit -> int -> bool -> int -> (bool * term list) option
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
@@ -458,9 +463,10 @@
     val compile = Code_Runtime.dynamic_value_strict
       (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
       thy (SOME target) (fn proc => fn g =>
-        fn card => fn size => g card size |> (Option.map o apsnd o map) proc) t' []
+        fn card => fn genuine_only => fn size => g card genuine_only size
+          |> (Option.map o apsnd o map) proc) t' []
   in
-    fn [card, size] => rpair NONE (compile card size |> 
+    fn genuine_only => fn [card, size] => rpair NONE (compile card genuine_only size |> 
       (if Config.get ctxt quickcheck_pretty then
         Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
   end;
diff -r fe2fd2f76f48 -r 97be233b32ed src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 14:47:01 2011 +0100
@@ -222,10 +222,11 @@
   let val ({elapsed, ...}, result) = Timing.timing e ()
   in (result, (description, Time.toMilliseconds elapsed)) end
   
-fun value (contains_existentials, ((potential, quiet), size)) ctxt cookie (code, value_name) =
+fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code, value_name) =
   let
-    val (get, put, put_ml) = cookie
+    val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
     fun message s = if quiet then () else Output.urgent_message s
+    fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
     val current_size = Unsynchronized.ref 0
     val current_result = Unsynchronized.ref Quickcheck.empty_result 
     fun excipit () =
@@ -260,20 +261,20 @@
         val _ = Quickcheck.add_timing compilation_time current_result
         fun haskell_string_of_bool v = if v then "True" else "False"
         val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
-        fun with_size k =
+        fun with_size genuine_only k =
           if k > size then
             (NONE, !current_result)
           else
             let
-              val _ = message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
+              val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
               val _ = current_size := k
               val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
                 (fn () => Isabelle_System.bash_output
-                  (executable ^ " " ^ haskell_string_of_bool potential  ^ " " ^ string_of_int k))
+                  (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
               val _ = Quickcheck.add_timing timing current_result
             in
               if response = "NONE\n" then
-                with_size (k + 1)
+                with_size genuine_only (k + 1)
               else
                 let
                   val output_value = the_default "NONE"
@@ -283,10 +284,22 @@
                     ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
                   val ctxt' = ctxt
                     |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
-                    |> Context.proof_map (exec false ml_code);
-                in (get ctxt' (), !current_result) end
+                    |> Context.proof_map (exec false ml_code);                 
+                  val counterexample = get ctxt' ()
+                in
+                  if is_genuine counterexample then
+                    (counterexample, !current_result)
+                  else
+                    let
+                      val cex = Option.map (rpair []) (counterexample_of counterexample)
+                    in
+                      (message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+                      message "Quickcheck continues to find a genuine counterexample...";
+                      with_size true (k + 1))
+                    end
+               end
             end 
-      in with_size 0 end
+      in with_size genuine_only 0 end
   in
     with_tmp_dir tmp_prefix run
   end;
@@ -294,8 +307,9 @@
 fun dynamic_value_strict opts cookie thy postproc t =
   let
     val ctxt = Proof_Context.init_global thy
-    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value opts ctxt cookie)
-      (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
+    fun evaluator naming program ((_, vs_ty), t) deps =
+      Exn.interruptible_capture (value opts ctxt cookie)
+        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
 
 (** counterexample generator **)
@@ -418,7 +432,8 @@
   let
     fun dest_result (Quickcheck.Result r) = r 
     val opts =
-      ((Config.get ctxt Quickcheck.potential, Config.get ctxt Quickcheck.quiet),
+      ((Config.get ctxt Quickcheck.genuine_only,
+       (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)),
         Config.get ctxt Quickcheck.size)
     val thy = Proof_Context.theory_of ctxt
     val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
@@ -432,8 +447,8 @@
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
         val (counterexample, result) = dynamic_value_strict (true, opts)
-          (Existential_Counterexample.get, Existential_Counterexample.put,
-            "Narrowing_Generators.put_existential_counterexample")
+          ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
+            "Narrowing_Generators.put_existential_counterexample"))
           thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
       in
         Quickcheck.Result
@@ -443,18 +458,22 @@
       end
     else
       let
-        val t' = fold_rev absfree (Term.add_frees t []) t
+        val frees = Term.add_frees t []
+        val t' = fold_rev absfree frees t
         fun wrap f t = list_abs (f (strip_abs t))
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         fun ensure_testable t =
           Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
+        fun is_genuine (SOME (true, _)) = true 
+          | is_genuine _ = false
+        val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
         val (counterexample, result) = dynamic_value_strict (false, opts)
-          (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
+          ((is_genuine, counterexample_of),
+            (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
           thy (apfst o Option.map o apsnd o map) (ensure_testable (finitize t'))
       in
         Quickcheck.Result
-         {counterexample =
-           Option.map (apsnd (((curry (op ~~)) (Term.add_free_names t [])) o map post_process)) counterexample,
+         {counterexample = counterexample_of counterexample,
           evaluation_terms = Option.map (K []) counterexample,
           timings = #timings (dest_result result), reports = #reports (dest_result result)}
       end
@@ -463,6 +482,7 @@
 fun test_goals ctxt _ insts goals =
   if (not (getenv "ISABELLE_GHC" = "")) then
     let
+      val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-narrowing...")
       val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
     in
       Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
diff -r fe2fd2f76f48 -r 97be233b32ed src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 14:47:01 2011 +0100
@@ -14,10 +14,10 @@
     -> (string * sort -> string * sort) option
   val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     -> (typ option * (term * term list)) list list
-  val mk_safe_if : Proof.context -> term * term * (bool -> term) -> term
+  val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
   val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
   type compile_generator =
-    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
   val generator_test_goal_terms :
     string * compile_generator -> Proof.context -> bool -> (string * typ) list
     -> (term * term list) list -> Quickcheck.result list
@@ -53,7 +53,7 @@
 (* testing functions: testing with increasing sizes (and cardinalities) *)
 
 type compile_generator =
-  Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
+  Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
 
 fun check_test_term t =
   let
@@ -69,31 +69,44 @@
 
 fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) =
   let
+    val genuine_only = Config.get ctxt Quickcheck.genuine_only
     val _ = check_test_term t
     val names = Term.add_free_names t []
     val current_size = Unsynchronized.ref 0
     val current_result = Unsynchronized.ref Quickcheck.empty_result 
     fun excipit () =
       "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
-    fun with_size test_fun k =
+    val act = if catch_code_errors then try else (fn f => SOME o f) 
+    val (test_fun, comp_time) = cpu_time "quickcheck compilation"
+        (fn () => act (compile ctxt) [(t, eval_terms)]);
+    val _ = Quickcheck.add_timing comp_time current_result
+    fun with_size test_fun genuine_only k =
       if k > Config.get ctxt Quickcheck.size then
         NONE
       else
         let
-          val _ = Quickcheck.message ctxt
-            ("[Quickcheck-" ^ name ^ "]Test data size: " ^ string_of_int k)
+          val _ = Quickcheck.verbose_message ctxt
+            ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
           val _ = current_size := k
           val ((result, report), timing) =
-            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
+            cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
           val _ = Quickcheck.add_timing timing current_result
           val _ = Quickcheck.add_report k report current_result
         in
-          case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
+          case result of
+            NONE => with_size test_fun genuine_only (k + 1)
+          | SOME (true, ts) => SOME (true, ts)
+          | SOME (false, ts) =>
+            let
+              val (ts1, ts2) = chop (length names) ts
+              val (eval_terms', _) = chop (length ts2) eval_terms
+              val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+            in
+              (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+              Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
+              with_size test_fun true k)
+            end
         end;
-    val act = if catch_code_errors then try else (fn f => SOME o f) 
-    val (test_fun, comp_time) = cpu_time "quickcheck compilation"
-        (fn () => act (compile ctxt) [(t, eval_terms)]);
-    val _ = Quickcheck.add_timing comp_time current_result
   in
     case test_fun of
       NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
@@ -101,7 +114,7 @@
     | SOME test_fun =>
       let
         val (response, exec_time) =
-          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
+          cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
         val _ = Quickcheck.add_response names eval_terms response current_result
         val _ = Quickcheck.add_timing exec_time current_result
       in !current_result end
@@ -147,25 +160,26 @@
 
 fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
   let
+    val genuine_only = Config.get ctxt Quickcheck.genuine_only
     val thy = Proof_Context.theory_of ctxt
     val (ts', eval_terms) = split_list ts
     val _ = map check_test_term ts'
     val names = Term.add_free_names (hd ts') []
     val Ts = map snd (Term.add_frees (hd ts') [])
     val current_result = Unsynchronized.ref Quickcheck.empty_result
-    fun test_card_size test_fun (card, size) =
+    fun test_card_size test_fun genuine_only (card, size) =
       (* FIXME: why decrement size by one? *)
       let
         val _ =
-          Quickcheck.message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
+          Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
             (if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
             "cardinality: " ^ string_of_int card)          
         val (ts, timing) =
           cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
-            (fn () => fst (test_fun [card, size - 1]))
+            (fn () => fst (test_fun genuine_only [card, size - 1]))
         val _ = Quickcheck.add_timing timing current_result
       in
-        Option.map (pair card) ts
+        Option.map (pair (card, size)) ts
       end
     val enumeration_card_size =
       if forall (fn T => Sign.of_sort thy (T,  ["Enum.enum"])) Ts then
@@ -184,10 +198,22 @@
         !current_result)
     | SOME test_fun =>
       let
-        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
-          SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
+        val _ = Quickcheck.message ctxt ("Testing conjecture with with Quickcheck-" ^ name ^ "...");
+        fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
+          SOME ((card, _), (true, ts)) =>
+            Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
+        | SOME ((card, size), (false, ts)) =>
+           let
+              val (ts1, ts2) = chop (length names) ts
+              val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
+              val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+            in
+              (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+              Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
+              test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))
+            end
         | NONE => ()
-      in !current_result end
+      in (test genuine_only enumeration_card_size; !current_result) end
   end
 
 fun get_finite_types ctxt =
@@ -270,11 +296,15 @@
 
 (* compilation of testing functions *)
 
-fun mk_safe_if ctxt (cond, then_t, else_t) =
-  @{term "Quickcheck.catch_match :: (bool * term list) option => (bool * term list) option => (bool * term list) option"}
-    $ (@{term "If :: bool => (bool * term list) option => (bool * term list) option => (bool * term list) option"}
-      $ cond $ then_t $ else_t true)
-    $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: (bool * term list) option"});
+fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine =
+  let
+    val T = fastype_of then_t
+    val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
+  in
+    Const (@{const_name "Quickcheck.catch_match"}, T --> T --> T) $ 
+      (if_t $ cond $ then_t $ else_t genuine) $
+      (if_t $ genuine_only $ none $ else_t false)
+  end
 
 fun collect_results f [] results = results
   | collect_results f (t :: ts) results =
diff -r fe2fd2f76f48 -r 97be233b32ed src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Dec 05 14:47:01 2011 +0100
@@ -11,10 +11,10 @@
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> term)) * seed
   val compile_generator_expr:
-    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
-  val put_counterexample: (unit -> int -> int -> seed -> (bool * term list) option * seed)
+    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
+  val put_counterexample: (unit -> int -> bool -> int -> seed -> (bool * term list) option * seed)
     -> Proof.context -> Proof.context
-  val put_counterexample_report: (unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed)
+  val put_counterexample_report: (unit -> int -> bool -> int -> seed -> ((bool * term list) option * (bool list * bool)) * seed)
     -> Proof.context -> Proof.context
   val setup: theory -> theory
 end;
@@ -60,7 +60,11 @@
     fun term_fun' () = #3 (! state) ();
   in ((random_fun', term_fun'), seed''') end;
 
-
+fun mk_if (b, t, e) =
+  let
+    val T = fastype_of t
+  in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
+  
 (** datatypes **)
 
 (* definitional scheme for random instances on datatypes *)
@@ -272,7 +276,7 @@
 
 structure Counterexample = Proof_Data
 (
-  type T = unit -> int -> int -> int * int -> (bool * term list) option * (int * int)
+  type T = unit -> int -> bool -> int -> int * int -> (bool * term list) option * (int * int)
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
@@ -280,7 +284,7 @@
 
 structure Counterexample_Report = Proof_Data
 (
-  type T = unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed
+  type T = unit -> int -> bool -> int -> seed -> ((bool * term list) option * (bool list * bool)) * seed
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample_Report"
 );
@@ -298,7 +302,10 @@
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
-    val check = Quickcheck_Common.mk_safe_if ctxt (result, Const (@{const_name "None"}, resultT),
+    val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
+    val genuine_only = Free (genuine_only_name, @{typ bool})
+    val none_t = Const (@{const_name "None"}, resultT)
+    val check = Quickcheck_Common.mk_safe_if genuine_only none_t (result, none_t,
       fn genuine => @{term "Some :: bool * term list => (bool * term list) option"} $
         HOLogic.mk_prod (Quickcheck_Common.reflect_bool genuine, terms))
     val return = HOLogic.pair_const resultT @{typ Random.seed};
@@ -313,11 +320,15 @@
         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
     fun mk_bindclause (_, _, i, T) = mk_scomp_split T
       (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
-  in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
+  in
+    lambda genuine_only
+      (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
+  end;
 
 fun mk_reporting_generator_expr ctxt (t, eval_terms) =
   let
     val thy = Proof_Context.theory_of ctxt
+    val resultT = @{typ "(bool * term list) option * (bool list * bool)"}
     val prop = fold_rev absfree (Term.add_frees t []) t
     val Ts = (map snd o fst o strip_abs) prop
     val bound_max = length Ts - 1
@@ -326,55 +337,52 @@
     val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
     val (assms, concl) = Quickcheck_Common.strip_imp prop'
-    val return =
-      @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
+    val return = HOLogic.pair_const resultT @{typ "Random.seed"};
     fun mk_assms_report i =
-      HOLogic.mk_prod (@{term "None :: term list option"},
+      HOLogic.mk_prod (@{term "None :: (bool * term list) option"},
         HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
           (replicate i @{term True} @ replicate (length assms - i) @{term False}),
         @{term False}))
     fun mk_concl_report b =
       HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}),
-        if b then @{term True} else @{term False})
-    val If =
-      @{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}
-    val concl_check = If $ concl $
-      HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true) $
-      HOLogic.mk_prod (@{term "Some :: term list => term list option"} $ terms, mk_concl_report false)
-    val check = fold_rev (fn (i, assm) => fn t => If $ assm $ t $ mk_assms_report i)
+        Quickcheck_Common.reflect_bool b)
+    val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
+    val genuine_only = Free (genuine_only_name, @{typ bool})
+    val none_t = HOLogic.mk_prod (@{term "None :: (bool * term list) option"}, mk_concl_report true)
+    val concl_check = Quickcheck_Common.mk_safe_if genuine_only none_t (concl, none_t,
+      fn genuine => HOLogic.mk_prod (@{term "Some :: bool * term list => (bool * term list) option"} $
+        HOLogic.mk_prod (Quickcheck_Common.reflect_bool genuine, terms), mk_concl_report false))
+    val check = fold_rev (fn (i, assm) => fn t => Quickcheck_Common.mk_safe_if genuine_only
+      (mk_assms_report i) (HOLogic.mk_not assm, mk_assms_report i, t))
       (map_index I assms) concl_check
-    val check' = @{term "Quickcheck.catch_match :: term list option * bool list * bool =>
-      term list option * bool list * bool => term list option * bool list * bool"} $ check $
-      (if Config.get ctxt Quickcheck.potential then
-        HOLogic.mk_prod (@{term "Some :: term list  => term list option"} $ terms, mk_concl_report false)
-      else
-        HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true))
     fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
     fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
     fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
       liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
     fun mk_split T = Sign.mk_const thy
-      (@{const_name prod_case}, [T, @{typ "unit => term"},
-        liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
+      (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
     fun mk_scomp_split T t t' =
-      mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
+      mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
     fun mk_bindclause (_, _, i, T) = mk_scomp_split T
       (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
   in
-    Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check'))
+    lambda genuine_only
+      (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
   end
 
 val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   ((mk_generator_expr, 
-    absdummy @{typ code_numeral} @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"}),
-    @{typ "code_numeral => Random.seed => (bool * term list) option * Random.seed"})
+    absdummy @{typ bool} (absdummy @{typ code_numeral}
+      @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"})),
+    @{typ "bool => code_numeral => Random.seed => (bool * term list) option * Random.seed"})
 
 val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   ((mk_reporting_generator_expr,
-    absdummy @{typ code_numeral}
-      @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"}),
-    @{typ "code_numeral => Random.seed => (term list option * (bool list * bool)) * Random.seed"})
+    absdummy @{typ bool} (absdummy @{typ code_numeral}
+      @{term "Pair (None, ([], False)) :: Random.seed =>
+        ((bool * term list) option * (bool list * bool)) * Random.seed"})),
+    @{typ "bool => code_numeral => Random.seed => ((bool * term list) option * (bool list * bool)) * Random.seed"})
     
     
 (* single quickcheck report *)
@@ -408,19 +416,22 @@
         val t' = mk_parametric_reporting_generator_expr ctxt ts;
         val compile = Code_Runtime.dynamic_value_strict
           (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
-          thy (SOME target) (fn proc => fn g => fn c => fn s => g c s #>> (apfst o Option.map o map) proc) t' [];
-        fun single_tester c s = compile c s |> Random_Engine.run
-        fun iterate_and_collect (card, size) 0 report = (NONE, report)
-          | iterate_and_collect (card, size) j report =
+          thy (SOME target)
+          (fn proc => fn g => fn c => fn b => fn s => g c b s
+            #>> (apfst o Option.map o apsnd o map) proc) t' [];
+        fun single_tester c b s = compile c b s |> Random_Engine.run
+        fun iterate_and_collect _ (card, size) 0 report = (NONE, report)
+          | iterate_and_collect genuine_only (card, size) j report =
             let
-              val (test_result, single_report) = apsnd Run (single_tester card size)
+              val (test_result, single_report) = apsnd Run (single_tester card genuine_only size)
               val report = collect_single_report single_report report
             in
-              case test_result of NONE => iterate_and_collect (card, size) (j - 1) report
-                | SOME q => (SOME (true, q), report)
+              case test_result of NONE => iterate_and_collect genuine_only (card, size) (j - 1) report
+                | SOME q => (SOME q, report)
             end
       in
-        fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
+        fn genuine_only => fn [card, size] =>
+          apsnd SOME (iterate_and_collect genuine_only (card, size) iterations empty_report)
       end
     else
       let
@@ -428,13 +439,17 @@
         val compile = Code_Runtime.dynamic_value_strict
           (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
           thy (SOME target)
-          (fn proc => fn g => fn c => fn s =>g c s #>> (Option.map o apsnd o map) proc) t' [];
-        fun single_tester c s = compile c s |> Random_Engine.run
-        fun iterate (card, size) 0 = NONE
-          | iterate (card, size) j =
-            case single_tester card size of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
+          (fn proc => fn g => fn c => fn b => fn s => g c b s
+            #>> (Option.map o apsnd o map) proc) t' [];
+        fun single_tester c b s = compile c b s |> Random_Engine.run
+        fun iterate _ (card, size) 0 = NONE
+          | iterate genuine_only (card, size) j =
+            case single_tester card genuine_only size of
+              NONE => iterate genuine_only (card, size) (j - 1)
+            | SOME q => SOME q
       in
-        fn [card, size] => (rpair NONE (iterate (card, size) iterations))
+        fn genuine_only => fn [card, size] =>
+          (rpair NONE (iterate genuine_only (card, size) iterations))
       end
   end;
 
diff -r fe2fd2f76f48 -r 97be233b32ed src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Dec 05 14:47:01 2011 +0100
@@ -411,25 +411,22 @@
 
 lemma
   "xs = [] ==> hd xs \<noteq> x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
 oops
 
 lemma
   "xs = [] ==> hd xs = x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
 oops
 
 lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
 oops
 
 text {* with the simple testing scheme *}
@@ -439,19 +436,16 @@
 
 lemma
   "xs = [] ==> hd xs \<noteq> x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
 oops
 
 lemma
   "xs = [] ==> hd xs = x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
 oops
 
 lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
 oops
 
 declare [[quickcheck_full_support = true]]
diff -r fe2fd2f76f48 -r 97be233b32ed src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Dec 05 14:44:46 2011 +0100
+++ b/src/Tools/quickcheck.ML	Mon Dec 05 14:47:01 2011 +0100
@@ -20,8 +20,9 @@
   val no_assms : bool Config.T
   val report : bool Config.T
   val timing : bool Config.T
-  val potential : bool Config.T
+  val genuine_only : bool Config.T
   val quiet : bool Config.T
+  val verbose : bool Config.T
   val timeout : real Config.T
   val allow_function_inversion : bool Config.T;
   val finite_types : bool Config.T
@@ -62,7 +63,10 @@
       -> Context.generic -> Context.generic
   (* basic operations *)
   val message : Proof.context -> string -> unit
+  val verbose_message : Proof.context -> string -> unit
   val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a
+  val pretty_counterex : Proof.context -> bool ->
+    ((bool * (string * term) list) * (term * term) list) option -> Pretty.T
   (* testing terms and proof states *)
   val mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
   val mk_batch_tester : Proof.context -> term list -> (int -> term list option) list option
@@ -172,8 +176,9 @@
 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
-val potential = Attrib.setup_config_bool @{binding quickcheck_potential} (K true)
+val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
 val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
+val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
 val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
 val allow_function_inversion =
   Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
@@ -288,11 +293,15 @@
     f ()
 
 fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s
-  
+
+fun verbose_message ctxt s = if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
+  then Output.urgent_message s else ()
+
 fun test_terms ctxt (limit_time, is_interactive) insts goals =
   case active_testers ctxt of
     [] => error "No active testers for quickcheck"
-  | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
+  | testers =>
+    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
       (fn () => Par_List.get_some (fn tester =>
       tester ctxt (length testers > 1) insts goals |>
       (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
@@ -302,6 +311,7 @@
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
+    val _ = message lthy "Quickchecking..."
     fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
       | strip t = t;
     val {goal = st, ...} = Proof.raw_goal state;
@@ -412,8 +422,9 @@
   | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
   | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
   | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
-  | parse_test_param ("potential", [arg]) = apsnd (Config.put_generic potential (read_bool arg))
+  | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
   | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
+  | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
   | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
   | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
   | parse_test_param ("allow_function_inversion", [arg]) =