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