src/HOL/Tools/Quickcheck/quickcheck_common.ML

 *)
 
 signature QUICKCHECK_COMMON =
 sig
   val strip_imp : term -> (term list * term)
+  val reflect_bool : bool -> term
   val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
     -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context 
   val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
     -> (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 * term) -> term
+  val mk_safe_if : Proof.context -> term * term * (bool -> term) -> 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 -> term list option * Quickcheck.report option
   val generator_test_goal_terms :
     string * compile_generator -> Proof.context -> bool -> (string * typ) list

 
 (* HOLogic's term functions *)
 
 fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
   | strip_imp A = ([], A)
+
+fun reflect_bool b = if b then @{term "True"} else @{term "False"}
 
 fun mk_undefined T = Const(@{const_name undefined}, T)
 
 (* testing functions: testing with increasing sizes (and cardinalities) *)
 

              handle TimeLimit.TimeOut => NONE)) test_funs)
   in
     (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
       [comp_time, exec_time])
   end
-
 
 fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
   let
     val thy = Proof_Context.theory_of ctxt
     val (ts', eval_terms) = split_list ts

   end
 
 (* compilation of testing functions *)
 
 fun mk_safe_if ctxt (cond, then_t, else_t) =
-  @{term "Quickcheck.catch_match :: term list option => term list option => term list option"}
-    $ (@{term "If :: bool => term list option => term list option => term list option"}
-      $ cond $ then_t $ else_t)
-    $ (if Config.get ctxt Quickcheck.potential then else_t else @{term "None :: term list option"});  
+  @{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 :: term list option"});  
 
 fun collect_results f [] results = results
   | collect_results f (t :: ts) results =
     let
       val result = f t

 (** generic parametric compilation **)
 
 fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts =
   let
     val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
-    fun mk_if (index, (t, eval_terms)) else_t =
-      if_t $ (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
+    fun mk_if (index, (t, eval_terms)) else_t = if_t $
+        (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
         (mk_generator_expr ctxt (t, eval_terms)) $ else_t
   in
     absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
   end