# HG changeset patch
# User bulwahn
# Date 1301658578 -7200
# Node ID 1e7b62c93f5d5f55a70f2a543b8c446a4acc814a
# Parent  bd416284a432f92ef107f44b11d1ba0b1ab4f62c
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall

diff -r bd416284a432 -r 1e7b62c93f5d src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 01 13:49:36 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 01 13:49:38 2011 +0200
@@ -355,7 +355,22 @@
 
 end
 
+subsection {* Bounded universal quantifiers *}
 
+class bounded_forall =
+  fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
+
+
+instantiation nat :: bounded_forall
+begin
+
+fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool"
+where
+  "bounded_forall P d = ((P 0) \<and> (if d > 0 then bounded_forall (%n. P (Suc n)) (d - 1) else True))"
+
+instance ..
+
+end
 
 subsection {* Defining combinators for any first-order data type *}
 
diff -r bd416284a432 -r 1e7b62c93f5d src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 01 13:49:36 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 01 13:49:38 2011 +0200
@@ -9,12 +9,14 @@
   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;
 
@@ -238,8 +240,6 @@
       @{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)) 
@@ -255,7 +255,7 @@
       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
@@ -267,7 +267,41 @@
   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
@@ -286,6 +320,15 @@
 );
 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 =
@@ -295,7 +338,7 @@
     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
@@ -310,12 +353,22 @@
       (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 =
@@ -324,6 +377,7 @@
   #> 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;
diff -r bd416284a432 -r 1e7b62c93f5d src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Apr 01 13:49:36 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Apr 01 13:49:38 2011 +0200
@@ -6,6 +6,7 @@
 
 signature QUICKCHECK_COMMON =
 sig
+  val strip_imp : term -> (term list * term)
   val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
     -> (string * sort -> string * sort) option
   val ensure_sort_datatype:
@@ -20,6 +21,11 @@
 structure Quickcheck_Common : QUICKCHECK_COMMON =
 struct
 
+(* HOLogic's term functions *)
+
+fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
+  | strip_imp A = ([], A)
+
 (** ensuring sort constraints **)
 
 fun perhaps_constrain thy insts raw_vs =
diff -r bd416284a432 -r 1e7b62c93f5d src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Apr 01 13:49:36 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Apr 01 13:49:38 2011 +0200
@@ -322,11 +322,9 @@
     val bound_max = length Ts - 1
     val bounds = map_index (fn (i, ty) =>
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
-    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
-      | strip_imp A = ([], A)
     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) = strip_imp prop'
+    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"};
     fun mk_assms_report i =