equal
deleted
inserted
replaced
1 theory FP0 = PreList: |
|
2 |
|
3 datatype 'a list = Nil ("[]") |
|
4 | Cons 'a "'a list" (infixr "#" 65) |
|
5 |
|
6 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) |
|
7 rev :: "'a list \<Rightarrow> 'a list" |
|
8 |
|
9 primrec |
|
10 "[] @ ys = ys" |
|
11 "(x # xs) @ ys = x # (xs @ ys)" |
|
12 |
|
13 primrec |
|
14 "rev [] = []" |
|
15 "rev (x # xs) = (rev xs) @ (x # [])" |
|
16 |
|
17 theorem rev_rev [simp]: "rev(rev xs) = xs" |
|
18 (*<*)oops(*>*) |
|
19 |
|
20 text{* |
|
21 \begin{exercise} |
|
22 Define a datatype of binary trees and a function @{term mirror} |
|
23 that mirrors a binary tree by swapping subtrees recursively. Prove |
|
24 @{prop"mirror(mirror t) = t"}. |
|
25 |
|
26 Define a function @{term flatten} that flattens a tree into a list |
|
27 by traversing it in infix order. Prove |
|
28 @{prop"flatten(mirror t) = rev(flatten t)"}. |
|
29 \end{exercise} |
|
30 *} |
|
31 end |
|