src/HOL/Tools/Quickcheck/exhaustive_generators.ML

 signature EXHAUSTIVE_GENERATORS =
 sig
   val compile_generator_expr:
     Proof.context -> (term * term list) list -> int list -> 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 -> term list option)
     -> Proof.context -> Proof.context
   val put_counterexample_batch: (unit -> (int -> term list option) list)
     -> Proof.context -> Proof.context
-  val smart_quantifier : bool Config.T;
-  val quickcheck_pretty : bool Config.T;
+  val put_validator_batch: (unit -> (int -> bool) list) -> Proof.context -> Proof.context
+  val smart_quantifier : bool Config.T
+  val quickcheck_pretty : bool Config.T
   val setup: theory -> theory
 end;
 
 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
 struct

     val none_t = @{term "None :: term list option"}
     fun mk_safe_if (cond, then_t, else_t) =
       @{term "Quickcheck_Exhaustive.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) $ none_t;
-    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
-        | strip_imp A = ([], A)
     fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
     fun mk_naive_test_term t =
       fold_rev mk_exhaustive_closure (frees ~~ term_vars) (mk_safe_if (t, none_t, return)) 
     fun mk_smart_test_term' concl bound_vars assms =
       let

       in
         fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
       end
     fun mk_smart_test_term t =
       let
-        val (assms, concl) = strip_imp t
+        val (assms, concl) = Quickcheck_Common.strip_imp t
       in
         mk_smart_test_term' concl [] assms
       end
     val mk_test_term =
       if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 

 
 val mk_parametric_generator_expr =
   Quickcheck_Common.gen_mk_parametric_generator_expr 
     ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
       @{typ "code_numeral => term list option"})
-  
+
+fun mk_validator_expr ctxt t =
+  let
+    fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
+    val thy = ProofContext.theory_of ctxt
+    val ctxt' = Variable.auto_fixes t ctxt
+    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+    val depth = Free (depth_name, @{typ code_numeral})
+    fun mk_bounded_forall (s, T) t =
+      Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
+        $ lambda (Free (s, T)) t $ depth
+    fun mk_implies (cond, then_t) =
+      @{term "If :: bool => bool => bool => bool"} $ cond $ then_t $ @{term False}
+    fun mk_naive_test_term t = fold_rev mk_bounded_forall (Term.add_frees t []) t 
+    fun mk_smart_test_term' concl bound_frees assms =
+      let
+        fun vars_of t = subtract (op =) bound_frees (Term.add_frees t [])
+        val (vars, check) =
+          case assms of [] => (vars_of concl, concl)
+            | assm :: assms => (vars_of assm, mk_implies (assm,
+                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_frees) assms))
+      in
+        fold_rev mk_bounded_forall vars check
+      end
+    fun mk_smart_test_term t =
+      let
+        val (assms, concl) = Quickcheck_Common.strip_imp t
+      in
+        mk_smart_test_term' concl [] assms
+      end
+    val mk_test_term =
+      if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
+  in lambda depth (mk_test_term t) end
+
+
 (** generator compiliation **)
 
 structure Counterexample = Proof_Data
 (
   type T = unit -> int -> int -> term list option

   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
 val put_counterexample_batch = Counterexample_Batch.put;
 
+structure Validator_Batch = Proof_Data
+(
+  type T = unit -> (int -> bool) list
+  (* FIXME avoid user error with non-user text *)
+  fun init _ () = error "Counterexample"
+);
+val put_validator_batch = Validator_Batch.put;
+
+
 val target = "Quickcheck";
   
 fun compile_generator_expr ctxt ts =
   let
     val thy = ProofContext.theory_of ctxt
     val t' = mk_parametric_generator_expr ctxt ts;
     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 map) proc) t' [];
+        fn card => fn size => g card size |> (Option.map o map) proc) t' []
   in
     fn [card, size] => rpair NONE (compile card size |> 
       (if Config.get ctxt quickcheck_pretty then
         Option.map (map Quickcheck_Common.post_process_term) else I))
   end;

     val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
     val compiles = Code_Runtime.dynamic_value_strict
       (Counterexample_Batch.get, put_counterexample_batch,
         "Exhaustive_Generators.put_counterexample_batch")
       thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
-      (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') [];
+      (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') []
   in
     map (fn compile => fn size => compile size
       |> Option.map (map Quickcheck_Common.post_process_term)) compiles
   end;
-  
+
+fun compile_validator_exprs ctxt ts =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val ts' = map (mk_validator_expr ctxt) ts;
+  in
+    Code_Runtime.dynamic_value_strict
+      (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
+      thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
+  end;
+
 (** setup **)
 
 val setup =
   Datatype.interpretation
     (Quickcheck_Common.ensure_sort_datatype (@{sort exhaustive}, instantiate_exhaustive_datatype))
   #> setup_smart_quantifier
   #> setup_quickcheck_pretty
   #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
-  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
+  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
+  #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
 
 end;