| author | fahadausaf <fahad.ausaf@icloud.com> |
| Mon, 13 Oct 2014 09:20:23 +0100 | |
| changeset 29 | 2345ba5b4264 |
| parent 28 | d3831bf423f2 |
| permissions | -rw-r--r-- |
| 28 | 1 |
theory MyInduction |
2 |
imports Main |
|
3 |
begin |
|
| 29 | 4 |
|
5 |
fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
6 |
"itrev [] ys = ys" | |
|
7 |
"itrev (x#xs) ys = itrev xs (x#ys)" |
|
8 |
||
9 |
lemma "itrev xs [] = rev xs" |
|
10 |
apply(induction xs) |
|
11 |
apply(auto) |
|
12 |
oops |
|
13 |
||
14 |
lemma "itrev xs ys = rev xs @ ys" |
|
15 |
apply(induction xs arbitrary: ys) |
|
16 |
apply auto |
|
17 |
done |
|
18 |
||
19 |