Theory SurjectiveCantor

section‹Interactive and automated theorem proving›
subsection‹SurjectiveCantor.thy (Figure 2 of \cite{J75})›
text‹The surjective Cantor theorem is used in \cite{J75} to illustrate some aspects of interactive and 
automated theorem proving in Isabelle/HOL as relevant for the paper. To keep the provided data material complete 
wrt. \cite{J75}, we include these data sources also here.›
theory SurjectiveCantor imports Main
begin 
text‹Surjective Cantor theorem: traditional interactive proof›
theorem SurjectiveCantor: "¬(∃G.∀F::'a⇒bool.∃X::'a. G X = F)" 
  proof
    assume 1: "∃G.∀F::'a⇒bool.∃X::'a. G X = F" 
    obtain g::"'a⇒('a⇒bool)" where 2: "∀F.∃X. g X = F" using 1 by auto 
    let ?F = "λX.¬ g X X" 
    have 3: "∃Y. g Y = ?F" using 2 by metis 
    obtain a::'a where 4: "g a = ?F" using 3 by auto 
    have 5: "g a a = ?F a" using 4 by metis 
    have 6: "g a a = (¬ g a a)" using 5 by auto 
    show False using 6 by auto 
  qed
text‹Avoiding proof by contradiction (Fuenmayor ‹&› Benzmüller, 2021)›
theorem SurjectiveCantor': "¬(∃G.∀F::'a⇒bool.∃X::'a. G X = F)" 
  proof - 
    {fix g :: "'a⇒('a⇒bool)"
      have 1: "∀X.∃Y.(¬g X Y) = (¬g Y Y)" by auto 
      have 2: "∀X.∃Y.(¬g X Y) = ((λZ.¬g Z Z) Y)" using 1 by auto 
      have 3: "∃F.∀X.∃Y.(¬g X Y) = (F Y)" using 2 by auto
      have 4: "∃F.∀X.¬(∀Y.(g X Y) = (F Y))" using 3 by auto 
      have "∃F.∀X.¬(g X = F)" using 4 by metis 
    }
    hence 5: "∀G.∃F::'a⇒bool.∀X::'a.¬(G X = F)" by auto 
    have 6: "¬(∃G.∀F::'a⇒bool.∃X::'a. G X = F)" using 5 by auto 
    thus ?thesis . ―‹done, avoiding proof by contradiction›
  qed
text‹Surjective Cantor theorem: automated proof by some internal/external theorem provers›
theorem SurjectiveCantor'': "¬(∃G.∀F::'a⇒bool.∃X::'a. G X = F)" 
  nitpick[expect=none] ―‹no counterexample found› 
  ―‹sledgehammer› ―‹most internal provers give up›
  ―‹sledgehammer[remote\_leo2 remote\_leo3]› ―‹proof found: leo provers succeed›
  oops
text‹Surjective Cantor theorem (wrong formalization attempt): the types are crucial›
theorem SurjectiveCantor''': "¬(∃G.∀F::'b.∃X::'a. G X = F)" 
  nitpick ―‹counterexample found for card 'a = 1 and card 'b = 1: G=(‹λ›x. (a1 := b1)›
  nitpick[satisfy, expect=genuine] ―‹model found for card 'a = 1 and card 'b = 2›
  nitpick[card 'a=2, card 'b=3, expect=none] ―‹no counterexample found› 
  oops 
end