1open HolKernel boolLib bossLib BasicProvers;
2open pred_setTheory arithmeticTheory listTheory rich_listTheory optionTheory
3     pairTheory relationTheory sortingTheory;
4open alistTheory;
5open lcsymtacs;
6
7val _ = new_theory "vec_map";
8
9val _ = temp_tight_equality ();
10
11val every_case_tac = BasicProvers.EVERY_CASE_TAC;
12
13val alist_to_vec_def =
14 Define
15  `(alist_to_vec l default 0 max = []) ���
16   (alist_to_vec [] default (SUC n) max = default :: alist_to_vec [] default n max) ���
17   (alist_to_vec ((x,y)::t) default (SUC n) max =
18    if SUC n ��� max then
19       if x = max - SUC n then
20          y :: alist_to_vec t default n max
21       else if x < max - SUC n then
22         alist_to_vec t default (SUC n) max
23       else
24         default :: alist_to_vec ((x,y)::t) default n max
25    else
26      [])`;
27
28val alist_to_vec_ind = fetch "-" "alist_to_vec_ind";
29
30val alist_to_vec_correct = Q.prove (
31`!l default cur max v.
32  SORTED $<= (MAP FST l) ���
33  cur ��� max ���
34  alist_to_vec l default cur max = v
35  ���
36  LENGTH v = cur ���
37  (!n x. n < cur ��� ALOOKUP l (max - cur + n) = SOME x ��� EL n v = x) ���
38  (!n. n < cur ��� ALOOKUP l (max - cur + n) = NONE ���  EL n v = default)`,
39 ho_match_mp_tac alist_to_vec_ind
40 >> rw [alist_to_vec_def]
41 >> `transitive $<=` by srw_tac [ARITH_ss] [transitive_def]
42 >> rw []
43 >> full_simp_tac (srw_ss()++ARITH_ss) [SORTED_EQ]
44 >> Cases_on `n` >> rw [EL_CONS] >> fs []
45    >- (FIRST_X_ASSUM match_mp_tac >> rw []
46        >> `max ��� SUC cur <> max + SUC n' ��� SUC cur` by decide_tac
47        >> `max + SUC n' - SUC cur = max + n' ��� cur` by decide_tac
48        >> metis_tac[])
49    >- (FIRST_X_ASSUM match_mp_tac >> rw []
50        >> `max ��� SUC cur <> max + SUC n' ��� SUC cur` by decide_tac
51        >> `max + SUC n' - SUC cur = max + n' ��� cur` by decide_tac
52        >> metis_tac[])
53    >- (ntac 2 (pop_assum mp_tac) >> rw []
54        >> imp_res_tac ALOOKUP_MEM
55        >> `MEM (max ��� SUC cur) (MAP FST l)` by (rw[MEM_MAP] >> metis_tac[FST])
56        >> res_tac
57        >> full_simp_tac (srw_ss()++ARITH_ss) [])
58    >- (FIRST_X_ASSUM match_mp_tac >> rw []
59        >> full_simp_tac (srw_ss()++ARITH_ss) []
60        >> `max + SUC n' ��� SUC cur  = max + n' ��� cur` by decide_tac
61        >> metis_tac[])
62    >- (FIRST_X_ASSUM match_mp_tac >> rw []
63        >> full_simp_tac (srw_ss()++ARITH_ss) []
64        >> `max + SUC n' ��� SUC cur = max + n' ��� cur` by decide_tac
65        >> metis_tac[])
66);
67
68val alist_to_vec_thm = Q.store_thm ("alist_to_vec_thm",
69`!l default max v.
70  SORTED $<= (MAP FST l) ���
71  alist_to_vec l default max max = v
72  ���
73  LENGTH v = max ���
74  (!n x. n < max ��� ALOOKUP l n = SOME x ��� EL n v = x) ���
75  (!n. n < max ��� ALOOKUP l n = NONE ���  EL n v = default)`,
76 rw [] >>
77 imp_res_tac alist_to_vec_correct >>
78 fs []);
79
80val dense_alist_to_vec_correct = Q.prove (
81`!y l n.
82  MAP FST l = MAP (\x. x + y) (COUNT_LIST (LENGTH l)) ���
83  n < LENGTH l
84  ���
85  ALOOKUP l (n + y) = SOME (EL n (MAP SND l))`,
86 Induct_on `n` >>
87 rw [] >>
88 Cases_on `l` >>
89 fs [COUNT_LIST_def] >>
90 PairCases_on `h` >>
91 fs [MAP_MAP_o, combinTheory.o_DEF] >>
92 rw [] >>
93 full_simp_tac (srw_ss()++ARITH_ss) [] >>
94 rw [] >>
95 FIRST_X_ASSUM (mp_tac o Q.SPECL [`SUC h0`,`t`]) >>
96 rw [] >>
97 `!h0 x. h0 + SUC x = x + SUC h0` by decide_tac >>
98 full_simp_tac bool_ss []);
99
100val dense_alist_to_vec_thm = Q.store_thm
101("dense_alist_to_vec_thm",
102 `!l n. MAP FST l = COUNT_LIST (LENGTH l) ��� n < LENGTH l
103        ���
104       ALOOKUP l n = SOME (EL n (MAP SND l))`,
105 metis_tac [SIMP_RULE (srw_ss()) [] (Q.SPEC `0` dense_alist_to_vec_correct)]);
106
107val _ = export_theory ();
108