quantHeuristicsScript.sml

1Theory quantHeuristics[bare]
2Ancestors
3  pair list option
4Libs
5  HolKernel Parse boolLib Drule BasicProvers metisLib simpLib
6  boolSimps pureSimps TotalDefn numLib ConseqConv
7
8(*
9quietdec := false;
10*)
11
12val _ = ParseExtras.temp_loose_equality()
13
14val list_ss  = arith_ss ++ listSimps.LIST_ss
15
16Definition GUESS_EXISTS_def:
17    GUESS_EXISTS i P = ((?v. P v) = (?fv. P (i fv)))
18End
19
20Definition GUESS_FORALL_def:
21    GUESS_FORALL i P = ((!v. P v) = (!fv. P (i fv)))
22End
23
24Theorem GUESS_EXISTS_FORALL_REWRITES:
25  (GUESS_EXISTS i P = (!v. P v ==> (?fv. P (i fv)))) /\
26  (GUESS_FORALL i P = (!v. ~(P v) ==> (?fv. ~(P (i fv)))))
27Proof
28SIMP_TAC std_ss [GUESS_EXISTS_def, GUESS_FORALL_def] THEN
29METIS_TAC[]
30QED
31
32
33Definition GUESS_EXISTS_POINT_def:
34    GUESS_EXISTS_POINT i P = (!fv. P (i fv))
35End
36
37Definition GUESS_FORALL_POINT_def:
38    GUESS_FORALL_POINT i P = (!fv. ~(P (i fv)))
39End
40
41Theorem GUESS_POINT_THM:
42  (GUESS_EXISTS_POINT i P ==> ((?v. P v) = T)) /\
43  (GUESS_FORALL_POINT i P ==> ((!v. P v) = F))
44Proof
45SIMP_TAC std_ss [GUESS_EXISTS_POINT_def, GUESS_FORALL_POINT_def] THEN
46METIS_TAC[]
47QED
48
49
50Definition GUESS_EXISTS_GAP_def:
51    GUESS_EXISTS_GAP i P =
52       (!v. P v ==> (?fv. v = (i fv)))
53End
54
55Definition GUESS_FORALL_GAP_def:
56    GUESS_FORALL_GAP i P =
57       (!v. ~(P v) ==> (?fv. v = (i fv)))
58End
59
60
61Theorem GUESS_REWRITES =
62   LIST_CONJ [GUESS_EXISTS_FORALL_REWRITES, GUESS_EXISTS_POINT_def, GUESS_FORALL_POINT_def,
63      GUESS_EXISTS_GAP_def, GUESS_FORALL_GAP_def];
64
65
66
67
68(******************************************************************************)
69(* Now the intended semantic                                                  *)
70(******************************************************************************)
71
72Theorem GUESS_EXISTS_POINT_THM:
73  !i P. GUESS_EXISTS_POINT i P ==> ($? P = T)
74Proof
75SIMP_TAC std_ss [GUESS_EXISTS_POINT_def, EXISTS_THM] THEN
76METIS_TAC[]
77QED
78
79Theorem GUESS_FORALL_POINT_THM:
80  !i P. GUESS_FORALL_POINT i P ==> (($! P) = F)
81Proof
82SIMP_TAC std_ss [GUESS_REWRITES, FORALL_THM] THEN
83METIS_TAC[]
84QED
85
86Theorem GUESS_EXISTS_THM:
87  !i P. GUESS_EXISTS i P ==> ($? P = ?fv. P (i fv))
88Proof
89SIMP_TAC std_ss [GUESS_REWRITES, EXISTS_THM] THEN
90METIS_TAC[]
91QED
92
93Theorem GUESS_FORALL_THM:
94  !i P. GUESS_FORALL i P ==> (($! P) = !fv. P (i fv))
95Proof
96SIMP_TAC std_ss [GUESS_REWRITES, FORALL_THM] THEN
97METIS_TAC[]
98QED
99
100
101Theorem GUESSES_UEXISTS_THM1:
102  !i P. GUESS_EXISTS (\x. i) P ==>
103        ($?! P = ((P i) /\ (!v. P v ==> (v = i))))
104Proof
105SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN
106METIS_TAC[]
107QED
108
109Theorem GUESSES_UEXISTS_THM2:
110  !i P. GUESS_EXISTS_GAP (\x. i) P ==> ($?! P = P i)
111Proof
112SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN
113METIS_TAC[]
114QED
115
116Theorem GUESSES_UEXISTS_THM3:
117  !i P. GUESS_EXISTS_POINT (\x. i) P ==>
118        ($?! P = (!v. P v ==> (v = i)))
119Proof
120SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN
121METIS_TAC[]
122QED
123
124Theorem GUESSES_UEXISTS_THM4:
125  !i P. GUESS_EXISTS_POINT (\x. i) P ==> GUESS_EXISTS_GAP (\x. i) P ==>
126        ($?! P = T)
127Proof
128SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN
129METIS_TAC[]
130QED
131
132
133Theorem GUESSES_NEG_DUALITY:
134  (GUESS_EXISTS i ($~ o P) =
135   GUESS_FORALL i P) /\
136
137  (GUESS_FORALL i ($~ o P) =
138   GUESS_EXISTS i P) /\
139
140  (GUESS_EXISTS_GAP i ($~ o P) =
141   GUESS_FORALL_GAP i P) /\
142
143  (GUESS_FORALL_GAP i ($~ o P) =
144   GUESS_EXISTS_GAP i P) /\
145
146  (GUESS_EXISTS_POINT  i ($~ o P) =
147   GUESS_FORALL_POINT i P) /\
148
149  (GUESS_FORALL_POINT i ($~ o P) =
150   GUESS_EXISTS_POINT  i P)
151Proof
152
153SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.o_DEF]
154QED
155
156
157Theorem GUESSES_NEG_REWRITE =
158SIMP_RULE std_ss [combinTheory.o_DEF]
159  (INST [``P:'b -> bool`` |-> ``\x:'b. (P x):bool``] GUESSES_NEG_DUALITY);
160
161
162Theorem GUESSES_WEAKEN_THM:
163  (GUESS_FORALL_GAP i P ==> GUESS_FORALL i P) /\
164  (GUESS_FORALL_POINT         i P ==> GUESS_FORALL i P) /\
165  (GUESS_EXISTS_POINT          i P ==> GUESS_EXISTS i P) /\
166  (GUESS_EXISTS_GAP i P ==> GUESS_EXISTS i P)
167Proof
168
169SIMP_TAC std_ss [GUESS_REWRITES] THEN
170METIS_TAC[]
171QED
172
173
174
175(******************************************************************************)
176(* Equations                                                                  *)
177(******************************************************************************)
178
179Theorem GUESS_RULES_EQUATION_EXISTS_POINT:
180  !i P Q.
181  (P i = Q i) ==>
182  GUESS_EXISTS_POINT (\xxx:unit. i) (\x. P x = Q x)
183Proof
184SIMP_TAC std_ss [GUESS_REWRITES]
185QED
186
187Theorem GUESS_RULES_EQUATION_FORALL_POINT:
188  !i P Q.
189  (!fv. ~(P (i fv) = Q (i fv))) ==>
190  GUESS_FORALL_POINT i (\x. P x = Q x)
191Proof
192SIMP_TAC std_ss [GUESS_REWRITES]
193QED
194
195Theorem GUESS_RULES_EQUATION_EXISTS_GAP:
196  !i.
197  GUESS_EXISTS_GAP (\xxx:unit. i) (\x. x = i)
198Proof
199SIMP_TAC std_ss [GUESS_REWRITES] THEN
200METIS_TAC[]
201QED
202
203(******************************************************************************)
204(* Trivial point guesses                                                      *)
205(******************************************************************************)
206
207Theorem GUESS_RULES_TRIVIAL_EXISTS_POINT:
208  !i P. P i ==>
209  GUESS_EXISTS_POINT (\xxx:unit. i) P
210Proof
211SIMP_TAC std_ss [GUESS_REWRITES]
212QED
213
214Theorem GUESS_RULES_TRIVIAL_FORALL_POINT:
215  !i P. ~(P i) ==>
216  GUESS_FORALL_POINT (\xxx:unit. i) P
217Proof
218SIMP_TAC std_ss [GUESS_REWRITES]
219QED
220
221(******************************************************************************)
222(* Trivial booleans                                                           *)
223(******************************************************************************)
224
225Theorem GUESS_RULES_BOOL:
226  GUESS_EXISTS_POINT (\ARB:unit. T) (\x. x) /\
227  GUESS_FORALL_POINT (\ARB:unit. F) (\x. x) /\
228  GUESS_EXISTS_GAP (\ARB:unit. T) (\x. x) /\
229  GUESS_FORALL_GAP (\ARB:unit. F) (\x. x)
230Proof
231SIMP_TAC std_ss [GUESS_REWRITES]
232QED
233
234
235
236(******************************************************************************)
237(* Cases                                                                      *)
238(******************************************************************************)
239
240Theorem GUESS_RULES_TWO_CASES:
241  !y Q. ((!x. ((x = y) \/ (?fv. x = Q fv)))) ==>
242  GUESS_FORALL_GAP Q (\x. x = y)
243Proof
244SIMP_TAC std_ss [GUESS_REWRITES] THEN
245METIS_TAC[]
246QED
247
248Theorem GUESS_RULES_ONE_CASE___FORALL_GAP:
249  !P Q. ((!x:'a. (?fv. x = Q fv))) ==>
250  GUESS_FORALL_GAP Q (P:'a -> bool)
251Proof
252SIMP_TAC std_ss [GUESS_REWRITES]
253QED
254
255Theorem GUESS_RULES_ONE_CASE___EXISTS_GAP:
256  !P Q. ((!x:'a. (?fv. x = Q fv))) ==>
257  GUESS_EXISTS_GAP Q (P:'a -> bool)
258Proof
259SIMP_TAC std_ss [GUESS_REWRITES]
260QED
261
262
263(******************************************************************************)
264(* Boolean operators                                                          *)
265(******************************************************************************)
266
267Theorem GUESS_RULES_NEG:
268  (GUESS_EXISTS i (\x. P x) ==>
269   GUESS_FORALL i (\x. ~(P x))) /\
270
271  (GUESS_EXISTS_GAP i (\x. P x) ==>
272   GUESS_FORALL_GAP i (\x. ~(P x))) /\
273
274  (GUESS_EXISTS_POINT  i (\x. P x) ==>
275   GUESS_FORALL_POINT i (\x. ~(P x))) /\
276
277  (GUESS_FORALL i (\x. P x) ==>
278   GUESS_EXISTS i (\x. ~(P x))) /\
279
280  (GUESS_FORALL_GAP i (\x. P x) ==>
281   GUESS_EXISTS_GAP i (\x. ~(P x))) /\
282
283  (GUESS_FORALL_POINT i (\x. P x) ==>
284   GUESS_EXISTS_POINT  i (\x. ~(P x)))
285Proof
286
287SIMP_TAC std_ss [GUESSES_NEG_REWRITE]
288QED
289
290
291Theorem GUESS_RULES_CONSTANT_EXISTS:
292  (GUESS_EXISTS i (\x. p)) = T
293Proof
294SIMP_TAC std_ss [GUESS_REWRITES]
295QED
296
297Theorem GUESS_RULES_CONSTANT_FORALL:
298  (GUESS_FORALL i (\x. p)) = T
299Proof
300SIMP_TAC std_ss [GUESS_REWRITES]
301QED
302
303Theorem GUESS_RULES_DISJ:
304  (GUESS_EXISTS_POINT i (\x. P x) ==>
305   GUESS_EXISTS_POINT i (\x. P x \/ Q x)) /\
306
307  (GUESS_EXISTS_POINT i (\x. Q x) ==>
308   GUESS_EXISTS_POINT i (\x. P x \/ Q x)) /\
309
310  (GUESS_EXISTS i (\x. P x) /\
311   GUESS_EXISTS i (\x. Q x) ==>
312   GUESS_EXISTS i (\x. P x \/ Q x)) /\
313
314  (* Not needed because of GUESS_RULES_CONSTANT_EXISTS, GUESS_RULES_CONSTANT_FORALL
315  (GUESS_EXISTS i (\x. P x) ==>
316   GUESS_EXISTS i (\x. P x \/ q)) /\
317
318  (GUESS_EXISTS i (\x. Q x) ==>
319   GUESS_EXISTS i (\x. p \/ Q x)) /\ *)
320
321  (GUESS_EXISTS_GAP i (\x. P x) /\
322   GUESS_EXISTS_GAP i (\x. Q x) ==>
323   GUESS_EXISTS_GAP i (\x. P x \/ Q x)) /\
324
325  (GUESS_FORALL (\xxx:unit. iK) (\x. P x) /\
326   GUESS_FORALL (\xxx:unit. iK) (\x. Q x) ==>
327   GUESS_FORALL (\xxx:unit. iK) (\x. P x \/ Q x)) /\
328
329  (GUESS_FORALL i (\x. P x) ==>
330   GUESS_FORALL i (\x. P x \/ q)) /\
331
332  (GUESS_FORALL i (\x. Q x) ==>
333   GUESS_FORALL i (\x. p \/ Q x)) /\
334
335  (GUESS_FORALL_POINT i (\x. P x) /\
336   GUESS_FORALL_POINT i (\x. Q x) ==>
337   GUESS_FORALL_POINT i (\x. P x \/ Q x)) /\
338
339  (GUESS_FORALL_GAP i (\x. P x) ==>
340   GUESS_FORALL_GAP i (\x. P x \/ Q x)) /\
341
342  (GUESS_FORALL_GAP i (\x. Q x) ==>
343   GUESS_FORALL_GAP i (\x. P x \/ Q x))
344Proof
345
346SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN
347METIS_TAC[]
348QED
349
350
351
352Theorem GUESS_RULES_CONJ = (
353let
354   val thm0 = INST [
355      ``P:'b->bool`` |-> ``$~ o (P:'b->bool)``,
356      ``Q:'b->bool`` |-> ``$~ o (Q:'b->bool)``,
357      ``p:bool`` |-> ``~p``,
358      ``q:bool`` |-> ``~q``] GUESS_RULES_DISJ
359   val thm1 = SIMP_RULE std_ss [GUESSES_NEG_REWRITE] thm0
360   val thm2 = REWRITE_RULE [GSYM DE_MORGAN_THM] thm1
361   val thm3 = SIMP_RULE std_ss [GUESSES_NEG_REWRITE] thm2
362in
363   thm3
364end)
365
366
367
368Theorem GUESS_RULES_IMP = (
369let
370   val thm0 = INST [
371      ``P:'b->bool`` |-> ``$~ o (P:'b->bool)``,
372      ``p:bool`` |-> ``~p``] GUESS_RULES_DISJ
373   val thm1 = SIMP_RULE std_ss [GUESSES_NEG_REWRITE] thm0
374   val thm2 = REWRITE_RULE [GSYM IMP_DISJ_THM] thm1
375in
376   thm2
377end)
378
379
380(*
381
382Code for generating theorems with rewriting using the basic ones.
383This is used for comming up with ideas for the lemma for
384COND and EXISTS_UNIQUE
385
386
387local
388
389(*
390val thmL = [GUESS_RULES_NEG, GUESS_RULES_DISJ, GUESS_RULES_CONJ,
391            GUESS_RULES_IMP, GUESSES_RULES_CONSTANT_EXISTS,
392            GUESSES_RULES_CONSTANT_FORALL, ELIM_UNLICKLY_THM]
393
394val tmL = [``\x:'a. P x <=> Q x``, ``\x. p <=> Q x``, ``\x. P x <=> q``]
395val rewr = [EQ_EXPAND]
396val tm = hd tmL
397
398val currentL = prepare_org_thms rewr tmL
399val ruleL = prepare_rules thmL
400*)
401
402val ELIM_UNLICKLY_THM = prove(
403``(F ==> GUESS_EXISTS_POINT i (\x. p)) /\
404  (F ==> GUESS_FORALL_POINT i (\x. p)) /\
405  (F ==> GUESS_EXISTS_GAP i (\x. p)) /\
406  (F ==> GUESS_FORALL_GAP i (\x. p))``,
407SIMP_TAC std_ss [])
408
409
410fun prepare_org_thms rewr tmL =
411let
412   val thmL0 = map (fn t => REWRITE_CONV rewr t handle UNCHANGED => REFL t) tmL
413   fun mk_guess_terms tm =
414      ([``GUESS_EXISTS_POINT (i:'b -> 'a) ^tm``,
415       ``GUESS_FORALL_POINT (i:'b -> 'a) ^tm``,
416       ``GUESS_EXISTS (i:'b -> 'a) ^tm``,
417       ``GUESS_FORALL (i:'b -> 'a) ^tm``,
418       ``GUESS_EXISTS_GAP (i:'b -> 'a) ^tm``,
419       ``GUESS_FORALL_GAP (i:'b -> 'a) ^tm``],
420      [``GUESS_EXISTS_POINT (K (iK:'a)) ^tm``,
421       ``GUESS_FORALL_POINT (K (iK:'a)) ^tm``,
422       ``GUESS_EXISTS (K (iK:'a)) ^tm``,
423       ``GUESS_FORALL (K (iK:'a)) ^tm``,
424       ``GUESS_EXISTS_GAP (K (iK:'a)) ^tm``,
425       ``GUESS_FORALL_GAP (K (iK:'a)) ^tm``])
426
427   fun basic_thms Pthm =
428   let
429       val (xtmL1, xtmL2) = mk_guess_terms (rhs (concl Pthm));
430       val xthmL1 = map ConseqConv.REFL_CONSEQ_CONV xtmL1;
431       val xthmL2 = map ConseqConv.REFL_CONSEQ_CONV xtmL2;
432       val Pthm' = GSYM Pthm;
433       val xthmL1' = map (CONV_RULE (RAND_CONV (RAND_CONV (K Pthm')))) xthmL1
434       val xthmL2' = map (CONV_RULE (RAND_CONV (RAND_CONV (K Pthm')))) xthmL2
435   in
436       (xthmL1', xthmL2')
437   end;
438
439   val (thmL1, thmL2) = unzip (map basic_thms thmL0);
440in
441   (flatten thmL1, flatten thmL2)
442end;
443
444
445fun prepare_rules thmL =
446   let
447      val thmL' = flatten (map BODY_CONJUNCTS thmL);
448   in
449      map (fn thm => fn thm2 => SOME (ConseqConv.STRENGTHEN_CONSEQ_CONV_RULE
450             (ConseqConv.CONSEQ_HO_REWRITE_CONV ([],[thm],[])) thm2) handle UNCHANGED => NONE) thmL'
451   end
452
453
454fun mapPartial f = ((map valOf) o (filter isSome) o (map f));
455
456fun apply_rules ruleL doneL [] = doneL
457  | apply_rules ruleL doneL (thm::currentL) =
458    let
459       val xthmL = mapPartial (fn r => r thm) ruleL;
460    in
461       if null xthmL then apply_rules ruleL (thm::doneL) currentL
462       else apply_rules ruleL doneL (xthmL @ currentL)
463    end;
464
465in
466   fun test_rules thmL rewr tmL =
467   let
468      val (currentL1, currentL2) = prepare_org_thms rewr tmL
469      val ruleL = prepare_rules thmL;
470
471      fun doit cL =
472        filter (fn x => not (same_const ((fst o dest_imp o concl) x) F))
473          (apply_rules ruleL [] cL);
474
475      val thmL1 = doit currentL1;
476      val thmL2 = doit currentL2;
477
478      val thm1' = SIMP_RULE (std_ss++boolSimps.CONJ_ss) [] (LIST_CONJ thmL1)
479      val thm2' = SIMP_RULE (std_ss++boolSimps.CONJ_ss) [thm1'] (LIST_CONJ thmL2)
480   in
481      CONJ thm2' thm1'
482   end
483end
484
485
486*)
487
488Theorem GUESS_RULES_EQUIV:
489  (GUESS_EXISTS_POINT i (\x. P x) /\
490   GUESS_EXISTS_POINT i (\x. Q x) ==>
491   GUESS_EXISTS_POINT i (\x. P x <=> Q x)) /\
492
493  (GUESS_FORALL_POINT i (\x. P x) /\
494   GUESS_FORALL_POINT i (\x. Q x) ==>
495   GUESS_EXISTS_POINT i (\x. P x <=> Q x)) /\
496
497  (GUESS_EXISTS_POINT i (\x. P x) /\
498   GUESS_FORALL_POINT i (\x. Q x) ==>
499   GUESS_FORALL_POINT i (\x. P x <=> Q x)) /\
500
501  (GUESS_FORALL_POINT i (\x. P x) /\
502   GUESS_EXISTS_POINT i (\x. Q x) ==>
503   GUESS_FORALL_POINT i (\x. P x <=> Q x)) /\
504
505  (GUESS_FORALL_GAP i (\x. P1 x) /\
506   GUESS_FORALL_GAP i (\x. P2 x) ==>
507   GUESS_FORALL_GAP i (\x. P1 x <=> P2 x)) /\
508
509  (GUESS_EXISTS_GAP i (\x. P1 x) /\
510   GUESS_EXISTS_GAP i (\x. P2 x) ==>
511   GUESS_FORALL_GAP i (\x. P1 x <=> P2 x)) /\
512
513  (GUESS_EXISTS_GAP i (\x. P1 x) /\
514   GUESS_FORALL_GAP i (\x. P2 x) ==>
515   GUESS_EXISTS_GAP i (\x. P1 x <=> P2 x)) /\
516
517  (GUESS_FORALL_GAP i (\x. P1 x) /\
518   GUESS_EXISTS_GAP i (\x. P2 x) ==>
519   GUESS_EXISTS_GAP i (\x. P1 x <=> P2 x))
520Proof
521
522SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN
523METIS_TAC[]
524QED
525
526
527Theorem GUESS_RULES_COND:
528   (GUESS_FORALL_POINT i (\x. P x) /\
529    GUESS_FORALL_POINT i (\x. Q x) ==>
530    GUESS_FORALL_POINT i (\x. if b x then P x else Q x)) /\
531
532   (GUESS_EXISTS_POINT i (\x. P x) /\
533    GUESS_EXISTS_POINT i (\x. Q x) ==>
534    GUESS_EXISTS_POINT i (\x. if b x then P x else Q x)) /\
535
536   (GUESS_EXISTS i (\x. P x) /\
537    GUESS_EXISTS i (\x. Q x) ==>
538    GUESS_EXISTS i (\x. if bc then P x else Q x)) /\
539
540   (GUESS_FORALL i (\x. P x) /\
541    GUESS_FORALL i (\x. Q x) ==>
542    GUESS_FORALL i (\x. if bc then P x else Q x)) /\
543
544   (GUESS_EXISTS_GAP i (\x. P x) /\
545    GUESS_EXISTS_GAP i (\x. Q x) ==>
546    GUESS_EXISTS_GAP i (\x. if b x then P x else Q x)) /\
547
548   (GUESS_FORALL_GAP i (\x. P x) /\
549    GUESS_FORALL_GAP i (\x. Q x) ==>
550    GUESS_FORALL_GAP i (\x. if b x then P x else Q x)) /\
551
552
553   (GUESS_FORALL_POINT i (\x. b x) /\
554    GUESS_FORALL_POINT i (\x. Q x) ==>
555    GUESS_FORALL_POINT i (\x. if b x then P x else Q x)) /\
556
557   (GUESS_FORALL_POINT i (\x. b x) /\
558    GUESS_EXISTS_POINT i (\x. Q x) ==>
559    GUESS_EXISTS_POINT i (\x. if b x then P x else Q x)) /\
560
561   (GUESS_EXISTS_POINT i (\x. b x) /\
562    GUESS_FORALL_POINT i (\x. P x) ==>
563    GUESS_FORALL_POINT i (\x. if b x then P x else Q x)) /\
564
565   (GUESS_EXISTS_POINT i (\x. b x) /\
566    GUESS_EXISTS_POINT i (\x. P x) ==>
567    GUESS_EXISTS_POINT i (\x. if b x then P x else Q x)) /\
568
569   (GUESS_FORALL_GAP i (\x. b x) /\
570    GUESS_EXISTS_GAP i (\x. P x) ==>
571    GUESS_EXISTS_GAP i (\x. if b x then P x else Q x)) /\
572
573   (GUESS_EXISTS_GAP i (\x. b x) /\
574    GUESS_EXISTS_GAP i (\x. Q x) ==>
575    GUESS_EXISTS_GAP i (\x. if b x then P x else Q x)) /\
576
577   (GUESS_EXISTS_GAP i (\x. b x) /\
578    GUESS_FORALL_GAP i (\x. Q x) ==>
579    GUESS_FORALL_GAP i (\x. if b x then P x else Q x)) /\
580
581   (GUESS_FORALL_GAP i (\x. b x) /\
582    GUESS_FORALL_GAP i (\x. P x) ==>
583    GUESS_FORALL_GAP i (\x. if b x then P x else Q x))
584Proof
585
586SIMP_TAC std_ss [GUESS_REWRITES] THEN
587METIS_TAC[]
588QED
589
590
591Theorem GUESS_RULES_FORALL___NEW_FV:
592  ((!y. GUESS_FORALL_POINT (iy y) (\x. P x y)) ==>
593   GUESS_FORALL_POINT (\fv. iy (FST fv) (SND fv)) (\x. !y. P x y)) /\
594
595  ((!y. GUESS_FORALL (iy y) (\x. P x y)) ==>
596   GUESS_FORALL (\fv. iy (FST fv) (SND fv)) (\x. !y. P x y)) /\
597
598  ((!y. GUESS_FORALL_GAP (iy y) (\x. P x y)) ==>
599   GUESS_FORALL_GAP (\fv. iy (FST fv) (SND fv)) (\x. !y. P x y)) /\
600
601  ((!y. GUESS_EXISTS_GAP (iy y) (\x. P x y)) ==>
602    GUESS_EXISTS_GAP (\fv. iy (FST fv) (SND fv)) (\x. !y. P x y))
603Proof
604
605SIMP_TAC std_ss [GUESS_REWRITES, FORALL_PROD, EXISTS_PROD] THEN
606METIS_TAC[]
607QED
608
609
610(* A variant of GUESS_RULES_FORALL___NEW_FV that eliminates unit directly. *)
611Theorem GUESS_RULES_FORALL___NEW_FV_1:
612  ((!y. GUESS_FORALL_POINT (\xxx:unit. (i y)) (\x. P (x:'c) (y:'a))) ==>
613   GUESS_FORALL_POINT i (\x. !y. P x y)) /\
614
615  ((!y. GUESS_FORALL (\xxx:unit. (i y)) (\x. P x y)) ==>
616   GUESS_FORALL i (\x. !y. P x y)) /\
617
618  ((!y. GUESS_FORALL_GAP (\xxx:unit. (i y)) (\x. P x y)) ==>
619   GUESS_FORALL_GAP i (\x. !y. P x y)) /\
620
621  ((!y. GUESS_EXISTS_GAP (\xxx:unit. (i y)) (\x. P x y)) ==>
622    GUESS_EXISTS_GAP i (\x. !y. P x y))
623Proof
624
625SIMP_TAC std_ss [GUESS_REWRITES, FORALL_PROD, EXISTS_PROD] THEN
626METIS_TAC[]
627QED
628
629
630Theorem GUESS_RULES_FORALL:
631  ((!y. GUESS_FORALL_POINT i (\x. P x y)) ==>
632   GUESS_FORALL_POINT i (\x. !y. P x y)) /\
633
634  ((!y. GUESS_FORALL i (\x. P x y)) ==>
635   GUESS_FORALL i (\x. !y. P x y)) /\
636
637  ((!y. GUESS_FORALL_GAP i (\x. P x y)) ==>
638   GUESS_FORALL_GAP i (\x. !y. P x y)) /\
639
640  ((!y. GUESS_EXISTS_POINT i (\x. P x y)) ==>
641   GUESS_EXISTS_POINT i (\x. !y. P x y)) /\
642
643  ((!y. GUESS_EXISTS (\xxx:unit. iK) (\x. P x y)) ==>
644   GUESS_EXISTS (\xxx:unit. iK) (\x. !y. P x y)) /\
645
646  ((!y. GUESS_EXISTS_GAP i (\x. P x y)) ==>
647    GUESS_EXISTS_GAP i (\x. !y. P x y))
648Proof
649
650SIMP_TAC std_ss [GUESS_REWRITES, FORALL_PROD, EXISTS_PROD] THEN
651METIS_TAC[]
652QED
653
654
655
656local
657
658fun mk_exists_thm thm =
659let
660   val thm0 = INST [
661      ``P:'c -> 'a -> bool`` |-> ``\x y. ~((P:'c -> 'a ->bool) x y)``] thm
662   val thm1 = BETA_RULE thm0
663   val thm2 = SIMP_RULE pure_ss [GSYM NOT_FORALL_THM, GSYM NOT_EXISTS_THM,
664        GUESSES_NEG_REWRITE] thm1
665in
666   thm2
667end;
668
669in
670
671Theorem GUESS_RULES_EXISTS___NEW_FV =
672    mk_exists_thm GUESS_RULES_FORALL___NEW_FV
673
674Theorem GUESS_RULES_EXISTS___NEW_FV_1 =
675    mk_exists_thm GUESS_RULES_FORALL___NEW_FV_1
676
677Theorem GUESS_RULES_EXISTS =
678    mk_exists_thm GUESS_RULES_FORALL;
679
680end
681
682
683Theorem GUESS_RULES_EXISTS_UNIQUE:
684  ((!y. GUESS_FORALL_POINT i (\x. P x y)) ==>
685   GUESS_FORALL_POINT i (\x. ?!y. P x y)) /\
686
687  ((!y. GUESS_EXISTS_GAP i (\x. P x y)) ==>
688   GUESS_EXISTS_GAP i (\x. ?!y. P x y))
689Proof
690
691SIMP_TAC std_ss [GUESS_REWRITES, EXISTS_UNIQUE_THM]
692QED
693
694
695Theorem QUANT_UNIT_ELIM[local]:
696  ((!x:unit. P x) = (P ())) /\
697  ((?x:unit. P x) = (P ()))
698Proof
699REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [
700  ASM_REWRITE_TAC[],
701  Cases_on `x` THEN ASM_REWRITE_TAC[],
702  Cases_on `x` THEN ASM_REWRITE_TAC[],
703  EXISTS_TAC ``()`` THEN ASM_REWRITE_TAC[]
704]
705QED
706
707
708
709Theorem GUESS_RULES_ELIM_UNIT:
710  (GUESS_FORALL_POINT (i:('a # unit) -> 'b) vt =
711   GUESS_FORALL_POINT (\x:'a. i (x,())) vt) /\
712
713  (GUESS_EXISTS_POINT (i:('a # unit) -> 'b) vt =
714   GUESS_EXISTS_POINT (\x:'a. i (x,())) vt) /\
715
716  (GUESS_EXISTS (i:('a # unit) -> 'b) vt =
717   GUESS_EXISTS (\x:'a. i (x,())) vt) /\
718
719  (GUESS_FORALL (i:('a # unit) -> 'b) vt =
720   GUESS_FORALL (\x:'a. i (x,())) vt) /\
721
722  (GUESS_EXISTS_GAP (i:('a # unit) -> 'b) vt =
723   GUESS_EXISTS_GAP (\x:'a. i (x,())) vt) /\
724
725  (GUESS_FORALL_GAP (i:('a # unit) -> 'b) vt =
726   GUESS_FORALL_GAP (\x:'a. i (x,())) vt)
727Proof
728
729SIMP_TAC std_ss [GUESS_REWRITES, FORALL_PROD,
730   EXISTS_PROD, QUANT_UNIT_ELIM]
731QED
732
733
734Theorem GUESS_RULES_STRENGTHEN_EXISTS_POINT:
735  !P Q. ((!x. P x ==> Q x) ==>
736  ((GUESS_EXISTS_POINT i P ==>
737    GUESS_EXISTS_POINT i Q)))
738Proof
739SIMP_TAC std_ss [GUESS_REWRITES] THEN
740METIS_TAC[]
741QED
742
743Theorem GUESS_RULES_STRENGTHEN_FORALL_GAP:
744  !P Q. ((!x. P x ==> Q x) ==>
745  ((GUESS_FORALL_GAP i P ==>
746    GUESS_FORALL_GAP i Q)))
747Proof
748SIMP_TAC std_ss [GUESS_REWRITES] THEN
749METIS_TAC[]
750QED
751
752Theorem GUESS_RULES_WEAKEN_FORALL_POINT:
753  !P Q. ((!x. Q x ==> P x) ==>
754  ((GUESS_FORALL_POINT i P ==>
755    GUESS_FORALL_POINT i Q)))
756Proof
757SIMP_TAC std_ss [GUESS_REWRITES] THEN
758METIS_TAC[]
759QED
760
761Theorem GUESS_RULES_WEAKEN_EXISTS_GAP:
762  !P Q. ((!x. Q x ==> P x) ==>
763  ((GUESS_EXISTS_GAP i P ==>
764    GUESS_EXISTS_GAP i Q)))
765Proof
766SIMP_TAC std_ss [GUESS_REWRITES] THEN
767METIS_TAC[]
768QED
769
770
771
772(*Basic theorems*)
773
774Theorem CONJ_NOT_OR_THM:
775  !A B. A /\ B = ~(~A \/ ~B)
776Proof
777REWRITE_TAC[DE_MORGAN_THM]
778QED
779
780
781Theorem EXISTS_NOT_FORALL_THM:
782  !P. ((?x. P x) = (~(!x. ~(P x))))
783Proof
784PROVE_TAC[]
785QED
786
787
788Theorem MOVE_EXISTS_IMP_THM:
789  (?x. ((!y. (~(P x y)) ==> R y) ==> Q x)) =
790         (((!y. (~(!x. P x y)) ==> R y)) ==> ?x. Q x)
791Proof
792         PROVE_TAC[]
793QED
794
795
796Theorem UNWIND_EXISTS_THM:
797   !a P. (?x. P x) = ((!x. ~(x = a) ==> ~(P x)) ==> P a)
798Proof
799 PROVE_TAC[]
800QED
801
802
803Theorem LEFT_IMP_AND_INTRO:
804   !x t1 t2. (t1 ==> t2) ==> ((x /\ t1) ==> (x /\ t2))
805Proof
806 PROVE_TAC[]
807QED
808
809Theorem RIGHT_IMP_AND_INTRO:
810   !x t1 t2. (t1 ==> t2) ==> ((t1 /\ x) ==> (t2 /\ x))
811Proof
812 PROVE_TAC[]
813QED
814
815
816Theorem LEFT_IMP_OR_INTRO:
817   !x t1 t2. (t1 ==> t2) ==> ((x \/ t1) ==> (x \/ t2))
818Proof
819 PROVE_TAC[]
820QED
821
822Theorem RIGHT_IMP_OR_INTRO:
823   !x t1 t2. (t1 ==> t2) ==> ((t1 \/ x) ==> (t2 \/ x))
824Proof
825 PROVE_TAC[]
826QED
827
828Theorem IMP_NEG_CONTRA:
829     !P i x. ~(P i) ==> (P x) ==> ~(x = i)
830Proof PROVE_TAC[]
831QED
832
833
834Theorem DISJ_IMP_INTRO:
835    (!x. P x \/ Q x) ==> ((~(P y) ==> Q y) /\ (~(Q y) ==> P y))
836Proof PROVE_TAC[]
837QED
838
839
840(******************************************************************************)
841(* Simple GUESSES                                                             *)
842(******************************************************************************)
843
844Definition SIMPLE_GUESS_EXISTS_def:
845    SIMPLE_GUESS_EXISTS (v : 'a) (i : 'a) (P : bool) =
846      (P ==> (v = i))
847End
848
849Theorem SIMPLE_GUESS_EXISTS_ALT_DEF:
850    (!v. SIMPLE_GUESS_EXISTS (v:'a) i (P v)) <=> (
851    GUESS_EXISTS_GAP ((K i):(unit -> 'a)) (\v. P v))
852Proof
853SIMP_TAC std_ss [SIMPLE_GUESS_EXISTS_def, GUESS_EXISTS_GAP_def]
854QED
855
856
857Definition SIMPLE_GUESS_FORALL_def:
858    SIMPLE_GUESS_FORALL (v : 'a) (i : 'a) (P : bool) =
859      (~P ==> (v = i))
860End
861
862Theorem SIMPLE_GUESS_FORALL_ALT_DEF:
863    (!v. SIMPLE_GUESS_FORALL (v:'a) i (P v)) <=> (
864    GUESS_FORALL_GAP ((K i):(unit -> 'a)) (\v. P v))
865Proof
866SIMP_TAC std_ss [SIMPLE_GUESS_FORALL_def, GUESS_FORALL_GAP_def]
867QED
868
869Theorem SIMPLE_GUESS_FORALL_THM:
870    !i P. (!v. SIMPLE_GUESS_FORALL v i (P v)) ==>
871    ((!v. P v) <=> (P i))
872Proof
873REWRITE_TAC [SIMPLE_GUESS_FORALL_def] THEN
874METIS_TAC[]
875QED
876
877Theorem SIMPLE_GUESS_EXISTS_THM:
878    !i P. (!v. SIMPLE_GUESS_EXISTS v i (P v)) ==>
879    ((?v. P v) <=> (P i))
880Proof
881REWRITE_TAC [SIMPLE_GUESS_EXISTS_def] THEN
882METIS_TAC[]
883QED
884
885Theorem SIMPLE_GUESS_UEXISTS_THM:
886    !i P.
887    (!v. SIMPLE_GUESS_EXISTS v i (P v)) ==>
888    ((?!v. P v) <=> (P i))
889Proof
890SIMP_TAC std_ss [SIMPLE_GUESS_EXISTS_def, EXISTS_UNIQUE_THM] THEN
891METIS_TAC[]
892QED
893
894Theorem SIMPLE_GUESS_SELECT_THM:
895    !i P.
896    (!v. SIMPLE_GUESS_EXISTS v i (P v)) ==>
897    ((@v. P v) = if P i then i else (@v. F))
898Proof
899SIMP_TAC std_ss [SIMPLE_GUESS_EXISTS_def] THEN
900REPEAT STRIP_TAC THEN
901Cases_on `P i` THEN ASM_REWRITE_TAC [] THENL [
902  SELECT_ELIM_TAC THEN
903  METIS_TAC[],
904
905  `!v. P v = F` by METIS_TAC[] THEN
906  ASM_REWRITE_TAC[]
907]
908QED
909
910
911Theorem SIMPLE_GUESS_SOME_THM:
912    !i P.
913    (!v. SIMPLE_GUESS_EXISTS v i (P v)) ==>
914    ((some v. P v) = (if P i then SOME i else NONE))
915Proof
916
917SIMP_TAC std_ss [SIMPLE_GUESS_EXISTS_def, some_def] THEN
918REPEAT STRIP_TAC THEN
919Cases_on `?v. P v` THEN (
920  ASM_REWRITE_TAC [] THEN
921  METIS_TAC[]
922)
923QED
924
925val SIMPLE_GUESS_TAC =
926  SIMP_TAC std_ss [SIMPLE_GUESS_FORALL_def, SIMPLE_GUESS_EXISTS_def] THEN METIS_TAC[];
927
928Theorem SIMPLE_GUESS_EXISTS_EQ_1:
929    !v:'a i. SIMPLE_GUESS_EXISTS v i (v = i)
930Proof
931  SIMPLE_GUESS_TAC
932QED
933
934Theorem SIMPLE_GUESS_EXISTS_EQ_2:
935    !v:'a i. SIMPLE_GUESS_EXISTS v i (i = v)
936Proof
937  SIMPLE_GUESS_TAC
938QED
939
940Theorem SIMPLE_GUESS_EXISTS_EQ_T:
941    !v. SIMPLE_GUESS_EXISTS v T v
942Proof
943  SIMPLE_GUESS_TAC
944QED
945
946Theorem SIMPLE_GUESS_FORALL_NEG:
947    !v:'a i P. SIMPLE_GUESS_EXISTS v i P ==> SIMPLE_GUESS_FORALL v i (~P)
948Proof
949  SIMPLE_GUESS_TAC
950QED
951
952Theorem SIMPLE_GUESS_EXISTS_NEG:
953    !v:'a i P. SIMPLE_GUESS_FORALL v i P ==> SIMPLE_GUESS_EXISTS v i (~P)
954Proof
955  SIMPLE_GUESS_TAC
956QED
957
958Theorem SIMPLE_GUESS_FORALL_OR_1:
959    !v:'a i P1 P2. SIMPLE_GUESS_FORALL v i P1 ==> SIMPLE_GUESS_FORALL v i (P1 \/ P2)
960Proof
961  SIMPLE_GUESS_TAC
962QED
963
964Theorem SIMPLE_GUESS_FORALL_OR_2:
965    !v:'a i P1 P2. SIMPLE_GUESS_FORALL v i P2 ==> SIMPLE_GUESS_FORALL v i (P1 \/ P2)
966Proof
967  SIMPLE_GUESS_TAC
968QED
969
970Theorem SIMPLE_GUESS_EXISTS_AND_1:
971    !v:'a i P1 P2. SIMPLE_GUESS_EXISTS v i P1 ==> SIMPLE_GUESS_EXISTS v i (P1 /\ P2)
972Proof
973  SIMPLE_GUESS_TAC
974QED
975
976Theorem SIMPLE_GUESS_EXISTS_AND_2:
977    !v:'a i P1 P2. SIMPLE_GUESS_EXISTS v i P2 ==> SIMPLE_GUESS_EXISTS v i (P1 /\ P2)
978Proof
979  SIMPLE_GUESS_TAC
980QED
981
982Theorem SIMPLE_GUESS_EXISTS_EXISTS:
983    !v:'a i P. (!v2. SIMPLE_GUESS_EXISTS v i (P v2)) ==>
984               SIMPLE_GUESS_EXISTS v i (?v2. P v2)
985Proof
986  SIMPLE_GUESS_TAC
987QED
988
989Theorem SIMPLE_GUESS_EXISTS_FORALL:
990    !v:'a i P. (!v2. SIMPLE_GUESS_EXISTS v i (P v2)) ==>
991               SIMPLE_GUESS_EXISTS v i (!v2. P v2)
992Proof
993  SIMPLE_GUESS_TAC
994QED
995
996Theorem SIMPLE_GUESS_FORALL_EXISTS:
997    !v:'a i P. (!v2. SIMPLE_GUESS_FORALL v i (P v2)) ==>
998               SIMPLE_GUESS_FORALL v i (?v2. P v2)
999Proof
1000  SIMPLE_GUESS_TAC
1001QED
1002
1003Theorem SIMPLE_GUESS_FORALL_FORALL:
1004    !v i P. (!v2. SIMPLE_GUESS_FORALL v i (P v2)) ==>
1005            SIMPLE_GUESS_FORALL v i (!v2. P v2)
1006Proof
1007  SIMPLE_GUESS_TAC
1008QED
1009
1010Theorem SIMPLE_GUESS_FORALL_IMP_1:
1011    !v:'a i P1 P2. SIMPLE_GUESS_EXISTS v i P1 ==> SIMPLE_GUESS_FORALL v i (P1 ==> P2)
1012Proof
1013  SIMPLE_GUESS_TAC
1014QED
1015
1016Theorem SIMPLE_GUESS_FORALL_IMP_2:
1017    !v:'a i P1 P2. SIMPLE_GUESS_FORALL v i P2 ==> SIMPLE_GUESS_FORALL v i (P1 ==> P2)
1018Proof
1019  SIMPLE_GUESS_TAC
1020QED
1021
1022Theorem SIMPLE_GUESS_EXISTS_EQ_FUN:
1023    !v:'a i t1 t2 f.
1024      SIMPLE_GUESS_EXISTS v i (f t1 = f t2) ==>
1025      SIMPLE_GUESS_EXISTS v i (t1 = t2)
1026Proof
1027  SIMPLE_GUESS_TAC
1028QED
1029
1030
1031(******************************************************************************)
1032(* Removing functions under quantifiers                                       *)
1033(******************************************************************************)
1034
1035
1036Definition IS_REMOVABLE_QUANT_FUN_def:
1037    IS_REMOVABLE_QUANT_FUN f = (!v. ?x. f x = v)
1038End
1039
1040Theorem IS_REMOVABLE_QUANT_FUN___EXISTS_THM:
1041    !f P. IS_REMOVABLE_QUANT_FUN f ==> ((?x. P (f x)) = (?x'. P x'))
1042Proof
1043REWRITE_TAC[IS_REMOVABLE_QUANT_FUN_def] THEN METIS_TAC[]
1044QED
1045
1046Theorem IS_REMOVABLE_QUANT_FUN___FORALL_THM:
1047    !f P. IS_REMOVABLE_QUANT_FUN f ==> ((!x. P (f x)) = (!x'. P x'))
1048Proof
1049REWRITE_TAC[IS_REMOVABLE_QUANT_FUN_def] THEN METIS_TAC[]
1050QED
1051
1052
1053
1054(* Theorems for the specialised logics *)
1055
1056Theorem PAIR_EQ_EXPAND:
1057  (((x:'a,y:'b) = X) = ((x = FST X) /\ (y = SND X))) /\
1058  ((X = (x,y)) = ((FST X = x) /\ (SND X = y)))
1059Proof
1060Cases_on `X` THEN
1061REWRITE_TAC[pairTheory.PAIR_EQ]
1062QED
1063
1064
1065Theorem PAIR_EQ_SIMPLE_EXPAND:
1066  (((x:'a,y:'b) = (x, y')) = (y = y')) /\
1067  (((y:'b,x:'a) = (y', x)) = (y = y')) /\
1068  (((FST X, y) = X) = (y = SND X)) /\
1069  (((x, SND X) = X) = (x = FST X)) /\
1070  ((X = (FST X, y)) = (SND X = y)) /\
1071  ((X = (x, SND X)) = (FST X = x))
1072Proof
1073Cases_on `X` THEN
1074ASM_REWRITE_TAC[pairTheory.PAIR_EQ]
1075QED
1076
1077
1078Theorem IS_SOME_EQ_NOT_NONE:
1079  !x. IS_SOME x = ~(x = NONE)
1080Proof
1081REWRITE_TAC[GSYM optionTheory.NOT_IS_SOME_EQ_NONE]
1082QED
1083
1084
1085Theorem ISL_exists:
1086    ISL x = (?l. x = INL l)
1087Proof
1088Cases_on `x` THEN SIMP_TAC std_ss []
1089QED
1090
1091Theorem ISR_exists:
1092    ISR x = (?r. x = INR r)
1093Proof
1094Cases_on `x` THEN SIMP_TAC std_ss []
1095QED
1096
1097Theorem INL_NEQ_ELIM:
1098    ((!l. x <> INL l) <=> (ISR x)) /\
1099    ((!l. INL l <> x) <=> (ISR x))
1100Proof
1101Cases_on `x` THEN SIMP_TAC std_ss []
1102QED
1103
1104Theorem INR_NEQ_ELIM:
1105    ((!r. x <> INR r) <=> (ISL x)) /\
1106    ((!r. INR r <> x) <=> (ISL x))
1107Proof
1108Cases_on `x` THEN SIMP_TAC std_ss []
1109QED
1110
1111Theorem LENGTH_LE_PLUS:
1112    (n + m) <= LENGTH l <=> (?l1 l2. (LENGTH l1 = n) /\ m <= LENGTH l2 /\ (l = l1 ++ l2))
1113Proof
1114SIMP_TAC list_ss [arithmeticTheory.LESS_EQ_EXISTS, LENGTH_EQ_NUM, GSYM LEFT_EXISTS_AND_THM,
1115  GSYM RIGHT_EXISTS_AND_THM] THEN
1116METIS_TAC[]
1117QED
1118
1119Theorem LENGTH_LE_NUM:
1120    n <= LENGTH l <=> (?l1 l2. (LENGTH l1 = n) /\ (l = l1 ++ l2))
1121Proof
1122SIMP_TAC list_ss [arithmeticTheory.LESS_EQ_EXISTS, LENGTH_EQ_NUM, GSYM LEFT_EXISTS_AND_THM,
1123  GSYM RIGHT_EXISTS_AND_THM]
1124QED
1125
1126
1127Theorem LENGTH_NIL_SYM =
1128  CONV_RULE (LHS_CONV SYM_CONV) (SPEC_ALL listTheory.LENGTH_NIL)
1129
1130Theorem LIST_LENGTH_COMPARE_1:
1131    ((LENGTH l < 1) <=> (l = [])) /\
1132    ((1 > LENGTH l) <=> (l = [])) /\
1133    ((0 >= LENGTH l) <=> (l = [])) /\
1134    ((LENGTH l <= 0) <=> (l = []))
1135Proof
1136`LENGTH l < 1 <=> (LENGTH l = 0)` by DECIDE_TAC THEN
1137`1 > LENGTH l <=> (LENGTH l = 0)` by DECIDE_TAC THEN
1138`0 >= LENGTH l <=> (LENGTH l = 0)` by DECIDE_TAC THEN
1139ASM_SIMP_TAC arith_ss [LENGTH_NIL]
1140QED
1141
1142
1143val LIST_LENGTH_THMS_0 = ((SPEC_ALL listTheory.LENGTH_NIL)::
1144                          (SPEC_ALL LENGTH_NIL_SYM)::
1145                          (BODY_CONJUNCTS LIST_LENGTH_COMPARE_1))
1146
1147(* prove length theormes generally *)
1148
1149local
1150  val len_t = ``LENGTH (l:'a list)``
1151
1152  fun mk_e l 0 = l
1153    | mk_e l n =
1154      mk_e (("e"^Int.toString n)::l) (n-1)
1155
1156  fun mk_base_length_thms n =
1157  let
1158    val n_t = mk_numeral (Arbnum.fromInt n)
1159    val pre_n_t = mk_numeral (Arbnum.fromInt (n-1))
1160    val es = mk_e [] n
1161
1162    (* equality *)
1163    val thm_eq = let
1164      val l = mk_eq (len_t, n_t);
1165      val thm_aux = SIMP_CONV arith_ss [LENGTH_EQ_NUM_compute, GSYM LEFT_EXISTS_AND_THM] l;
1166    in
1167      CONV_RULE (RHS_CONV (RENAME_VARS_CONV es)) thm_aux
1168    end
1169
1170    (* equality plus *)
1171    val thm_eqp = let
1172      val l = mk_eq (len_t, mk_plus(n_t, mk_var("x", ``:num``)));
1173      val thm_aux = SIMP_CONV list_ss [LENGTH_EQ_NUM, GSYM LEFT_EXISTS_AND_THM, thm_eq] l;
1174    in
1175      CONV_RULE (RHS_CONV (RENAME_VARS_CONV ["l'"])) thm_aux
1176    end
1177
1178    (* less equal *)
1179    val thm_le = let
1180      val l = mk_leq (n_t, len_t);
1181      val thm_aux = SIMP_CONV list_ss [LENGTH_LE_NUM, thm_eq, GSYM LEFT_EXISTS_AND_THM] l;
1182    in
1183      CONV_RULE (RHS_CONV (RENAME_VARS_CONV ["l'"])) thm_aux
1184    end
1185
1186    (* less equal plus *)
1187    val thm_lep = let
1188      val l = mk_leq (mk_plus(n_t, mk_var("x", ``:num``)), len_t);
1189      val thm_aux = SIMP_CONV list_ss [LENGTH_LE_PLUS, thm_eq, GSYM LEFT_EXISTS_AND_THM] l;
1190    in
1191      CONV_RULE (RHS_CONV (RENAME_VARS_CONV ["l'"])) thm_aux
1192    end
1193
1194    (* less *)
1195    val thm_less = let
1196      val l = mk_less (pre_n_t, len_t);
1197      val thm_aux = SIMP_CONV list_ss [arithmeticTheory.LESS_EQ, thm_le] l;
1198    in
1199      thm_aux
1200    end
1201  in
1202    (thm_eq, thm_eqp, thm_le, thm_lep, thm_less)
1203  end
1204
1205in
1206
1207fun mk_length_n_thms 0 = LIST_LENGTH_THMS_0
1208  | mk_length_n_thms n =
1209let
1210  fun lhs_rule c = CONV_RULE (LHS_CONV c)
1211  val (eq_thm, eqp_thm, le_thm, lep_thm, less_thm) = mk_base_length_thms n
1212
1213  val eq_thm_sym = lhs_rule SYM_CONV eq_thm
1214  val ge_thm = lhs_rule (REWR_CONV (GSYM arithmeticTheory.GREATER_EQ)) le_thm
1215  val greater_thm = lhs_rule (REWR_CONV (GSYM arithmeticTheory.GREATER_DEF)) less_thm
1216  val gep_thm = lhs_rule (REWR_CONV (GSYM arithmeticTheory.GREATER_EQ)) lep_thm
1217  val leps_thm = lhs_rule (RATOR_CONV (RAND_CONV (REWR_CONV (GSYM arithmeticTheory.ADD_SYM)))) lep_thm
1218  val geps_thm = lhs_rule (REWR_CONV (GSYM arithmeticTheory.GREATER_EQ)) leps_thm
1219
1220  val eqp_thm_sym = lhs_rule SYM_CONV eqp_thm
1221  val eqps_thm = lhs_rule (RHS_CONV (REWR_CONV (GSYM arithmeticTheory.ADD_SYM))) eqp_thm
1222  val eqps_thm_sym = lhs_rule SYM_CONV eqps_thm
1223
1224in
1225  [eq_thm, eq_thm_sym, less_thm, greater_thm, le_thm, ge_thm, lep_thm, gep_thm, leps_thm, geps_thm, eqp_thm, eqp_thm_sym, eqps_thm, eqps_thm_sym]
1226end
1227
1228fun mk_length_upto_n_thms 0 = LIST_LENGTH_THMS_0
1229  | mk_length_upto_n_thms n =
1230       (mk_length_n_thms n) @ (mk_length_upto_n_thms (n-1))
1231
1232end
1233
1234Theorem LIST_LENGTH_0 = LIST_CONJ (mk_length_upto_n_thms 0);
1235Theorem LIST_LENGTH_1 = LIST_CONJ (mk_length_upto_n_thms 1);
1236Theorem LIST_LENGTH_2[unlisted]  = LIST_CONJ (mk_length_upto_n_thms 2)
1237Theorem LIST_LENGTH_3[unlisted] = LIST_CONJ (mk_length_upto_n_thms 3)
1238Theorem LIST_LENGTH_4[unlisted] = LIST_CONJ (mk_length_upto_n_thms 4)
1239Theorem LIST_LENGTH_5[unlisted] = LIST_CONJ (mk_length_upto_n_thms 5)
1240Theorem LIST_LENGTH_7[unlisted] = LIST_CONJ (mk_length_upto_n_thms 7)
1241Theorem LIST_LENGTH_10[unlisted] = LIST_CONJ (mk_length_upto_n_thms 10)
1242Theorem LIST_LENGTH_15[unlisted] = LIST_CONJ (mk_length_upto_n_thms 15)
1243Theorem LIST_LENGTH_20[unlisted] = LIST_CONJ (mk_length_upto_n_thms 20)
1244Theorem LIST_LENGTH_25[unlisted] = LIST_CONJ (mk_length_upto_n_thms 25)
1245
1246Theorem LIST_LENGTH_COMPARE_SUC:
1247  (SUC x <= LENGTH l <=> ?l' e1. x <= LENGTH l' /\ (l = e1::l')) /\
1248  (LENGTH l >= SUC x <=> ?l' e1. x <= LENGTH l' /\ (l = e1::l')) /\
1249  ((LENGTH l = SUC x) <=> ?l' e1. (LENGTH l' = x) /\ (l = e1::l')) /\
1250  ((SUC x = LENGTH l) <=> ?l' e1. (LENGTH l' = x) /\ (l = e1::l'))
1251Proof
1252SIMP_TAC std_ss [arithmeticTheory.ADD1, LIST_LENGTH_1]
1253QED
1254
1255(* alternative to LIST_LENGTH_n theorems (also use PULL_EXISTS) *)
1256Theorem LENGTH_TO_EXISTS_CONS:
1257  (n < LENGTH xs <=> (?y ys. (xs = y :: ys) /\ n <= LENGTH ys))
1258  /\
1259  (LENGTH xs > n <=> (?y ys. (xs = y :: ys) /\ n <= LENGTH ys))
1260  /\
1261  (0 < n ==> ((LENGTH xs = n) <=> (?y ys. (xs = y :: ys) /\ (LENGTH ys = PRE n))))
1262  /\
1263  (0 < n ==> ((n = LENGTH xs) <=> (?y ys. (xs = y :: ys) /\ (LENGTH ys = PRE n))))
1264  /\
1265  (0 < n ==> (n <= LENGTH xs <=> (?y ys. (xs = y :: ys) /\ PRE n <= LENGTH ys)))
1266  /\
1267  (0 < n ==> (LENGTH xs >= n <=> (?y ys. (xs = y :: ys) /\ PRE n <= LENGTH ys)))
1268  /\
1269  (0 < x ==> (PRE (x + y) = PRE x + y))
1270  /\
1271  (0 < y ==> (PRE (x + y) = x + PRE y))
1272Proof
1273  simp_tac list_ss [] \\ Cases_on `xs` \\ simp_tac list_ss []
1274QED
1275
1276(* Useful rewrites *)
1277val HD_TL_EQ_TAC = REPEAT (Cases THEN SIMP_TAC list_ss [] THEN SPEC_ALL_TAC)
1278
1279Theorem HD_TL_EQ_1[simp]:
1280  !l. (HD l :: TL l = l) <=> l <> []
1281Proof HD_TL_EQ_TAC
1282QED
1283
1284Theorem HD_TL_EQ_2[local]:
1285    !l. (HD l :: (HD (TL l)) :: (TL (TL l)) = l) <=> (LENGTH l > 1)
1286Proof
1287HD_TL_EQ_TAC
1288QED
1289
1290Theorem HD_TL_EQ_3[local]:
1291    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (TL (TL (TL l))) = l) <=> (LENGTH l > 2)
1292Proof
1293HD_TL_EQ_TAC
1294QED
1295
1296Theorem HD_TL_EQ_4[local]:
1297    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: TL (TL (TL (TL l))) = l) <=> (LENGTH l > 3)
1298Proof
1299HD_TL_EQ_TAC
1300QED
1301
1302Theorem HD_TL_EQ_5[local]:
1303    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1304        (HD (TL (TL (TL (TL l))))) :: TL (TL (TL (TL (TL l)))) = l) <=> (LENGTH l > 4)
1305Proof
1306HD_TL_EQ_TAC
1307QED
1308
1309Theorem HD_TL_EQ_6[local]:
1310    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1311        (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: TL (TL (TL (TL (TL (TL l))))) = l) <=> (LENGTH l > 5)
1312Proof
1313HD_TL_EQ_TAC
1314QED
1315
1316Theorem HD_TL_EQ_7[local]:
1317    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1318        (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) ::
1319        HD (TL (TL (TL (TL (TL (TL l)))))) :: TL (TL (TL (TL (TL (TL (TL l)))))) = l) <=> (LENGTH l > 6)
1320Proof
1321HD_TL_EQ_TAC
1322QED
1323
1324Theorem HD_TL_EQ_8[local]:
1325    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1326        (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) ::
1327        HD (TL (TL (TL (TL (TL (TL l)))))) :: HD (TL (TL (TL (TL (TL (TL (TL l))))))) ::
1328        TL (TL (TL (TL (TL (TL (TL (TL l))))))) = l) <=> (LENGTH l > 7)
1329Proof
1330HD_TL_EQ_TAC
1331QED
1332
1333Theorem HD_TL_EQ_9[local]:
1334    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1335        (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) ::
1336        HD (TL (TL (TL (TL (TL (TL l)))))) :: HD (TL (TL (TL (TL (TL (TL (TL l))))))) ::
1337        HD (TL (TL (TL (TL (TL (TL (TL (TL l)))))))) :: TL (TL (TL (TL (TL (TL (TL (TL (TL l)))))))) = l) <=> (LENGTH l > 8)
1338Proof
1339HD_TL_EQ_TAC
1340QED
1341
1342
1343Theorem HD_TL_EQ_NIL_1[local]:
1344  !l. ([HD l] = l) <=> (LENGTH l = 1)
1345Proof HD_TL_EQ_TAC
1346QED
1347
1348Theorem HD_TL_EQ_NIL_1_bothways[simp] =
1349        CONJ HD_TL_EQ_NIL_1
1350             (CONV_RULE (STRIP_QUANT_CONV
1351                         (LAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])))
1352                        HD_TL_EQ_NIL_1)
1353
1354Theorem HD_TL_EQ_NIL_2[local]:
1355    !l. (HD l :: (HD (TL l)) :: [] = l) <=> (LENGTH l = 2)
1356Proof
1357HD_TL_EQ_TAC
1358QED
1359
1360Theorem HD_TL_EQ_NIL_3[local]:
1361    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: [] = l) <=> (LENGTH l = 3)
1362Proof
1363HD_TL_EQ_TAC
1364QED
1365
1366Theorem HD_TL_EQ_NIL_4[local]:
1367    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: [] = l) <=> (LENGTH l = 4)
1368Proof
1369HD_TL_EQ_TAC
1370QED
1371
1372Theorem HD_TL_EQ_NIL_5[local]:
1373    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1374        (HD (TL (TL (TL (TL l))))) :: [] = l) <=> (LENGTH l = 5)
1375Proof
1376HD_TL_EQ_TAC
1377QED
1378
1379Theorem HD_TL_EQ_NIL_6[local]:
1380    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1381        (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: [] = l) <=> (LENGTH l = 6)
1382Proof
1383HD_TL_EQ_TAC
1384QED
1385
1386Theorem HD_TL_EQ_NIL_7[local]:
1387    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1388        (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) ::
1389        HD (TL (TL (TL (TL (TL (TL l)))))) :: [] = l) <=> (LENGTH l = 7)
1390Proof
1391HD_TL_EQ_TAC
1392QED
1393
1394Theorem HD_TL_EQ_NIL_8[local]:
1395    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1396        (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) ::
1397        HD (TL (TL (TL (TL (TL (TL l)))))) :: HD (TL (TL (TL (TL (TL (TL (TL l))))))) ::
1398        [] = l) <=> (LENGTH l = 8)
1399Proof
1400HD_TL_EQ_TAC
1401QED
1402
1403Theorem HD_TL_EQ_NIL_9[local]:
1404    !l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) ::
1405        (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) ::
1406        HD (TL (TL (TL (TL (TL (TL l)))))) :: HD (TL (TL (TL (TL (TL (TL (TL l))))))) ::
1407        HD (TL (TL (TL (TL (TL (TL (TL (TL l)))))))) :: [] = l) <=> (LENGTH l = 9)
1408Proof
1409HD_TL_EQ_TAC
1410QED
1411
1412val HD_TL_EQ_THMS_1 = [
1413  HD_TL_EQ_1,
1414  HD_TL_EQ_2,
1415  HD_TL_EQ_3,
1416  HD_TL_EQ_4,
1417  HD_TL_EQ_5,
1418  HD_TL_EQ_6,
1419  HD_TL_EQ_7,
1420  HD_TL_EQ_8,
1421  HD_TL_EQ_9,
1422  HD_TL_EQ_NIL_1,
1423  HD_TL_EQ_NIL_2,
1424  HD_TL_EQ_NIL_3,
1425  HD_TL_EQ_NIL_4,
1426  HD_TL_EQ_NIL_5,
1427  HD_TL_EQ_NIL_6,
1428  HD_TL_EQ_NIL_7,
1429  HD_TL_EQ_NIL_8,
1430  HD_TL_EQ_NIL_9]
1431
1432val HD_TL_EQ_THMS_2 = map (
1433 CONV_RULE (QUANT_CONV (LHS_CONV (REWR_CONV EQ_SYM_EQ)))) HD_TL_EQ_THMS_1
1434
1435Theorem HD_TL_EQ_THMS[unlisted] =
1436        LIST_CONJ (HD_TL_EQ_THMS_1 @ HD_TL_EQ_THMS_2)
1437
1438(* alternative to HD_TL_EQ_THMS for any length *)
1439Theorem CONS_EQ_REWRITE:
1440  ((x :: xs = ys) <=> 1 <= LENGTH ys /\ (x = HD ys) /\ (xs = TL ys))
1441  /\
1442  ((ys = x :: xs) <=> 1 <= LENGTH ys /\ (HD ys = x) /\ (TL ys = xs))
1443  /\
1444  (0 < n ==> (n <= LENGTH (TL ys) <=> n + 1 <= LENGTH ys))
1445  /\
1446  (n <= m ==> (n <= rhs /\ m <= rhs <=> m <= rhs))
1447  /\
1448  (([] = TL ys) <=> LENGTH ys <= 1)
1449  /\
1450  ((TL ys = []) <=> LENGTH ys <= 1)
1451  /\
1452  (LENGTH (TL ys) <= n <=> LENGTH ys <= n + 1)
1453  /\
1454  (m <= n /\ n <= m <=> (m = n))
1455  /\
1456  (m <= LENGTH ys /\ (n = LENGTH ys) <=> m <= n /\ (n = LENGTH ys))
1457Proof
1458  Cases_on `ys` \\ simp_tac list_ss []
1459  \\ Cases_on `t` \\ simp_tac list_ss []
1460QED
1461
1462Theorem SOME_THE_EQ:
1463    !opt. (SOME (THE opt) = opt) <=> IS_SOME opt
1464Proof
1465Cases THEN SIMP_TAC std_ss []
1466QED
1467
1468Theorem SOME_THE_EQ_SYM:
1469    !opt. (opt = SOME (THE opt)) <=> IS_SOME opt
1470Proof
1471Cases THEN SIMP_TAC std_ss []
1472QED
1473
1474Theorem FST_PAIR_EQ:
1475  !p p2. ((FST p, p2) = p) <=> (p2 = SND p)
1476Proof
1477Cases THEN SIMP_TAC std_ss []
1478QED
1479
1480Theorem SND_PAIR_EQ:
1481  !p p1. ((p1, SND p) = p) <=> (p1 = FST p)
1482Proof
1483Cases THEN SIMP_TAC std_ss []
1484QED
1485
1486Theorem FST_PAIR_EQ_SYM:
1487  !p p2. (p = (FST p, p2)) <=> (SND p = p2)
1488Proof
1489Cases THEN SIMP_TAC std_ss []
1490QED
1491
1492Theorem SND_PAIR_EQ_SYM:
1493  !p p1. (p = (p1, SND p)) <=> (FST p = p1)
1494Proof
1495Cases THEN SIMP_TAC std_ss []
1496QED