DeepSyntaxScript.sml
1Theory DeepSyntax
2Ancestors
3 integer int_arith pred_set
4Libs
5 Datatype simpLib
6
7val _ = ParseExtras.temp_loose_equality()
8
9Datatype:
10 deep_form =
11 Conjn deep_form deep_form
12 | Disjn deep_form deep_form
13 | Negn deep_form
14 | UnrelatedBool bool
15 | xLT int | LTx int
16 | xEQ int
17 | xDivided int int
18End
19
20Definition eval_form_def:
21 (eval_form (Conjn f1 f2) x = eval_form f1 x /\ eval_form f2 x) /\
22 (eval_form (Disjn f1 f2) x = eval_form f1 x \/ eval_form f2 x) /\
23 (eval_form (Negn f) x = ~eval_form f x) /\
24 (eval_form (UnrelatedBool b) x = b) /\
25 (eval_form (xLT i) x = x < i) /\
26 (eval_form (LTx i) x = i < x) /\
27 (eval_form (xEQ i) x = (x = i)) /\
28 (eval_form (xDivided i1 i2) x = i1 int_divides x + i2)
29End
30
31Definition neginf_def:
32 (neginf (Conjn f1 f2) = Conjn (neginf f1) (neginf f2)) /\
33 (neginf (Disjn f1 f2) = Disjn (neginf f1) (neginf f2)) /\
34 (neginf (Negn f) = Negn (neginf f)) /\
35 (neginf (UnrelatedBool b) = UnrelatedBool b) /\
36 (neginf (xLT i) = UnrelatedBool T) /\
37 (neginf (LTx i) = UnrelatedBool F) /\
38 (neginf (xEQ i) = UnrelatedBool F) /\
39 (neginf (xDivided i1 i2) = xDivided i1 i2)
40End
41
42Definition posinf_def:
43 (posinf (Conjn f1 f2) = Conjn (posinf f1) (posinf f2)) /\
44 (posinf (Disjn f1 f2) = Disjn (posinf f1) (posinf f2)) /\
45 (posinf (Negn f) = Negn (posinf f)) /\
46 (posinf (UnrelatedBool b) = UnrelatedBool b) /\
47 (posinf (xLT i) = UnrelatedBool F) /\
48 (posinf (LTx i) = UnrelatedBool T) /\
49 (posinf (xEQ i) = UnrelatedBool F) /\
50 (posinf (xDivided i1 i2) = xDivided i1 i2)
51End
52
53Theorem neginf_ok:
54 !f. ?y. !x. x < y ==> (eval_form f x = eval_form (neginf f) x)
55Proof
56 Induct THEN SRW_TAC [][eval_form_def, neginf_def] THENL [
57 Q.EXISTS_TAC `int_min y y'` THEN PROVE_TAC [INT_MIN_LT],
58 Q.EXISTS_TAC `int_min y y'` THEN PROVE_TAC [INT_MIN_LT],
59 PROVE_TAC [],
60 PROVE_TAC [INT_LT_GT],
61 PROVE_TAC [INT_LT_REFL]
62 ]
63QED
64
65Theorem posinf_ok:
66 !f. ?y. !x. y < x ==> (eval_form f x = eval_form (posinf f) x)
67Proof
68 Induct THEN SRW_TAC [][eval_form_def, posinf_def] THENL [
69 Q.EXISTS_TAC `int_max y y'` THEN PROVE_TAC [INT_MAX_LT],
70 Q.EXISTS_TAC `int_max y y'` THEN PROVE_TAC [INT_MAX_LT],
71 PROVE_TAC [INT_LT_GT],
72 PROVE_TAC [],
73 PROVE_TAC [INT_LT_REFL]
74 ]
75QED
76
77Definition alldivide_def:
78 (alldivide (Conjn f1 f2) d = alldivide f1 d /\ alldivide f2 d) /\
79 (alldivide (Disjn f1 f2) d = alldivide f1 d /\ alldivide f2 d) /\
80 (alldivide (Negn f) d = alldivide f d) /\
81 (alldivide (UnrelatedBool b) d = T) /\
82 (alldivide (xLT i) d = T) /\
83 (alldivide (LTx i) d = T) /\
84 (alldivide (xEQ i) d = T) /\
85 (alldivide (xDivided i1 i2) d = i1 int_divides d)
86End
87
88Theorem add_d_neginf:
89 !f x y d. alldivide f d ==>
90 (eval_form (neginf f) x = eval_form (neginf f) (x + y * d))
91Proof
92 Induct THEN SRW_TAC [][eval_form_def, neginf_def, alldivide_def] THENL [
93 PROVE_TAC [],
94 PROVE_TAC [],
95 `i int_divides y * d` by PROVE_TAC [INT_DIVIDES_RMUL] THEN
96 `x + y * d + i0 = y * d + (x + i0)` by
97 CONV_TAC (AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM)) THEN
98 PROVE_TAC [INT_DIVIDES_LADD]
99 ]
100QED
101
102Theorem add_d_posinf:
103 !f x y d. alldivide f d ==>
104 (eval_form (posinf f) x = eval_form (posinf f) (x + y * d))
105Proof
106 Induct THEN SRW_TAC [][eval_form_def, posinf_def, alldivide_def] THENL [
107 PROVE_TAC [],
108 PROVE_TAC [],
109 `i int_divides y * d` by PROVE_TAC [INT_DIVIDES_RMUL] THEN
110 `x + y * d + i0 = y * d + (x + i0)` by
111 CONV_TAC (AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM)) THEN
112 PROVE_TAC [INT_DIVIDES_LADD]
113 ]
114QED
115
116Theorem neginf_disj1_implies_exoriginal:
117 !f d i.
118 alldivide f d ==> 0 < i /\ i <= d /\ eval_form (neginf f) i ==>
119 ?x. eval_form f x
120Proof
121 SRW_TAC [][] THEN
122 STRIP_ASSUME_TAC (Q.SPEC `f` neginf_ok) THEN
123 `0 < d` by PROVE_TAC [INT_LTE_TRANS] THEN
124 `?c. i - c * d < y` by PROVE_TAC [can_get_small] THEN
125 FULL_SIMP_TAC std_ss [int_sub, INT_NEG_LMUL] THEN
126 PROVE_TAC [add_d_neginf]
127QED
128
129Theorem posinf_disj1_implies_exoriginal:
130 !f d i.
131 alldivide f d ==> 0 < i /\ i <= d /\ eval_form (posinf f) i ==>
132 ?x. eval_form f x
133Proof
134 SRW_TAC [][] THEN
135 STRIP_ASSUME_TAC (Q.SPEC `f` posinf_ok) THEN
136 `0 < d` by PROVE_TAC [INT_LTE_TRANS] THEN
137 `?c. y < i + c * d` by PROVE_TAC [can_get_big] THEN
138 PROVE_TAC [add_d_posinf]
139QED
140
141Definition Aset_def:
142 (Aset pos (Conjn f1 f2) = Aset pos f1 UNION Aset pos f2) /\
143 (Aset pos (Disjn f1 f2) = Aset pos f1 UNION Aset pos f2) /\
144 (Aset pos (Negn f) = Aset (~pos) f) /\
145 (Aset pos (UnrelatedBool b) = {}) /\
146 (Aset pos (xLT i) = if pos then {i} else {}) /\
147 (Aset pos (LTx i) = if pos then {} else {i + 1}) /\
148 (Aset pos (xEQ i) = if pos then {i + 1} else {i}) /\
149 (Aset pos (xDivided i1 i2) = {})
150End
151
152Definition Bset_def:
153 (Bset pos (Conjn f1 f2) = Bset pos f1 UNION Bset pos f2) /\
154 (Bset pos (Disjn f1 f2) = Bset pos f1 UNION Bset pos f2) /\
155 (Bset pos (Negn f) = Bset (~pos) f) /\
156 (Bset pos (UnrelatedBool b) = {}) /\
157 (Bset pos (xLT i) = if pos then {} else {i + ~1}) /\
158 (Bset pos (LTx i) = if pos then {i} else {}) /\
159 (Bset pos (xEQ i) = if pos then {i + ~1} else {i}) /\
160 (Bset pos (xDivided i1 i2) = {})
161End
162
163Theorem predset_lemma[local]:
164 !P Q R. P UNION Q SUBSET R = P SUBSET R /\ Q SUBSET R
165Proof
166 SRW_TAC [][SUBSET_DEF, IN_UNION] THEN PROVE_TAC []
167QED
168
169Theorem neginf_inductive_case[local]:
170 !g x d f pos.
171 alldivide f d /\ 0 < d /\ eval_form g x /\
172 (!j b. 0 < j /\ j <= d /\ b IN Bset pos f ==> ~eval_form g (b + j)) /\
173 Bset pos f SUBSET Bset T g ==>
174 if pos then eval_form f x ==> eval_form f (x - d)
175 else eval_form f (x - d) ==> eval_form f x
176Proof
177 NTAC 3 GEN_TAC THEN Induct THENL [
178 GEN_TAC THEN RULE_ASSUM_TAC (Q.SPEC `pos`) THEN
179 REPEAT STRIP_TAC THEN
180 FULL_SIMP_TAC std_ss [IN_UNION, predset_lemma, Bset_def,
181 eval_form_def, alldivide_def] THEN PROVE_TAC [],
182 GEN_TAC THEN RULE_ASSUM_TAC (Q.SPEC `pos`) THEN
183 REPEAT STRIP_TAC THEN
184 FULL_SIMP_TAC std_ss [IN_UNION, predset_lemma, Bset_def, alldivide_def,
185 eval_form_def] THEN PROVE_TAC [],
186 GEN_TAC THEN SIMP_TAC std_ss [Bset_def, eval_form_def] THEN
187 RULE_ASSUM_TAC (Q.SPEC `~pos`) THEN
188 REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [alldivide_def] THEN
189 PROVE_TAC [],
190 SIMP_TAC std_ss [eval_form_def],
191 SRW_TAC [] [eval_form_def, Bset_def] THENL [
192 (* easy case: x < i ==> x - d < i *)
193 `x < i + d` by PROVE_TAC [INT_LT_ADD2, INT_ADD_RID] THEN
194 PROVE_TAC [INT_LT_SUB_RADD],
195 (* harder case: x - d < i ==> x < i *)
196 SPOSE_NOT_THEN ASSUME_TAC THEN
197 FULL_SIMP_TAC std_ss [not_less, GSYM INT_LT_ADDNEG2, IN_SING] THEN
198 `x - d <= i + ~1` by PROVE_TAC [less_to_leq_samel] THEN
199 FULL_SIMP_TAC std_ss [INT_LE_SUB_RADD] THEN
200 `?k. (x = (i + ~1) + k) /\ 0 < k /\ k <= d` by
201 PROVE_TAC [in_additive_range] THEN PROVE_TAC []
202 ],
203 SRW_TAC [][eval_form_def, Bset_def] THENL [
204 (* harder case: i < x ==> i < x - d *)
205 SPOSE_NOT_THEN ASSUME_TAC THEN
206 FULL_SIMP_TAC std_ss [INT_NOT_LT, INT_LE_SUB_RADD, IN_SING] THEN
207 `?k. (x = i + k) /\ 0 < k /\ k <= d` by
208 PROVE_TAC [in_additive_range] THEN
209 PROVE_TAC [],
210 FULL_SIMP_TAC std_ss [GSYM INT_NEG_LT0, INT_LT_SUB_LADD] THEN
211 `i + d + ~d < x` by PROVE_TAC [INT_LT_ADD2, INT_ADD_RID] THEN
212 FULL_SIMP_TAC std_ss [GSYM INT_ADD_ASSOC, INT_ADD_RINV, INT_ADD_RID]
213 ],
214 SRW_TAC [][eval_form_def, Bset_def, IN_SING] THENL [
215 FIRST_X_ASSUM (MP_TAC o Q.SPEC `1`) THEN
216 ASM_SIMP_TAC std_ss [GSYM INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_RID,
217 INT_NOT_LE] THEN
218 CONV_TAC intReduce.REDUCE_CONV THEN PROVE_TAC [INT_DISCRETE, INT_ADD_LID],
219 FIRST_X_ASSUM (MP_TAC o Q.SPEC `d`) THEN
220 ASM_SIMP_TAC std_ss [GSYM INT_ADD_ASSOC, int_sub, INT_ADD_RID,
221 INT_LE_REFL, INT_ADD_LINV]
222 ],
223 SRW_TAC [][eval_form_def, Bset_def, IN_SING, alldivide_def,
224 int_sub] THEN
225 `x + ~d + i0 = x + i0 + ~d`
226 by CONV_TAC(AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM)) THEN
227 POP_ASSUM SUBST_ALL_TAC THEN
228 `i int_divides ~d` by PROVE_TAC [INT_DIVIDES_NEG] THEN
229 PROVE_TAC [INT_DIVIDES_LADD, INT_DIVIDES_RADD]
230 ]
231QED
232
233val neginf_lemma =
234 GEN_ALL (SIMP_RULE std_ss [SUBSET_REFL]
235 (Q.INST [`g` |-> `f`, `pos` |-> `T`]
236 (SPEC_ALL neginf_inductive_case)))
237
238Theorem posinf_inductive_case[local]:
239 !g x d f pos.
240 alldivide f d /\ 0 < d /\ eval_form g x /\
241 (!j b. 0 < j /\ j <= d /\ b IN Aset pos f ==> ~eval_form g (b + ~j)) /\
242 Aset pos f SUBSET Aset T g ==>
243 if pos then eval_form f x ==> eval_form f (x + d)
244 else eval_form f (x + d) ==> eval_form f x
245Proof
246 NTAC 3 GEN_TAC THEN Induct THENL [
247 GEN_TAC THEN RULE_ASSUM_TAC (Q.SPEC `pos`) THEN
248 ASM_SIMP_TAC std_ss [alldivide_def, eval_form_def, Aset_def,
249 predset_lemma, IN_UNION] THEN REPEAT STRIP_TAC THEN
250 FULL_SIMP_TAC std_ss [] THEN PROVE_TAC [],
251 GEN_TAC THEN RULE_ASSUM_TAC (Q.SPEC `pos`) THEN
252 ASM_SIMP_TAC std_ss [alldivide_def, eval_form_def, Aset_def,
253 predset_lemma, IN_UNION] THEN REPEAT STRIP_TAC THEN
254 FULL_SIMP_TAC std_ss [] THEN PROVE_TAC [],
255 GEN_TAC THEN RULE_ASSUM_TAC (Q.SPEC `~pos`) THEN
256 ASM_SIMP_TAC std_ss [alldivide_def, eval_form_def, Aset_def,
257 predset_lemma, IN_UNION] THEN REPEAT STRIP_TAC THEN
258 FULL_SIMP_TAC std_ss [] THEN PROVE_TAC [],
259 SIMP_TAC std_ss [eval_form_def],
260 SRW_TAC [][Aset_def, eval_form_def, IN_SING, alldivide_def] THENL [
261 SPOSE_NOT_THEN (MP_TAC o
262 REWRITE_RULE [INT_NOT_LT, GSYM INT_LE_SUB_RADD]) THEN
263 STRIP_TAC THEN
264 `?k. (x = i - k) /\ 0 < k /\ k <= d` by
265 PROVE_TAC [in_subtractive_range] THEN
266 PROVE_TAC [int_sub],
267 FULL_SIMP_TAC std_ss [GSYM INT_NEG_LT0] THEN
268 PROVE_TAC [INT_ADD_ASSOC, INT_ADD_RINV, INT_ADD_RID, INT_LT_ADD2]
269 ],
270 SRW_TAC [][Aset_def, eval_form_def, IN_SING, alldivide_def] THENL [
271 PROVE_TAC [INT_ADD_RID, INT_LT_ADD2],
272 SPOSE_NOT_THEN (ASSUME_TAC o REWRITE_RULE [not_less]) THEN
273 `i + 1 <= x + d` by PROVE_TAC [less_to_leq_samer] THEN
274 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [GSYM INT_LE_SUB_RADD]) THEN
275 `?k. (x = i + 1 - k) /\ 0 < k /\ k <= d` by
276 PROVE_TAC [in_subtractive_range] THEN
277 PROVE_TAC [int_sub]
278 ],
279 SRW_TAC [][Aset_def, eval_form_def, IN_SING, alldivide_def] THENL [
280 FIRST_X_ASSUM (MP_TAC o Q.SPEC `1`) THEN
281 ASM_SIMP_TAC std_ss [GSYM INT_ADD_ASSOC, INT_ADD_RINV, INT_ADD_RID] THEN
282 CONV_TAC intReduce.REDUCE_CONV THEN PROVE_TAC [INT_DISCRETE, INT_ADD_LID,
283 INT_NOT_LE],
284 FIRST_X_ASSUM (MP_TAC o Q.SPEC `d`) THEN
285 ASM_SIMP_TAC std_ss [GSYM INT_ADD_ASSOC, INT_LE_REFL, INT_ADD_RID,
286 INT_ADD_RINV]
287 ],
288 SRW_TAC [][Aset_def, eval_form_def, IN_SING, alldivide_def] THEN
289 `x + d + i0 = x + i0 + d` by
290 CONV_TAC (AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM)) THEN
291 PROVE_TAC [INT_DIVIDES_LADD, INT_DIVIDES_RADD]
292 ]
293QED
294
295val posinf_lemma =
296 GEN_ALL (SIMP_RULE std_ss [SUBSET_REFL]
297 (Q.INST [`g` |-> `f`, `pos` |-> `T`]
298 (SPEC_ALL posinf_inductive_case)))
299
300Theorem neginf_exoriginal_implies_rhs:
301 !f d x.
302 alldivide f d /\ 0 < d ==>
303 eval_form f x ==>
304 (?i. 0 < i /\ i <= d /\ eval_form (neginf f) i) \/
305 (?j b. 0 < j /\ j <= d /\ b IN Bset T f /\ eval_form f (b + j))
306Proof
307 REPEAT STRIP_TAC THEN
308 Cases_on
309 `?j b. 0 < j /\ j <= d /\ b IN Bset T f /\ eval_form f (b + j)`
310 THENL [
311 ASM_REWRITE_TAC [],
312 DISJ1_TAC THEN
313 POP_ASSUM (fn th =>
314 `!j b. 0 < j /\ j <= d /\ b IN Bset T f ==> ~eval_form f (b + j)`
315 by PROVE_TAC [th]) THEN
316 Q.SUBGOAL_THEN `!x. eval_form f x ==> eval_form f (x - d)`
317 ASSUME_TAC THENL [
318 PROVE_TAC [neginf_lemma],
319 STRIP_ASSUME_TAC (Q.SPEC `f` neginf_ok) THEN
320 `!c. 0 < c ==> eval_form f (x - c * d)`
321 by PROVE_TAC [top_and_lessers] THEN
322 `?e. 0 < e /\ x - e * d < y` by PROVE_TAC [can_get_small] THEN
323 `eval_form f (x - e * d)` by PROVE_TAC [] THEN
324 `eval_form (neginf f) (x - e * d)` by PROVE_TAC [] THEN
325 `?k. 0 < x - e * d - k * d /\ x - e * d - k * d <= d` by
326 PROVE_TAC [subtract_to_small] THEN
327 FULL_SIMP_TAC std_ss [int_sub, INT_NEG_LMUL] THEN
328 PROVE_TAC [add_d_neginf]
329 ]
330 ]
331QED
332
333Theorem posinf_exoriginal_implies_rhs:
334 !f d x.
335 alldivide f d /\ 0 < d ==>
336 eval_form f x ==>
337 (?i. 0 < i /\ i <= d /\ eval_form (posinf f) i) \/
338 (?j b. 0 < j /\ j <= d /\ b IN Aset T f /\ eval_form f (b + ~j))
339Proof
340 REPEAT STRIP_TAC THEN
341 Cases_on
342 `?j b. 0 < j /\ j <= d /\ b IN Aset T f /\ eval_form f (b + ~j)`
343 THENL [
344 ASM_REWRITE_TAC [],
345 DISJ1_TAC THEN
346 POP_ASSUM (fn th =>
347 `!j b. 0 < j /\ j <= d /\ b IN Aset T f ==> ~eval_form f (b + ~j)`
348 by PROVE_TAC [th]) THEN
349 Q.SUBGOAL_THEN `!x. eval_form f x ==> eval_form f (x + d)`
350 ASSUME_TAC THENL [
351 PROVE_TAC [posinf_lemma],
352 STRIP_ASSUME_TAC (Q.SPEC `f` posinf_ok) THEN
353 `!c. 0 < c ==> eval_form f (x + c * d)`
354 by PROVE_TAC [bot_and_greaters] THEN
355 `?e. 0 < e /\ y < x + e * d` by PROVE_TAC [can_get_big] THEN
356 `eval_form f (x + e * d)` by PROVE_TAC [] THEN
357 `eval_form (posinf f) (x + e * d)` by PROVE_TAC [] THEN
358 `?k. 0 < x + e * d - k * d /\ x + e * d - k * d <= d` by
359 PROVE_TAC [subtract_to_small] THEN
360 FULL_SIMP_TAC std_ss [int_sub, INT_NEG_LMUL] THEN
361 PROVE_TAC [add_d_posinf]
362 ]
363 ]
364QED
365
366
367
368Theorem neginf_exoriginal_eq_rhs:
369 !f d.
370 alldivide f d /\ 0 < d ==>
371 ((?x. eval_form f x) =
372 (?i. K (0 < i /\ i <= d) i /\ eval_form (neginf f) i) \/
373 (?b j. (b IN Bset T f /\ K (0 < j /\ j <= d) j) /\
374 eval_form f (b + j)))
375Proof
376 REPEAT STRIP_TAC THEN EQ_TAC THEN
377 REWRITE_TAC [combinTheory.K_THM, GSYM INT_NEG_MINUS1] THEN
378 REPEAT STRIP_TAC THENL [
379 IMP_RES_TAC neginf_exoriginal_implies_rhs THEN PROVE_TAC [],
380 PROVE_TAC [neginf_disj1_implies_exoriginal],
381 PROVE_TAC []
382 ]
383QED
384
385Theorem posinf_exoriginal_eq_rhs:
386 !f d.
387 alldivide f d /\ 0 < d ==>
388 ((?x. eval_form f x) =
389 (?i. K (0 < i /\ i <= d) i /\ eval_form (posinf f) i) \/
390 (?b j. (b IN Aset T f /\ K (0 < j /\ j <= d) j) /\
391 eval_form f (b + ~1 * j)))
392Proof
393 REPEAT STRIP_TAC THEN EQ_TAC THEN
394 REWRITE_TAC [combinTheory.K_THM, GSYM INT_NEG_MINUS1] THEN
395 REPEAT STRIP_TAC THENL [
396 IMP_RES_TAC posinf_exoriginal_implies_rhs THEN PROVE_TAC [],
397 PROVE_TAC [posinf_disj1_implies_exoriginal],
398 PROVE_TAC []
399 ]
400QED
401
402(* useful additional rewrites for the d.p. *)
403Theorem in_bset:
404 ((?b. b IN Bset pos (Conjn f1 f2) /\ P b) =
405 (?b. b IN Bset pos f1 /\ P b) \/ (?b. b IN Bset pos f2 /\ P b)) /\
406 ((?b. b IN Bset pos (Disjn f1 f2) /\ P b) =
407 (?b. b IN Bset pos f1 /\ P b) \/ (?b. b IN Bset pos f2 /\ P b)) /\
408 ((?b. b IN Bset T (Negn f) /\ P b) = (?b. b IN Bset F f /\ P b)) /\
409 ((?b. b IN Bset F (Negn f) /\ P b) = (?b. b IN Bset T f /\ P b)) /\
410 ((?b. b IN Bset pos (UnrelatedBool b0) /\ P b) = F) /\
411 ((?b. b IN Bset T (xLT i) /\ P b) = F) /\
412 ((?b. b IN Bset F (xLT i) /\ P b) = P (i + ~1)) /\
413 ((?b. b IN Bset T (LTx i) /\ P b) = P i) /\
414 ((?b. b IN Bset F (LTx i) /\ P b) = F) /\
415 ((?b. b IN Bset T (xEQ i) /\ P b) = P (i + ~1)) /\
416 ((?b. b IN Bset F (xEQ i) /\ P b) = P i) /\
417 ((?b. b IN Bset pos (xDivided i1 i2) /\ P b) = F)
418Proof
419 SIMP_TAC std_ss [IN_UNION, NOT_IN_EMPTY, IN_SING, Bset_def] THEN
420 PROVE_TAC []
421QED
422
423Theorem in_aset:
424 ((?a. a IN Aset pos (Conjn f1 f2) /\ P a) =
425 (?a. a IN Aset pos f1 /\ P a) \/ (?a. a IN Aset pos f2 /\ P a)) /\
426 ((?a. a IN Aset pos (Disjn f1 f2) /\ P a) =
427 (?a. a IN Aset pos f1 /\ P a) \/ (?a. a IN Aset pos f2 /\ P a)) /\
428 ((?a. a IN Aset T (Negn f) /\ P a) = (?a. a IN Aset F f /\ P a)) /\
429 ((?a. a IN Aset F (Negn f) /\ P a) = (?a. a IN Aset T f /\ P a)) /\
430 ((?a. a IN Aset pos (UnrelatedBool a0) /\ P a) = F) /\
431 ((?a. a IN Aset T (xLT i) /\ P a) = P i) /\
432 ((?a. a IN Aset F (xLT i) /\ P a) = F) /\
433 ((?a. a IN Aset T (LTx i) /\ P a) = F) /\
434 ((?a. a IN Aset F (LTx i) /\ P a) = P (i + 1)) /\
435 ((?a. a IN Aset T (xEQ i) /\ P a) = P (i + 1)) /\
436 ((?a. a IN Aset F (xEQ i) /\ P a) = P i) /\
437 ((?a. a IN Aset pos (xDivided i1 i2) /\ P a) = F)
438Proof
439 SIMP_TAC std_ss [IN_UNION, NOT_IN_EMPTY, IN_SING, Aset_def] THEN
440 PROVE_TAC []
441QED