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