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