chapter \<open>Exercise Sheet -- Week 2\<close> text \<open>Important disclaimer for the whole exercise part of this course: \<^item> Whenever you just got stuck on some sub-proofs, then use sorry for these parts. \<^item> Please still submit these partial solutions, since it may help all students to discuss these potentially common problems. \<^item> It is still fine to tick the check-box of partially solved exercises, as long as you can explain the intended solution and the problem that you ran into. \<close> theory Exercise02 imports Main begin section \<open>Overview of basic proof rules\<close> text \<open>various rules\<close> thm excluded_middle (* LEM *) thm ccontr (* proof by contradiction *) thm arg_cong fun_cong (* function application congruence rules *) text \<open>elimination rules\<close> thm disjE conjE exE allE impE notE text \<open>introduction rules\<close> thm disjI1 disjI2 conjI exI allI impI notI section \<open>Overall Setup\<close> text \<open>There is a well known proof that there is no surjective function from A to the power-set of A via Cantor's diagonalization argument. In this theory file we represent sets as characteristic functions from the carrier to booleans. E.g., the set {1,5,6,7,...} of natural numbers would be represented by @{term "\<lambda> n :: nat. n = 1 \<or> n \<ge> 5"}.\<close> type_synonym 'a cf_set = "'a \<Rightarrow> bool" text \<open>Definition of surjectivity of a function\<close> definition surjective :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where "surjective f = (\<forall> b. \<exists> a. f a = b)" text \<open>The statement we are now interested in is @{prop "\<not> (\<exists> f :: 'a \<Rightarrow> 'a cf_set. surjective f)"}.\<close> text \<open>The proof roughly works as follows: assume such a function f exists, then define g x = (\<not> f x x) and show that g is not in the image of f.\<close> section \<open>Exercise 1.a -- 3 points\<close> text \<open>Prove the upcoming lemma cantor1. Try to minimize the number of proof-qed blocks. You may find the following elimination rule for surjectivity useful, as well as @{thm fun_cong} and @{thm arg_cong}.\<close> text \<open>Hint: in the proof you sometimes have to make explicit type constraints explicit, e.g., as in fix f :: "'a \<Rightarrow> 'a cf_set" "\<exists> f :: 'a \<Rightarrow> 'a cf_set. surjective f" \<close> lemma surjectiveE: "surjective f \<Longrightarrow> \<exists> a. f a = b" unfolding surjective_def by auto lemma cantor1: "\<not> (\<exists> f :: 'a \<Rightarrow> 'a cf_set. surjective f)" sorry section \<open>Exercise 1.b -- 2 points\<close> text \<open>Think about why it was necessary to add type-constraints. What would possible go wrong without these constraints? Is it a problem of Isabelle (in being too restrictive), or are the formulas and statements itself problematic?\<close> section \<open>Exercise 2 -- 5 points\<close> text \<open>Prove the same theorem again, but this time you may only apply single proof-steps, i.e., no auto (or other automatic methods). And of course you are not allowed to refer @{thm cantor1}. At a certain step you might find the lemma bool_diffE useful. If you need another very basic proof step on properties of boolean negation and equality, then that proof-step can be done by auto.\<close> lemma bool_diffE: "b = (\<not> b) \<Longrightarrow> P" by auto lemma cantor2: "\<not> (\<exists> f :: 'a \<Rightarrow> 'a cf_set. surjective f)" sorry end