theory Demo5 imports Main begin (* HINT FOR ONLINE DEMO Start your first proof attempt with itrev xs [] = rev xs then generalize by introducing ys, and finally quantify over ys. Each generalization should be motivated by the previous failed proof attempt. This example can also be found in the Isabelle/HOL tutorial. *) primrec itrev :: "'a list \ 'a list \ 'a list" where "itrev [] ys = ys" | "itrev (x#xs) ys = itrev xs (x#ys)" lemma helper1: "itrev xs l = (rev xs) @ l" apply (induct xs arbitrary: l) apply simp apply simp done lemma itrev_rev : "itrev xs [] = rev xs" by (simp add: helper1) end