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+
−
+
−
+
−