# HG changeset patch
# User bulwahn
# Date 1320942377 -3600
# Node ID fb4ac1dd4fdeefa72c28135aaa976647e9510df6
# Parent  9f4d3e68ae9836e95751919f0771c5dfa408b32e
adding some test cases for preprocessing and narrowing

diff -r 9f4d3e68ae98 -r fb4ac1dd4fde src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Thu Nov 10 17:26:15 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Thu Nov 10 17:26:17 2011 +0100
@@ -380,4 +380,22 @@
 
 end
 
+subsection {* Examples with HOL quantifiers *}
+
+lemma
+  "\<forall> xs ys. xs = [] --> xs = ys"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+  "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+  "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+
 end
diff -r 9f4d3e68ae98 -r fb4ac1dd4fde src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Thu Nov 10 17:26:15 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Thu Nov 10 17:26:17 2011 +0100
@@ -66,6 +66,11 @@
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
 oops
 
+lemma "a # xs = ys @ [a] ==> EX zs. xs = zs @ [a] & ys = a#zs"
+quickcheck[narrowing, expect = counterexample]
+quickcheck[exhaustive, random, expect = no_counterexample]
+oops
+
 subsection {* Simple list examples *}
 
 lemma "rev xs = xs"