equal
deleted
inserted
replaced
1 theory FP0 = PreList: |
1 theory FP0 = PreList: |
2 |
|
3 section{*Functional Programming/Modelling*} |
|
4 |
2 |
5 datatype 'a list = Nil ("[]") |
3 datatype 'a list = Nil ("[]") |
6 | Cons 'a "'a list" (infixr "#" 65) |
4 | Cons 'a "'a list" (infixr "#" 65) |
7 |
5 |
8 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) |
6 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) |
14 |
12 |
15 primrec |
13 primrec |
16 "rev [] = []" |
14 "rev [] = []" |
17 "rev (x # xs) = (rev xs) @ (x # [])" |
15 "rev (x # xs) = (rev xs) @ (x # [])" |
18 |
16 |
19 subsection{*An Introductory Proof*} |
|
20 |
|
21 theorem rev_rev [simp]: "rev(rev xs) = xs" |
17 theorem rev_rev [simp]: "rev(rev xs) = xs" |
22 oops |
18 (*<*)oops(*>*) |
23 |
19 |
24 |
20 |
25 text{* |
21 text{* |
26 \begin{exercise} |
22 \begin{exercise} |
27 Define a datatype of binary trees and a function @{term mirror} |
23 Define a datatype of binary trees and a function @{term mirror} |