author  paulson 
Thu, 26 Sep 2002 10:51:29 +0200  
changeset 13585  db4005b40cc6 
parent 12372  cd3a09c7dac9 
child 13763  f94b569cd610 
permissions  rwrr 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

1 
(* Title: HOL/Hilbert_Choice.thy 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

2 
ID: $Id$ 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

4 
Copyright 2001 University of Cambridge 
12023  5 
*) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

6 

12023  7 
header {* Hilbert's epsilonoperator and everything to do with the Axiom of Choice *} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

8 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

9 
theory Hilbert_Choice = NatArith 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

10 
files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"): 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

11 

12298  12 

13 
subsection {* Hilbert's epsilon *} 

14 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

15 
consts 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

16 
Eps :: "('a => bool) => 'a" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

17 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

18 
syntax (input) 
12298  19 
"_Eps" :: "[pttrn, bool] => 'a" ("(3\<epsilon>_./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

20 
syntax (HOL) 
12298  21 
"_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

22 
syntax 
12298  23 
"_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

24 
translations 
12298  25 
"SOME x. P" == "Eps (%x. P)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

26 

12298  27 
axioms 
28 
someI: "P (x::'a) ==> P (SOME x. P x)" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

29 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

30 

12298  31 
constdefs 
32 
inv :: "('a => 'b) => ('b => 'a)" 

33 
"inv(f :: 'a => 'b) == %y. SOME x. f x = y" 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

34 

12298  35 
Inv :: "'a set => ('a => 'b) => ('b => 'a)" 
36 
"Inv A f == %x. SOME y. y : A & f y = x" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

37 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

38 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

39 
use "Hilbert_Choice_lemmas.ML" 
12372  40 
declare someI_ex [elim?]; 
41 

13585  42 
lemma Inv_mem: "[ f ` A = B; x \<in> B ] ==> Inv A f x \<in> A" 
43 
apply (unfold Inv_def) 

44 
apply (fast intro: someI2) 

45 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

46 

12298  47 
lemma tfl_some: "\<forall>P x. P x > P (Eps P)" 
48 
 {* dynamicallyscoped fact for TFL *} 

49 
by (blast intro: someI) 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

50 

12298  51 

52 
subsection {* Least value operator *} 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

53 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

54 
constdefs 
12298  55 
LeastM :: "['a => 'b::ord, 'a => bool] => 'a" 
56 
"LeastM m P == SOME x. P x & (ALL y. P y > m x <= m y)" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

57 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

58 
syntax 
12298  59 
"_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0, 4, 10] 10) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

60 
translations 
12298  61 
"LEAST x WRT m. P" == "LeastM m (%x. P)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

62 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

63 
lemma LeastMI2: 
12298  64 
"P x ==> (!!y. P y ==> m x <= m y) 
65 
==> (!!x. P x ==> \<forall>y. P y > m x \<le> m y ==> Q x) 

66 
==> Q (LeastM m P)" 

67 
apply (unfold LeastM_def) 

68 
apply (rule someI2_ex) 

69 
apply blast 

70 
apply blast 

71 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

72 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

73 
lemma LeastM_equality: 
12298  74 
"P k ==> (!!x. P x ==> m k <= m x) 
75 
==> m (LEAST x WRT m. P x) = (m k::'a::order)" 

76 
apply (rule LeastMI2) 

77 
apply assumption 

78 
apply blast 

79 
apply (blast intro!: order_antisym) 

80 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

81 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

82 
lemma wf_linord_ex_has_least: 
12298  83 
"wf r ==> ALL x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k 
84 
==> EX x. P x & (!y. P y > (m x,m y):r^*)" 

85 
apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) 

86 
apply (drule_tac x = "m`Collect P" in spec) 

87 
apply force 

88 
done 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

89 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

90 
lemma ex_has_least_nat: 
12298  91 
"P k ==> EX x. P x & (ALL y. P y > m x <= (m y::nat))" 
92 
apply (simp only: pred_nat_trancl_eq_le [symmetric]) 

93 
apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) 

94 
apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le) 

95 
apply assumption 

96 
done 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

97 

12298  98 
lemma LeastM_nat_lemma: 
99 
"P k ==> P (LeastM m P) & (ALL y. P y > m (LeastM m P) <= (m y::nat))" 

100 
apply (unfold LeastM_def) 

101 
apply (rule someI_ex) 

102 
apply (erule ex_has_least_nat) 

103 
done 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

104 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

105 
lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard] 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

106 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

107 
lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)" 
12298  108 
apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) 
109 
apply assumption 

110 
apply assumption 

111 
done 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

112 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

113 

12298  114 
subsection {* Greatest value operator *} 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

115 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

116 
constdefs 
12298  117 
GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" 
118 
"GreatestM m P == SOME x. P x & (ALL y. P y > m y <= m x)" 

119 

120 
Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10) 

121 
"Greatest == GreatestM (%x. x)" 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

122 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

123 
syntax 
12298  124 
"_GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" 
125 
("GREATEST _ WRT _. _" [0, 4, 10] 10) 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

126 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

127 
translations 
12298  128 
"GREATEST x WRT m. P" == "GreatestM m (%x. P)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

129 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

130 
lemma GreatestMI2: 
12298  131 
"P x ==> (!!y. P y ==> m y <= m x) 
132 
==> (!!x. P x ==> \<forall>y. P y > m y \<le> m x ==> Q x) 

133 
==> Q (GreatestM m P)" 

134 
apply (unfold GreatestM_def) 

135 
apply (rule someI2_ex) 

136 
apply blast 

137 
apply blast 

138 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

139 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

140 
lemma GreatestM_equality: 
12298  141 
"P k ==> (!!x. P x ==> m x <= m k) 
142 
==> m (GREATEST x WRT m. P x) = (m k::'a::order)" 

143 
apply (rule_tac m = m in GreatestMI2) 

144 
apply assumption 

145 
apply blast 

146 
apply (blast intro!: order_antisym) 

147 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

148 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

149 
lemma Greatest_equality: 
12298  150 
"P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k" 
151 
apply (unfold Greatest_def) 

152 
apply (erule GreatestM_equality) 

153 
apply blast 

154 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

155 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

156 
lemma ex_has_greatest_nat_lemma: 
12298  157 
"P k ==> ALL x. P x > (EX y. P y & ~ ((m y::nat) <= m x)) 
158 
==> EX y. P y & ~ (m y < m k + n)" 

159 
apply (induct_tac n) 

160 
apply force 

161 
apply (force simp add: le_Suc_eq) 

162 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

163 

12298  164 
lemma ex_has_greatest_nat: 
165 
"P k ==> ALL y. P y > m y < b 

166 
==> EX x. P x & (ALL y. P y > (m y::nat) <= m x)" 

167 
apply (rule ccontr) 

168 
apply (cut_tac P = P and n = "b  m k" in ex_has_greatest_nat_lemma) 

169 
apply (subgoal_tac [3] "m k <= b") 

170 
apply auto 

171 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

172 

12298  173 
lemma GreatestM_nat_lemma: 
174 
"P k ==> ALL y. P y > m y < b 

175 
==> P (GreatestM m P) & (ALL y. P y > (m y::nat) <= m (GreatestM m P))" 

176 
apply (unfold GreatestM_def) 

177 
apply (rule someI_ex) 

178 
apply (erule ex_has_greatest_nat) 

179 
apply assumption 

180 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

181 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

182 
lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

183 

12298  184 
lemma GreatestM_nat_le: 
185 
"P x ==> ALL y. P y > m y < b 

186 
==> (m x::nat) <= m (GreatestM m P)" 

187 
apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 

188 
done 

189 

190 

191 
text {* \medskip Specialization to @{text GREATEST}. *} 

192 

193 
lemma GreatestI: "P (k::nat) ==> ALL y. P y > y < b ==> P (GREATEST x. P x)" 

194 
apply (unfold Greatest_def) 

195 
apply (rule GreatestM_natI) 

196 
apply auto 

197 
done 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

198 

12298  199 
lemma Greatest_le: 
200 
"P x ==> ALL y. P y > y < b ==> (x::nat) <= (GREATEST x. P x)" 

201 
apply (unfold Greatest_def) 

202 
apply (rule GreatestM_nat_le) 

203 
apply auto 

204 
done 

205 

206 

207 
subsection {* The Meson proof procedure *} 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

208 

12298  209 
subsubsection {* Negation Normal Form *} 
210 

211 
text {* de Morgan laws *} 

212 

213 
lemma meson_not_conjD: "~(P&Q) ==> ~P  ~Q" 

214 
and meson_not_disjD: "~(PQ) ==> ~P & ~Q" 

215 
and meson_not_notD: "~~P ==> P" 

216 
and meson_not_allD: "!!P. ~(ALL x. P(x)) ==> EX x. ~P(x)" 

217 
and meson_not_exD: "!!P. ~(EX x. P(x)) ==> ALL x. ~P(x)" 

218 
by fast+ 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

219 

12298  220 
text {* Removal of @{text ">"} and @{text "<>"} (positive and 
221 
negative occurrences) *} 

222 

223 
lemma meson_imp_to_disjD: "P>Q ==> ~P  Q" 

224 
and meson_not_impD: "~(P>Q) ==> P & ~Q" 

225 
and meson_iff_to_disjD: "P=Q ==> (~P  Q) & (~Q  P)" 

226 
and meson_not_iffD: "~(P=Q) ==> (P  Q) & (~P  ~Q)" 

227 
 {* Much more efficient than @{prop "(P & ~Q)  (Q & ~P)"} for computing CNF *} 

228 
by fast+ 

229 

230 

231 
subsubsection {* Pulling out the existential quantifiers *} 

232 

233 
text {* Conjunction *} 

234 

235 
lemma meson_conj_exD1: "!!P Q. (EX x. P(x)) & Q ==> EX x. P(x) & Q" 

236 
and meson_conj_exD2: "!!P Q. P & (EX x. Q(x)) ==> EX x. P & Q(x)" 

237 
by fast+ 

238 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

239 

12298  240 
text {* Disjunction *} 
241 

242 
lemma meson_disj_exD: "!!P Q. (EX x. P(x))  (EX x. Q(x)) ==> EX x. P(x)  Q(x)" 

243 
 {* DO NOT USE with forallSkolemization: makes fewer schematic variables!! *} 

244 
 {* With exSkolemization, makes fewer Skolem constants *} 

245 
and meson_disj_exD1: "!!P Q. (EX x. P(x))  Q ==> EX x. P(x)  Q" 

246 
and meson_disj_exD2: "!!P Q. P  (EX x. Q(x)) ==> EX x. P  Q(x)" 

247 
by fast+ 

248 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

249 

12298  250 
subsubsection {* Generating clauses for the Meson Proof Procedure *} 
251 

252 
text {* Disjunctions *} 

253 

254 
lemma meson_disj_assoc: "(PQ)R ==> P(QR)" 

255 
and meson_disj_comm: "PQ ==> QP" 

256 
and meson_disj_FalseD1: "FalseP ==> P" 

257 
and meson_disj_FalseD2: "PFalse ==> P" 

258 
by fast+ 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

259 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

260 
use "meson_lemmas.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

261 
use "Tools/meson.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

262 
setup meson_setup 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

263 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

264 
end 