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