14592

1 
(* Title: HOL/ex/Quickcheck_Examples.thy


2 
ID: $Id$


3 
Author: Stefan Berghofer


4 
Copyright 2004 TU Muenchen


5 
*)


6 


7 
header {* Examples for the 'quickcheck' command *}


8 

16417

9 
theory Quickcheck_Examples imports Main begin

14592

10 


11 
text {*


12 
The 'quickcheck' command allows to find counterexamples by evaluating


13 
formulae under an assignment of free variables to random values.


14 
In contrast to 'refute', it can deal with inductive datatypes,


15 
but cannot handle quantifiers.


16 
*}


17 


18 
subsection {* Lists *}


19 


20 
theorem "map g (map f xs) = map (g o f) xs"


21 
quickcheck


22 
oops


23 


24 
theorem "map g (map f xs) = map (f o g) xs"


25 
quickcheck


26 
oops


27 


28 
theorem "rev (xs @ ys) = rev ys @ rev xs"


29 
quickcheck


30 
oops


31 


32 
theorem "rev (xs @ ys) = rev xs @ rev ys"


33 
quickcheck


34 
oops


35 


36 
theorem "rev (rev xs) = xs"


37 
quickcheck


38 
oops


39 


40 
theorem "rev xs = xs"


41 
quickcheck


42 
oops


43 


44 
consts


45 
occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"


46 
primrec


47 
"occurs a [] = 0"


48 
"occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"


49 


50 
consts


51 
del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"


52 
primrec


53 
"del1 a [] = []"


54 
"del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"


55 


56 
(* A lemma, you'd think to be true from our experience with delAll*)


57 
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"


58 
 {* Wrong. Precondition needed.*}


59 
quickcheck


60 
oops


61 


62 
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"


63 
quickcheck


64 
 {* Also wrong.*}


65 
oops


66 


67 
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"


68 
quickcheck


69 
apply (induct_tac xs)


70 
apply auto


71 
 {* Correct! *}


72 
done


73 


74 
consts


75 
replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"


76 
primrec


77 
"replace a b [] = []"


78 
"replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))


79 
else (x#(replace a b xs)))"


80 


81 
lemma "occurs a xs = occurs b (replace a b xs)"


82 
quickcheck


83 
 {* Wrong. Precondition needed.*}


84 
oops


85 


86 
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"


87 
quickcheck


88 
apply (induct_tac xs)


89 
apply auto


90 
done


91 


92 


93 
subsection {* Trees *}


94 


95 
datatype 'a tree = Twig  Leaf 'a  Branch "'a tree" "'a tree"


96 


97 
consts


98 
leaves :: "'a tree \<Rightarrow> 'a list"


99 
primrec


100 
"leaves Twig = []"


101 
"leaves (Leaf a) = [a]"


102 
"leaves (Branch l r) = (leaves l) @ (leaves r)"


103 


104 
consts


105 
plant :: "'a list \<Rightarrow> 'a tree"


106 
primrec


107 
"plant [] = Twig "


108 
"plant (x#xs) = Branch (Leaf x) (plant xs)"


109 


110 
consts


111 
mirror :: "'a tree \<Rightarrow> 'a tree"


112 
primrec


113 
"mirror (Twig) = Twig "


114 
"mirror (Leaf a) = Leaf a "


115 
"mirror (Branch l r) = Branch (mirror r) (mirror l)"


116 


117 
theorem "plant (rev (leaves xt)) = mirror xt"


118 
quickcheck


119 
{* Wrong! *}


120 
oops


121 


122 
theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"


123 
quickcheck


124 
{* Wrong! *}


125 
oops


126 


127 
datatype 'a ntree = Tip "'a"  Node "'a" "'a ntree" "'a ntree"


128 


129 
consts


130 
inOrder :: "'a ntree \<Rightarrow> 'a list"


131 
primrec


132 
"inOrder (Tip a)= [a]"


133 
"inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"


134 


135 
consts


136 
root :: "'a ntree \<Rightarrow> 'a"


137 
primrec


138 
"root (Tip a) = a"


139 
"root (Node f x y) = f"


140 


141 
theorem "hd(inOrder xt) = root xt"


142 
quickcheck


143 
{* Wrong! *}


144 
oops


145 


146 
end


147 


148 
