cantor.thy

theory cantor
  imports Main
begin

definition map :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
  "map A B = {f. \<forall>a\<in>A. f a \<in> B}"

definition surj where
  "surj A B f = (f \<in> map A B \<and> (\<forall>b\<in>B. \<exists>a\<in>A. f a = b))"

theorem "s \<in> map X (map X {True,False}) \<Longrightarrow> \<not> surj X (map X {True,False}) s"
proof auto
  assume s_map: "s \<in> map X (map X {True,False})"
  and s_surj: "surj X (map X {True, False}) s"

  define d :: "'a \<Rightarrow> bool" where
    "d \<equiv> \<lambda>x. (if s x x then False else True)"

  have s_diag_map: "\<And>x. x \<in> X \<Longrightarrow> s x x \<in> {True,False}"
    using s_map unfolding map_def by auto

  have d_map: "d \<in> map X {True,False}"
    unfolding map_def d_def
    by auto

  obtain x where x: "x \<in> X" "s x = d"
    by (meson cantor.surj_def d_map s_surj)
  
  have "\<And>y. y \<in> X \<Longrightarrow> s y \<noteq> d"
  proof
    fix y
    assume "y \<in> X" "s y = d"
    have "s y y \<noteq> d y"
      by (simp add: d_def)
    show False
      using \<open>s y = d\<close> \<open>s y y \<noteq> d y\<close> by auto
  qed

  show False
    using \<open>\<And>thesis. (\<And>x. \<lbrakk>x \<in> X; s x = d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \<open>\<And>y. y \<in> X \<Longrightarrow> s y \<noteq> d\<close> by auto
qed

end