equal
deleted
inserted
replaced
1 theory ToyList |
|
2 imports Datatype |
|
3 begin |
|
4 |
|
5 datatype 'a list = Nil ("[]") |
|
6 | Cons 'a "'a list" (infixr "#" 65) |
|
7 |
|
8 (* This is the append function: *) |
|
9 primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
|
10 where |
|
11 "[] @ ys = ys" | |
|
12 "(x # xs) @ ys = x # (xs @ ys)" |
|
13 |
|
14 primrec rev :: "'a list => 'a list" where |
|
15 "rev [] = []" | |
|
16 "rev (x # xs) = (rev xs) @ (x # [])" |
|
17 lemma app_Nil2 [simp]: "xs @ [] = xs" |
|
18 apply(induct_tac xs) |
|
19 apply(auto) |
|
20 done |
|
21 |
|
22 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" |
|
23 apply(induct_tac xs) |
|
24 apply(auto) |
|
25 done |
|
26 |
|
27 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" |
|
28 apply(induct_tac xs) |
|
29 apply(auto) |
|
30 done |
|
31 |
|
32 theorem rev_rev [simp]: "rev(rev xs) = xs" |
|
33 apply(induct_tac xs) |
|
34 apply(auto) |
|
35 done |
|
36 |
|
37 end |
|