src/HOL/ex/Quickcheck_Examples.thy

--- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Nov 22 10:42:07 2010 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Nov 22 11:34:50 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/ex/Quickcheck_Examples.thy
-    Author:     Stefan Berghofer
-    Copyright   2004 TU Muenchen
+    Author:     Stefan Berghofer, Lukas Bulwahn
+    Copyright   2004 - 2010 TU Muenchen
 *)
 
 header {* Examples for the 'quickcheck' command *}
@@ -19,19 +19,24 @@
 subsection {* Lists *}
 
 theorem "map g (map f xs) = map (g o f) xs"
-  quickcheck[expect = no_counterexample]
+  quickcheck[size = 3]
+  quickcheck[generator = random, expect = no_counterexample]
+  quickcheck[generator = small, size = 3, iterations = 1, report = false, expect = no_counterexample]
   oops
 
 theorem "map g (map f xs) = map (f o g) xs"
-  quickcheck[expect = counterexample]
+  quickcheck[generator = random, expect = counterexample]
+  quickcheck[generator = small, report = false]
   oops
 
 theorem "rev (xs @ ys) = rev ys @ rev xs"
   quickcheck[expect = no_counterexample]
+  quickcheck[generator = small, expect = no_counterexample, report = false]
   oops
 
 theorem "rev (xs @ ys) = rev xs @ rev ys"
-  quickcheck[expect = counterexample]
+  quickcheck[generator = small, expect = counterexample, report = false]
+  quickcheck[generator = random, expect = counterexample]
   oops
 
 theorem "rev (rev xs) = xs"
@@ -39,6 +44,7 @@
   oops
 
 theorem "rev xs = xs"
+  quickcheck[generator = small]
   quickcheck[expect = counterexample]
   oops
 
@@ -49,11 +55,13 @@
   | "app (f # fs) x = app fs (f x)"
 
 lemma "app (fs @ gs) x = app gs (app fs x)"
-  quickcheck[expect = no_counterexample]
+  quickcheck[generator = random, expect = no_counterexample]
+  quickcheck[generator = small, iterations = 1, size = 4, expect = no_counterexample]
   by (induct fs arbitrary: x) simp_all
 
 lemma "app (fs @ gs) x = app fs (app gs x)"
-  quickcheck[expect = counterexample]
+  quickcheck[generator = random, expect = counterexample]
+  quickcheck[generator = small, expect = counterexample]
   oops
 
 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
@@ -67,15 +75,18 @@
 text {* A lemma, you'd think to be true from our experience with delAll *}
 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
   -- {* Wrong. Precondition needed.*}
+  quickcheck[generator = small]
   quickcheck[expect = counterexample]
   oops
 
 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+  quickcheck[generator = small]
   quickcheck[expect = counterexample]
     -- {* Also wrong.*}
   oops
 
 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+  quickcheck[generator = small]
   quickcheck[expect = no_counterexample]
   by (induct xs) auto
 
@@ -85,6 +96,7 @@
                             else (x#(replace a b xs)))"
 
 lemma "occurs a xs = occurs b (replace a b xs)"
+  quickcheck[generator = small]
   quickcheck[expect = counterexample]
   -- {* Wrong. Precondition needed.*}
   oops
@@ -133,8 +145,88 @@
   | "root (Node f x y) = f"
 
 theorem "hd (inOrder xt) = root xt"
+  quickcheck[generator = small]
   quickcheck[expect = counterexample]
     --{* Wrong! *} 
   oops
 
+
+subsection {* Exhaustive Testing beats Random Testing *}
+
+text {* Here are some examples from mutants from the List theory
+where exhaustive testing beats random testing *}
+
+lemma
+  "[] ~= xs ==> hd xs = last (x # xs)"
+quickcheck[generator = random]
+quickcheck[generator = small, report = false, expect = counterexample]
+oops
+
+lemma
+  assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
+  shows "drop n xs = takeWhile P xs"
+quickcheck[generator = random, iterations = 10000, report = false, quiet]
+quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
+oops
+
+lemma
+  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
+quickcheck[generator = random, iterations = 10000, report = false, quiet]
+quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
+oops
+
+lemma
+  "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
+quickcheck[generator = random, iterations = 10000, report = false, quiet]
+quickcheck[generator = small, expect = counterexample]
+oops
+
+lemma
+  "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
+quickcheck[generator = random, iterations = 1000, report = false, quiet]
+quickcheck[generator = small, expect = counterexample]
+oops
+
+lemma
+  "ns ! k < length ns ==> k <= listsum ns"
+quickcheck[generator = random, iterations = 10000, report = true, quiet]
+quickcheck[generator = small, expect = counterexample]
+oops
+
+lemma
+  "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
+quickcheck[generator = random, iterations = 10000, report = true]
+quickcheck[generator = small, expect = counterexample]
+oops
+
+lemma
+"i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
+quickcheck[generator = random]
+quickcheck[generator = small, expect = counterexample]
+oops
+
+lemma
+  "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
+quickcheck[generator = random]
+quickcheck[generator = small, expect = counterexample]
+oops
+
+lemma
+  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
+quickcheck[generator = random]
+quickcheck[generator = small]
+oops
+
+lemma
+  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. {..<i} (length ys)]"
+quickcheck[generator = random]
+quickcheck[generator = small, expect = counterexample]
+oops
+
+lemma
+  "(ys = zs) = (xs @ ys = splice xs zs)"
+quickcheck[generator = random]
+quickcheck[generator = small, expect = counterexample]
+oops
+
 end