# HG changeset patch
# User bulwahn
# Date 1323084966 -3600
# Node ID 90028fd2f1faf5e3dc9cbba03748e1989b52fa71
# Parent  3b5a735897c36db3cc7acf7af02790bbdb51bcb9
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly

diff -r 3b5a735897c3 -r 90028fd2f1fa src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Dec 05 12:36:05 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Dec 05 12:36:06 2011 +0100
@@ -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
 
@@ -404,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
diff -r 3b5a735897c3 -r 90028fd2f1fa src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 12:36:05 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 12:36:06 2011 +0100
@@ -14,7 +14,7 @@
     -> (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 : term -> term * term * (bool -> term) -> term
+  val mk_safe_if : 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 -> bool -> int list -> (bool * term list) option * Quickcheck.report option
@@ -295,13 +295,13 @@
 
 (* compilation of testing functions *)
 
-fun mk_safe_if genuine_only (cond, then_t, else_t) =
+fun mk_safe_if genuine_only (cond, then_t, else_t) genuine =
   let
     val T = @{typ "(bool * term list) option"}
     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 true) $
+      (if_t $ cond $ then_t $ else_t genuine) $
       (if_t $ genuine_only $ Const (@{const_name "None"}, T) $ else_t false)
   end
 
diff -r 3b5a735897c3 -r 90028fd2f1fa src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Dec 05 12:36:05 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Dec 05 12:36:06 2011 +0100
@@ -317,7 +317,7 @@
       (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
   in
     lambda genuine_only
-      (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)))
+      (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
   end;
 
 fun mk_reporting_generator_expr ctxt (t, eval_terms) =