section \Solutions for Session 9\
theory Solutions09
imports Demo09
begin
subsection \Exercise 1\
lemma map_cong [fundef_cong]:
"xs = ys \ (\x. x \ set ys \ f x = g x) \ map f xs = map g ys"
by (induction xs arbitrary: ys) auto
fun mirror
where
"mirror (Tree n ts) = Tree n (rev (map mirror ts))"
text \
Prove that \mirror\ is self-inverse, that is:
\
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" by (induction xs) auto
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" by (induction xs) auto
lemma rev_rev [simp]: "rev (rev xs) = xs" by (induction xs) auto
lemma map_map [simp]: "map f (map g xs) = map (f \ g) xs" by (induction xs) auto
lemma map_idI [intro]: "(\x. x \ set xs \ f x = x) \ map f xs = xs"
by (induction xs) auto
lemma rev_map [simp]: "rev (map f xs) = map f (rev xs)"
by (induction xs) auto
lemma "mirror (mirror t) = t"
by (induction t) auto
subsection \Exercise 2\
text \
Give a direct proof of the fact:
\
lemma Nonterm_empty_imp_minimal:
assumes "Nonterm r = {}"
shows "minimal r"
proof (unfold minimal_def, intro allI impI)
fix Q :: "'a set" assume "Q \ {}"
from assms have "\x\Q. \y\Q. (y, x) \ r \ Q = {}" by (unfold Nonterm_def) blast
with \Q \ {}\ show "\z\Q. \y. (y, z) \ r \ y \ Q" by blast
qed
end