1open HolKernel boolLib bossLib BasicProvers;
2open pred_setTheory arithmeticTheory listTheory rich_listTheory optionTheory
3     pairTheory relationTheory sortingTheory;
4open alistTheory;
5
6val _ = new_theory "vec_map";
7
8val _ = temp_tight_equality ();
9
10val every_case_tac = BasicProvers.EVERY_CASE_TAC;
11
12Definition alist_to_vec_def :
13  (alist_to_vec l default 0 max = []) /\
14  (alist_to_vec [] default (SUC n) max = default :: alist_to_vec [] default n max) /\
15  (alist_to_vec ((x,y)::t) default (SUC n) max =
16    if SUC n <= max then
17       if x = max - SUC n then
18          y :: alist_to_vec t default n max
19       else if x < max - SUC n then
20         alist_to_vec t default (SUC n) max
21       else
22         default :: alist_to_vec ((x,y)::t) default n max
23    else
24      [])
25End
26
27val alist_to_vec_ind = fetch "-" "alist_to_vec_ind";
28
29Theorem alist_to_vec_correct[local] :
30 !l default cur max v.
31  SORTED $<= (MAP FST l) /\
32  cur <= max /\
33  alist_to_vec l default cur max = v
34  ==>
35  LENGTH v = cur /\
36  (!n x. n < cur /\ ALOOKUP l (max - cur + n) = SOME x ==> EL n v = x) /\
37  (!n. n < cur /\ ALOOKUP l (max - cur + n) = NONE ==>  EL n v = default)
38Proof
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[])
66QED
67
68Theorem 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)
76Proof
77 rw [] >>
78 imp_res_tac alist_to_vec_correct >>
79 fs []
80QED
81
82Theorem dense_alist_to_vec_correct[local] :
83 !y l n.
84  MAP FST l = MAP (\x. x + y) (COUNT_LIST (LENGTH l)) /\
85  n < LENGTH l
86  ==>
87  ALOOKUP l (n + y) = SOME (EL n (MAP SND l))
88Proof
89 Induct_on `n` >>
90 rw [] >>
91 Cases_on `l` >>
92 fs [COUNT_LIST_def] >>
93 PairCases_on `h` >>
94 fs [MAP_MAP_o, combinTheory.o_DEF] >>
95 rw [] >>
96 full_simp_tac (srw_ss()++ARITH_ss) [] >>
97 rw [] >>
98 FIRST_X_ASSUM (mp_tac o Q.SPECL [`SUC h0`,`t`]) >>
99 rw [] >>
100 `!h0 x. h0 + SUC x = x + SUC h0` by decide_tac >>
101 full_simp_tac bool_ss []
102QED
103
104Theorem dense_alist_to_vec_thm :
105 !l n. MAP FST l = COUNT_LIST (LENGTH l) /\ n < LENGTH l
106        ==>
107       ALOOKUP l n = SOME (EL n (MAP SND l))
108Proof
109 metis_tac [SIMP_RULE (srw_ss()) [] (Q.SPEC `0` dense_alist_to_vec_correct)]
110QED
111
112val _ = export_theory ();
113