summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Cantor.thy

author | blanchet |

Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) | |

changeset 58306 | 117ba6cbe414 |

parent 55640 | abc140f21caa |

child 58614 | 7338eb25226c |

permissions | -rw-r--r-- |

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

1 (* Title: HOL/Isar_Examples/Cantor.thy

2 Author: Markus Wenzel, TU Muenchen

3 *)

5 header {* Cantor's Theorem *}

7 theory Cantor

8 imports Main

9 begin

11 text_raw {* \footnote{This is an Isar version of the final example of

12 the Isabelle/HOL manual \cite{isabelle-HOL}.} *}

14 text {* Cantor's Theorem states that every set has more subsets than

15 it has elements. It has become a favorite basic example in pure

16 higher-order logic since it is so easily expressed: \[\all{f::\alpha

17 \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}

18 \all{x::\alpha} f \ap x \not= S\]

20 Viewing types as sets, $\alpha \To \idt{bool}$ represents the

21 powerset of $\alpha$. This version of the theorem states that for

22 every function from $\alpha$ to its powerset, some subset is outside

23 its range. The Isabelle/Isar proofs below uses HOL's set theory,

24 with the type $\alpha \ap \idt{set}$ and the operator

25 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *}

27 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"

28 proof

29 let ?S = "{x. x \<notin> f x}"

30 show "?S \<notin> range f"

31 proof

32 assume "?S \<in> range f"

33 then obtain y where "?S = f y" ..

34 then show False

35 proof (rule equalityCE)

36 assume "y \<in> f y"

37 assume "y \<in> ?S"

38 then have "y \<notin> f y" ..

39 with `y : f y` show ?thesis by contradiction

40 next

41 assume "y \<notin> ?S"

42 assume "y \<notin> f y"

43 then have "y \<in> ?S" ..

44 with `y \<notin> ?S` show ?thesis by contradiction

45 qed

46 qed

47 qed

49 text {* How much creativity is required? As it happens, Isabelle can

50 prove this theorem automatically using best-first search.

51 Depth-first search would diverge, but best-first search successfully

52 navigates through the large search space. The context of Isabelle's

53 classical prover contains rules for the relevant constructs of HOL's

54 set theory. *}

56 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"

57 by best

59 text {* While this establishes the same theorem internally, we do not

60 get any idea of how the proof actually works. There is currently no

61 way to transform internal system-level representations of Isabelle

62 proofs back into Isar text. Writing intelligible proof documents

63 really is a creative process, after all. *}

65 end