equal
deleted
inserted
replaced
1 (*<*) |
|
2 theory Snoc = Main: |
|
3 (*>*) |
|
4 subsection {* Lists *} |
|
5 |
|
6 text {* |
|
7 Define a primitive recursive function @{text snoc} that appends an element |
|
8 at the \emph{right} end of a list. Do not use @{text"@"} itself. |
|
9 *} |
|
10 |
|
11 consts |
|
12 snoc :: "'a list => 'a => 'a list" |
|
13 |
|
14 text {* |
|
15 Prove the following theorem: |
|
16 *} |
|
17 |
|
18 theorem rev_cons: "rev (x # xs) = snoc (rev xs) x" |
|
19 (*<*)oops(*>*) |
|
20 |
|
21 text {* |
|
22 Hint: you need to prove a suitable lemma first. |
|
23 *} |
|
24 |
|
25 (*<*) |
|
26 end |
|
27 (*>*) |
|