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