patternMatchesScript.sml

1Theory patternMatches[bare]
2Ancestors
3  option list
4Libs
5  HolKernel Parse boolLib Drule BasicProvers simpLib TotalDefn
6  ConseqConv numLib quantHeuristicsLib metisLib
7
8val std_ss = numLib.std_ss
9val list_ss  = numLib.arith_ss ++ listSimps.LIST_ss
10
11val _ = ParseExtras.temp_loose_equality()
12
13
14(***************************************************)
15(* Auxiliary stuff                                 *)
16(***************************************************)
17
18Theorem IS_SOME_OPTION_MAP[local]:
19    !f v. IS_SOME (OPTION_MAP f v) = IS_SOME v
20Proof
21Cases_on `v` THEN
22SIMP_TAC list_ss []
23QED
24
25Theorem some_eq_SOME[local]:
26    !P x. ((some x. P x) = SOME x) ==> (P x)
27Proof
28SIMP_TAC std_ss [some_def] THEN
29REPEAT STRIP_TAC THEN
30SELECT_ELIM_TAC THEN
31PROVE_TAC[]
32QED
33
34Theorem some_var_bool_T:
35    (some x. x) = SOME T
36Proof
37  `(some x. x) = (some x. (x = T))` by REWRITE_TAC[] THEN
38  ONCE_ASM_REWRITE_TAC[] THEN
39  PURE_REWRITE_TAC[optionTheory.some_EQ] THEN
40  REWRITE_TAC[]
41QED
42
43Theorem some_var_bool_F:
44    (some x. ~x) = SOME F
45Proof
46  `(some x. ~x) = (some x. (x = F))` by REWRITE_TAC[] THEN
47  ONCE_ASM_REWRITE_TAC[] THEN
48  PURE_REWRITE_TAC[optionTheory.some_EQ] THEN
49  REWRITE_TAC[]
50QED
51
52Theorem some_eq_NONE[local]:
53    !P. ((some x. P x) = NONE) <=> (!x. ~(P x))
54Proof
55SIMP_TAC std_ss [some_def]
56QED
57
58Theorem some_IS_SOME[local]:
59    !P. (IS_SOME (some x. P x)) <=> (?x. P x)
60Proof
61SIMP_TAC (std_ss++boolSimps.LIFT_COND_ss) [some_def]
62QED
63
64Theorem some_IS_SOME_EXISTS[local]:
65    !P. (IS_SOME (some x. P x)) <=> (?x. P x /\ ((some x. P x) = SOME x))
66Proof
67GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN (
68  ASM_SIMP_TAC std_ss []
69) THEN
70Cases_on `some x. P x` THEN FULL_SIMP_TAC std_ss [] THEN
71MATCH_MP_TAC some_eq_SOME THEN
72ASM_REWRITE_TAC[]
73QED
74
75Theorem OPTION_MAP_EQ_OPTION_MAP[local]:
76  (OPTION_MAP f x = OPTION_MAP f' x') =
77  (((x = NONE) /\ (x' = NONE)) \/
78   (?y y'. (x = SOME y) /\ (x' = SOME y') /\ (f y = f' y')))
79Proof
80
81Cases_on `x` THEN Cases_on `x'` THEN (
82  SIMP_TAC std_ss []
83)
84QED
85
86
87(***************************************************)
88(* Main Definitions                                *)
89(***************************************************)
90
91(* rows of a case-expression consist of a
92   - pattern p
93   - guard g
94   - rhs r
95
96   A row matches an input value i with a variable
97   binding v, iff the following
98   predicate holds. *)
99Definition PMATCH_ROW_COND_def[nocompute]:   PMATCH_ROW_COND pat guard inp v =
100  (pat v = inp) /\ (guard v)
101End
102
103(* With this we can easily define the semantics of a row *)
104Definition PMATCH_ROW_def[nocompute]:   PMATCH_ROW pat guard rhs i =
105  (OPTION_MAP rhs (some v. PMATCH_ROW_COND pat guard i v))
106End
107
108
109(* We defined semantics of single rows. Let's extend
110   it to multiple ones, i.e. full pattern matches now. *)
111Definition PMATCH_INCOMPLETE_def:   PMATCH_INCOMPLETE = ARB
112End
113Definition PMATCH_def[nocompute]:
114  (PMATCH v [] = PMATCH_INCOMPLETE) /\
115  (PMATCH v (r::rs) = option_CASE (r v) (PMATCH v rs) I)
116End
117
118
119(***************************************************)
120(* Constants for parsing magic                     *)
121(***************************************************)
122
123(* We need some dummy constant without any semnatic meaning
124   for setting up some parser magic. It is HOL 4 specific
125   and boring technical stuff. You can safely ignore the following. *)
126
127val _ = new_constant ("PMATCH_magic_1", type_of ``PMATCH``)
128
129val _ = new_constant ("PMATCH_ROW_magic_1", type_of
130   ``\abc. PMATCH_ROW (\x. FST (abc x)) (\x. FST (SND (abc x))) (\x. SND (SND ((abc x))))``)
131
132val _ = new_constant ("PMATCH_ROW_magic_0", type_of
133   ``\abc. PMATCH_ROW (\x:unit. FST abc) (\x. FST (SND abc)) (\x. SND (SND (abc)))``)
134
135val _ = new_constant ("PMATCH_ROW_magic_4", type_of
136   ``\abc. PMATCH_ROW (\x:unit. FST abc) (\x. FST (SND abc)) (\x. SND (SND (abc)))``)
137
138val _ = new_constant ("PMATCH_ROW_magic_2", type_of
139   ``\(pat:'a) (g:bool) (res:'b). (pat,g,res)``)
140
141val _ = new_constant ("PMATCH_ROW_magic_3", type_of
142   ``\(pat:'a) (res:'b). (pat,T,res)``)
143
144
145
146(***************************************************)
147(* Congruences for termination                     *)
148(***************************************************)
149
150(* Pattern matches expressed via PMATCH should
151   be usable in recursive function defintions. In  order
152   to be able to do this, we need to set up some
153   congruence theorems that guide the automatic
154   wellfoundedness (termination) checker. *)
155
156Theorem PMATCH_ROW_CONG:
157  !p p' g g' r r' v v'.
158     (p = p') /\ (v = v') /\
159     (!x. (v = (p x)) ==> (g x = g' x)) /\
160     (!x. ((v = (p x)) /\ (g x)) ==>
161          (r x = r' x)) ==>
162  (PMATCH_ROW p g r v = PMATCH_ROW p' g' r' v')
163Proof
164
165REPEAT STRIP_TAC THEN
166ASM_SIMP_TAC (std_ss++boolSimps.CONJ_ss) [PMATCH_ROW_def,
167  PMATCH_ROW_COND_def] THEN
168Cases_on `some x. (p' x = v') /\ (g' x)` THEN (
169  ASM_SIMP_TAC std_ss []
170) THEN
171POP_ASSUM (fn thm => MP_TAC (HO_MATCH_MP (SPEC_ALL some_eq_SOME) thm)) THEN
172ASM_SIMP_TAC std_ss []
173QED
174
175
176Theorem PMATCH_CONG:
177  !v v' rows rows' r r'. ((v = v') /\ (r v' = r' v') /\
178        (PMATCH v' rows = PMATCH v' rows')) ==>
179  (PMATCH v (r :: rows) = PMATCH v' (r' :: rows'))
180Proof
181SIMP_TAC std_ss [PMATCH_def]
182QED
183
184val _ = DefnBase.export_cong "PMATCH_ROW_CONG";
185val _ = DefnBase.export_cong "PMATCH_CONG";
186
187
188(***************************************************)
189(* Rewrites                                        *)
190(***************************************************)
191
192Theorem PMATCH_ROW_EQ_AUX:
193    ((!i. (?x. PMATCH_ROW_COND p  g  i x) =
194          (?x'. PMATCH_ROW_COND p' g' i x')) /\
195     (!x x'. ((p x = p' x') /\ g x /\ g' x') ==> (r x = r' x'))) ==>
196    (PMATCH_ROW p  g  r  = PMATCH_ROW p' g' r')
197Proof
198REPEAT STRIP_TAC THEN
199SIMP_TAC std_ss [FUN_EQ_THM, PMATCH_ROW_def,
200  OPTION_MAP_EQ_OPTION_MAP] THEN
201CONV_TAC (RENAME_VARS_CONV ["i"]) THEN
202GEN_TAC THEN
203Q.PAT_X_ASSUM `!i. (_ = _)` (fn thm => ASSUME_TAC (Q.SPEC `i` thm))  THEN
204Tactical.REVERSE (Cases_on `?x. PMATCH_ROW_COND p g i x`) THEN (
205  FULL_SIMP_TAC std_ss []
206) THEN
207DISJ2_TAC THEN
208`IS_SOME (some x. PMATCH_ROW_COND p g i x) /\
209 IS_SOME (some x. PMATCH_ROW_COND p' g' i x)` by (
210  ASM_SIMP_TAC std_ss [some_IS_SOME] THEN
211  PROVE_TAC[]
212) THEN
213FULL_SIMP_TAC std_ss [some_IS_SOME_EXISTS] THEN
214FULL_SIMP_TAC std_ss [PMATCH_ROW_COND_def]
215QED
216
217Theorem PMATCH_ROW_EQ_NONE:
218    (PMATCH_ROW p g r i = NONE) <=>
219    (!x. ~(PMATCH_ROW_COND p g i x))
220Proof
221SIMP_TAC std_ss [PMATCH_ROW_def, some_eq_NONE]
222QED
223
224Theorem PMATCH_ROW_EQ_SOME:
225    (PMATCH_ROW p g r i = SOME y) ==>
226    (?x. (PMATCH_ROW_COND p g i x) /\ (y = r x))
227Proof
228SIMP_TAC std_ss [PMATCH_ROW_def] THEN
229REPEAT STRIP_TAC THEN
230Q.EXISTS_TAC `z` THEN
231IMP_RES_TAC some_eq_SOME THEN
232ASM_SIMP_TAC std_ss []
233QED
234
235
236Theorem PMATCH_COND_SELECT_UNIQUE:
237    !p g i.
238    (!x1 x2. (g x1 /\ g x2 /\ (p x1 = p x2)) ==> (x1 = x2)) ==>
239    !x. PMATCH_ROW_COND p g i x ==>
240    ((@y. PMATCH_ROW_COND p g i y) = x)
241Proof
242
243SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN
244METIS_TAC[]
245QED
246
247Theorem PMATCH_ROW_COND_DEF_GSYM:
248    PMATCH_ROW_COND pat guard inp v =
249    ((inp = pat v) /\ (guard v))
250Proof
251SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN
252PROVE_TAC[]
253QED
254
255
256Theorem PMATCH_EVAL:
257   (PMATCH v [] = PMATCH_INCOMPLETE) /\
258   (PMATCH v ((PMATCH_ROW p g r) :: rs) =
259      if (?x. (PMATCH_ROW_COND p g v x)) then
260         (r (@x. PMATCH_ROW_COND p g v x)) else PMATCH v rs)
261Proof
262
263SIMP_TAC std_ss [PMATCH_def] THEN
264Cases_on `PMATCH_ROW p g r v` THENL [
265  FULL_SIMP_TAC std_ss [PMATCH_ROW_def, some_eq_NONE],
266
267  FULL_SIMP_TAC std_ss [PMATCH_ROW_def, some_def] THEN
268  METIS_TAC[]
269]
270QED
271
272Theorem PMATCH_EVAL_MATCH:
273   ~(PMATCH_ROW p g r v = NONE) ==>
274   (PMATCH v ((PMATCH_ROW p g r) :: rs) =
275      (r (@x. PMATCH_ROW_COND p g v x)))
276Proof
277
278SIMP_TAC std_ss [PMATCH_EVAL,
279 PMATCH_ROW_EQ_NONE]
280QED
281
282
283(***************************************************)
284(* Changing rows and removing redundant ones       *)
285(***************************************************)
286
287(* For many of automatic methods, we need to show
288   that two PMATCH expressions which are derived from
289   each other by modifying or dropping rows are equivalent.
290   We want to perform these proofs in an a way that can be
291   automated nicely. In the following, we provide lemmata that
292   given an established equivalence, allow adding
293   a row to both or a single side.
294   By starting with an empty list and iterating, one can
295   use this method to construct the desired correspondance. *)
296Theorem PMATCH_EXTEND_BASE:
297  !v_old v_new. (PMATCH v_old [] = PMATCH v_new [])
298Proof
299SIMP_TAC std_ss [PMATCH_def]
300QED
301
302Theorem PMATCH_EXTEND_BOTH:
303  !v_old v_new rows_old rows_new r_old r_new.
304  (r_old v_old = r_new v_new) ==>
305  (PMATCH v_old rows_old = PMATCH v_new rows_new) ==>
306  (PMATCH v_old (r_old::rows_old) = PMATCH v_new (r_new :: rows_new))
307Proof
308SIMP_TAC std_ss [PMATCH_def]
309QED
310
311Theorem PMATCH_EXTEND_BOTH_ID:
312  !v rows_old rows_new r.
313  (PMATCH v rows_old = PMATCH v rows_new) ==>
314  (PMATCH v (r::rows_old) = PMATCH v (r :: rows_new))
315Proof
316SIMP_TAC std_ss [PMATCH_def]
317QED
318
319Theorem PMATCH_EXTEND_OLD:
320  !v_old v_new rows_old rows_new r_old.
321  (r_old v_old = NONE) ==>
322  (PMATCH v_old rows_old = PMATCH v_new rows_new) ==>
323  (PMATCH v_old (r_old::rows_old) = PMATCH v_new rows_new)
324Proof
325SIMP_TAC std_ss [PMATCH_def]
326QED
327
328
329
330(***************************************************)
331(* Simplifying case expressions                    *)
332(***************************************************)
333
334(* We can now construct equivalences of case expressions, provided
335   we can reason about the semantics of single rows. So,
336   let's now consider useful theorems for single rows. *)
337
338(* Add an injective function to the pattern and the value.
339   This can be used to eliminate constructors. *)
340Theorem PMATCH_ROW_REMOVE_FUN:
341  !ff v p g r. (!x y. (ff x = ff y) ==> (x = y)) ==>
342
343  (PMATCH_ROW (\x. (ff (p x))) g r (ff v) =
344   PMATCH_ROW (\x. (p x)) g r v)
345Proof
346
347REPEAT STRIP_TAC THEN
348`!x y. (ff x = ff y) = (x = y)` by PROVE_TAC[] THEN
349ASM_SIMP_TAC std_ss [PMATCH_ROW_def, PMATCH_ROW_COND_def]
350QED
351
352
353(* The following lemma looks rather complicated. It is
354   intended to work together with PMATCH_ROW_REMOVE_FUN to
355   propagate information in the var cases.
356
357   as an example consider
358
359   val t = ``PMATCH (SOME x, y) [
360     PMATCH_ROW (\x. (SOME x, 0)) (K T) (\x. (SOME (x + y)));
361     PMATCH_ROW (\(x', y). (x', y)) (K T) (\(x', y). x')
362   ]``
363
364   We want to simplify this to
365
366   val t = ``PMATCH (x, y) [
367     PMATCH_ROW (\x. (x, 0)) (K T) (\x. (SOME (x + y)));
368     PMATCH_ROW (\(x'', y). (x'', y)) (K T) (\(x'', y). SOME x'')
369   ]``
370
371   This is done via PMATCH_ROWS_SIMP and PMATCH_ROWS_SIMP_SOUNDNESS.
372   We need to show that the rows correspond to each other.
373
374   For the first row, PMATCH_ROW_REMOVE_FUN is used with
375
376   v := (x, y)
377   ff (x, y) := (SOME x, y)
378
379   p x := (x, 0)
380   r x := SOME (x + y)
381
382
383   For the second row, PMATCH_ROW_REMOVE_FUN is used with
384
385   v := (SOME x, y)
386   v' := (x, y)
387   p (x', y) := (x', y)
388   r (x', y) := x'
389   p' (x'', y) = (x'', y)
390   f (x'', y) := (SOME x'', y)
391*)
392
393Theorem PMATCH_ROW_EXTEND_INPUT:
394  !v v' f' f p g r p' .
395  ((!x'. (v' = p' x') ==> (p (f x') = v)) /\
396   (!x. (v = p x) ==> ?x'. (p' x' = v')) /\
397   (!x y. (p x = p y) ==> (x = y))) ==>
398  (PMATCH_ROW p (g (f' v')) (r (f' v')) v =
399   PMATCH_ROW p' (\x. g (f' (p' x)) (f x)) (\x. r (f' (p' x)) (f x)) v')
400Proof
401
402REPEAT STRIP_TAC THEN
403ASM_SIMP_TAC std_ss [PMATCH_ROW_def] THEN
404`IS_SOME (some x. PMATCH_ROW_COND p' (\x. g (f' (p' x)) (f x)) v' x) =
405 IS_SOME (some x. PMATCH_ROW_COND p (g (f' v')) v x)` by (
406   ASM_SIMP_TAC std_ss [some_IS_SOME, PMATCH_ROW_COND_def] THEN
407   METIS_TAC[]
408) THEN
409Tactical.REVERSE (Cases_on `IS_SOME (some x. PMATCH_ROW_COND p (g (f' v')) v x)`) THEN (
410  FULL_SIMP_TAC std_ss []
411) THEN
412FULL_SIMP_TAC std_ss [some_IS_SOME_EXISTS] THEN
413FULL_SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN
414METIS_TAC[]
415QED
416
417
418Theorem PMATCH_ROW_REMOVE_FUN_VAR:
419  !v v' f p g r p' .
420  ((!x'. (v' = p' x') = (p (f x') = v)) /\
421  ((!x. (v = p x) ==> ?x'. f x' = x)) /\
422  ((!x y. (p x = p y) ==> (x = y)))) ==>
423  (PMATCH_ROW p g r v =
424   PMATCH_ROW p' (\x. g (f x)) (\x. r (f x)) v')
425Proof
426
427REPEAT STRIP_TAC THEN
428ASM_SIMP_TAC std_ss [PMATCH_ROW_def] THEN
429`IS_SOME (some x. PMATCH_ROW_COND p' (\x. g (f x)) v' x) =
430 IS_SOME (some x. PMATCH_ROW_COND p g v x)` by (
431   ASM_SIMP_TAC std_ss [some_IS_SOME, PMATCH_ROW_COND_def] THEN
432   METIS_TAC[]
433) THEN
434Tactical.REVERSE (Cases_on `IS_SOME (some x. PMATCH_ROW_COND p g v x)`) THEN (
435  FULL_SIMP_TAC std_ss []
436) THEN
437FULL_SIMP_TAC std_ss [some_IS_SOME_EXISTS] THEN
438FULL_SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN
439METIS_TAC[]
440QED
441
442
443(***************************************************)
444(* Equivalent sets of rows                         *)
445(***************************************************)
446
447Definition PMATCH_EQUIV_ROWS_def:
448 PMATCH_EQUIV_ROWS v rows1 rows2 = (
449 (PMATCH v rows1 = PMATCH v rows2) /\
450 ((?r. MEM r rows1 /\ IS_SOME (r v)) =
451  (?r. MEM r rows2 /\ IS_SOME (r v))))
452End
453
454
455Theorem PMATCH_EQUIV_ROWS_EQUIV_EXPAND:
456    PMATCH_EQUIV_ROWS v rows1 rows2 = (
457    PMATCH_EQUIV_ROWS v rows1 = PMATCH_EQUIV_ROWS v rows2)
458Proof
459
460SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def, FUN_EQ_THM] THEN
461METIS_TAC[]
462QED
463
464Theorem PMATCH_EQUIV_ROWS_is_equiv_1:
465    (!v rows. (PMATCH_EQUIV_ROWS v rows rows))
466Proof
467SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def]
468QED
469
470
471Theorem PMATCH_EQUIV_ROWS_is_equiv_2:
472    (!v rows1 rows2. ((PMATCH_EQUIV_ROWS v rows1 rows2) =
473                      (PMATCH_EQUIV_ROWS v rows2 rows1)))
474Proof
475SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def] THEN METIS_TAC[]
476QED
477
478Theorem PMATCH_EQUIV_ROWS_is_equiv_3:
479    (!v rows1 rows2 rows3.
480       (PMATCH_EQUIV_ROWS v rows1 rows2) ==>
481       (PMATCH_EQUIV_ROWS v rows2 rows3) ==>
482       (PMATCH_EQUIV_ROWS v rows1 rows3))
483Proof
484SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def]
485QED
486
487Theorem PMATCH_EQUIV_ROWS_MATCH:
488    PMATCH_EQUIV_ROWS v rows1 rows2 ==>
489    (PMATCH v rows1 = PMATCH v rows2)
490Proof
491SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def]
492QED
493
494Theorem PMATCH_APPEND_SEM:
495    !v rows1 rows2. PMATCH v (rows1 ++ rows2) = (
496      if (?r. MEM r rows1 /\ IS_SOME (r v)) then PMATCH v rows1 else PMATCH v rows2)
497Proof
498REPEAT GEN_TAC THEN
499Induct_on `rows1` THEN1 (
500  SIMP_TAC list_ss []
501) THEN
502ASM_SIMP_TAC list_ss [PMATCH_def, RIGHT_AND_OVER_OR, EXISTS_OR_THM] THEN
503GEN_TAC THEN
504Cases_on `h v` THEN (
505  ASM_SIMP_TAC std_ss []
506)
507QED
508
509Theorem PMATCH_EQUIV_APPEND:
510  !v rows1a rows1b rows2a rows2b.
511  (PMATCH_EQUIV_ROWS v rows1a rows1b) ==>
512  (PMATCH_EQUIV_ROWS v rows2a rows2b) ==>
513  (PMATCH_EQUIV_ROWS v (rows1a ++ rows2a) (rows1b ++ rows2b))
514Proof
515REPEAT STRIP_TAC THEN
516FULL_SIMP_TAC list_ss [PMATCH_EQUIV_ROWS_def, RIGHT_AND_OVER_OR,
517  EXISTS_OR_THM, PMATCH_APPEND_SEM]
518QED
519
520
521Theorem PMATCH_EQUIV_ROWS_CONS_NONE:
522  (row v = NONE) ==> (
523  PMATCH_EQUIV_ROWS v (row::rows) =
524  PMATCH_EQUIV_ROWS v rows)
525Proof
526
527SIMP_TAC list_ss [GSYM PMATCH_EQUIV_ROWS_EQUIV_EXPAND,
528  PMATCH_EQUIV_ROWS_def, RIGHT_AND_OVER_OR,
529  EXISTS_OR_THM, PMATCH_def]
530QED
531
532
533
534(***************************************************)
535(* Simple removal of redundant rows                *)
536(***************************************************)
537
538(* If we have a row that matches, everything after it can be dropped *)
539Theorem PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS_EQUIV:
540  !v rows n. ((n < LENGTH rows) /\ (IS_SOME ((EL n rows) v))) ==>
541  (PMATCH_EQUIV_ROWS v rows (TAKE (SUC n) rows))
542Proof
543
544REPEAT STRIP_TAC THEN
545`PMATCH_EQUIV_ROWS v (TAKE (SUC n) rows ++ DROP (SUC n) rows)
546                     (TAKE (SUC n) rows)`
547   suffices_by FULL_SIMP_TAC list_ss [] THEN
548
549SIMP_TAC std_ss [PMATCH_EQUIV_ROWS_def, PMATCH_APPEND_SEM] THEN
550SIMP_TAC list_ss [] THEN
551
552`?r. MEM r (TAKE (SUC n) rows) /\ IS_SOME (r v)` suffices_by METIS_TAC[] THEN
553Q.EXISTS_TAC `EL n (TAKE (SUC n) rows)` THEN
554ASM_SIMP_TAC list_ss [rich_listTheory.MEM_TAKE, rich_listTheory.EL_MEM,
555  listTheory.LENGTH_TAKE, rich_listTheory.EL_TAKE]
556QED
557
558
559Theorem PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS:
560  !v rows n. ((n < LENGTH rows) /\ (IS_SOME ((EL n rows) v))) ==>
561  (PMATCH v rows = PMATCH v (TAKE (SUC n) rows))
562Proof
563
564REPEAT STRIP_TAC THEN
565MATCH_MP_TAC PMATCH_EQUIV_ROWS_MATCH THEN
566MATCH_MP_TAC PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS_EQUIV THEN
567ASM_REWRITE_TAC[]
568QED
569
570
571
572(* A row is redundant, if (but not(!) only if) it is made
573   redundant by exactly one
574   row above. This is simple to test and often already very
575   helful. More fancy tests involving multiple rows follow below. *)
576Theorem PMATCH_ROWS_DROP_REDUNDANT:
577  !r1 r2 rows1 rows2 rows3 v.
578  (IS_SOME (r2 v) ==> IS_SOME (r1 v)) ==>
579  (PMATCH v (rows1 ++ (r1 :: rows2) ++ (r2 :: rows3)) =
580   PMATCH v (rows1 ++ (r1 :: rows2) ++ rows3))
581Proof
582
583REPEAT STRIP_TAC THEN
584SIMP_TAC (list_ss++boolSimps.CONJ_ss) [PMATCH_APPEND_SEM, RIGHT_AND_OVER_OR, EXISTS_OR_THM] THEN
585
586Cases_on `?r. MEM r rows1 /\ IS_SOME (r v)` THEN (
587  ASM_REWRITE_TAC []
588) THEN
589Cases_on `IS_SOME (r1 v)` THEN ASM_REWRITE_TAC[] THEN
590Cases_on `?r. MEM r rows2 /\ IS_SOME (r v)` THEN (
591  ASM_REWRITE_TAC []
592) THEN
593FULL_SIMP_TAC std_ss [PMATCH_def]
594QED
595
596
597Theorem PMATCH_ROWS_DROP_REDUNDANT_PMATCH_ROWS:
598  !p g r p' g' r' rows1 rows2 rows3 v.
599  (!x'. (v = p' x') /\ (g' x') ==> (?x. (p' x' = p x) /\ (g x))) ==>
600  (PMATCH v (rows1 ++ (PMATCH_ROW p g r :: rows2) ++ (PMATCH_ROW p' g' r' :: rows3)) =
601   PMATCH v (rows1 ++ (PMATCH_ROW p g r :: rows2) ++ rows3))
602Proof
603
604REPEAT STRIP_TAC THEN
605MATCH_MP_TAC PMATCH_ROWS_DROP_REDUNDANT THEN
606SIMP_TAC std_ss [PMATCH_ROW_def, optionTheory.some_def,
607  PMATCH_ROW_COND_def, IS_SOME_OPTION_MAP] THEN
608Cases_on `?x'. (p' x' = v) /\ g' x'` THEN (
609  ASM_SIMP_TAC std_ss []
610) THEN
611METIS_TAC[IS_SOME_DEF]
612QED
613
614
615
616(***************************************************)
617(* Simple removal of subsumed rows                 *)
618(***************************************************)
619
620(* Some rows are not redundant in the classical sense, but can
621   safely be dropped nevertheless. A redundant row never matches,
622   because it is shaddowed by a previous row. One can also
623   drop rows, if a later row matches if they match and returns the
624   same value. I will call such rows subsumed. *)
625
626Theorem PMATCH_ROWS_DROP_SUBSUMED:
627  !r1 r2 rows1 rows2 rows3 v.
628  ((!x. (r1 v = SOME x) ==> (r2 v = SOME x)) /\
629   (IS_SOME (r1 v) ==> EVERY (\row. (row v = NONE)) rows2)) ==>
630  (PMATCH v (rows1 ++ (r1 :: (rows2 ++ (r2 :: rows3)))) =
631   PMATCH v (rows1 ++ rows2 ++ (r2 :: rows3)))
632Proof
633
634REPEAT STRIP_TAC THEN
635REWRITE_TAC [GSYM rich_listTheory.APPEND_ASSOC_CONS] THEN
636SIMP_TAC (list_ss++boolSimps.CONJ_ss) [PMATCH_APPEND_SEM, RIGHT_AND_OVER_OR, EXISTS_OR_THM] THEN
637
638Cases_on `?r. MEM r rows1 /\ IS_SOME (r v)` THEN (
639  ASM_REWRITE_TAC []
640) THEN
641Cases_on `?r. MEM r rows2 /\ IS_SOME (r v)` THEN (
642  ASM_REWRITE_TAC []
643) THENL [
644  SIMP_TAC std_ss [PMATCH_def] THEN
645  Cases_on `r1 v` THEN (
646    FULL_SIMP_TAC std_ss [EVERY_MEM]
647  ) THEN
648  RES_TAC THEN
649  FULL_SIMP_TAC std_ss [],
650
651  Cases_on `r1 v` THEN (
652    ASM_SIMP_TAC std_ss []
653  ) THEN
654  FULL_SIMP_TAC std_ss [PMATCH_def]
655]
656QED
657
658Theorem PMATCH_ROWS_DROP_SUBSUMED_PMATCH_ROWS:
659  !p g r p' g' r' rows1 rows2 rows3 v.
660  ((!x. (v = p x) /\ (g x) ==> (?x'. (p x = p' x') /\ (g' x'))) /\
661   (!x x'. ((v = p x) /\ (p x = p' x') /\ g x /\ g' x') ==>
662           (r x = r' x')) /\
663   (!x. ((v = p x) /\ (g x)) ==> EVERY (\row. (row (p x) = NONE)) rows2)) ==>
664  (PMATCH v (rows1 ++ (PMATCH_ROW p g r :: (rows2 ++ (PMATCH_ROW p' g' r' :: rows3)))) =
665   PMATCH v (rows1 ++ rows2 ++ (PMATCH_ROW p' g' r' :: rows3)))
666Proof
667
668REPEAT STRIP_TAC THEN
669MATCH_MP_TAC PMATCH_ROWS_DROP_SUBSUMED THEN
670SIMP_TAC std_ss [PMATCH_ROW_def, optionTheory.some_def,
671  PMATCH_ROW_COND_def, IS_SOME_OPTION_MAP] THEN
672Cases_on `?x. (p x = v) /\ g x` THEN (
673  ASM_SIMP_TAC std_ss []
674) THEN
675REPEAT STRIP_TAC THENL [
676  PROVE_TAC[],
677
678  SELECT_ELIM_TAC THEN
679  CONJ_TAC THEN1 PROVE_TAC[] THEN
680  REPEAT STRIP_TAC THEN
681  SELECT_ELIM_TAC THEN
682  PROVE_TAC[],
683
684  FULL_SIMP_TAC std_ss [] THEN
685  METIS_TAC[]
686]
687QED
688
689
690(* A common case for removing subsumed rows
691   is removing ARB rows that are introduced by
692   translating a classical case-expression naively. *)
693Theorem PMATCH_REMOVE_ARB:
694  !p g r v rows.
695  (!x. r x = ARB) ==>
696  (PMATCH v (SNOC (PMATCH_ROW p g r) rows) =
697   PMATCH v rows)
698Proof
699
700Induct_on `rows` THENL [
701  SIMP_TAC list_ss [PMATCH_EVAL, PMATCH_INCOMPLETE_def],
702  ASM_SIMP_TAC list_ss [PMATCH_def]
703]
704QED
705
706(* Introduce explicit catch-all at end *)
707Theorem PMATCH_INTRO_CATCHALL:
708  PMATCH v rows = PMATCH v (SNOC (PMATCH_ROW (\_0. _0) (\_0. T) (\_0. ARB)) rows)
709Proof
710SIMP_TAC std_ss [PMATCH_REMOVE_ARB]
711QED
712
713
714Theorem PMATCH_REMOVE_ARB_NO_OVERLAP:
715  !v p g r rows1 rows2.
716  ((!x. (r x = ARB)) /\
717   (!x. ((v = p x) /\ (g x)) ==> EVERY (\row. (row (p x) = NONE)) rows2)) ==>
718  (PMATCH v (rows1 ++ ((PMATCH_ROW p g r) :: rows2)) =
719   PMATCH v (rows1 ++ rows2))
720Proof
721
722REPEAT STRIP_TAC THEN
723ONCE_REWRITE_TAC [PMATCH_INTRO_CATCHALL] THEN
724SIMP_TAC list_ss [SNOC_APPEND,
725  rich_listTheory.APPEND_ASSOC_CONS] THEN
726MATCH_MP_TAC PMATCH_ROWS_DROP_SUBSUMED_PMATCH_ROWS THEN
727ASM_SIMP_TAC std_ss []
728QED
729
730
731
732(***************************************************)
733(* Fancy redundancy check                          *)
734(***************************************************)
735
736(* Let's first define when a row is redundant.
737   The predicate PMATCH_ROW_REDUNDANT v rs i holds,
738   iff row number i is redundant for input v in the
739   list of rows rs. *)
740Definition PMATCH_ROW_REDUNDANT_def:
741  PMATCH_ROW_REDUNDANT v rs i = (
742  (i < LENGTH rs /\ (IS_SOME ((EL i rs) v) ==>
743    (?j. ((j < i) /\ IS_SOME ((EL j rs) v))))))
744End
745
746Theorem PMATCH_ROW_REDUNDANT_NIL:
747    PMATCH_ROW_REDUNDANT v [] i = F
748Proof
749SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_def]
750QED
751
752Theorem PMATCH_ROW_REDUNDANT_0:
753    PMATCH_ROW_REDUNDANT v (r::rs) 0 <=> (r v = NONE)
754Proof
755SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_def]
756QED
757
758Theorem PMATCH_ROW_REDUNDANT_SUC:
759  !v r rs i.
760     PMATCH_ROW_REDUNDANT v (r::rs) (SUC i) <=>
761     (r v <> NONE /\ i < LENGTH rs) \/ PMATCH_ROW_REDUNDANT v rs i
762Proof
763  SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [PMATCH_ROW_REDUNDANT_def] THEN
764  REPEAT STRIP_TAC THEN
765  EQ_TAC THENL [
766    STRIP_TAC THEN
767    Cases_on `j` THENL [
768      Cases_on `r v` THEN FULL_SIMP_TAC list_ss [],
769
770      Q.RENAME1_TAC `SUC j' < SUC i` THEN STRIP_TAC THEN
771      Q.EXISTS_TAC `j'` THEN
772      FULL_SIMP_TAC list_ss []
773    ],
774
775    REPEAT STRIP_TAC THEN Cases_on ‘r v’ >> FULL_SIMP_TAC list_ss [] >| [
776      Q.EXISTS_TAC `SUC j` THEN SRW_TAC[][],
777      Q.EXISTS_TAC ‘0’ >> SRW_TAC[][]
778    ]
779  ]
780QED
781
782
783Theorem PMATCH_ROW_REDUNDANT_APPEND_LT:
784    !v rs1 rs2 i.
785    i < LENGTH rs1 ==>
786    (PMATCH_ROW_REDUNDANT v (rs1 ++ rs2) i =
787     PMATCH_ROW_REDUNDANT v rs1 i)
788Proof
789SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_def] THEN
790REPEAT STRIP_TAC THEN
791FULL_SIMP_TAC (list_ss++boolSimps.CONJ_ss) [rich_listTheory.EL_APPEND1]
792QED
793
794Theorem PMATCH_ROW_REDUNDANT_APPEND_GE:
795    !v rs1 rs2 i.
796    ~(i < LENGTH rs1) ==>
797    (PMATCH_ROW_REDUNDANT v (rs1 ++ rs2) i <=> (
798     (~(EVERY (\r. r v = NONE) rs1) /\
799        (i < LENGTH rs1 + LENGTH rs2)) \/
800     PMATCH_ROW_REDUNDANT v rs2 (i - LENGTH rs1)))
801Proof
802
803SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_def, MEM_EL, EXISTS_MEM, GSYM LEFT_EXISTS_AND_THM] THEN
804REPEAT STRIP_TAC THEN
805FULL_SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [arithmeticTheory.NOT_LESS, rich_listTheory.EL_APPEND2,
806  quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE] THEN
807REPEAT STRIP_TAC THEN
808EQ_TAC THEN STRIP_TAC THENL [
809  Cases_on `j < LENGTH rs1` THENL [
810    FULL_SIMP_TAC list_ss [rich_listTheory.EL_APPEND1] THEN
811    METIS_TAC[],
812
813    FULL_SIMP_TAC list_ss [arithmeticTheory.NOT_LESS, rich_listTheory.EL_APPEND2] THEN
814    DISJ2_TAC THEN
815    Q.EXISTS_TAC `j - LENGTH rs1` THEN
816    FULL_SIMP_TAC arith_ss []
817  ],
818
819  Q.RENAME1_TAC `j' < LENGTH rs1` THEN
820  Q.EXISTS_TAC `j'` THEN
821  ASM_SIMP_TAC arith_ss [rich_listTheory.EL_APPEND1],
822
823
824  Q.EXISTS_TAC `j + LENGTH rs1` THEN
825  ASM_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2]
826]
827QED
828
829
830(* We can accumulate redundancy information for all rows.
831   This is done via IS_REDUNDANT_ROWS_INFO v rows c infos.
832   If the n-th entry of list infos is true, then the n-th
833   row of rows is redundant for input v. If it is not true,
834   it may or may not be redundant.
835
836   The parameter c is used for accumulating information
837   of all rows already in the info. If none of the rows
838   in rows matches, c holds. *)
839Definition IS_REDUNDANT_ROWS_INFO_def:
840  IS_REDUNDANT_ROWS_INFO v rows c infos <=> (
841  (LENGTH rows = LENGTH infos) /\
842  (!i. i < LENGTH rows ==> EL i infos ==>
843     PMATCH_ROW_REDUNDANT v rows i) /\
844  (EVERY (\r. r v = NONE) rows ==> c))
845End
846
847
848(* This setup allows to build up such an info
849   row by row. We start with a list of empty rows
850   and add new rows at the end using the information in c. *)
851Theorem IS_REDUNDANT_ROWS_INFO_NIL:
852  !v. IS_REDUNDANT_ROWS_INFO v [] T []
853Proof
854SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def]
855QED
856
857
858Theorem IS_REDUNDANT_ROWS_INFO_SNOC:
859  !v rows c infos r i c'.
860  IS_REDUNDANT_ROWS_INFO v rows c infos ==>
861  ((r v = NONE) ==> c ==> c') ==>
862  (c ==> i ==> (r v = NONE)) ==>
863  IS_REDUNDANT_ROWS_INFO v (SNOC r rows) c' (SNOC i infos)
864Proof
865
866REPEAT STRIP_TAC THEN
867FULL_SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def, SNOC_APPEND] THEN
868REPEAT STRIP_TAC THEN
869Cases_on `i' < LENGTH infos` THEN1 (
870  FULL_SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_APPEND_LT, rich_listTheory.EL_APPEND1]
871) THEN
872
873`i' = LENGTH infos` by DECIDE_TAC THEN
874Cases_on `c` THEN FULL_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2, PMATCH_ROW_REDUNDANT_APPEND_GE,
875  PMATCH_ROW_REDUNDANT_0]
876QED
877
878
879(* However, we still need to specialise this for
880   rows of the from PMATCH_ROW. For this case, it is handy
881   to use an auxiliary definition. *)
882Definition PMATCH_ROW_COND_EX_def:   PMATCH_ROW_COND_EX i p g =
883?x. PMATCH_ROW_COND p g i x
884End
885
886
887Theorem IS_REDUNDANT_ROWS_INFO_SNOC_PMATCH_ROW:
888  !v rows c infos p g r c'.
889  IS_REDUNDANT_ROWS_INFO v rows c infos ==>
890  (~(PMATCH_ROW_COND_EX v p g) ==> (c = c')) ==>
891  IS_REDUNDANT_ROWS_INFO v (SNOC (PMATCH_ROW p g r) rows) c' (SNOC (c ==> ~(PMATCH_ROW_COND_EX v p g)) infos)
892Proof
893
894REPEAT STRIP_TAC THEN
895MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] IS_REDUNDANT_ROWS_INFO_SNOC) THEN
896Q.EXISTS_TAC `c` THEN
897FULL_SIMP_TAC std_ss [PMATCH_ROW_EQ_NONE, PMATCH_ROW_COND_EX_def] THEN
898METIS_TAC[]
899QED
900
901(* A rewrite rule useful for proofs. *)
902Theorem IS_REDUNDANT_ROWS_INFO_CONS:
903
904  IS_REDUNDANT_ROWS_INFO v (row::rows) c (i::infos') = (
905  (LENGTH rows = LENGTH infos') /\
906  (i ==> ((row v) = NONE)) /\
907  ((row v = NONE) ==> IS_REDUNDANT_ROWS_INFO v rows c infos')
908)
909Proof
910
911EQ_TAC THEN SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def] THEN
912REPEAT STRIP_TAC THENL [
913  Q.PAT_X_ASSUM `!i'. _` (MP_TAC o SPEC ``0``) THEN
914  ASM_SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_0],
915
916  Q.PAT_X_ASSUM `!i'. _` (MP_TAC o Q.SPEC `SUC i'`) THEN
917  FULL_SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_SUC],
918
919  sg `(i'=0) \/ (?i''. (i' = SUC i''))` THENL [
920     Cases_on `i'` THEN SIMP_TAC std_ss [],
921    FULL_SIMP_TAC list_ss [],
922    ALL_TAC
923  ] THEN
924  FULL_SIMP_TAC list_ss [PMATCH_ROW_REDUNDANT_0, PMATCH_ROW_REDUNDANT_SUC] THEN
925  Tactical.REVERSE (Cases_on `row v`) THEN (
926    FULL_SIMP_TAC std_ss []
927  )
928]
929QED
930
931
932(* We can use such a REDUNDANT_ROWS_INFO to prune
933   the a pattern match *)
934
935Definition APPLY_REDUNDANT_ROWS_INFO_def:
936  (APPLY_REDUNDANT_ROWS_INFO is xs = MAP SND (
937    FILTER (\x. ~ (FST  x)) (ZIP (is, xs))))
938End
939
940Theorem APPLY_REDUNDANT_ROWS_INFO_THMS:
941  (APPLY_REDUNDANT_ROWS_INFO [] [] = []) /\
942  (!is x xs. (APPLY_REDUNDANT_ROWS_INFO (T::is) (x::xs) =
943     (APPLY_REDUNDANT_ROWS_INFO is xs))) /\
944  (!is x xs. (APPLY_REDUNDANT_ROWS_INFO (F::is) (x::xs) =
945     x::(APPLY_REDUNDANT_ROWS_INFO is xs)))
946Proof
947
948SIMP_TAC list_ss [APPLY_REDUNDANT_ROWS_INFO_def]
949QED
950
951
952Theorem PMATCH_ROWS_DROP_REDUNDANT_ROWS_INFO_EQUIV:
953  !v c rows infos. IS_REDUNDANT_ROWS_INFO v rows c infos ==>
954  (PMATCH_EQUIV_ROWS v rows (APPLY_REDUNDANT_ROWS_INFO infos rows))
955Proof
956
957GEN_TAC THEN
958Induct_on `rows` THEN1 (
959  SIMP_TAC (list_ss++QUANT_INST_ss [std_qp]) [
960    IS_REDUNDANT_ROWS_INFO_def,
961    APPLY_REDUNDANT_ROWS_INFO_def,
962    PMATCH_EQUIV_ROWS_is_equiv_1]
963) THEN
964CONV_TAC (RENAME_VARS_CONV ["row"]) THEN
965REPEAT STRIP_TAC THEN
966`?i infos'. infos = i::infos'` by (
967  Cases_on `infos` THEN
968  FULL_SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def]
969) THEN
970FULL_SIMP_TAC std_ss [IS_REDUNDANT_ROWS_INFO_CONS] THEN
971Q.PAT_X_ASSUM `!c infos. _` (MP_TAC o Q.SPECL [`c`, `infos'`]) THEN
972Cases_on `i` THENL [
973  FULL_SIMP_TAC std_ss [APPLY_REDUNDANT_ROWS_INFO_THMS,
974    PMATCH_EQUIV_ROWS_CONS_NONE],
975
976  Cases_on `row v` THEN (
977    FULL_SIMP_TAC std_ss [APPLY_REDUNDANT_ROWS_INFO_THMS,
978      PMATCH_EQUIV_ROWS_CONS_NONE, PMATCH_EQUIV_ROWS_EQUIV_EXPAND]
979  ) THEN
980  STRIP_TAC THEN
981  ASM_SIMP_TAC list_ss [PMATCH_EQUIV_ROWS_def,
982    GSYM PMATCH_EQUIV_ROWS_EQUIV_EXPAND, RIGHT_AND_OVER_OR,
983    EXISTS_OR_THM, PMATCH_def]
984]
985QED
986
987Theorem REDUNDANT_ROWS_INFO_TO_PMATCH_EQ:
988  !v c rows infos. IS_REDUNDANT_ROWS_INFO v rows c infos ==>
989  (PMATCH v rows =
990   PMATCH v (APPLY_REDUNDANT_ROWS_INFO infos rows))
991Proof
992
993REPEAT STRIP_TAC THEN
994MATCH_MP_TAC PMATCH_EQUIV_ROWS_MATCH THEN
995MATCH_MP_TAC PMATCH_ROWS_DROP_REDUNDANT_ROWS_INFO_EQUIV THEN
996PROVE_TAC[]
997QED
998
999
1000(* We get exhautiveness information for free using
1001   the accumulated information in c *)
1002Definition PMATCH_IS_EXHAUSTIVE_def:
1003   PMATCH_IS_EXHAUSTIVE v rs = (
1004   EXISTS (\r. IS_SOME (r v)) rs)
1005End
1006
1007
1008Theorem PMATCH_IS_EXHAUSTIVE_REWRITES:
1009   (!v. (PMATCH_IS_EXHAUSTIVE v [] = F)) /\
1010
1011   (!v r rs. (PMATCH_IS_EXHAUSTIVE v (r::rs) =
1012     ~(r v = NONE) \/ PMATCH_IS_EXHAUSTIVE v rs))
1013Proof
1014
1015SIMP_TAC list_ss [PMATCH_IS_EXHAUSTIVE_def,
1016quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE]
1017QED
1018
1019
1020Theorem IS_REDUNDANT_ROWS_INFO_EXTRACT_IS_EXHAUSTIVE:
1021    !v rows c infos.
1022    IS_REDUNDANT_ROWS_INFO v rows c infos ==>
1023    ~c ==> PMATCH_IS_EXHAUSTIVE v rows
1024Proof
1025
1026SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def,
1027  PMATCH_IS_EXHAUSTIVE_def, combinTheory.o_DEF,
1028  quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE
1029]
1030QED
1031
1032
1033(* One can easily mark rows as not redundant without proof.
1034   This is handy for avoiding complicated procedures to check,
1035   whether some element of infos is true or false. If in doub
1036   replace it with false. Technically this is done by
1037   building a pairwise conjunction with a given list.  *)
1038Definition REDUNDANT_ROWS_INFOS_CONJ_def:
1039  REDUNDANT_ROWS_INFOS_CONJ ip1 ip2 =
1040     (MAP2 (\i1 i2. i1 /\ i2) ip1 ip2)
1041End
1042
1043Theorem REDUNDANT_ROWS_INFOS_CONJ_REWRITE:
1044  (REDUNDANT_ROWS_INFOS_CONJ [] [] = []) /\
1045  (REDUNDANT_ROWS_INFOS_CONJ (i1 :: is1) (i2::is2) =
1046  (i1 /\ i2) :: (REDUNDANT_ROWS_INFOS_CONJ is1 is2))
1047Proof
1048SIMP_TAC list_ss [REDUNDANT_ROWS_INFOS_CONJ_def]
1049QED
1050
1051(* So, we can weaken an existing REDUNDANT_ROWS_INFOS *)
1052Theorem REDUNDANT_ROWS_INFOS_CONJ_THM:
1053  !v rows c infos c' infos'.
1054    IS_REDUNDANT_ROWS_INFO v rows c infos ==>
1055    (LENGTH infos' = LENGTH infos) ==>
1056    IS_REDUNDANT_ROWS_INFO v rows (c \/ c') (REDUNDANT_ROWS_INFOS_CONJ infos infos')
1057Proof
1058
1059SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def,
1060  REDUNDANT_ROWS_INFOS_CONJ_def, MAP2_MAP, EL_MAP, EL_ZIP]
1061QED
1062
1063
1064(* Strengthening requires proof though *)
1065Definition REDUNDANT_ROWS_INFOS_DISJ_def:
1066  REDUNDANT_ROWS_INFOS_DISJ ip1 ip2 =
1067     (MAP2 (\i1 i2. i1 \/ i2) ip1 ip2)
1068End
1069
1070Theorem REDUNDANT_ROWS_INFOS_DISJ_THM:
1071  !v rows c infos c' infos'.
1072    IS_REDUNDANT_ROWS_INFO v rows c infos ==>
1073    IS_REDUNDANT_ROWS_INFO v rows c' infos' ==>
1074    IS_REDUNDANT_ROWS_INFO v rows (c /\ c') (REDUNDANT_ROWS_INFOS_DISJ infos infos')
1075Proof
1076
1077SIMP_TAC list_ss [IS_REDUNDANT_ROWS_INFO_def,
1078  REDUNDANT_ROWS_INFOS_DISJ_def, MAP2_MAP, EL_MAP, EL_ZIP] THEN
1079METIS_TAC[]
1080QED
1081
1082
1083(* One can use the always correct, but usually much too complicated
1084   strongest redundant_rows_info for strengthening *)
1085
1086Definition STRONGEST_REDUNDANT_ROWS_INFO_AUX_def:
1087  (STRONGEST_REDUNDANT_ROWS_INFO_AUX v [] p infos = (p, infos)) /\
1088  (STRONGEST_REDUNDANT_ROWS_INFO_AUX v (r::rows) p infos =
1089   STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows (p /\ (r v = NONE))
1090   (SNOC (p ==> (r v = NONE)) infos))
1091End
1092
1093Definition STRONGEST_REDUNDANT_ROWS_INFO_def:
1094  STRONGEST_REDUNDANT_ROWS_INFO v rows =
1095  SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows T [])
1096End
1097
1098Theorem LENGTH_STRONGEST_REDUNDANT_ROWS_INFO_AUX:
1099    !v rows p infos.
1100      LENGTH (SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos)) =
1101      (LENGTH rows + LENGTH infos)
1102Proof
1103
1104Induct_on `rows` THEN (
1105  ASM_SIMP_TAC list_ss [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def]
1106)
1107QED
1108
1109Theorem FST_STRONGEST_REDUNDANT_ROWS_INFO_AUX:
1110    !v rows p infos.
1111      FST (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos) =
1112      (p /\ EVERY (\r. r v = NONE) rows)
1113Proof
1114
1115Induct_on `rows` THEN (
1116  ASM_SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def]
1117)
1118QED
1119
1120
1121
1122Theorem EL1_STRONGEST_REDUNDANT_ROWS_INFO_AUX:
1123    !v rows p infos i.
1124      (i < LENGTH infos) ==>
1125      (EL i (SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos)) =
1126       EL i infos)
1127Proof
1128
1129Induct_on `rows` THEN (
1130  ASM_SIMP_TAC (list_ss++boolSimps.EQUIV_EXTRACT_ss) [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def, SNOC_APPEND, rich_listTheory.EL_APPEND1]
1131)
1132QED
1133
1134
1135Theorem EL2_STRONGEST_REDUNDANT_ROWS_INFO_AUX:
1136    !v rows p infos i.
1137      (i >= LENGTH infos /\ i < LENGTH rows + LENGTH infos) ==>
1138      (EL i (SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos)) =
1139       ((p /\ EVERY (\r. r v = NONE) (TAKE (i - LENGTH infos) rows)) ==> ((EL (i - LENGTH infos) rows) v = NONE)))
1140Proof
1141
1142GEN_TAC THEN
1143Induct_on `rows` THEN1 (
1144  SIMP_TAC list_ss []
1145) THEN
1146SIMP_TAC list_ss [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def] THEN
1147REPEAT STRIP_TAC THEN
1148Cases_on `i = LENGTH infos` THEN1 (
1149  ASM_SIMP_TAC list_ss [SNOC_APPEND, EL1_STRONGEST_REDUNDANT_ROWS_INFO_AUX, rich_listTheory.EL_APPEND2]
1150) THEN
1151Q.PAT_X_ASSUM `!p infos. _` (MP_TAC o Q.SPECL [
1152  `p /\ (h (v:'a) = NONE)`, `SNOC (p ==> (h (v:'a) = NONE)) infos`, `i`]) THEN
1153ASM_SIMP_TAC list_ss [SNOC_APPEND, GSYM arithmeticTheory.ADD1] THEN
1154REPEAT STRIP_TAC THEN
1155ASM_SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [] THEN
1156REPEAT STRIP_TAC THEN
1157`(i - LENGTH infos) = SUC (i - SUC (LENGTH infos))` by DECIDE_TAC THEN
1158ASM_SIMP_TAC list_ss []
1159QED
1160
1161
1162Theorem LENGTH_STRONGEST_REDUNDANT_ROWS_INFO:
1163    LENGTH (STRONGEST_REDUNDANT_ROWS_INFO v rows) = LENGTH rows
1164Proof
1165
1166SIMP_TAC list_ss [STRONGEST_REDUNDANT_ROWS_INFO_def,
1167  LENGTH_STRONGEST_REDUNDANT_ROWS_INFO_AUX]
1168QED
1169
1170Theorem EL_STRONGEST_REDUNDANT_ROWS_INFO:
1171    !v rows i.
1172      (i < LENGTH rows) ==>
1173      (EL i (STRONGEST_REDUNDANT_ROWS_INFO v rows) =
1174       ((EVERY (\r. r v = NONE) (TAKE i rows)) ==>
1175        ((EL i rows) v = NONE)))
1176Proof
1177
1178SIMP_TAC list_ss [STRONGEST_REDUNDANT_ROWS_INFO_def,
1179  EL2_STRONGEST_REDUNDANT_ROWS_INFO_AUX]
1180QED
1181
1182
1183Theorem STRONGEST_REDUNDANT_ROWS_INFO_OK:
1184
1185    IS_REDUNDANT_ROWS_INFO v rows (EVERY (\r. r v = NONE) rows)
1186      (STRONGEST_REDUNDANT_ROWS_INFO v rows)
1187Proof
1188
1189SIMP_TAC std_ss [IS_REDUNDANT_ROWS_INFO_def,
1190  EL_STRONGEST_REDUNDANT_ROWS_INFO,
1191  LENGTH_STRONGEST_REDUNDANT_ROWS_INFO,
1192  PMATCH_ROW_REDUNDANT_def] THEN
1193REPEAT STRIP_TAC THEN
1194Cases_on `EL i rows v` THEN1 (
1195  FULL_SIMP_TAC list_ss []
1196) THEN
1197FULL_SIMP_TAC list_ss [EXISTS_MEM] THEN
1198`?j. j < i /\ (EL j rows = e)` suffices_by (
1199  STRIP_TAC THEN Q.EXISTS_TAC `j` THEN
1200  ASM_SIMP_TAC std_ss [] THEN
1201  Cases_on `e v` THEN FULL_SIMP_TAC std_ss []
1202) THEN
1203Q.PAT_X_ASSUM `MEM e _` MP_TAC THEN
1204ASM_SIMP_TAC (list_ss++boolSimps.CONJ_ss) [MEM_EL,rich_listTheory.EL_TAKE] THEN
1205PROVE_TAC[]
1206QED
1207
1208
1209(* IN order to automate this procedure, we need a few
1210   simple, additional lemmata  *)
1211
1212Theorem PMATCH_ROW_COND_EX_FULL_DEF:
1213   PMATCH_ROW_COND_EX i p g =
1214   ?x. (i = p x) /\ g x
1215Proof
1216SIMP_TAC std_ss [PMATCH_ROW_COND_EX_def, PMATCH_ROW_COND_def] THEN
1217METIS_TAC[]
1218QED
1219
1220Theorem PMATCH_ROW_COND_EX_WEAKEN:
1221  !f v p g p' g'.
1222
1223  ~(PMATCH_ROW_COND_EX v p g) ==>
1224  (!x. p' x = p (f x)) ==>
1225  (PMATCH_ROW_COND_EX v p' g' =
1226   PMATCH_ROW_COND_EX v p' (\x. g' x /\ ~(g (f x))))
1227Proof
1228
1229SIMP_TAC std_ss [PMATCH_ROW_COND_EX_def, PMATCH_ROW_COND_def] THEN
1230REPEAT STRIP_TAC THEN
1231CONSEQ_CONV_TAC (K EXISTS_EQ___CONSEQ_CONV) THEN
1232SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [] THEN
1233METIS_TAC[]
1234QED
1235
1236Theorem PMATCH_ROW_COND_EX_FALSE:
1237  !v p g.
1238  (!x. ~(g x)) ==>
1239  (PMATCH_ROW_COND_EX v p g = F)
1240Proof
1241
1242SIMP_TAC std_ss [PMATCH_ROW_COND_EX_def, PMATCH_ROW_COND_def]
1243QED
1244
1245Theorem PMATCH_ROW_COND_EX_IMP_REWRITE:
1246  !v p g p' g' RES.
1247  PMATCH_ROW_COND_EX v p g ==>
1248  (!x. g x ==> ((?x'. (p' x' = p x) /\ g' x') = RES)) ==>
1249  (PMATCH_ROW_COND_EX v p' g' = RES)
1250Proof
1251
1252SIMP_TAC std_ss [PMATCH_ROW_COND_EX_def, PMATCH_ROW_COND_def,
1253  GSYM LEFT_FORALL_IMP_THM]
1254QED
1255
1256(* Use this simple contradiction to bring
1257   PMATCH_IS_EXHAUSTIVE in the form we need for
1258   automation *)
1259Theorem PMATCH_IS_EXHAUSTIVE_CONTRADICT:
1260  !v rs.
1261  (EVERY (\r. r v = NONE) rs ==> F) ==>
1262  (PMATCH_IS_EXHAUSTIVE v rs)
1263Proof
1264
1265REPEAT STRIP_TAC THEN
1266FULL_SIMP_TAC list_ss [PMATCH_IS_EXHAUSTIVE_def,
1267  combinTheory.o_DEF, quantHeuristicsTheory.IS_SOME_EQ_NOT_NONE]
1268QED
1269
1270
1271Theorem PMATCH_ROW_EVAL_COND_EX:
1272    PMATCH_ROW_COND_EX i p g ==>
1273    ((PMATCH_ROW p g r i) = SOME (r (@x. PMATCH_ROW_COND p g i x)))
1274Proof
1275
1276SIMP_TAC std_ss [PMATCH_ROW_def, some_def, PMATCH_ROW_COND_EX_def]
1277QED
1278
1279Theorem PMATCH_ROW_NEQ_NONE:
1280    (PMATCH_ROW p g r i <> NONE) <=>
1281    (PMATCH_ROW_COND_EX i p g)
1282Proof
1283
1284SIMP_TAC std_ss [PMATCH_ROW_def, some_eq_NONE,
1285  PMATCH_ROW_COND_EX_def]
1286QED
1287
1288
1289(***************************************************)
1290(* ELIMINATE DOUBLE VAR-BINDS                      *)
1291(***************************************************)
1292
1293(* If a variable is used multiple times in a pattern,
1294   we can via the following theorem introduce a fresh variable
1295   and add the connection between the old and the newly created
1296   var to the guard. *)
1297Theorem PMATCH_ROW_REMOVE_DOUBLE_BINDS_THM:
1298  !g p1 g1 r1 p2 g2 r2.
1299   ((!x y. (p1 x = p1 y) ==> (x = y)) /\
1300   (!x. (p2 (g x) = p1 x)) /\
1301   (!x'. g2 x' = (?x. (x' = g x) /\ g1 x)) /\
1302   (!x. r2 (g x) = r1 x)) ==>
1303
1304  (PMATCH_ROW p1 g1 r1 = PMATCH_ROW p2 g2 r2)
1305Proof
1306
1307SIMP_TAC (std_ss++boolSimps.CONJ_ss) [PMATCH_ROW_def, FUN_EQ_THM,
1308  optionTheory.some_def, PMATCH_ROW_COND_def,
1309  GSYM RIGHT_EXISTS_AND_THM] THEN
1310REPEAT STRIP_TAC THEN
1311Cases_on `?x'. (p1 x' = x) /\ g1 x'` THEN (
1312  ASM_REWRITE_TAC[optionTheory.OPTION_MAP_DEF]
1313) THEN
1314SELECT_ELIM_TAC THEN ASM_REWRITE_TAC[] THEN
1315SELECT_ELIM_TAC THEN
1316REPEAT STRIP_TAC THEN (
1317  METIS_TAC[]
1318)
1319QED
1320
1321
1322
1323(***************************************************)
1324(* ELIMINATE GUARDS                                *)
1325(***************************************************)
1326
1327(* We can eliminate guards by replacing them with true
1328   and add the guard in form of a conditional.
1329   Notice that all the rows after the guard are
1330   duplicated. We heavily rely on simplification
1331   of PMATCH to avoid a huge blowup of term-size,
1332   when applying the following rule. *)
1333Theorem GUARDS_ELIM_THM:
1334  !v rs1 rs2 p g r.
1335  (!x1 x2. (p x1 = p x2) ==> (x1 = x2)) ==> (
1336  PMATCH v (rs1++(PMATCH_ROW p g r)::rs2) =
1337  PMATCH v (rs1++(PMATCH_ROW p (\x. T) (\x.
1338   if g x then r x else
1339   PMATCH (p x) rs2))::rs2))
1340Proof
1341
1342REPEAT STRIP_TAC THEN
1343SIMP_TAC std_ss [PMATCH_APPEND_SEM] THEN
1344Cases_on `?r. MEM r rs1 /\ IS_SOME (r v)` THEN (
1345  ASM_REWRITE_TAC[]
1346) THEN
1347SIMP_TAC std_ss [PMATCH_EVAL, PMATCH_ROW_COND_def] THEN
1348Tactical.REVERSE (Cases_on `?x. p x = v`) THEN (
1349  FULL_SIMP_TAC std_ss []
1350) THEN
1351`!x'. (p x' = v) <=> (x' = x)` by METIS_TAC[] THEN
1352ASM_SIMP_TAC (std_ss++boolSimps.CONJ_ss) []
1353QED
1354
1355
1356
1357(***************************************************)
1358(* THEOREMS ABOUT FLATTENING                       *)
1359(***************************************************)
1360
1361(* The content of this section is still experimental.
1362   It is likely to chnage quite a bit still. *)
1363Definition PMATCH_FLATTEN_FUN_def:
1364  PMATCH_FLATTEN_FUN p g row v = (
1365    option_CASE (some x. PMATCH_ROW_COND p g v x)
1366      NONE (\x. row x x))
1367End
1368
1369
1370Theorem PMATCH_FLATTEN_THM_AUX[local]:
1371   (PMATCH v [PMATCH_ROW p g (\x. (PMATCH x (MAP (\r. r x) rows')))]) =
1372   (PMATCH v (MAP (\r. (PMATCH_FLATTEN_FUN p g r)) rows'))
1373Proof
1374
1375REPEAT GEN_TAC THEN
1376Induct_on `rows'` THEN1 (
1377  Cases_on `some x. PMATCH_ROW_COND p g v x` THEN
1378  ASM_SIMP_TAC list_ss [PMATCH_def, PMATCH_ROW_def]
1379) THEN
1380
1381Q.PAT_X_ASSUM `_ = _` (ASSUME_TAC o GSYM) THEN
1382FULL_SIMP_TAC list_ss [PMATCH_def, PMATCH_ROW_def] THEN
1383Q.PAT_X_ASSUM `_ = _` (K ALL_TAC) THEN
1384
1385Cases_on `some x. PMATCH_ROW_COND p g v x` THEN (
1386  ASM_SIMP_TAC std_ss [PMATCH_FLATTEN_FUN_def]
1387)
1388QED
1389
1390
1391Theorem PMATCH_FLATTEN_THM_SINGLE:
1392   !v p g rows.
1393 (!x. PMATCH_IS_EXHAUSTIVE x (MAP (\r. r x) rows)) ==>
1394PMATCH_EQUIV_ROWS v [PMATCH_ROW p g (\x. (PMATCH x (MAP (\r. r x) rows)))] (MAP (\r. (PMATCH_FLATTEN_FUN p g r)) rows)
1395Proof
1396
1397REPEAT STRIP_TAC THEN
1398SIMP_TAC list_ss [PMATCH_EQUIV_ROWS_def, PMATCH_FLATTEN_THM_AUX] THEN
1399SIMP_TAC list_ss [PMATCH_ROW_def, IS_SOME_OPTION_MAP, some_IS_SOME,
1400  listTheory.MEM_MAP, GSYM LEFT_EXISTS_AND_THM] THEN
1401
1402SIMP_TAC std_ss [PMATCH_FLATTEN_FUN_def, some_def] THEN
1403Cases_on `?x. PMATCH_ROW_COND p g v x` THEN (
1404  ASM_SIMP_TAC std_ss [PMATCH_ROW_COND_def]
1405) THEN
1406FULL_SIMP_TAC std_ss [PMATCH_IS_EXHAUSTIVE_def,
1407  listTheory.EXISTS_MEM, listTheory.MEM_MAP,
1408  GSYM LEFT_EXISTS_AND_THM]
1409QED
1410
1411
1412Theorem PMATCH_FLATTEN_THM:
1413   !v p g rows1 rows2 rows.
1414 (!x. PMATCH_IS_EXHAUSTIVE x (MAP (\r. r x) rows)) ==>
1415(PMATCH v (rows1 ++ (PMATCH_ROW p g (\x. (PMATCH x (MAP (\r. r x) rows))))::rows2) =
1416 PMATCH v (rows1 ++ (MAP (\r. (PMATCH_FLATTEN_FUN p g r)) rows) ++ rows2))
1417Proof
1418
1419REPEAT STRIP_TAC THEN
1420MATCH_MP_TAC PMATCH_EQUIV_ROWS_MATCH THEN
1421REWRITE_TAC[GSYM APPEND_ASSOC] THEN
1422MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] PMATCH_EQUIV_APPEND) THEN
1423REWRITE_TAC[PMATCH_EQUIV_ROWS_is_equiv_1] THEN
1424ONCE_REWRITE_TAC [prove (``x::xs = [x] ++ xs``, SIMP_TAC list_ss [])] THEN
1425MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] PMATCH_EQUIV_APPEND) THEN
1426REWRITE_TAC[PMATCH_EQUIV_ROWS_is_equiv_1] THEN
1427MATCH_MP_TAC PMATCH_FLATTEN_THM_SINGLE THEN
1428ASM_REWRITE_TAC[]
1429QED
1430
1431
1432Theorem PMATCH_FLATTEN_FUN_PMATCH_ROW:
1433  !p.
1434  (!x1 x2. (p x1 = p x2) ==> (x1 = x2)) ==> (
1435
1436  !g p' g' r'.
1437  PMATCH_FLATTEN_FUN p g (\x. PMATCH_ROW p' (g' x) (r' x)) =
1438  PMATCH_ROW (\x. (p (p' x))) (\x. (g (p' x)) /\ (g' (p' x) x)) (\x. r' (p' x) x))
1439Proof
1440
1441REPEAT STRIP_TAC THEN
1442SIMP_TAC std_ss [PMATCH_FLATTEN_FUN_def, FUN_EQ_THM, PMATCH_ROW_def] THEN
1443CONV_TAC (RENAME_VARS_CONV ["v"]) THEN GEN_TAC THEN
1444Cases_on ` some x. PMATCH_ROW_COND p g v x` THEN1 (
1445  FULL_SIMP_TAC list_ss [some_eq_NONE, PMATCH_ROW_COND_def] THEN
1446  PROVE_TAC[]
1447) THEN
1448
1449ASM_SIMP_TAC std_ss [] THEN
1450FULL_SIMP_TAC std_ss [PMATCH_ROW_COND_def] THEN
1451Q.PAT_X_ASSUM `_ = SOME x` (fn thm =>
1452  ASSUME_TAC (HO_MATCH_MP some_eq_SOME thm)) THEN
1453`!x'. (p x' = v) = (x' = x)` by PROVE_TAC[] THEN
1454ASM_SIMP_TAC (std_ss++boolSimps.CONJ_ss) [] THEN
1455Cases_on `(some x'. (p' x' = x) /\ g' x x')` THEN (
1456  ASM_SIMP_TAC std_ss []
1457) THEN
1458Q.PAT_X_ASSUM `_ = SOME x'` (fn thm =>
1459  ASSUME_TAC (HO_MATCH_MP some_eq_SOME thm)) THEN
1460ASM_SIMP_TAC std_ss []
1461QED
1462
1463
1464
1465
1466
1467(***************************************************)
1468(* UNROLLING PREDICATES                            *)
1469(***************************************************)
1470
1471Definition PMATCH_ROW_COND_NOT_EX_OR_EQ_def:   PMATCH_ROW_COND_NOT_EX_OR_EQ (i:'a) (r : 'a -> 'b option) rows =
1472(~(r i <> NONE) \/ ((EXISTS (\row. row i <> NONE) rows) /\
1473     (THE (r i) = PMATCH i rows)))
1474End
1475
1476Theorem PMATCH_ROW_COND_NOT_EX_OR_EQ_FIRST_ROW:
1477    !i r r' rows.
1478
1479    (r' i <> NONE) ==>
1480    ((PMATCH_ROW_COND_NOT_EX_OR_EQ i r (r'::rows)) =
1481    ((r i <> NONE) ==>
1482      (r i = r' i)))
1483Proof
1484
1485SIMP_TAC list_ss [PMATCH_ROW_COND_NOT_EX_OR_EQ_def, PMATCH_def] THEN
1486REPEAT GEN_TAC THEN
1487Cases_on `r' i` THEN Cases_on `r i` THEN (
1488  SIMP_TAC std_ss []
1489)
1490QED
1491
1492
1493Theorem PMATCH_ROW_COND_NOT_EX_OR_EQ_NIL:
1494    PMATCH_ROW_COND_NOT_EX_OR_EQ i r [] =
1495    ((r i <> NONE) ==> F)
1496Proof
1497
1498SIMP_TAC list_ss [PMATCH_ROW_COND_NOT_EX_OR_EQ_def]
1499QED
1500
1501
1502Theorem PMATCH_ROW_COND_NOT_EX_OR_EQ_NOT_FIRST_ROW:
1503    PMATCH_ROW_COND_NOT_EX_OR_EQ i r' rows ==>
1504    (PMATCH_ROW_COND_NOT_EX_OR_EQ i r (r'::rows) =
1505    (PMATCH_ROW_COND_NOT_EX_OR_EQ i r rows))
1506Proof
1507
1508SIMP_TAC list_ss [PMATCH_ROW_COND_NOT_EX_OR_EQ_def, PMATCH_def] THEN
1509Cases_on `r i` THEN ASM_SIMP_TAC std_ss [] THEN
1510Cases_on `r' i` THEN ASM_SIMP_TAC std_ss []
1511QED
1512
1513Theorem PMATCH_PRED_UNROLL_NIL:
1514    !P v. P (PMATCH v []) = P ARB
1515Proof
1516  SIMP_TAC std_ss [PMATCH_def, PMATCH_INCOMPLETE_def]
1517QED
1518
1519
1520Theorem PMATCH_PRED_UNROLL_CONS:
1521  !P v r rows.
1522     P (PMATCH v (r::rows)) <=> (
1523       ((r v <> NONE) ==> P (THE (r v))) /\
1524       ((PMATCH_ROW_COND_NOT_EX_OR_EQ v r rows) ==>
1525         P (PMATCH v rows)))
1526Proof
1527
1528REPEAT STRIP_TAC THEN
1529SIMP_TAC std_ss [PMATCH_def, PMATCH_ROW_def, some_def,
1530  PMATCH_ROW_COND_NOT_EX_OR_EQ_def,
1531  PMATCH_ROW_COND_EX_def] THEN
1532Cases_on `r v` THEN ASM_SIMP_TAC std_ss [] THEN
1533METIS_TAC[]
1534QED
1535
1536
1537Definition PMATCH_EXPAND_PRED_def:   (PMATCH_EXPAND_PRED P v rows_before [] = (~(PMATCH_IS_EXHAUSTIVE v (REVERSE rows_before)) ==> P ARB)) /\
1538
1539  (PMATCH_EXPAND_PRED P v rows_before (r::rows_after) = (
1540  ((r v <> NONE) ==> (EVERY (\r'. (r' v <> NONE) ==> (r' v = r v)) rows_before)
1541  ==> P (THE (r v))) /\ PMATCH_EXPAND_PRED P v (r::rows_before) rows_after))
1542End
1543
1544
1545Theorem PMATCH_EXPAND_PRED_THM_GEN:
1546  !P v rows_before rows_after.
1547         PMATCH_EXPAND_PRED P v rows_before rows_after <=> (
1548         EVERY (\r. PMATCH_ROW_COND_NOT_EX_OR_EQ v r rows_after ) rows_before ==>
1549         P (PMATCH v rows_after))
1550Proof
1551
1552Induct_on `rows_after` THEN1 (
1553  SIMP_TAC list_ss [PMATCH_EXPAND_PRED_def, PMATCH_IS_EXHAUSTIVE_def, PMATCH_def, PMATCH_INCOMPLETE_def, PMATCH_ROW_COND_NOT_EX_OR_EQ_NIL, combinTheory.o_DEF, rich_listTheory.EVERY_REVERSE]
1554) THEN
1555
1556ASM_SIMP_TAC list_ss [PMATCH_EXPAND_PRED_def, PMATCH_IS_EXHAUSTIVE_def, PMATCH_PRED_UNROLL_CONS] THEN
1557POP_ASSUM (K ALL_TAC) THEN
1558REPEAT GEN_TAC THEN
1559Q.RENAME1_TAC `P (THE (r v))` THEN
1560Cases_on `r v` THENL [
1561  ASM_SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [EVERY_MEM] THEN
1562  REPEAT STRIP_TAC THEN
1563  METIS_TAC[PMATCH_ROW_COND_NOT_EX_OR_EQ_NOT_FIRST_ROW],
1564
1565
1566  Q.RENAME1_TAC `r v = SOME x` THEN
1567  ASM_SIMP_TAC std_ss [PMATCH_ROW_COND_NOT_EX_OR_EQ_FIRST_ROW] THEN
1568
1569  Cases_on `PMATCH_ROW_COND_NOT_EX_OR_EQ v r rows_after` THEN (
1570    ASM_SIMP_TAC std_ss []
1571  ) THEN
1572  Cases_on `EVERY (\r'. r' v <> NONE ==> (r' v = SOME x)) rows_before` THENL [
1573    FULL_SIMP_TAC (std_ss++boolSimps.EQUIV_EXTRACT_ss) [EVERY_MEM, PMATCH_ROW_COND_NOT_EX_OR_EQ_def] THEN
1574    METIS_TAC[],
1575
1576
1577    ASM_SIMP_TAC std_ss [] THEN
1578    FULL_SIMP_TAC std_ss [EVERY_MEM, PMATCH_ROW_COND_NOT_EX_OR_EQ_def] THEN1 (FULL_SIMP_TAC std_ss []) THEN
1579
1580    STRIP_TAC THEN
1581    POP_ASSUM (MP_TAC o Q.SPEC `r'`) THEN
1582    Q.PAT_X_ASSUM `THE (r v) = _` (ASSUME_TAC o GSYM) THEN
1583    ASM_SIMP_TAC std_ss [] THEN
1584    Cases_on `r' v` THEN FULL_SIMP_TAC std_ss []
1585  ]
1586]
1587QED
1588
1589
1590Theorem PMATCH_EXPAND_PRED_THM:
1591  !P v rows.
1592         P (PMATCH v rows) <=>
1593         PMATCH_EXPAND_PRED P v [] rows
1594Proof
1595
1596SIMP_TAC list_ss [PMATCH_EXPAND_PRED_THM_GEN]
1597QED
1598
1599
1600Definition PMATCH_ROW_LIFT_def:   PMATCH_ROW_LIFT f r = \x. OPTION_MAP f (r x)
1601End
1602
1603Theorem PMATCH_LIFT_THM:
1604  !f v rows.
1605    PMATCH_IS_EXHAUSTIVE v rows ==>
1606    (f (PMATCH v rows) =
1607     PMATCH v (MAP (PMATCH_ROW_LIFT f) rows))
1608Proof
1609
1610GEN_TAC THEN GEN_TAC THEN
1611Induct_on `rows` THEN (
1612  FULL_SIMP_TAC list_ss [PMATCH_def, PMATCH_IS_EXHAUSTIVE_def]
1613) THEN
1614CONV_TAC (RENAME_VARS_CONV ["r"]) THEN
1615GEN_TAC THEN
1616Cases_on `r v` THEN (
1617  ASM_SIMP_TAC std_ss [PMATCH_ROW_LIFT_def]
1618)
1619QED
1620
1621
1622Theorem PMATCH_ROW_LIFT_THM:
1623    !f p g r.
1624    PMATCH_ROW_LIFT f (PMATCH_ROW p g r) =
1625    PMATCH_ROW p g (\x. f (r x))
1626Proof
1627
1628REPEAT STRIP_TAC THEN
1629SIMP_TAC std_ss [PMATCH_ROW_LIFT_def, PMATCH_ROW_def, FUN_EQ_THM] THEN
1630Cases_on `some v. PMATCH_ROW_COND p g x v` THEN (
1631  ASM_SIMP_TAC std_ss []
1632)
1633QED
1634
1635
1636Theorem PMATCH_IS_EXHAUSTIVE_LIFT:
1637    !f v rows.
1638    PMATCH_IS_EXHAUSTIVE v rows ==>
1639    PMATCH_IS_EXHAUSTIVE v (MAP (PMATCH_ROW_LIFT f) rows)
1640Proof
1641
1642SIMP_TAC list_ss [PMATCH_IS_EXHAUSTIVE_def, EXISTS_MAP, PMATCH_ROW_LIFT_def,
1643  IS_SOME_MAP]
1644QED