| author | Chengsong |
| Tue, 08 Nov 2022 23:24:54 +0000 | |
| changeset 621 | 17c7611fb0a9 |
| parent 95 | a33d3040bf7e |
| 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 |