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