equal
deleted
inserted
replaced
139 | "mirror (Branch l r) = Branch (mirror r) (mirror l)" |
139 | "mirror (Branch l r) = Branch (mirror r) (mirror l)" |
140 |
140 |
141 theorem "plant (rev (leaves xt)) = mirror xt" |
141 theorem "plant (rev (leaves xt)) = mirror xt" |
142 quickcheck[random, expect = counterexample] |
142 quickcheck[random, expect = counterexample] |
143 quickcheck[exhaustive, expect = counterexample] |
143 quickcheck[exhaustive, expect = counterexample] |
144 \<comment>\<open>Wrong!\<close> |
144 \<comment> \<open>Wrong!\<close> |
145 oops |
145 oops |
146 |
146 |
147 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt" |
147 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt" |
148 quickcheck[random, expect = counterexample] |
148 quickcheck[random, expect = counterexample] |
149 quickcheck[exhaustive, expect = counterexample] |
149 quickcheck[exhaustive, expect = counterexample] |
150 \<comment>\<open>Wrong!\<close> |
150 \<comment> \<open>Wrong!\<close> |
151 oops |
151 oops |
152 |
152 |
153 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree" |
153 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree" |
154 |
154 |
155 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where |
155 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where |
161 | "root (Node f x y) = f" |
161 | "root (Node f x y) = f" |
162 |
162 |
163 theorem "hd (inOrder xt) = root xt" |
163 theorem "hd (inOrder xt) = root xt" |
164 quickcheck[random, expect = counterexample] |
164 quickcheck[random, expect = counterexample] |
165 quickcheck[exhaustive, expect = counterexample] |
165 quickcheck[exhaustive, expect = counterexample] |
166 \<comment>\<open>Wrong!\<close> |
166 \<comment> \<open>Wrong!\<close> |
167 oops |
167 oops |
168 |
168 |
169 |
169 |
170 subsection \<open>Exhaustive Testing beats Random Testing\<close> |
170 subsection \<open>Exhaustive Testing beats Random Testing\<close> |
171 |
171 |