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