author  wenzelm 
Thu, 01 Dec 2005 22:03:01 +0100  
changeset 18324  d1c4b1112e33 
parent 17876  b9c92f384109 
child 24893  b8ef7afe3a6b 
permissions  rwrr 
2469  1 
(* Title: ZF/AC/OrdQuant.thy 
2 
ID: $Id$ 

3 
Authors: Krzysztof Grabczewski and L C Paulson 

4 
*) 

5 

13253  6 
header {*Special quantifiers*} 
7 

16417  8 
theory OrdQuant imports Ordinal begin 
2469  9 

13253  10 
subsection {*Quantifiers and union operator for ordinals*} 
11 

12620  12 
constdefs 
13298  13 

2469  14 
(* Ordinal Quantifiers *) 
12620  15 
oall :: "[i, i => o] => o" 
16 
"oall(A, P) == ALL x. x<A > P(x)" 

13298  17 

12620  18 
oex :: "[i, i => o] => o" 
19 
"oex(A, P) == EX x. x<A & P(x)" 

2469  20 

21 
(* Ordinal Union *) 

12620  22 
OUnion :: "[i, i => i] => i" 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

23 
"OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}" 
13298  24 

2469  25 
syntax 
12620  26 
"@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10) 
27 
"@oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10) 

28 
"@OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10) 

2469  29 

30 
translations 

31 
"ALL x<a. P" == "oall(a, %x. P)" 

32 
"EX x<a. P" == "oex(a, %x. P)" 

33 
"UN x<a. B" == "OUnion(a, %x. B)" 

34 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
6093
diff
changeset

35 
syntax (xsymbols) 
12620  36 
"@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10) 
37 
"@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10) 

38 
"@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10) 

14565  39 
syntax (HTML output) 
40 
"@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10) 

41 
"@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10) 

42 
"@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10) 

12620  43 

44 

13302  45 
subsubsection {*simplification of the new quantifiers*} 
12825  46 

47 

13169  48 
(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize 
13298  49 
is proved. Ord_atomize would convert this rule to 
12825  50 
x < 0 ==> P(x) == True, which causes dire effects!*) 
51 
lemma [simp]: "(ALL x<0. P(x))" 

13298  52 
by (simp add: oall_def) 
12825  53 

54 
lemma [simp]: "~(EX x<0. P(x))" 

13298  55 
by (simp add: oex_def) 
12825  56 

57 
lemma [simp]: "(ALL x<succ(i). P(x)) <> (Ord(i) > P(i) & (ALL x<i. P(x)))" 

13298  58 
apply (simp add: oall_def le_iff) 
59 
apply (blast intro: lt_Ord2) 

12825  60 
done 
61 

62 
lemma [simp]: "(EX x<succ(i). P(x)) <> (Ord(i) & (P(i)  (EX x<i. P(x))))" 

13298  63 
apply (simp add: oex_def le_iff) 
64 
apply (blast intro: lt_Ord2) 

12825  65 
done 
66 

13302  67 
subsubsection {*Union over ordinals*} 
13118  68 

12620  69 
lemma Ord_OUN [intro,simp]: 
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13149
diff
changeset

70 
"[ !!x. x<A ==> Ord(B(x)) ] ==> Ord(\<Union>x<A. B(x))" 
13298  71 
by (simp add: OUnion_def ltI Ord_UN) 
12620  72 

73 
lemma OUN_upper_lt: 

13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13149
diff
changeset

74 
"[ a<A; i < b(a); Ord(\<Union>x<A. b(x)) ] ==> i < (\<Union>x<A. b(x))" 
12620  75 
by (unfold OUnion_def lt_def, blast ) 
76 

77 
lemma OUN_upper_le: 

13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13149
diff
changeset

78 
"[ a<A; i\<le>b(a); Ord(\<Union>x<A. b(x)) ] ==> i \<le> (\<Union>x<A. b(x))" 
12820  79 
apply (unfold OUnion_def, auto) 
12620  80 
apply (rule UN_upper_le ) 
13298  81 
apply (auto simp add: lt_def) 
12620  82 
done 
2469  83 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

84 
lemma Limit_OUN_eq: "Limit(i) ==> (\<Union>x<i. x) = i" 
12620  85 
by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord) 
86 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

87 
(* No < version; consider (\<Union>i\<in>nat.i)=nat *) 
12620  88 
lemma OUN_least: 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

89 
"(!!x. x<A ==> B(x) \<subseteq> C) ==> (\<Union>x<A. B(x)) \<subseteq> C" 
12620  90 
by (simp add: OUnion_def UN_least ltI) 
91 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

92 
(* No < version; consider (\<Union>i\<in>nat.i)=nat *) 
12620  93 
lemma OUN_least_le: 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

94 
"[ Ord(i); !!x. x<A ==> b(x) \<le> i ] ==> (\<Union>x<A. b(x)) \<le> i" 
12620  95 
by (simp add: OUnion_def UN_least_le ltI Ord_0_le) 
96 

97 
lemma le_implies_OUN_le_OUN: 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

98 
"[ !!x. x<A ==> c(x) \<le> d(x) ] ==> (\<Union>x<A. c(x)) \<le> (\<Union>x<A. d(x))" 
12620  99 
by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN) 
100 

101 
lemma OUN_UN_eq: 

102 
"(!!x. x:A ==> Ord(B(x))) 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

103 
==> (\<Union>z < (\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z < B(x). C(z))" 
13298  104 
by (simp add: OUnion_def) 
12620  105 

106 
lemma OUN_Union_eq: 

107 
"(!!x. x:X ==> Ord(x)) 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

108 
==> (\<Union>z < Union(X). C(z)) = (\<Union>x\<in>X. \<Union>z < x. C(z))" 
13298  109 
by (simp add: OUnion_def) 
12620  110 

12763  111 
(*So that rule_format will get rid of ALL x<A...*) 
112 
lemma atomize_oall [symmetric, rulify]: 

113 
"(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))" 

114 
by (simp add: oall_def atomize_all atomize_imp) 

115 

13302  116 
subsubsection {*universal quantifier for ordinals*} 
13169  117 

118 
lemma oallI [intro!]: 

119 
"[ !!x. x<A ==> P(x) ] ==> ALL x<A. P(x)" 

13298  120 
by (simp add: oall_def) 
13169  121 

122 
lemma ospec: "[ ALL x<A. P(x); x<A ] ==> P(x)" 

13298  123 
by (simp add: oall_def) 
13169  124 

125 
lemma oallE: 

126 
"[ ALL x<A. P(x); P(x) ==> Q; ~x<A ==> Q ] ==> Q" 

13298  127 
by (simp add: oall_def, blast) 
13169  128 

129 
lemma rev_oallE [elim]: 

130 
"[ ALL x<A. P(x); ~x<A ==> Q; P(x) ==> Q ] ==> Q" 

13298  131 
by (simp add: oall_def, blast) 
13169  132 

133 

134 
(*Trival rewrite rule; (ALL x<a.P)<>P holds only if a is not 0!*) 

135 
lemma oall_simp [simp]: "(ALL x<a. True) <> True" 

13170  136 
by blast 
13169  137 

138 
(*Congruence rule for rewriting*) 

139 
lemma oall_cong [cong]: 

13298  140 
"[ a=a'; !!x. x<a' ==> P(x) <> P'(x) ] 
13289
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

141 
==> oall(a, %x. P(x)) <> oall(a', %x. P'(x))" 
13169  142 
by (simp add: oall_def) 
143 

144 

13302  145 
subsubsection {*existential quantifier for ordinals*} 
13169  146 

147 
lemma oexI [intro]: 

148 
"[ P(x); x<A ] ==> EX x<A. P(x)" 

13298  149 
apply (simp add: oex_def, blast) 
13169  150 
done 
151 

152 
(*Not of the general form for such rules; ~EX has become ALL~ *) 

153 
lemma oexCI: 

154 
"[ ALL x<A. ~P(x) ==> P(a); a<A ] ==> EX x<A. P(x)" 

13298  155 
apply (simp add: oex_def, blast) 
13169  156 
done 
157 

158 
lemma oexE [elim!]: 

159 
"[ EX x<A. P(x); !!x. [ x<A; P(x) ] ==> Q ] ==> Q" 

13298  160 
apply (simp add: oex_def, blast) 
13169  161 
done 
162 

163 
lemma oex_cong [cong]: 

13298  164 
"[ a=a'; !!x. x<a' ==> P(x) <> P'(x) ] 
13289
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

165 
==> oex(a, %x. P(x)) <> oex(a', %x. P'(x))" 
13169  166 
apply (simp add: oex_def cong add: conj_cong) 
167 
done 

168 

169 

13302  170 
subsubsection {*Rules for OrdinalIndexed Unions*} 
13169  171 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

172 
lemma OUN_I [intro]: "[ a<i; b: B(a) ] ==> b: (\<Union>z<i. B(z))" 
13170  173 
by (unfold OUnion_def lt_def, blast) 
13169  174 

175 
lemma OUN_E [elim!]: 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

176 
"[ b : (\<Union>z<i. B(z)); !!a.[ b: B(a); a<i ] ==> R ] ==> R" 
13170  177 
apply (unfold OUnion_def lt_def, blast) 
13169  178 
done 
179 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

180 
lemma OUN_iff: "b : (\<Union>x<i. B(x)) <> (EX x<i. b : B(x))" 
13170  181 
by (unfold OUnion_def oex_def lt_def, blast) 
13169  182 

183 
lemma OUN_cong [cong]: 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

184 
"[ i=j; !!x. x<j ==> C(x)=D(x) ] ==> (\<Union>x<i. C(x)) = (\<Union>x<j. D(x))" 
13169  185 
by (simp add: OUnion_def lt_def OUN_iff) 
186 

13298  187 
lemma lt_induct: 
13169  188 
"[ i<k; !!x.[ x<k; ALL y<x. P(y) ] ==> P(x) ] ==> P(i)" 
189 
apply (simp add: lt_def oall_def) 

13298  190 
apply (erule conjE) 
191 
apply (erule Ord_induct, assumption, blast) 

13169  192 
done 
193 

13253  194 

195 
subsection {*Quantification over a class*} 

196 

197 
constdefs 

198 
"rall" :: "[i=>o, i=>o] => o" 

199 
"rall(M, P) == ALL x. M(x) > P(x)" 

200 

201 
"rex" :: "[i=>o, i=>o] => o" 

202 
"rex(M, P) == EX x. M(x) & P(x)" 

203 

204 
syntax 

205 
"@rall" :: "[pttrn, i=>o, o] => o" ("(3ALL _[_]./ _)" 10) 

206 
"@rex" :: "[pttrn, i=>o, o] => o" ("(3EX _[_]./ _)" 10) 

207 

208 
syntax (xsymbols) 

209 
"@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10) 

210 
"@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10) 

14565  211 
syntax (HTML output) 
212 
"@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10) 

213 
"@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10) 

13253  214 

215 
translations 

216 
"ALL x[M]. P" == "rall(M, %x. P)" 

217 
"EX x[M]. P" == "rex(M, %x. P)" 

218 

13298  219 

220 
subsubsection{*Relativized universal quantifier*} 

13253  221 

222 
lemma rallI [intro!]: "[ !!x. M(x) ==> P(x) ] ==> ALL x[M]. P(x)" 

223 
by (simp add: rall_def) 

224 

225 
lemma rspec: "[ ALL x[M]. P(x); M(x) ] ==> P(x)" 

226 
by (simp add: rall_def) 

227 

228 
(*Instantiates x first: better for automatic theorem proving?*) 

13298  229 
lemma rev_rallE [elim]: 
13253  230 
"[ ALL x[M]. P(x); ~ M(x) ==> Q; P(x) ==> Q ] ==> Q" 
13298  231 
by (simp add: rall_def, blast) 
13253  232 

233 
lemma rallE: "[ ALL x[M]. P(x); P(x) ==> Q; ~ M(x) ==> Q ] ==> Q" 

234 
by blast 

235 

236 
(*Trival rewrite rule; (ALL x[M].P)<>P holds only if A is nonempty!*) 

237 
lemma rall_triv [simp]: "(ALL x[M]. P) <> ((EX x. M(x)) > P)" 

238 
by (simp add: rall_def) 

239 

240 
(*Congruence rule for rewriting*) 

241 
lemma rall_cong [cong]: 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13302
diff
changeset

242 
"(!!x. M(x) ==> P(x) <> P'(x)) ==> (ALL x[M]. P(x)) <> (ALL x[M]. P'(x))" 
13253  243 
by (simp add: rall_def) 
244 

13298  245 

246 
subsubsection{*Relativized existential quantifier*} 

13253  247 

248 
lemma rexI [intro]: "[ P(x); M(x) ] ==> EX x[M]. P(x)" 

249 
by (simp add: rex_def, blast) 

250 

251 
(*The best argument order when there is only one M(x)*) 

252 
lemma rev_rexI: "[ M(x); P(x) ] ==> EX x[M]. P(x)" 

253 
by blast 

254 

255 
(*Not of the general form for such rules; ~EX has become ALL~ *) 

256 
lemma rexCI: "[ ALL x[M]. ~P(x) ==> P(a); M(a) ] ==> EX x[M]. P(x)" 

257 
by blast 

258 

259 
lemma rexE [elim!]: "[ EX x[M]. P(x); !!x. [ M(x); P(x) ] ==> Q ] ==> Q" 

260 
by (simp add: rex_def, blast) 

261 

262 
(*We do not even have (EX x[M]. True) <> True unless A is nonempty!!*) 

263 
lemma rex_triv [simp]: "(EX x[M]. P) <> ((EX x. M(x)) & P)" 

264 
by (simp add: rex_def) 

265 

266 
lemma rex_cong [cong]: 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13302
diff
changeset

267 
"(!!x. M(x) ==> P(x) <> P'(x)) ==> (EX x[M]. P(x)) <> (EX x[M]. P'(x))" 
13253  268 
by (simp add: rex_def cong: conj_cong) 
269 

13289
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

270 
lemma rall_is_ball [simp]: "(\<forall>x[%z. z\<in>A]. P(x)) <> (\<forall>x\<in>A. P(x))" 
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

271 
by blast 
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

272 

53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

273 
lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <> (\<exists>x\<in>A. P(x))" 
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

274 
by blast 
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

275 

13253  276 
lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (ALL x[M]. P(x))"; 
277 
by (simp add: rall_def atomize_all atomize_imp) 

278 

279 
declare atomize_rall [symmetric, rulify] 

280 

281 
lemma rall_simps1: 

282 
"(ALL x[M]. P(x) & Q) <> (ALL x[M]. P(x)) & ((ALL x[M]. False)  Q)" 

283 
"(ALL x[M]. P(x)  Q) <> ((ALL x[M]. P(x))  Q)" 

284 
"(ALL x[M]. P(x) > Q) <> ((EX x[M]. P(x)) > Q)" 

13298  285 
"(~(ALL x[M]. P(x))) <> (EX x[M]. ~P(x))" 
13253  286 
by blast+ 
287 

288 
lemma rall_simps2: 

289 
"(ALL x[M]. P & Q(x)) <> ((ALL x[M]. False)  P) & (ALL x[M]. Q(x))" 

290 
"(ALL x[M]. P  Q(x)) <> (P  (ALL x[M]. Q(x)))" 

291 
"(ALL x[M]. P > Q(x)) <> (P > (ALL x[M]. Q(x)))" 

292 
by blast+ 

293 

13289
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

294 
lemmas rall_simps [simp] = rall_simps1 rall_simps2 
13253  295 

296 
lemma rall_conj_distrib: 

297 
"(ALL x[M]. P(x) & Q(x)) <> ((ALL x[M]. P(x)) & (ALL x[M]. Q(x)))" 

298 
by blast 

299 

300 
lemma rex_simps1: 

301 
"(EX x[M]. P(x) & Q) <> ((EX x[M]. P(x)) & Q)" 

302 
"(EX x[M]. P(x)  Q) <> (EX x[M]. P(x))  ((EX x[M]. True) & Q)" 

303 
"(EX x[M]. P(x) > Q) <> ((ALL x[M]. P(x)) > ((EX x[M]. True) & Q))" 

304 
"(~(EX x[M]. P(x))) <> (ALL x[M]. ~P(x))" 

305 
by blast+ 

306 

307 
lemma rex_simps2: 

308 
"(EX x[M]. P & Q(x)) <> (P & (EX x[M]. Q(x)))" 

309 
"(EX x[M]. P  Q(x)) <> ((EX x[M]. True) & P)  (EX x[M]. Q(x))" 

310 
"(EX x[M]. P > Q(x)) <> (((ALL x[M]. False)  P) > (EX x[M]. Q(x)))" 

311 
by blast+ 

312 

13289
53e201efdaa2
miniscoping for classbounded quantifiers (rall and rex)
paulson
parents:
13253
diff
changeset

313 
lemmas rex_simps [simp] = rex_simps1 rex_simps2 
13253  314 

315 
lemma rex_disj_distrib: 

316 
"(EX x[M]. P(x)  Q(x)) <> ((EX x[M]. P(x))  (EX x[M]. Q(x)))" 

317 
by blast 

318 

319 

13298  320 
subsubsection{*Onepoint rule for bounded quantifiers*} 
13253  321 

322 
lemma rex_triv_one_point1 [simp]: "(EX x[M]. x=a) <> ( M(a))" 

323 
by blast 

324 

325 
lemma rex_triv_one_point2 [simp]: "(EX x[M]. a=x) <> ( M(a))" 

326 
by blast 

327 

328 
lemma rex_one_point1 [simp]: "(EX x[M]. x=a & P(x)) <> ( M(a) & P(a))" 

329 
by blast 

330 

331 
lemma rex_one_point2 [simp]: "(EX x[M]. a=x & P(x)) <> ( M(a) & P(a))" 

332 
by blast 

333 

334 
lemma rall_one_point1 [simp]: "(ALL x[M]. x=a > P(x)) <> ( M(a) > P(a))" 

335 
by blast 

336 

337 
lemma rall_one_point2 [simp]: "(ALL x[M]. a=x > P(x)) <> ( M(a) > P(a))" 

338 
by blast 

339 

340 

13298  341 
subsubsection{*Sets as Classes*} 
342 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13615
diff
changeset

343 
constdefs setclass :: "[i,i] => o" ("##_" [40] 40) 
13362  344 
"setclass(A) == %x. x : A" 
13298  345 

13362  346 
lemma setclass_iff [simp]: "setclass(A,x) <> x : A" 
347 
by (simp add: setclass_def) 

13298  348 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13615
diff
changeset

349 
lemma rall_setclass_is_ball [simp]: "(\<forall>x[##A]. P(x)) <> (\<forall>x\<in>A. P(x))" 
13298  350 
by auto 
351 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13615
diff
changeset

352 
lemma rex_setclass_is_bex [simp]: "(\<exists>x[##A]. P(x)) <> (\<exists>x\<in>A. P(x))" 
13298  353 
by auto 
354 

355 

13169  356 
ML 
357 
{* 

358 
val oall_def = thm "oall_def" 

359 
val oex_def = thm "oex_def" 

360 
val OUnion_def = thm "OUnion_def" 

361 

362 
val oallI = thm "oallI"; 

363 
val ospec = thm "ospec"; 

364 
val oallE = thm "oallE"; 

365 
val rev_oallE = thm "rev_oallE"; 

366 
val oall_simp = thm "oall_simp"; 

367 
val oall_cong = thm "oall_cong"; 

368 
val oexI = thm "oexI"; 

369 
val oexCI = thm "oexCI"; 

370 
val oexE = thm "oexE"; 

371 
val oex_cong = thm "oex_cong"; 

372 
val OUN_I = thm "OUN_I"; 

373 
val OUN_E = thm "OUN_E"; 

374 
val OUN_iff = thm "OUN_iff"; 

375 
val OUN_cong = thm "OUN_cong"; 

376 
val lt_induct = thm "lt_induct"; 

377 

13253  378 
val rall_def = thm "rall_def" 
379 
val rex_def = thm "rex_def" 

380 

381 
val rallI = thm "rallI"; 

382 
val rspec = thm "rspec"; 

383 
val rallE = thm "rallE"; 

384 
val rev_oallE = thm "rev_oallE"; 

385 
val rall_cong = thm "rall_cong"; 

386 
val rexI = thm "rexI"; 

387 
val rexCI = thm "rexCI"; 

388 
val rexE = thm "rexE"; 

389 
val rex_cong = thm "rex_cong"; 

390 

13169  391 
val Ord_atomize = 
13253  392 
atomize ([("OrdQuant.oall", [ospec]),("OrdQuant.rall", [rspec])]@ 
13298  393 
ZF_conn_pairs, 
13253  394 
ZF_mem_pairs); 
17876  395 
change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all)); 
13169  396 
*} 
397 

13462  398 
text {* Setting up the onepointrule simproc *} 
13253  399 

13462  400 
ML_setup {* 
401 
local 

13253  402 

18324  403 
val unfold_rex_tac = unfold_tac [rex_def]; 
404 
fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac; 

13253  405 
val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac; 
406 

18324  407 
val unfold_rall_tac = unfold_tac [rall_def]; 
408 
fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac; 

13253  409 
val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac; 
410 

411 
in 

412 

17002  413 
val defREX_regroup = Simplifier.simproc (the_context ()) 
13462  414 
"defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex; 
17002  415 
val defRALL_regroup = Simplifier.simproc (the_context ()) 
13462  416 
"defined RALL" ["ALL x[M]. P(x) > Q(x)"] rearrange_ball; 
13253  417 

418 
end; 

13462  419 

420 
Addsimprocs [defRALL_regroup,defREX_regroup]; 

13253  421 
*} 
422 

2469  423 
end 