# HG changeset patch
# User bulwahn
# Date 1320942375 -3600
# Node ID 9f4d3e68ae9836e95751919f0771c5dfa408b32e
# Parent  34de78f802aaf8eaee28db6879db497750c64307
adding a minimalistic preprocessing rewriting common boolean operators; tuned

diff -r 34de78f802aa -r 9f4d3e68ae98 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Nov 10 14:46:38 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Nov 10 17:26:15 2011 +0100
@@ -209,6 +209,29 @@
 
 datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
 
+(* minimalistic preprocessing *)
+
+fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) = 
+  let
+    val (a', t') = strip_all t
+  in ((a, T) :: a', t') end
+  | strip_all t = ([], t);
+
+fun preprocess ctxt t =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
+    val rewrs = map (swap o dest) @{thms all_simps} @
+      (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}])
+    val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
+    val (vs, body) = strip_all t'
+    val vs' = Variable.variant_frees ctxt [t'] vs
+  in
+    subst_bounds (map Free (rev vs'), body)
+  end
+
+(* instantiation of type variables with concrete types *)
+ 
 fun instantiate_goals lthy insts goals =
   let
     fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
@@ -219,11 +242,11 @@
       map (fn (check_goal, eval_terms) =>
         if not (null (Term.add_tfree_names check_goal [])) then
           map (fn T =>
-            (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
+            (pair (SOME T) o Term o apfst (preprocess lthy))
               (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
               handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy)
         else
-          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
+          [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
     val error_msg =
       cat_lines
         (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)