author | Christian Urban <christian.urban@kcl.ac.uk> |
Sat, 19 Mar 2022 09:53:48 +0000 | |
changeset 452 | 4aded96b3923 |
parent 95 | a33d3040bf7e |
permissions | -rw-r--r-- |
theory MyInduction imports Main begin fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where "itrev [] ys = ys" | "itrev (x#xs) ys = itrev xs (x#ys)" lemma "itrev xs [] = rev xs" apply(induction xs) apply(auto) oops lemma "itrev xs ys = rev xs @ ys" apply(induction xs arbitrary: ys) apply auto done