src/HOL/ex/Quickcheck_Examples.thy
 changeset 14592 dd1a2905ea73 child 16417 9bc16273c2d4
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Fri Apr 16 18:09:24 2004 +0200
1.3 @@ -0,0 +1,148 @@
1.4 +(*  Title:      HOL/ex/Quickcheck_Examples.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Stefan Berghofer
1.7 +    Copyright   2004 TU Muenchen
1.8 +*)
1.9 +
1.10 +header {* Examples for the 'quickcheck' command *}
1.11 +
1.12 +theory Quickcheck_Examples = Main:
1.13 +
1.14 +text {*
1.15 +The 'quickcheck' command allows to find counterexamples by evaluating
1.16 +formulae under an assignment of free variables to random values.
1.17 +In contrast to 'refute', it can deal with inductive datatypes,
1.18 +but cannot handle quantifiers.
1.19 +*}
1.20 +
1.21 +subsection {* Lists *}
1.22 +
1.23 +theorem "map g (map f xs) = map (g o f) xs"
1.24 +  quickcheck
1.25 +  oops
1.26 +
1.27 +theorem "map g (map f xs) = map (f o g) xs"
1.28 +  quickcheck
1.29 +  oops
1.30 +
1.31 +theorem "rev (xs @ ys) = rev ys @ rev xs"
1.32 +  quickcheck
1.33 +  oops
1.34 +
1.35 +theorem "rev (xs @ ys) = rev xs @ rev ys"
1.36 +  quickcheck
1.37 +  oops
1.38 +
1.39 +theorem "rev (rev xs) = xs"
1.40 +  quickcheck
1.41 +  oops
1.42 +
1.43 +theorem "rev xs = xs"
1.44 +  quickcheck
1.45 +  oops
1.46 +
1.47 +consts
1.48 +  occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
1.49 +primrec
1.50 +  "occurs a [] = 0"
1.51 +  "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
1.52 +
1.53 +consts
1.54 +  del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.55 +primrec
1.56 +  "del1 a [] = []"
1.57 +  "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
1.58 +
1.59 +(* A lemma, you'd think to be true from our experience with delAll*)
1.60 +lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
1.61 +  -- {* Wrong. Precondition needed.*}
1.62 +  quickcheck
1.63 +  oops
1.64 +
1.65 +lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
1.66 +  quickcheck
1.67 +    -- {* Also wrong.*}
1.68 +  oops
1.69 +
1.70 +lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
1.71 +  quickcheck
1.72 +  apply (induct_tac xs)
1.73 +  apply auto
1.74 +    -- {* Correct! *}
1.75 +  done
1.76 +
1.77 +consts
1.78 +  replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.79 +primrec
1.80 +  "replace a b [] = []"
1.81 +  "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
1.82 +                            else (x#(replace a b xs)))"
1.83 +
1.84 +lemma "occurs a xs = occurs b (replace a b xs)"
1.85 +  quickcheck
1.86 +  -- {* Wrong. Precondition needed.*}
1.87 +  oops
1.88 +
1.89 +lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
1.90 +  quickcheck
1.91 +  apply (induct_tac xs)
1.92 +  apply auto
1.93 +  done
1.94 +
1.95 +
1.96 +subsection {* Trees *}
1.97 +
1.98 +datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
1.99 +
1.100 +consts
1.101 +  leaves :: "'a tree \<Rightarrow> 'a list"
1.102 +primrec
1.103 +  "leaves Twig = []"
1.104 +  "leaves (Leaf a) = [a]"
1.105 +  "leaves (Branch l r) = (leaves l) @ (leaves r)"
1.106 +
1.107 +consts
1.108 +  plant :: "'a list \<Rightarrow> 'a tree"
1.109 +primrec
1.110 +  "plant [] = Twig "
1.111 +  "plant (x#xs) = Branch (Leaf x) (plant xs)"
1.112 +
1.113 +consts
1.114 +  mirror :: "'a tree \<Rightarrow> 'a tree"
1.115 +primrec
1.116 +  "mirror (Twig) = Twig "
1.117 +  "mirror (Leaf a) = Leaf a "
1.118 +  "mirror (Branch l r) = Branch (mirror r) (mirror l)"
1.119 +
1.120 +theorem "plant (rev (leaves xt)) = mirror xt"
1.121 +  quickcheck
1.122 +    --{* Wrong! *}
1.123 +  oops
1.124 +
1.125 +theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
1.126 +  quickcheck
1.127 +    --{* Wrong! *}
1.128 +  oops
1.129 +
1.130 +datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
1.131 +
1.132 +consts
1.133 +  inOrder :: "'a ntree \<Rightarrow> 'a list"
1.134 +primrec
1.135 +  "inOrder (Tip a)= [a]"
1.136 +  "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
1.137 +
1.138 +consts
1.139 +  root :: "'a ntree \<Rightarrow> 'a"
1.140 +primrec
1.141 +  "root (Tip a) = a"
1.142 +  "root (Node f x y) = f"
1.143 +
1.144 +theorem "hd(inOrder xt) = root xt"
1.145 +  quickcheck
1.146 +    --{* Wrong! *}
1.147 +  oops
1.148 +
1.149 +end
1.150 +
1.151 +
```