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