1(* ========================================================================= *)
2(* FILE          : updateScript.sml                                          *)
3(* DESCRIPTION   : Function update using lists                               *)
4(*                                                                           *)
5(* AUTHOR        : (c) Anthony Fox, University of Cambridge                  *)
6(* DATE          : 2005-2007                                                 *)
7(* ========================================================================= *)
8
9(* interactive use:
10  app load ["wordsLib", "rich_listTheory", "my_listTheory"];
11*)
12
13open HolKernel boolLib bossLib;
14open Parse Q combinTheory arithmeticTheory wordsTheory;
15open listTheory rich_listTheory my_listTheory;
16
17val _ = new_theory "update";
18
19(* ------------------------------------------------------------------------- *)
20
21infix \\ << >>
22
23val op \\ = op THEN;
24val op << = op THENL;
25val op >> = op THEN1;
26
27val _ = set_fixity "|:"  (Infix(NONASSOC, 320));
28
29val _ = set_fixity "=+>" (Infix(NONASSOC, 320));
30val _ = set_fixity "=+<" (Infix(NONASSOC, 320));
31
32val _ = set_fixity ":+>" (Infix(NONASSOC, 320));
33val _ = set_fixity ":+<" (Infix(NONASSOC, 320));
34
35val _ = set_fixity "|:>" (Infix(NONASSOC, 320));
36val _ = set_fixity "|:<" (Infix(NONASSOC, 320));
37
38val _ = computeLib.auto_import_definitions := false;
39
40val LUPDATE_def = xDefine "LUPDATE"
41  `$|: a l = \m b.
42      if a <=+ b /\ w2n b - w2n a < LENGTH l then
43        EL (w2n b - w2n a) l
44      else m b`;
45
46val Ua_def = xDefine "Ua" `$=+> = $=+`;
47val Ub_def = xDefine "Ub" `$=+< = $=+`;
48
49val LUa_def = xDefine "LUa" `$|:> = $|:`;
50val LUb_def = xDefine "LUb" `$|:< = $|:`;
51
52val FUa_def = xDefine "FUa" `$:+> = $:+`;
53val FUb_def = xDefine "FUb" `$:+< = $:+`;
54
55val JOIN_def = Define`
56  JOIN n x y =
57    let lx = LENGTH x and ly = LENGTH y in
58    let j = MIN n lx in
59       GENLIST
60         (\i. if i < n then
61                if i < lx then EL i x else EL (i - j) y
62              else
63                if i - j < ly then EL (i - j) y else EL i x)
64         (MAX (j + ly) lx)`;
65
66val _ = computeLib.auto_import_definitions := true;
67
68(* ------------------------------------------------------------------------- *)
69
70val JOIN_lem = prove(`!a b. MAX (SUC a) (SUC b) = SUC (MAX a b)`,
71   RW_TAC std_ss [MAX_DEF]);
72
73val JOIN_TAC =
74  CONJ_TAC >> RW_TAC list_ss [LENGTH_GENLIST,MAX_DEF,MIN_DEF]
75    \\ Cases
76    \\ RW_TAC list_ss [MAX_DEF,MIN_DEF,LENGTH_GENLIST,EL_GENLIST,
77         ADD_CLAUSES,HD_GENLIST]
78    \\ FULL_SIMP_TAC arith_ss [NOT_LESS]
79    \\ RW_TAC arith_ss [GENLIST,TL_SNOC,EL_SNOC,NULL_LENGTH,EL_GENLIST,
80         LENGTH_TL,LENGTH_GENLIST,LENGTH_SNOC,(GSYM o CONJUNCT2) EL]
81    \\ SIMP_TAC list_ss [];
82
83val JOIN = store_thm("JOIN",
84  `(!n ys. JOIN n [] ys = ys) /\
85   (!xs. JOIN 0 xs [] = xs) /\
86   (!x xs y ys. JOIN 0 (x::xs) (y::ys) = y :: JOIN 0 xs ys) /\
87   (!n xs y ys. JOIN (SUC n) (x::xs) ys = x :: (JOIN n xs ys))`,
88  RW_TAC (list_ss++boolSimps.LET_ss) [JOIN_def,JOIN_lem]
89    \\ MATCH_MP_TAC LIST_EQ
90    << [
91      Cases_on `n` >> RW_TAC arith_ss [LENGTH_GENLIST,EL_GENLIST] \\ JOIN_TAC
92        \\ `?p. LENGTH ys = SUC p` by METIS_TAC [ADD1,LESS_ADD_1,ADD_CLAUSES]
93        \\ ASM_SIMP_TAC list_ss [HD_GENLIST],
94      RW_TAC arith_ss [LENGTH_GENLIST,EL_GENLIST],
95      JOIN_TAC, JOIN_TAC]);
96
97(* ------------------------------------------------------------------------- *)
98
99val APPLY_LUPDATE_THM = store_thm("APPLY_LUPDATE_THM",
100  `!a b l m. (a |: l) m b =
101      let na = w2n a and nb = w2n b in
102      let d = nb - na in
103        if na <= nb /\ d < LENGTH l then EL d l else m b`,
104  NTAC 2 Cases
105    \\ RW_TAC (std_ss++boolSimps.LET_ss) [WORD_LS,LUPDATE_def]
106    \\ FULL_SIMP_TAC arith_ss []);
107
108val UPDATE_LUPDATE = store_thm("UPDATE_LUPDATE",
109   `!a b m. (a =+ b) m = (a |: [b]) m`,
110  RW_TAC (std_ss++boolSimps.LET_ss) [FUN_EQ_THM,LUPDATE_def,UPDATE_def]
111    \\ Cases_on `a = x`
112    \\ ASM_SIMP_TAC list_ss [WORD_LOWER_EQ_REFL]
113    \\ ASM_SIMP_TAC arith_ss [WORD_LOWER_OR_EQ,WORD_LO]);
114
115val LUPDATE_LUPDATE = store_thm("LUPDATE_LUPDATE",
116  `!a b x y m. (a |: y) ((b |: x) m) =
117     let lx = LENGTH x and ly = LENGTH y in
118        if a <=+ b then
119          if w2n b - w2n a <= ly then
120            if ly - (w2n b - w2n a) < lx then
121              (a |: (y ++ BUTFIRSTN (ly - (w2n b - w2n a)) x)) m
122            else
123              (a |: y) m
124          else
125            (a |: y) ((b |: x) m)
126        else (* b <+ a *)
127          if w2n a - w2n b < lx then
128            (b |: JOIN (w2n a - w2n b) x y) m
129          else
130            (b |: x) ((a |: y) m)`,
131  REPEAT STRIP_TAC \\ SIMP_TAC (bool_ss++boolSimps.LET_ss) []
132    \\ Cases_on `a <=+ b`
133    \\ FULL_SIMP_TAC std_ss [WORD_NOT_LOWER_EQUAL,WORD_LS,WORD_LO]
134    << [
135      Cases_on `w2n b <= w2n a + LENGTH y` \\ ASM_SIMP_TAC std_ss []
136        \\ `w2n b - w2n a <= LENGTH y` by DECIDE_TAC
137        \\ ntac 2 (rw[LUPDATE_def,WORD_LS,FUN_EQ_THM,EL_DROP,EL_APPEND1,EL_APPEND2,DROP])
138        \\ fs[] \\ rw[] \\ fs[],
139      REWRITE_TAC [FUN_EQ_THM] \\ RW_TAC arith_ss []
140        << [
141          RW_TAC (arith_ss++boolSimps.LET_ss) [WORD_LS,LUPDATE_def,JOIN_def,
142                 EL_GENLIST,LENGTH_GENLIST,MIN_DEF,MAX_DEF]
143            \\ FULL_SIMP_TAC arith_ss [],
144          FULL_SIMP_TAC arith_ss [NOT_LESS]
145            \\ IMP_RES_TAC LENGTH_NIL
146            \\ RW_TAC (arith_ss++boolSimps.LET_ss) [WORD_LS,LUPDATE_def]
147            \\ FULL_SIMP_TAC arith_ss []]]);
148
149(* ------------------------------------------------------------------------- *)
150
151val UPDATE_SORT_RULE1 = store_thm("UPDATE_SORT_RULE1",
152  `!R m a b d e. (!x y. R x y ==> ~(x = y)) ==>
153     ((a =+> e) ((b =+> d) m) =
154         if R a b then
155           (b =+< d) ((a =+> e) m)
156         else
157           (a =+< e) ((b =+> d) m))`,
158  METIS_TAC [Ua_def,Ub_def,UPDATE_COMMUTES]);
159
160val UPDATE_SORT_RULE2 = store_thm("UPDATE_SORT_RULE2",
161  `!R m a b d e. (!x y. R x y ==> ~(x = y)) ==>
162     ((a =+> e) ((b =+< d) m) =
163         if R a b then
164           (b =+< d) ((a =+> e) m)
165         else
166           (a =+< e) ((b =+< d) m))`,
167  METIS_TAC [Ua_def,Ub_def,UPDATE_COMMUTES]);
168
169val UPDATE_EQ_RULE = store_thm("UPDATE_EQ_RULE",
170  `((a =+< e) ((a =+> d) m) = (a =+> e) m) /\
171   ((a =+< e) ((a =+< d) m) = (a =+< e) m) /\
172   ((a =+> e) ((a =+> d) m) = (a =+> e) m)`,
173  REWRITE_TAC [Ua_def,Ub_def,UPDATE_EQ]);
174
175val FCP_UPDATE_SORT_RULE1 = store_thm("FCP_UPDATE_SORT_RULE1",
176  `!R m a b d e. (!x y. R x y ==> ~(x = y)) ==>
177     ((a :+> e) ((b :+> d) m) =
178         if R a b then
179           (b :+< d) ((a :+> e) m)
180         else
181           (a :+< e) ((b :+> d) m))`,
182  METIS_TAC [FUa_def,FUb_def,fcpTheory.FCP_UPDATE_COMMUTES]);
183
184val FCP_UPDATE_SORT_RULE2 = store_thm("FCP_UPDATE_SORT_RULE2",
185  `!R m a b d e. (!x y. R x y ==> ~(x = y)) ==>
186     ((a :+> e) ((b :+< d) m) =
187         if R a b then
188           (b :+< d) ((a :+> e) m)
189         else
190           (a :+< e) ((b :+< d) m))`,
191  METIS_TAC [FUa_def,FUb_def,fcpTheory.FCP_UPDATE_COMMUTES]);
192
193val FCP_UPDATE_EQ_RULE = store_thm("FCP_UPDATE_EQ_RULE",
194  `((a :+< e) ((a :+> d) m) = (a :+> e) m) /\
195   ((a :+< e) ((a :+< d) m) = (a :+< e) m) /\
196   ((a :+> e) ((a :+> d) m) = (a :+> e) m)`,
197  REWRITE_TAC [FUa_def,FUb_def,fcpTheory.FCP_UPDATE_EQ]);
198
199val LIST_UPDATE_SORT_RULE1 = save_thm("LIST_UPDATE_SORT_RULE1",
200  METIS_PROVE [LUa_def,LUb_def,LUPDATE_LUPDATE]
201    ``!a b x y m. (a |:> y) ((b |:> x) m) =
202        let lx = LENGTH x and ly = LENGTH y in
203           if a <=+ b then
204             if w2n b - w2n a <= ly then
205               if ly - (w2n b - w2n a) < lx then
206                 (a |:> y ++ BUTFIRSTN (ly - (w2n b - w2n a)) x) m
207               else
208                 (a |:> y) m
209             else
210               (a |:< y) ((b |:> x) m)
211           else (* b <+ a *)
212             if w2n a - w2n b < lx then
213               (b |:> JOIN (w2n a - w2n b) x y) m
214             else
215               (b |:> x) ((a |:> y) m)``);
216
217val LIST_UPDATE_SORT_RULE2 = save_thm("LIST_UPDATE_SORT_RULE2",
218  METIS_PROVE [LUa_def,LUb_def,LUPDATE_LUPDATE]
219    ``!a b x y m. (a |:> y) ((b |:< x) m) =
220        let lx = LENGTH x and ly = LENGTH y in
221           if a <=+ b then
222             if w2n b - w2n a <= ly then
223               if ly - (w2n b - w2n a) < lx then
224                 (a |:> y ++ BUTFIRSTN (ly - (w2n b - w2n a)) x) m
225               else
226                 (a |:> y) m
227             else
228               (a |:< y) ((b |:< x) m)
229           else (* b <+ a *)
230             if w2n a - w2n b < lx then
231               (b |:> JOIN (w2n a - w2n b) x y) m
232             else
233               (b |:> x) ((a |:> y) m)``);
234
235(* ------------------------------------------------------------------------- *)
236
237val _ = export_theory();
238