1 (*<*) |
|
2 theory Aufgabe1 = Main: |
|
3 (*>*) |
|
4 |
|
5 subsection {* Lists *} |
|
6 |
|
7 text{* |
|
8 Define a function @{term replace}, such that @{term"replace x y zs"} |
|
9 yields @{term zs} with every occurrence of @{term x} replaced by @{term y}. |
|
10 *} |
|
11 |
|
12 consts replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
13 |
|
14 text {* |
|
15 Prove or disprove (by counter example) the following theorems. |
|
16 You may have to prove some lemmas first. |
|
17 *}; |
|
18 |
|
19 theorem "rev(replace x y zs) = replace x y (rev zs)" |
|
20 (*<*)oops(*>*) |
|
21 |
|
22 theorem "replace x y (replace u v zs) = replace u v (replace x y zs)" |
|
23 (*<*)oops(*>*) |
|
24 |
|
25 theorem "replace y z (replace x y zs) = replace x z zs" |
|
26 (*<*)oops(*>*) |
|
27 |
|
28 text{* Define two functions for removing elements from a list: |
|
29 @{term"del1 x xs"} deletes the first occurrence (from the left) of |
|
30 @{term x} in @{term xs}, @{term"delall x xs"} all of them. *} |
|
31 |
|
32 consts del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
33 delall :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
34 |
|
35 |
|
36 text {* |
|
37 Prove or disprove (by counter example) the following theorems. |
|
38 *}; |
|
39 |
|
40 theorem "del1 x (delall x xs) = delall x xs" |
|
41 (*<*)oops(*>*) |
|
42 |
|
43 theorem "delall x (delall x xs) = delall x xs" |
|
44 (*<*)oops(*>*) |
|
45 |
|
46 theorem "delall x (del1 x xs) = delall x xs" |
|
47 (*<*)oops(*>*) |
|
48 |
|
49 theorem "del1 x (del1 y zs) = del1 y (del1 x zs)" |
|
50 (*<*)oops(*>*) |
|
51 |
|
52 theorem "delall x (del1 y zs) = del1 y (delall x zs)" |
|
53 (*<*)oops(*>*) |
|
54 |
|
55 theorem "delall x (delall y zs) = delall y (delall x zs)" |
|
56 (*<*)oops(*>*) |
|
57 |
|
58 theorem "del1 y (replace x y xs) = del1 x xs" |
|
59 (*<*)oops(*>*) |
|
60 |
|
61 theorem "delall y (replace x y xs) = delall x xs" |
|
62 (*<*)oops(*>*) |
|
63 |
|
64 theorem "replace x y (delall x zs) = delall x zs" |
|
65 (*<*)oops(*>*) |
|
66 |
|
67 theorem "replace x y (delall z zs) = delall z (replace x y zs)" |
|
68 (*<*)oops(*>*) |
|
69 |
|
70 theorem "rev(del1 x xs) = del1 x (rev xs)" |
|
71 (*<*)oops(*>*) |
|
72 |
|
73 theorem "rev(delall x xs) = delall x (rev xs)" |
|
74 (*<*)oops(*>*) |
|
75 |
|
76 (*<*) |
|
77 end |
|
78 (*>*) |
|