1 |
|
2 (*<*) theory a1 = Main: (*>*) |
|
3 |
|
4 subsection {* List functions *} |
|
5 |
|
6 text{* Define a function @{text sum}, which computes the sum of |
|
7 elements of a list of natural numbers. *} |
|
8 |
|
9 (*<*) consts (*>*) |
|
10 sum :: "nat list \<Rightarrow> nat" |
|
11 |
|
12 text{* Then, define a function @{text flatten} which flattens a list |
|
13 of lists by appending the member lists. *} |
|
14 |
|
15 (*<*) consts (*>*) |
|
16 flatten :: "'a list list \<Rightarrow> 'a list" |
|
17 |
|
18 text{* Test your function by applying them to the following example lists: *} |
|
19 |
|
20 |
|
21 lemma "sum [2::nat, 4, 8] = x" |
|
22 (*<*) oops (*>*) |
|
23 |
|
24 lemma "flatten [[2::nat, 3], [4, 5], [7, 9]] = x" |
|
25 (*<*) oops (*>*) |
|
26 |
|
27 |
|
28 text{* Prove the following statements, or give a counterexample: *} |
|
29 |
|
30 |
|
31 lemma "length (flatten xs) = sum (map length xs)" |
|
32 (*<*) oops (*>*) |
|
33 |
|
34 lemma sum_append: "sum (xs @ ys) = sum xs + sum ys" |
|
35 (*<*) oops (*>*) |
|
36 |
|
37 lemma flatten_append: "flatten (xs @ ys) = flatten xs @ flatten ys" |
|
38 (*<*) oops (*>*) |
|
39 |
|
40 lemma "flatten (map rev (rev xs)) = rev (flatten xs)" |
|
41 (*<*) oops (*>*) |
|
42 |
|
43 lemma "flatten (rev (map rev xs)) = rev (flatten xs)" |
|
44 (*<*) oops (*>*) |
|
45 |
|
46 lemma "list_all (list_all P) xs = list_all P (flatten xs)" |
|
47 (*<*) oops (*>*) |
|
48 |
|
49 lemma "flatten (rev xs) = flatten xs" |
|
50 (*<*) oops (*>*) |
|
51 |
|
52 lemma "sum (rev xs) = sum xs" |
|
53 (*<*) oops (*>*) |
|
54 |
|
55 |
|
56 text{* Find a predicate @{text P} which satisfies *} |
|
57 |
|
58 lemma "list_all P xs \<longrightarrow> length xs \<le> sum xs" |
|
59 (*<*) oops (*>*) |
|
60 |
|
61 text{* Define, by means of primitive recursion, a function @{text |
|
62 exists} which checks whether an element satisfying a given property is |
|
63 contained in the list: *} |
|
64 |
|
65 |
|
66 (*<*) consts (*>*) |
|
67 list_exists :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)" |
|
68 |
|
69 text{* Test your function on the following examples: *} |
|
70 |
|
71 |
|
72 lemma "list_exists (\<lambda> n. n < 3) [4::nat, 3, 7] = b" |
|
73 (*<*) oops (*>*) |
|
74 |
|
75 lemma "list_exists (\<lambda> n. n < 4) [4::nat, 3, 7] = b" |
|
76 (*<*) oops (*>*) |
|
77 |
|
78 text{* Prove the following statements: *} |
|
79 |
|
80 lemma list_exists_append: |
|
81 "list_exists P (xs @ ys) = (list_exists P xs \<or> list_exists P ys)" |
|
82 (*<*) oops (*>*) |
|
83 |
|
84 lemma "list_exists (list_exists P) xs = list_exists P (flatten xs)" |
|
85 (*<*) oops (*>*) |
|
86 |
|
87 text{* You could have defined @{text list_exists} only with the aid of |
|
88 @{text list_all}. Do this now, i.e. define a function @{text |
|
89 list_exists2} and show that it is equivalent to @{text list_exists}. *} |
|
90 |
|
91 |
|
92 (*<*) end (*>*) |
|
93 |
|