theory Demo3 = Main: consts sep :: "'a \ 'a list \ 'a list" recdef sep "measure (\(a, xs). size xs)" "sep (a, x#y#zs) = x # a # sep (a,y#zs)" "sep (a, xs) = xs" print_theorems lemma "map f (sep (x,xs)) = sep (f x, map f xs)" oops -- solution lemma "map f (sep (x,xs)) = sep (f x, map f xs)" apply (induct x xs rule: sep.induct) apply auto done end