author  wenzelm 
Fri, 23 Apr 1999 11:50:35 +0200  
changeset 6494  ab1442d2e4e1 
parent 6444  2ebe9e630cab 
child 6505  2863855a6902 
permissions  rwrr 
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Isar_examples/Cantor.thy 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

4 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

5 
Cantor's theorem (see also 'Isabelle's ObjectLogics'). 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

6 
*) 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

7 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

8 
theory Cantor = Main:; 
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

9 

6494  10 

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

12 
proof; 

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

14 
show "??S ~: range f"; 

15 
proof; 

16 
assume "??S : range f"; 

17 
then; show False; 

18 
proof; 

19 
fix y; 

20 
assume "??S = f y"; 

21 
then; show ??thesis; 

22 
proof (rule equalityCE); 

23 
assume y_in_S: "y : ??S"; 

24 
assume y_in_fy: "y : f y"; 

25 
from y_in_S; have y_notin_fy: "y ~: f y"; ..; 

26 
from y_notin_fy y_in_fy; show ??thesis; ..; 

27 
next; 

28 
assume y_notin_S: "y ~: ??S"; 

29 
assume y_notin_fy: "y ~: f y"; 

30 
from y_notin_S; have y_in_fy: "y : f y"; ..; 

31 
from y_notin_fy y_in_fy; show ??thesis; ..; 

32 
qed; 

33 
qed; 

34 
qed; 

35 
qed; 

36 

37 

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

39 
proof; 

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

41 
show "??S ~: range f"; 

42 
proof; 

43 
assume "??S : range f"; 

44 
then; show False; 

45 
proof; 

46 
fix y; 

47 
assume "??S = f y"; 

48 
then; show ??thesis; 

49 
proof (rule equalityCE); 

50 
assume "y : ??S"; then; have y_notin_fy: "y ~: f y"; ..; 

51 
assume "y : f y"; 

52 
from y_notin_fy it; show ??thesis; ..; 

53 
next; 

54 
assume "y ~: ??S"; then; have y_in_fy: "y : f y"; ..; 

55 
assume "y ~: f y"; 

56 
from it y_in_fy; show ??thesis; ..; 

57 
qed; 

58 
qed; 

59 
qed; 

60 
qed; 

61 

62 

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

64 
by (best elim: equalityCE); 

65 

6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

66 

2ebe9e630cab
Miscellaneous Isabelle/Isar examples for HigherOrder Logic.
wenzelm
parents:
diff
changeset

67 
end; 