author  wenzelm 
Wed, 19 Mar 2008 22:47:35 +0100  
changeset 26339  7825c83c9eff 
parent 24893  b8ef7afe3a6b 
child 26480  544cef16045b 
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 

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

24893  17 
definition 
18 
oex :: "[i, i => o] => o" where 

12620  19 
"oex(A, P) == EX x. x<A & P(x)" 
2469  20 

24893  21 
definition 
2469  22 
(* Ordinal Union *) 
24893  23 
OUnion :: "[i, i => i] => i" where 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13462
diff
changeset

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

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

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

2469  30 

31 
translations 

24893  32 
"ALL x<a. P" == "CONST oall(a, %x. P)" 
33 
"EX x<a. P" == "CONST oex(a, %x. P)" 

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

2469  35 

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

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

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

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

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

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

12620  44 

45 

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

48 

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

13298  53 
by (simp add: oall_def) 
12825  54 

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

13298  56 
by (simp add: oex_def) 
12825  57 

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

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

12825  61 
done 
62 

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

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

12825  66 
done 
67 

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

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

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

74 
lemma OUN_upper_lt: 

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

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

78 
lemma OUN_upper_le: 

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

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

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

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

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

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

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

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

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

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

98 
lemma le_implies_OUN_le_OUN: 

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

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

102 
lemma OUN_UN_eq: 

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

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

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

107 
lemma OUN_Union_eq: 

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

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

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

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

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

115 
by (simp add: oall_def atomize_all atomize_imp) 

116 

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

119 
lemma oallI [intro!]: 

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

13298  121 
by (simp add: oall_def) 
13169  122 

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

13298  124 
by (simp add: oall_def) 
13169  125 

126 
lemma oallE: 

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

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

130 
lemma rev_oallE [elim]: 

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

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

134 

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

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

13170  137 
by blast 
13169  138 

139 
(*Congruence rule for rewriting*) 

140 
lemma oall_cong [cong]: 

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

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

145 

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

148 
lemma oexI [intro]: 

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

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

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

154 
lemma oexCI: 

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

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

159 
lemma oexE [elim!]: 

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

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

164 
lemma oex_cong [cong]: 

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

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

169 

170 

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

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

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

176 
lemma OUN_E [elim!]: 

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

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

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

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

184 
lemma OUN_cong [cong]: 

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

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

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

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

13169  193 
done 
194 

13253  195 

196 
subsection {*Quantification over a class*} 

197 

24893  198 
definition 
199 
"rall" :: "[i=>o, i=>o] => o" where 

13253  200 
"rall(M, P) == ALL x. M(x) > P(x)" 
201 

24893  202 
definition 
203 
"rex" :: "[i=>o, i=>o] => o" where 

13253  204 
"rex(M, P) == EX x. M(x) & P(x)" 
205 

206 
syntax 

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

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

209 

210 
syntax (xsymbols) 

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

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

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

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

13253  216 

217 
translations 

24893  218 
"ALL x[M]. P" == "CONST rall(M, %x. P)" 
219 
"EX x[M]. P" == "CONST rex(M, %x. P)" 

13253  220 

13298  221 

222 
subsubsection{*Relativized universal quantifier*} 

13253  223 

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

225 
by (simp add: rall_def) 

226 

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

228 
by (simp add: rall_def) 

229 

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

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

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

236 
by blast 

237 

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

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

240 
by (simp add: rall_def) 

241 

242 
(*Congruence rule for rewriting*) 

243 
lemma rall_cong [cong]: 

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

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

13298  247 

248 
subsubsection{*Relativized existential quantifier*} 

13253  249 

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

251 
by (simp add: rex_def, blast) 

252 

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

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

255 
by blast 

256 

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

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

259 
by blast 

260 

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

262 
by (simp add: rex_def, blast) 

263 

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

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

266 
by (simp add: rex_def) 

267 

268 
lemma rex_cong [cong]: 

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

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

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

272 
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

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

274 

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

275 
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

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

277 

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

280 

281 
declare atomize_rall [symmetric, rulify] 

282 

283 
lemma rall_simps1: 

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

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

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

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

290 
lemma rall_simps2: 

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

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

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

294 
by blast+ 

295 

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

296 
lemmas rall_simps [simp] = rall_simps1 rall_simps2 
13253  297 

298 
lemma rall_conj_distrib: 

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

300 
by blast 

301 

302 
lemma rex_simps1: 

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

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

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

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

307 
by blast+ 

308 

309 
lemma rex_simps2: 

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

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

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

313 
by blast+ 

314 

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

315 
lemmas rex_simps [simp] = rex_simps1 rex_simps2 
13253  316 

317 
lemma rex_disj_distrib: 

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

319 
by blast 

320 

321 

13298  322 
subsubsection{*Onepoint rule for bounded quantifiers*} 
13253  323 

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

325 
by blast 

326 

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

328 
by blast 

329 

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

331 
by blast 

332 

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

334 
by blast 

335 

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

337 
by blast 

338 

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

340 
by blast 

341 

342 

13298  343 
subsubsection{*Sets as Classes*} 
344 

24893  345 
definition 
346 
setclass :: "[i,i] => o" ("##_" [40] 40) where 

13362  347 
"setclass(A) == %x. x : A" 
13298  348 

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

13298  351 

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

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

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

355 
lemma rex_setclass_is_bex [simp]: "(\<exists>x[##A]. P(x)) <> (\<exists>x\<in>A. P(x))" 
13298  356 
by auto 
357 

358 

13169  359 
ML 
360 
{* 

361 
val Ord_atomize = 

24893  362 
atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@ 
13298  363 
ZF_conn_pairs, 
13253  364 
ZF_mem_pairs); 
26339  365 
*} 
366 
declaration {* fn _ => 

367 
Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all)) 

13169  368 
*} 
369 

13462  370 
text {* Setting up the onepointrule simproc *} 
13253  371 

13462  372 
ML_setup {* 
373 
local 

13253  374 

24893  375 
val unfold_rex_tac = unfold_tac [@{thm rex_def}]; 
18324  376 
fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac; 
13253  377 
val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac; 
378 

24893  379 
val unfold_rall_tac = unfold_tac [@{thm rall_def}]; 
18324  380 
fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac; 
13253  381 
val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac; 
382 

383 
in 

384 

24893  385 
val defREX_regroup = Simplifier.simproc @{theory} 
13462  386 
"defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex; 
24893  387 
val defRALL_regroup = Simplifier.simproc @{theory} 
13462  388 
"defined RALL" ["ALL x[M]. P(x) > Q(x)"] rearrange_ball; 
13253  389 

390 
end; 

13462  391 

392 
Addsimprocs [defRALL_regroup,defREX_regroup]; 

13253  393 
*} 
394 

2469  395 
end 