1(* ========================================================================= *) 2(* FILE : updateScript.sml *) 3(* DESCRIPTION : Function update with lists *) 4(* DATE : 2011 *) 5(* ========================================================================= *) 6 7open HolKernel Parse boolLib bossLib; 8open rich_listTheory sortingTheory; 9 10val _ = new_theory "update"; 11 12(* ------------------------------------------------------------------------ 13 Definitions 14 ------------------------------------------------------------------------ *) 15 16val FIND_def = Define` 17 (FIND P [] = NONE) /\ 18 (FIND P (h::t) = if P h then SOME h else FIND P t)`; 19 20val OVERRIDE_def = tDefine "OVERRIDE" 21 `(OVERRIDE [] = []) /\ 22 (OVERRIDE (x::t) = x :: OVERRIDE (FILTER (\y. FST x <> FST y) t))` 23 (WF_REL_TAC `measure LENGTH` 24 THEN SRW_TAC [] [rich_listTheory.LENGTH_FILTER_LEQ, 25 DECIDE ``!a b. a <= b ==> a < SUC b``]); 26 27val LIST_UPDATE_def = Define` 28 (LIST_UPDATE [] = I) /\ 29 (LIST_UPDATE (h::t) = (FST h =+ SND h) o LIST_UPDATE t)`; 30 31(* ------------------------------------------------------------------------ 32 Theorems 33 ------------------------------------------------------------------------ *) 34 35val LIST_UPDATE_LOOKUP = Q.store_thm("LIST_UPDATE_LOOKUP", 36 `!l f i. 37 LIST_UPDATE l f i = 38 case FIND (\x. FST x = i) l 39 of SOME (_,e) => e 40 | NONE => f i`, 41 Induct 42 THEN SRW_TAC [] [LIST_UPDATE_def, FIND_def, combinTheory.UPDATE_def] 43 THEN Cases_on `h` 44 THEN SRW_TAC [] []); 45 46val FILTER_OVERRIDE_lem = Q.prove( 47 `(((\y. x <> y) o FST) = (\y. x <> FST y)) /\ 48 (((\y. x <> y /\ P y) o FST) = (\y. x <> FST y /\ P (FST y)))`, 49 SRW_TAC [] [FUN_EQ_THM] 50 THEN METIS_TAC []); 51 52val FILTER_OVERRIDE = Q.prove( 53 `!P l. 54 OVERRIDE (FILTER (P o FST) l) = 55 FILTER (P o FST) (OVERRIDE l)`, 56 Induct_on `l` THEN SRW_TAC [] [OVERRIDE_def] 57 THEN Q.PAT_ASSUM `!P. x` 58 (fn thm => 59 Q.SPEC_THEN `\y. FST h <> y` ASSUME_TAC thm 60 THEN Q.SPEC_THEN `\y. FST h <> y /\ P y` ASSUME_TAC thm) 61 THEN FULL_SIMP_TAC (srw_ss()) 62 [FILTER_OVERRIDE_lem, rich_listTheory.FILTER_FILTER] 63 THEN SRW_TAC [] [FILTER_EQ] 64 THEN METIS_TAC []); 65 66val FIND_FILTER = Q.prove( 67 `!l i j. 68 i <> j ==> 69 (FIND (\x. FST x = i) (FILTER (\y. j <> FST y) l) = 70 FIND (\x. FST x = i) l)`, 71 Induct_on `l` THEN SRW_TAC [] [FIND_def]); 72 73val FIND_OVERRIDE = Q.prove( 74 `!l i j. 75 i <> j ==> 76 (FIND (\x. FST x = i) (OVERRIDE (FILTER (\y. j <> FST y) l)) = 77 FIND (\x. FST x = i) (OVERRIDE l))`, 78 Induct 79 THEN SRW_TAC [] [OVERRIDE_def, FIND_def] 80 THEN Q.SPEC_THEN `\y. FST h <> y` 81 (ASSUME_TAC o REWRITE_RULE [FILTER_OVERRIDE_lem]) 82 FILTER_OVERRIDE 83 THEN ASM_SIMP_TAC std_ss [FIND_FILTER]); 84 85val LIST_UPDATE_OVERRIDE = Q.store_thm("LIST_UPDATE_OVERRIDE", 86 `!l. LIST_UPDATE l = LIST_UPDATE (OVERRIDE l)`, 87 REWRITE_TAC [FUN_EQ_THM] 88 THEN Induct_on `l` 89 THEN SRW_TAC [] [OVERRIDE_def, LIST_UPDATE_def, combinTheory.UPDATE_def] 90 THEN SRW_TAC [] [LIST_UPDATE_LOOKUP, FIND_OVERRIDE]); 91 92(* ------------------------------------------------------------------------ *) 93 94val FIND_APPEND_lem = Q.prove( 95 `!h l1 l2. 96 ~MEM (FST h) (MAP FST l1) ==> 97 (FIND (\x. FST x = FST h) (l1 ++ l2) = FIND (\x. FST x = FST h) l2)`, 98 Induct_on `l1` THEN SRW_TAC [] [FIND_def]); 99 100val FIND_APPEND_lem2 = Q.prove( 101 `!y l1 l2. 102 FST h <> y ==> 103 (FIND (\x. FST x = y) (l1 ++ h::l2) = 104 FIND (\x. FST x = y) (l1 ++ l2))`, 105 Induct_on `l1` THEN SRW_TAC [] [FIND_def]); 106 107val FIND_ALL_DISTINCT = Q.prove( 108 `!l1 l2 y. 109 ALL_DISTINCT (MAP FST l1) /\ PERM l1 l2 ==> 110 (FIND (\x. FST x = y) l1 = FIND (\x. FST x = y) l2)`, 111 Induct 112 THEN SRW_TAC [] [FIND_def] 113 THENL [ 114 FULL_SIMP_TAC std_ss [sortingTheory.PERM_CONS_EQ_APPEND] 115 THEN Q.ISPEC_THEN `FST` IMP_RES_TAC sortingTheory.PERM_MAP 116 THEN `!x. MEM x (MAP FST l1) = MEM x (MAP FST (M ++ N))` 117 by IMP_RES_TAC sortingTheory.PERM_MEM_EQ 118 THEN `~MEM (FST h) (MAP FST M)` 119 by METIS_TAC [listTheory.MEM_APPEND, listTheory.MAP_APPEND] 120 THEN SRW_TAC [] [FIND_APPEND_lem, FIND_def], 121 FULL_SIMP_TAC std_ss [sortingTheory.PERM_CONS_EQ_APPEND] 122 THEN SRW_TAC [] [FIND_APPEND_lem2] 123 ]); 124 125val LIST_UPDATE_ALL_DISTINCT = Q.store_thm("LIST_UPDATE_ALL_DISTINCT", 126 `!l1 l2. 127 ALL_DISTINCT (MAP FST l2) /\ PERM l1 l2 ==> 128 (LIST_UPDATE l1 = LIST_UPDATE l2)`, 129 SRW_TAC [] [FUN_EQ_THM, LIST_UPDATE_LOOKUP] 130 THEN METIS_TAC [FIND_ALL_DISTINCT, sortingTheory.PERM_SYM]); 131 132val ALL_DISTINCT_OVERRIDE = Q.prove( 133 `!l. ALL_DISTINCT (MAP FST (OVERRIDE l))`, 134 Induct 135 THEN SRW_TAC [] [OVERRIDE_def, listTheory.MEM_FILTER, 136 listTheory.FILTER_ALL_DISTINCT, 137 FILTER_OVERRIDE |> Q.SPEC `\y. FST h <> y` 138 |> REWRITE_RULE [FILTER_OVERRIDE_lem], 139 FILTER_MAP |> Q.ISPECL [`\y. FST h <> y`,`FST`] 140 |> REWRITE_RULE [FILTER_OVERRIDE_lem] |> GSYM]); 141 142val ALL_DISTINCT_QSORT = Q.prove( 143 `!l R. ALL_DISTINCT (MAP FST l) ==> ALL_DISTINCT (MAP FST (QSORT R l))`, 144 METIS_TAC [sortingTheory.QSORT_PERM, sortingTheory.PERM_MAP, 145 sortingTheory.ALL_DISTINCT_PERM]); 146 147val LIST_UPDATE_SORT_OVERRIDE = Q.store_thm("LIST_UPDATE_SORT_OVERRIDE", 148 `!R l. LIST_UPDATE l = LIST_UPDATE (QSORT R (OVERRIDE l))`, 149 METIS_TAC [LIST_UPDATE_OVERRIDE, LIST_UPDATE_ALL_DISTINCT, 150 sortingTheory.QSORT_PERM, ALL_DISTINCT_OVERRIDE, ALL_DISTINCT_QSORT]); 151 152(* ------------------------------------------------------------------------ *) 153 154val LIST_UPDATE1 = Q.prove( 155 `(!l1 l2 r1 r2. 156 (l1 =+ r1) o (l2 =+ r2) = LIST_UPDATE [(l1,r1); (l2,r2)]) /\ 157 (!l r t. (l =+ r) o LIST_UPDATE t = LIST_UPDATE ((l,r)::t)) /\ 158 (!l1 l2 r1 r2 f. 159 (l1 =+ r1) ((l2 =+ r2) f) = LIST_UPDATE [(l1,r1); (l2,r2)] f) /\ 160 (!l r t f. (l =+ r) (LIST_UPDATE t f) = LIST_UPDATE ((l,r)::t) f)`, 161 SRW_TAC [] [LIST_UPDATE_def]); 162 163val LIST_UPDATE2 = Q.prove( 164 `(!l1 l2. LIST_UPDATE l1 o LIST_UPDATE l2 = LIST_UPDATE (l1 ++ l2)) /\ 165 (!l1 l2 r. LIST_UPDATE l1 o (l2 =+ r) = LIST_UPDATE (SNOC (l2,r) l1)) /\ 166 (!l1 l2 f. 167 LIST_UPDATE l1 (LIST_UPDATE l2 f) = LIST_UPDATE (l1 ++ l2) f) /\ 168 (!l1 l2 r f. LIST_UPDATE l1 ((l2 =+ r) f) = LIST_UPDATE (SNOC (l2,r) l1) f)`, 169 REPEAT CONJ_TAC 170 THEN Induct THEN SRW_TAC [] [LIST_UPDATE_def]); 171 172val LIST_UPDATE_THMS = Theory.save_thm("LIST_UPDATE_THMS", 173 CONJ LIST_UPDATE1 LIST_UPDATE2); 174 175(* ------------------------------------------------------------------------ 176 Duplicate theorems about update from combinTheory 177 ------------------------------------------------------------------------ *) 178 179val _ = List.map Theory.save_thm 180 (let open combinTheory in 181 [("APPLY_UPDATE_ID", APPLY_UPDATE_ID), 182 ("APPLY_UPDATE_THM", APPLY_UPDATE_THM), 183 ("SAME_KEY_UPDATE_DIFFER", SAME_KEY_UPDATE_DIFFER), 184 ("UPDATE_APPLY_ID", UPDATE_APPLY_ID), 185 ("UPDATE_APPLY_IMP_ID", UPDATE_APPLY_IMP_ID), 186 ("UPDATE_COMMUTES", UPDATE_COMMUTES), 187 ("UPDATE_EQ", UPDATE_EQ), 188 ("UPDATE_def", UPDATE_def)] 189 end) 190 191(* ------------------------------------------------------------------------ *) 192 193val _ = export_theory(); 194