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

theory Solutions08
  imports Main
begin

subsection \<open>Exercise 1\<close>

text \<open>
Prove the following lemma only using implicit proof methods.
\<close>
lemma "(A \<inter> B) \<union> (A \<inter> C) \<subseteq> A \<inter> (B \<union> C)"
proof
  fix x assume "x \<in> (A \<inter> B) \<union> (A \<inter> C)"
  then show "x \<in> A \<inter> (B \<union> C)"
  proof
    assume "x \<in> A \<inter> B"
    then obtain "x \<in> A" and "x \<in> B" ..
    from \<open>x \<in> B\<close> have "x \<in> B \<union> C" ..
    with \<open>x \<in> A\<close> show ?thesis ..
  next
    assume "x \<in> A \<inter> C"
    then obtain "x \<in> A" and "x \<in> C" ..
    from \<open>x \<in> C\<close> have "x \<in> B \<union> C" ..
    with \<open>x \<in> A\<close> show ?thesis ..
  qed
qed


subsection \<open>Exercise 2\<close>

text \<open>
Prove the following lemma (giving an alternative definition of surjectivity
of a function \<open>f\<close> between to sets \<open>A\<close> and \<open>B\<close>) only using the @{method rule} method.
\<close>
lemma "(\<forall>y\<in>B. \<exists>x\<in>A. f x = y) \<longleftrightarrow> B \<subseteq> f ` A"
proof (rule iffI)
  assume "\<forall>y\<in>B. \<exists>x\<in>A. f x = y"
  show "B \<subseteq> f ` A"
  proof (rule subsetI)
    fix y assume "y \<in> B"
    from \<open>\<forall>y\<in>B. \<exists>x\<in>A. f x = y\<close> and \<open>y \<in> B\<close>
    have "\<exists>x\<in>A. f x = y" by (rule bspec)
    then obtain x where "f x = y" and "x \<in> A" by (rule bexE)
    from \<open>x \<in> A\<close> have "f x \<in> f ` A" by (rule imageI)
    from \<open>f x = y\<close> show "y \<in> f ` A" using \<open>f x \<in> f ` A\<close> by (rule subst)
  qed
next
  assume "B \<subseteq> f ` A"
  show "\<forall>y\<in>B. \<exists>x\<in>A. f x = y"
  proof (rule ballI)
    fix y assume "y \<in> B"
    from \<open>B \<subseteq> f ` A\<close> and \<open>y \<in> B\<close> have "y \<in> f ` A" by (rule subsetD)
    then obtain x where "y = f x" and "x \<in> A" by (rule imageE)
    from \<open>y = f x\<close> have "f x = y" by (rule sym)
    then show "\<exists>x\<in>A. f x = y" using \<open>x \<in> A\<close> by (rule bexI)
  qed
qed

end