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