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

src/HOL/Isar_examples/Cantor.thy

author | wenzelm |

Wed Jun 13 18:30:11 2007 +0200 (2007-06-13) | |

changeset 23373 | ead82c82da9e |

parent 16417 | 9bc16273c2d4 |

child 31758 | 3edd5f813f01 |

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

tuned proofs: avoid implicit prems;

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

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 *)

6 header {* Cantor's Theorem *}

8 theory Cantor imports Main begin

10 text_raw {*

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

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

13 *}

15 text {*

16 Cantor's Theorem states that every set has more subsets than it has

17 elements. It has become a favorite basic example in pure

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

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

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

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

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

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

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

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

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

28 *}

30 theorem "EX S. S ~: range (f :: 'a => 'a set)"

31 proof

32 let ?S = "{x. x ~: f x}"

33 show "?S ~: range f"

34 proof

35 assume "?S : range f"

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

37 then show False

38 proof (rule equalityCE)

39 assume "y : f y"

40 assume "y : ?S" then have "y ~: f y" ..

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

42 next

43 assume "y ~: ?S"

44 assume "y ~: f y" then have "y : ?S" ..

45 with `y ~: ?S` show ?thesis by contradiction

46 qed

47 qed

48 qed

50 text {*

51 How much creativity is required? As it happens, Isabelle can prove

52 this theorem automatically using best-first search. Depth-first

53 search would diverge, but best-first search successfully navigates

54 through the large search space. The context of Isabelle's classical

55 prover contains rules for the relevant constructs of HOL's set

56 theory.

57 *}

59 theorem "EX S. S ~: range (f :: 'a => 'a set)"

60 by best

62 text {*

63 While this establishes the same theorem internally, we do not get

64 any idea of how the proof actually works. There is currently no way

65 to transform internal system-level representations of Isabelle

66 proofs back into Isar text. Writing intelligible proof documents

67 really is a creative process, after all.

68 *}

70 end