section \<open>Solutions for Session 9\<close>

theory Solutions09
  imports Demo09
begin

subsection \<open>Exercise 1\<close>

lemma map_cong [fundef_cong]:
  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> 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 \<open>
Prove that \<open>mirror\<close> is self-inverse, that is:
\<close>
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 \<circ> g) xs" by (induction xs) auto

lemma map_idI [intro]: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> 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 \<open>Exercise 2\<close>

text \<open>
Give a direct proof of the fact:
\<close>
lemma Nonterm_empty_imp_minimal:
  assumes "Nonterm r = {}"
  shows "minimal r"
proof (unfold minimal_def, intro allI impI)
  fix Q :: "'a set" assume "Q \<noteq> {}"
  from assms have "\<forall>x\<in>Q. \<exists>y\<in>Q. (y, x) \<in> r \<Longrightarrow> Q = {}" by (unfold Nonterm_def) blast
  with \<open>Q \<noteq> {}\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" by blast
qed

end