17 *} |
17 *} |
18 |
18 |
19 subsection {* Lists *} |
19 subsection {* Lists *} |
20 |
20 |
21 theorem "map g (map f xs) = map (g o f) xs" |
21 theorem "map g (map f xs) = map (g o f) xs" |
22 quickcheck |
22 quickcheck[expect = no_counterexample] |
23 oops |
23 oops |
24 |
24 |
25 theorem "map g (map f xs) = map (f o g) xs" |
25 theorem "map g (map f xs) = map (f o g) xs" |
26 quickcheck |
26 quickcheck[expect = counterexample] |
27 oops |
27 oops |
28 |
28 |
29 theorem "rev (xs @ ys) = rev ys @ rev xs" |
29 theorem "rev (xs @ ys) = rev ys @ rev xs" |
30 quickcheck |
30 quickcheck[expect = no_counterexample] |
31 oops |
31 oops |
32 |
32 |
33 theorem "rev (xs @ ys) = rev xs @ rev ys" |
33 theorem "rev (xs @ ys) = rev xs @ rev ys" |
34 quickcheck |
34 quickcheck[expect = counterexample] |
35 oops |
35 oops |
36 |
36 |
37 theorem "rev (rev xs) = xs" |
37 theorem "rev (rev xs) = xs" |
38 quickcheck |
38 quickcheck[expect = no_counterexample] |
39 oops |
39 oops |
40 |
40 |
41 theorem "rev xs = xs" |
41 theorem "rev xs = xs" |
42 quickcheck |
42 quickcheck[expect = counterexample] |
43 oops |
43 oops |
44 |
44 |
45 text {* An example involving functions inside other data structures *} |
45 text {* An example involving functions inside other data structures *} |
46 |
46 |
47 primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where |
47 primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where |
48 "app [] x = x" |
48 "app [] x = x" |
49 | "app (f # fs) x = app fs (f x)" |
49 | "app (f # fs) x = app fs (f x)" |
50 |
50 |
51 lemma "app (fs @ gs) x = app gs (app fs x)" |
51 lemma "app (fs @ gs) x = app gs (app fs x)" |
52 quickcheck |
52 quickcheck[expect = no_counterexample] |
53 by (induct fs arbitrary: x) simp_all |
53 by (induct fs arbitrary: x) simp_all |
54 |
54 |
55 lemma "app (fs @ gs) x = app fs (app gs x)" |
55 lemma "app (fs @ gs) x = app fs (app gs x)" |
56 quickcheck |
56 quickcheck[expect = counterexample] |
57 oops |
57 oops |
58 |
58 |
59 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where |
59 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where |
60 "occurs a [] = 0" |
60 "occurs a [] = 0" |
61 | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" |
61 | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" |
65 | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" |
65 | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" |
66 |
66 |
67 text {* A lemma, you'd think to be true from our experience with delAll *} |
67 text {* A lemma, you'd think to be true from our experience with delAll *} |
68 lemma "Suc (occurs a (del1 a xs)) = occurs a xs" |
68 lemma "Suc (occurs a (del1 a xs)) = occurs a xs" |
69 -- {* Wrong. Precondition needed.*} |
69 -- {* Wrong. Precondition needed.*} |
70 quickcheck |
70 quickcheck[expect = counterexample] |
71 oops |
71 oops |
72 |
72 |
73 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" |
73 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" |
74 quickcheck |
74 quickcheck[expect = counterexample] |
75 -- {* Also wrong.*} |
75 -- {* Also wrong.*} |
76 oops |
76 oops |
77 |
77 |
78 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" |
78 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" |
79 quickcheck |
79 quickcheck[expect = no_counterexample] |
80 by (induct xs) auto |
80 by (induct xs) auto |
81 |
81 |
82 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
82 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
83 "replace a b [] = []" |
83 "replace a b [] = []" |
84 | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) |
84 | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) |
85 else (x#(replace a b xs)))" |
85 else (x#(replace a b xs)))" |
86 |
86 |
87 lemma "occurs a xs = occurs b (replace a b xs)" |
87 lemma "occurs a xs = occurs b (replace a b xs)" |
88 quickcheck |
88 quickcheck[expect = counterexample] |
89 -- {* Wrong. Precondition needed.*} |
89 -- {* Wrong. Precondition needed.*} |
90 oops |
90 oops |
91 |
91 |
92 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)" |
92 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)" |
93 quickcheck |
93 quickcheck[expect = no_counterexample] |
94 by (induct xs) simp_all |
94 by (induct xs) simp_all |
95 |
95 |
96 |
96 |
97 subsection {* Trees *} |
97 subsection {* Trees *} |
98 |
98 |
111 "mirror (Twig) = Twig " |
111 "mirror (Twig) = Twig " |
112 | "mirror (Leaf a) = Leaf a " |
112 | "mirror (Leaf a) = Leaf a " |
113 | "mirror (Branch l r) = Branch (mirror r) (mirror l)" |
113 | "mirror (Branch l r) = Branch (mirror r) (mirror l)" |
114 |
114 |
115 theorem "plant (rev (leaves xt)) = mirror xt" |
115 theorem "plant (rev (leaves xt)) = mirror xt" |
116 quickcheck |
116 quickcheck[expect = counterexample] |
117 --{* Wrong! *} |
117 --{* Wrong! *} |
118 oops |
118 oops |
119 |
119 |
120 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt" |
120 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt" |
121 quickcheck |
121 quickcheck[expect = counterexample] |
122 --{* Wrong! *} |
122 --{* Wrong! *} |
123 oops |
123 oops |
124 |
124 |
125 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree" |
125 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree" |
126 |
126 |