author  wenzelm 
Fri, 28 Sep 2001 20:08:05 +0200  
changeset 11635  fd242f857508 
parent 11591  4b171ad4ff65 
child 14981  e73f8140af78 
permissions  rwrr 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/ex/Hilbert_Classical.thy 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

5 
*) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

6 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

7 
header {* Hilbert's choice and classical logic *} 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

8 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

9 
theory Hilbert_Classical = Main: 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

10 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

11 
text {* 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

12 
Derivation of the classical law of tertiumnondatur by means of 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

13 
Hilbert's choice operator (due to M. J. Beeson and J. Harrison). 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

14 
*} 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

15 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

16 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

17 
subsection {* Proof text *} 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

18 

11591  19 
theorem tnd: "A \<or> \<not> A" 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

20 
proof  
11590  21 
let ?P = "\<lambda>X. X = False \<or> X = True \<and> A" 
22 
let ?Q = "\<lambda>X. X = False \<and> A \<or> X = True" 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

23 

11590  24 
have a: "?P (Eps ?P)" 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

25 
proof (rule someI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

26 
have "False = False" .. 
11590  27 
thus "?P False" .. 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

28 
qed 
11590  29 
have b: "?Q (Eps ?Q)" 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

30 
proof (rule someI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

31 
have "True = True" .. 
11590  32 
thus "?Q True" .. 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

33 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

34 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

35 
from a show ?thesis 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

36 
proof 
11590  37 
assume "Eps ?P = True \<and> A" 
38 
hence A .. 

39 
thus ?thesis .. 

40 
next 

41 
assume P: "Eps ?P = False" 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

42 
from b show ?thesis 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

43 
proof 
11590  44 
assume "Eps ?Q = False \<and> A" 
45 
hence A .. 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

46 
thus ?thesis .. 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

47 
next 
11590  48 
assume Q: "Eps ?Q = True" 
49 
have neq: "?P \<noteq> ?Q" 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

50 
proof 
11590  51 
assume "?P = ?Q" 
52 
hence "Eps ?P = Eps ?Q" by (rule arg_cong) 

53 
also note P 

54 
also note Q 

11635  55 
finally show False by (rule False_neq_True) 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

56 
qed 
11590  57 
have "\<not> A" 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

58 
proof 
11590  59 
assume a: A 
60 
have "?P = ?Q" 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

61 
proof 
11590  62 
fix x show "?P x = ?Q x" 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

63 
proof 
11590  64 
assume "?P x" 
65 
thus "?Q x" 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

66 
proof 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

67 
assume "x = False" 
11590  68 
from this and a have "x = False \<and> A" .. 
69 
thus "?Q x" .. 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

70 
next 
11590  71 
assume "x = True \<and> A" 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

72 
hence "x = True" .. 
11590  73 
thus "?Q x" .. 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

74 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

75 
next 
11590  76 
assume "?Q x" 
77 
thus "?P x" 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

78 
proof 
11590  79 
assume "x = False \<and> A" 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

80 
hence "x = False" .. 
11590  81 
thus "?P x" .. 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

82 
next 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

83 
assume "x = True" 
11590  84 
from this and a have "x = True \<and> A" .. 
85 
thus "?P x" .. 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

86 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

87 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

88 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

89 
with neq show False by contradiction 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

90 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

91 
thus ?thesis .. 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

92 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

93 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

94 
qed 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

95 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

96 

11591  97 
subsection {* Proof term of text *} 
98 

99 
text {* 

100 
{\small @{prf [display, margin = 80] tnd}} 

101 
*} 

102 

103 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

104 
subsection {* Proof script *} 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

105 

11590  106 
theorem tnd': "A \<or> \<not> A" 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

107 
apply (subgoal_tac 
11590  108 
"(((SOME x. x = False \<or> x = True \<and> A) = False) \<or> 
109 
((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and> 

110 
(((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or> 

111 
((SOME x. x = False \<and> A \<or> x = True) = True))") 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

112 
prefer 2 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

113 
apply (rule conjI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

114 
apply (rule someI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

115 
apply (rule disjI1) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

116 
apply (rule refl) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

117 
apply (rule someI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

118 
apply (rule disjI2) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

119 
apply (rule refl) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

120 
apply (erule conjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

121 
apply (erule disjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

122 
apply (erule disjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

123 
apply (erule conjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

124 
apply (erule disjI1) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

125 
prefer 2 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

126 
apply (erule conjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

127 
apply (erule disjI1) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

128 
apply (subgoal_tac 
11590  129 
"(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq> 
130 
(\<lambda>x. (x = False) \<and> A \<or> (x = True))") 

11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

131 
prefer 2 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

132 
apply (rule notI) 
11590  133 
apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong) 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

134 
apply (drule trans, assumption) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

135 
apply (drule sym) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

136 
apply (drule trans, assumption) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

137 
apply (erule False_neq_True) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

138 
apply (rule disjI2) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

139 
apply (rule notI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

140 
apply (erule notE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

141 
apply (rule ext) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

142 
apply (rule iffI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

143 
apply (erule disjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

144 
apply (rule disjI1) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

145 
apply (erule conjI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

146 
apply assumption 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

147 
apply (erule conjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

148 
apply (erule disjI2) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

149 
apply (erule disjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

150 
apply (erule conjE) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

151 
apply (erule disjI1) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

152 
apply (rule disjI2) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

153 
apply (erule conjI) 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

154 
apply assumption 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

155 
done 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

156 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

157 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

158 
subsection {* Proof term of script *} 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

159 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

160 
text {* 
11591  161 
{\small @{prf [display, margin = 80] tnd'}} 
11584
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

162 
*} 
c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

163 

c8e98b9498b4
derive tertiumnondatur by means of Hilbert's choice operator;
wenzelm
parents:
diff
changeset

164 
end 