equal
deleted
inserted
replaced
39 |
39 |
40 theorem "rev xs = xs" |
40 theorem "rev xs = xs" |
41 quickcheck |
41 quickcheck |
42 oops |
42 oops |
43 |
43 |
|
44 text {* An example involving functions inside other data structures *} |
|
45 |
|
46 consts app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" |
|
47 |
|
48 primrec |
|
49 "app [] x = x" |
|
50 "app (f # fs) x = app fs (f x)" |
|
51 |
|
52 lemma "app (fs @ gs) x = app gs (app fs x)" |
|
53 quickcheck |
|
54 by (induct fs arbitrary: x) simp_all |
|
55 |
|
56 lemma "app (fs @ gs) x = app fs (app gs x)" |
|
57 quickcheck |
|
58 oops |
|
59 |
44 consts |
60 consts |
45 occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" |
61 occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" |
46 primrec |
62 primrec |
47 "occurs a [] = 0" |
63 "occurs a [] = 0" |
48 "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" |
64 "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" |
51 del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" |
67 del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" |
52 primrec |
68 primrec |
53 "del1 a [] = []" |
69 "del1 a [] = []" |
54 "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" |
70 "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" |
55 |
71 |
56 (* A lemma, you'd think to be true from our experience with delAll*) |
72 text {* A lemma, you'd think to be true from our experience with delAll *} |
57 lemma "Suc (occurs a (del1 a xs)) = occurs a xs" |
73 lemma "Suc (occurs a (del1 a xs)) = occurs a xs" |
58 -- {* Wrong. Precondition needed.*} |
74 -- {* Wrong. Precondition needed.*} |
59 quickcheck |
75 quickcheck |
60 oops |
76 oops |
61 |
77 |