section \Solutions for Session 8\ theory Solutions08 imports Main begin subsection \Exercise 1\ text \ Prove the following lemma only using implicit proof methods. \ lemma "(A \ B) \ (A \ C) \ A \ (B \ C)" proof fix x assume "x \ (A \ B) \ (A \ C)" then show "x \ A \ (B \ C)" proof assume "x \ A \ B" then obtain "x \ A" and "x \ B" .. from \x \ B\ have "x \ B \ C" .. with \x \ A\ show ?thesis .. next assume "x \ A \ C" then obtain "x \ A" and "x \ C" .. from \x \ C\ have "x \ B \ C" .. with \x \ A\ show ?thesis .. qed qed subsection \Exercise 2\ text \ Prove the following lemma (giving an alternative definition of surjectivity of a function \f\ between to sets \A\ and \B\) only using the @{method rule} method. \ lemma "(\y\B. \x\A. f x = y) \ B \ f ` A" proof (rule iffI) assume "\y\B. \x\A. f x = y" show "B \ f ` A" proof (rule subsetI) fix y assume "y \ B" from \\y\B. \x\A. f x = y\ and \y \ B\ have "\x\A. f x = y" by (rule bspec) then obtain x where "f x = y" and "x \ A" by (rule bexE) from \x \ A\ have "f x \ f ` A" by (rule imageI) from \f x = y\ show "y \ f ` A" using \f x \ f ` A\ by (rule subst) qed next assume "B \ f ` A" show "\y\B. \x\A. f x = y" proof (rule ballI) fix y assume "y \ B" from \B \ f ` A\ and \y \ B\ have "y \ f ` A" by (rule subsetD) then obtain x where "y = f x" and "x \ A" by (rule imageE) from \y = f x\ have "f x = y" by (rule sym) then show "\x\A. f x = y" using \x \ A\ by (rule bexI) qed qed end