1198090Srdivacky 2198090Srdivackyopen HolKernel boolLib bossLib Parse; 3198090Srdivackyopen pred_setTheory wordsTheory wordsLib arithmeticTheory; 4198090Srdivackyopen set_sepTheory progTheory lpc_devicesTheory; 5198090Srdivackyopen listTheory pairTheory combinTheory addressTheory; 6198090Srdivacky 7198090Srdivackyval _ = new_theory "lpc_prog"; 8198090Srdivacky 9198090Srdivacky 10198090Srdivackyinfix \\ 11198090Srdivackyval op \\ = op THEN; 12198090Srdivacky 13198090Srdivackyval RW = REWRITE_RULE; 14198090Srdivackyval RW1 = ONCE_REWRITE_RULE; 15198090Srdivacky 16198090Srdivacky 17198090Srdivacky(* ----------------------------------------------------------------------------- *) 18198090Srdivacky(* The LPC set *) 19198090Srdivacky(* ----------------------------------------------------------------------------- *) 20198090Srdivacky 21198090Srdivackyval _ = Hol_datatype ` 22198090Srdivacky lpc_el = tReg of word4 => word32 23198090Srdivacky | tStatus of arm_bit => bool 24198090Srdivacky | tRom of word32 => word8 option 25198090Srdivacky | tRam of word32 => word8 option 26198090Srdivacky | tTime of num 27198090Srdivacky | tUart0 of (word8 list # num # word8 list # num) 28198090Srdivacky | tUndef of bool`; 29198090Srdivacky 30198090Srdivackyval lpc_el_11 = DB.fetch "-" "lpc_el_11"; 31198090Srdivackyval lpc_el_distinct = DB.fetch "-" "lpc_el_distinct"; 32198090Srdivacky 33198090Srdivackyval _ = Parse.type_abbrev("lpc_set",``:lpc_el set``); 34198090Srdivacky 35198090Srdivacky 36198090Srdivacky(* ----------------------------------------------------------------------------- *) 37198090Srdivacky(* State reader functions *) 38198090Srdivacky(* ----------------------------------------------------------------------------- *) 39198090Srdivacky 40198090Srdivackyval ty = (type_of o snd o dest_comb) ``LPC_NEXT s1 s2`` 41198090Srdivackyval _ = Parse.type_abbrev("lpc_state",ty); 42198090Srdivacky 43198090Srdivackyval LPC_READ_REG_def = Define ` 44198090Srdivacky LPC_READ_REG a ((s,p):lpc_state) = ARM_READ_REG a s`; 45198090Srdivacky 46198090Srdivackyval LPC_READ_STATUS_def = Define ` 47198090Srdivacky LPC_READ_STATUS a ((s,p):lpc_state) = ARM_READ_STATUS a s`; 48198090Srdivacky 49198090Srdivackyval LPC_READ_TIME_def = Define ` 50198090Srdivacky LPC_READ_TIME ((s,(time,rom,ram,p)):lpc_state) = time`; 51198090Srdivacky 52198090Srdivackyval LPC_READ_ROM_def = Define ` 53198090Srdivacky LPC_READ_ROM a ((s,(time,rom,ram,p)):lpc_state) = rom a`; 54198090Srdivacky 55198090Srdivackyval LPC_READ_RAM_def = Define ` 56198090Srdivacky LPC_READ_RAM a ((s,(time,rom,ram,p)):lpc_state) = ram a`; 57198090Srdivacky 58198090Srdivackyval LPC_READ_UART0_def = Define ` 59198090Srdivacky LPC_READ_UART0 ((s,(time,rom,ram,uart0,p)):lpc_state) = UART0_READ uart0`; 60198090Srdivacky 61198090Srdivackyval ARM_OK_def = Define ` 62198090Srdivacky ARM_OK state = 63198090Srdivacky (ARM_ARCH state = ARMv4) /\ (ARM_EXTENSIONS state = {}) /\ 64198090Srdivacky (ARM_UNALIGNED_SUPPORT state) /\ (ARM_READ_EVENT_REGISTER state) /\ 65198090Srdivacky ~(ARM_READ_INTERRUPT_WAIT state) /\ ~(ARM_READ_SCTLR sctlrV state) /\ 66198090Srdivacky (ARM_READ_SCTLR sctlrA state) /\ ~(ARM_READ_SCTLR sctlrU state) /\ 67198090Srdivacky (ARM_READ_IT state = 0w) /\ ~(ARM_READ_STATUS psrJ state) /\ 68198090Srdivacky ~(ARM_READ_STATUS psrT state) /\ ~(ARM_READ_STATUS psrE state) /\ 69198090Srdivacky (ARM_MODE state = 16w)`; 70198090Srdivacky 71val LPC_READ_UNDEF_def = Define ` 72 LPC_READ_UNDEF ((s,p):lpc_state) = ~ARM_OK s /\ ~PERIPHERALS_OK p`; 73 74 75(* ----------------------------------------------------------------------------- *) 76(* Converting from lpc_state to lpc_set *) 77(* ----------------------------------------------------------------------------- *) 78 79val lpc2set'_def = Define ` 80 lpc2set' (rs,st:arm_bit set,is,ms,tt:unit set,ua:unit set,ud:unit set) (s:lpc_state) = 81 IMAGE (\a. tReg a (LPC_READ_REG a s)) rs UNION 82 IMAGE (\a. tStatus a (LPC_READ_STATUS a s)) st UNION 83 IMAGE (\a. tRom a (LPC_READ_ROM a s)) is UNION 84 IMAGE (\a. tRam a (LPC_READ_RAM a s)) ms UNION 85 IMAGE (\a. tTime (LPC_READ_TIME s)) tt UNION 86 IMAGE (\a. tUart0 (LPC_READ_UART0 s)) ua UNION 87 IMAGE (\a. tUndef (LPC_READ_UNDEF s)) ud`; 88 89val lpc2set_def = Define `lpc2set s = lpc2set' (UNIV,UNIV,UNIV,UNIV,UNIV,UNIV,UNIV) s`; 90val lpc2set''_def = Define `lpc2set'' x s = lpc2set s DIFF lpc2set' x s`; 91 92(* theorems *) 93 94val lpc2set'_SUBSET_lpc2set = prove( 95 ``!y s. lpc2set' y s SUBSET lpc2set s``, 96 SIMP_TAC std_ss [pairTheory.FORALL_PROD] 97 \\ SIMP_TAC std_ss [SUBSET_DEF,lpc2set'_def,lpc2set_def,IN_IMAGE,IN_UNION,IN_UNIV] 98 \\ METIS_TAC [NOT_IN_EMPTY]); 99 100val SPLIT_lpc2set = prove( 101 ``!x s. SPLIT (lpc2set s) (lpc2set' x s, lpc2set'' x s)``, 102 REPEAT STRIP_TAC 103 \\ ASM_SIMP_TAC std_ss [SPLIT_def,EXTENSION,IN_UNION,IN_DIFF,lpc2set''_def] 104 \\ `lpc2set' x s SUBSET lpc2set s` by METIS_TAC [lpc2set'_SUBSET_lpc2set] 105 \\ SIMP_TAC bool_ss [DISJOINT_DEF,EXTENSION,IN_INTER,NOT_IN_EMPTY,IN_DIFF] 106 \\ METIS_TAC [SUBSET_DEF]); 107 108val SUBSET_lpc2set = prove( 109 ``!u s. u SUBSET lpc2set s = ?y. u = lpc2set' y s``, 110 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 111 \\ ASM_REWRITE_TAC [lpc2set'_SUBSET_lpc2set] 112 \\ Q.EXISTS_TAC `( 113 { a |a| ?x. tReg a x IN u }, 114 { a |a| ?x. tStatus a x IN u }, 115 { a |a| ?x. tRom a x IN u }, 116 { a |a| ?x. tRam a x IN u }, 117 { a |a| ?x. tTime x IN u }, 118 { a |a| ?x. tUart0 x IN u }, 119 { a |a| ?x. tUndef x IN u })` 120 \\ FULL_SIMP_TAC std_ss [lpc2set'_def,lpc2set_def,EXTENSION,SUBSET_DEF,IN_IMAGE, 121 IN_UNION,GSPECIFICATION,IN_INSERT,NOT_IN_EMPTY,IN_UNIV] 122 \\ STRIP_TAC \\ ASM_REWRITE_TAC [] \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 METIS_TAC [] 123 \\ PAT_ASSUM ``!x:'a. b:bool`` IMP_RES_TAC \\ FULL_SIMP_TAC std_ss [lpc_el_11,lpc_el_distinct]); 124 125val SPLIT_lpc2set_EXISTS = prove( 126 ``!s u v. SPLIT (lpc2set s) (u,v) = ?y. (u = lpc2set' y s) /\ (v = lpc2set'' y s)``, 127 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_REWRITE_TAC [SPLIT_lpc2set] 128 \\ FULL_SIMP_TAC bool_ss [SPLIT_def,lpc2set'_def,lpc2set''_def] 129 \\ `u SUBSET (lpc2set s)` by 130 (FULL_SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_UNION] \\ METIS_TAC []) 131 \\ FULL_SIMP_TAC std_ss [SUBSET_lpc2set] \\ Q.EXISTS_TAC `y` \\ REWRITE_TAC [] 132 \\ FULL_SIMP_TAC std_ss [EXTENSION,IN_DIFF,IN_UNION,DISJOINT_DEF,NOT_IN_EMPTY,IN_INTER] 133 \\ METIS_TAC []); 134 135val IN_lpc2set = (SIMP_RULE std_ss [oneTheory.one] o prove)(`` 136 (!a x s. tReg a x IN (lpc2set s) = (x = LPC_READ_REG a s)) /\ 137 (!a x s. tReg a x IN (lpc2set' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_REG a s) /\ a IN rs) /\ 138 (!a x s. tReg a x IN (lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_REG a s) /\ ~(a IN rs)) /\ 139 (!a x s. tStatus a x IN (lpc2set s) = (x = LPC_READ_STATUS a s)) /\ 140 (!a x s. tStatus a x IN (lpc2set' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_STATUS a s) /\ a IN st) /\ 141 (!a x s. tStatus a x IN (lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_STATUS a s) /\ ~(a IN st)) /\ 142 (!a x s. tRom a x IN (lpc2set s) = (x = LPC_READ_ROM a s)) /\ 143 (!a x s. tRom a x IN (lpc2set' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_ROM a s) /\ a IN is) /\ 144 (!a x s. tRom a x IN (lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_ROM a s) /\ ~(a IN is)) /\ 145 (!a x s. tRam a x IN (lpc2set s) = (x = LPC_READ_RAM a s)) /\ 146 (!a x s. tRam a x IN (lpc2set' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_RAM a s) /\ a IN ms) /\ 147 (!a x s. tRam a x IN (lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_RAM a s) /\ ~(a IN ms)) /\ 148 (!a x s. tTime x IN (lpc2set s) = (x = LPC_READ_TIME s)) /\ 149 (!a x s. tTime x IN (lpc2set' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_TIME s) /\ a IN tt) /\ 150 (!a x s. tTime x IN (lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_TIME s) /\ ~(a IN tt)) /\ 151 (!a x s. tUart0 x IN (lpc2set s) = (x = LPC_READ_UART0 s)) /\ 152 (!a x s. tUart0 x IN (lpc2set' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_UART0 s) /\ a IN ua) /\ 153 (!a x s. tUart0 x IN (lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_UART0 s) /\ ~(a IN ua)) /\ 154 (!a x s. tUndef x IN (lpc2set s) = (x = LPC_READ_UNDEF s)) /\ 155 (!a x s. tUndef x IN (lpc2set' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_UNDEF s) /\ a IN ud) /\ 156 (!a x s. tUndef x IN (lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = (x = LPC_READ_UNDEF s) /\ ~(a IN ud))``, 157 SRW_TAC [] [lpc2set'_def,lpc2set''_def,lpc2set_def,IN_UNION,IN_DIFF,oneTheory.one] 158 \\ METIS_TAC []); 159 160val SET_NOT_EQ = prove( 161 ``!x y. ~(x = y:'a set) = ?a. ~(a IN x = a IN y)``, 162 FULL_SIMP_TAC std_ss [EXTENSION]) 163 164val lpc2set''_11 = prove( 165 ``!y y' s s'. (lpc2set'' y' s' = lpc2set'' y s) ==> (y = y')``, 166 REPEAT STRIP_TAC 167 \\ `?rs st is ms tt ua ud. y = (rs,st,is,ms,tt,ua,ud)` by METIS_TAC [PAIR] 168 \\ `?rs2 st2 is2 ms2 tt2 ua2 ud2. y' = (rs2,st2,is2,ms2,tt2,ua2,ud2)` by METIS_TAC [PAIR] 169 \\ FULL_SIMP_TAC std_ss [] \\ CCONTR_TAC 170 \\ FULL_SIMP_TAC std_ss [EXTENSION] 171 THEN1 (`~((?y. tReg x y IN lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = 172 (?y. tReg x y IN lpc2set'' (rs2,st2,is2,ms2,tt2,ua2,ud2) s'))` by 173 FULL_SIMP_TAC std_ss [IN_lpc2set] THEN1 METIS_TAC []) 174 THEN1 (`~((?y. tStatus x y IN lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = 175 (?y. tStatus x y IN lpc2set'' (rs2,st2,is2,ms2,tt2,ua2,ud2) s'))` by 176 FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] THEN1 METIS_TAC []) 177 THEN1 (`~((?y. tRom x y IN lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = 178 (?y. tRom x y IN lpc2set'' (rs2,st2,is2,ms2,tt2,ua2,ud2) s'))` by 179 FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] THEN1 METIS_TAC []) 180 THEN1 (`~((?y. tRam x y IN lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = 181 (?y. tRam x y IN lpc2set'' (rs2,st2,is2,ms2,tt2,ua2,ud2) s'))` by 182 FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] THEN1 METIS_TAC []) 183 THEN1 (`~((?y. tTime y IN lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = 184 (?y. tTime y IN lpc2set'' (rs2,st2,is2,ms2,tt2,ua2,ud2) s'))` by 185 FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] THEN1 METIS_TAC []) 186 THEN1 (`~((?y. tUart0 y IN lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = 187 (?y. tUart0 y IN lpc2set'' (rs2,st2,is2,ms2,tt2,ua2,ud2) s'))` by 188 FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] THEN1 METIS_TAC []) 189 THEN1 (`~((?y. tUndef y IN lpc2set'' (rs,st,is,ms,tt,ua,ud) s) = 190 (?y. tUndef y IN lpc2set'' (rs2,st2,is2,ms2,tt2,ua2,ud2) s'))` by 191 FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] THEN1 METIS_TAC [])); 192 193val DELETE_lpc2set = (SIMP_RULE std_ss [oneTheory.one] o prove)(`` 194 (!a s. (lpc2set' (rs,st,is,ms,tt,ua,ud) s) DELETE tReg a (LPC_READ_REG a s) = 195 (lpc2set' (rs DELETE a,st,is,ms,tt,ua,ud) s)) /\ 196 (!a s. (lpc2set' (rs,st,is,ms,tt,ua,ud) s) DELETE tStatus a (LPC_READ_STATUS a s) = 197 (lpc2set' (rs,st DELETE a,is,ms,tt,ua,ud) s)) /\ 198 (!a s. (lpc2set' (rs,st,is,ms,tt,ua,ud) s) DELETE tRom a (LPC_READ_ROM a s) = 199 (lpc2set' (rs,st,is DELETE a,ms,tt,ua,ud) s)) /\ 200 (!a s. (lpc2set' (rs,st,is,ms,tt,ua,ud) s) DELETE tRam a (LPC_READ_RAM a s) = 201 (lpc2set' (rs,st,is,ms DELETE a,tt,ua,ud) s)) /\ 202 (!a s. (lpc2set' (rs,st,is,ms,tt,ua,ud) s) DELETE tTime (LPC_READ_TIME s) = 203 (lpc2set' (rs,st,is,ms,tt DELETE a,ua,ud) s)) /\ 204 (!a s. (lpc2set' (rs,st,is,ms,tt,ua,ud) s) DELETE tUart0 (LPC_READ_UART0 s) = 205 (lpc2set' (rs,st,is,ms,tt,ua DELETE a,ud) s)) /\ 206 (!a s. (lpc2set' (rs,st,is,ms,tt,ua,ud) s) DELETE tUndef (LPC_READ_UNDEF s) = 207 (lpc2set' (rs,st,is,ms,tt,ua,ud DELETE a) s))``, 208 SRW_TAC [] [lpc2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR, 209 EXISTS_OR_THM,IN_DELETE,IN_INSERT,NOT_IN_EMPTY,oneTheory.one] 210 \\ Cases_on `x` \\ SRW_TAC [] [] \\ METIS_TAC []); 211 212val EMPTY_lpc2set = prove(`` 213 (lpc2set' (rs,st,is,ms,tt,ua,ud) s = {}) = 214 (rs = {}) /\ (st = {}) /\ (is = {}) /\ (ms = {}) /\ (tt = {}) /\ (ua = {}) /\ (ud = {})``, 215 SRW_TAC [] [lpc2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR,EXISTS_OR_THM] 216 \\ METIS_TAC []); 217 218 219(* ----------------------------------------------------------------------------- *) 220(* Defining the LPC_MODEL *) 221(* ----------------------------------------------------------------------------- *) 222 223val tR_def = Define `tR a x = SEP_EQ {tReg a x}`; 224val tM_def = Define `tM a x = SEP_EQ {tRam a x}`; 225val tS_def = Define `tS a x = SEP_EQ {tStatus a x}`; 226val tU_def = Define `tU x = SEP_EQ {tUndef x}`; 227val tT_def = Define `tT x = SEP_EQ {tTime x}`; 228val tUART0_def = Define `tUART0 x = SEP_EQ {tUart0 x}`; 229 230val tPC_def = Define `tPC x = tR 15w x * tU F * cond (ALIGNED x)`; 231 232val LPC_ROM_def = Define `LPC_ROM (a,w:word32) = 233 { tRom (a+3w) (SOME ((31 >< 24) w)) ; 234 tRom (a+2w) (SOME ((23 >< 16) w)) ; 235 tRom (a+1w) (SOME ((15 >< 8) w)) ; 236 tRom (a+0w) (SOME (( 7 >< 0) w)) }`; 237 238val LPC_MODEL_def = Define ` 239 LPC_MODEL = (lpc2set, LPC_NEXT, LPC_ROM, (\x y. (x:lpc_state) = y))`; 240 241 242(* theorems *) 243 244val lemma = 245 METIS_PROVE [SPLIT_lpc2set] 246 ``p (lpc2set' y s) ==> (?u v. SPLIT (lpc2set s) (u,v) /\ p u /\ (\v. v = lpc2set'' y s) v)``; 247 248val LPC_SPEC_SEMANTICS = store_thm("LPC_SPEC_SEMANTICS", 249 ``SPEC LPC_MODEL p {} q = 250 !y s seq. p (lpc2set' y s) /\ rel_sequence LPC_NEXT seq s ==> 251 ?k. q (lpc2set' y (seq k)) /\ (lpc2set'' y s = lpc2set'' y (seq k))``, 252 SIMP_TAC bool_ss [GSYM RUN_EQ_SPEC,RUN_def,LPC_MODEL_def,STAR_def,SEP_REFINE_def] 253 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC 254 THEN1 (FULL_SIMP_TAC bool_ss [SPLIT_lpc2set_EXISTS] \\ METIS_TAC []) 255 \\ Q.PAT_ASSUM `!s r. b` (STRIP_ASSUME_TAC o UNDISCH o SPEC_ALL o 256 (fn th => MATCH_MP th (UNDISCH lemma)) o Q.SPECL [`s`,`(\v. v = lpc2set'' y s)`]) 257 \\ FULL_SIMP_TAC bool_ss [SPLIT_lpc2set_EXISTS] 258 \\ IMP_RES_TAC lpc2set''_11 \\ Q.EXISTS_TAC `i` \\ METIS_TAC []); 259 260 261(* ----------------------------------------------------------------------------- *) 262(* Theorems for construction of |- SPEC LPC_MODEL ... *) 263(* ----------------------------------------------------------------------------- *) 264 265val SEP_EQ_STAR_LEMMA = prove( 266 ``!p s t. (SEP_EQ t * p) s <=> t SUBSET s /\ (t SUBSET s ==> p (s DIFF t))``, 267 METIS_TAC [EQ_STAR]); 268 269val FLIP_CONJ = prove(``!b c. b /\ (b ==> c) = b /\ c``,METIS_TAC []); 270 271val EXPAND_STAR = 272 GEN_ALL o (SIMP_CONV std_ss [tR_def,tM_def,tS_def,tU_def,tT_def,tUART0_def, 273 SEP_EQ_STAR_LEMMA,INSERT_SUBSET,IN_lpc2set,DELETE_lpc2set, 274 DIFF_INSERT,DIFF_EMPTY,EMPTY_SUBSET] THENC SIMP_CONV std_ss [FLIP_CONJ] 275 THENC REWRITE_CONV [GSYM CONJ_ASSOC]) 276 277val STAR_lpc2set = save_thm("STAR_lpc2set",LIST_CONJ (map EXPAND_STAR 278 [``(tR a x * p) (lpc2set' (rs,st,is,ms,tt,ua,ud) s)``, 279 ``(tM a x * p) (lpc2set' (rs,st,is,ms,tt,ua,ud) s)``, 280 ``(tS a x * p) (lpc2set' (rs,st,is,ms,tt,ua,ud) s)``, 281 ``(tU x * p) (lpc2set' (rs,st,is,ms,tt,ua,ud) s)``, 282 ``(tT x * p) (lpc2set' (rs,st,is,ms,tt,ua,ud) s)``, 283 ``(tUART0 x * p) (lpc2set' (rs,st,is,ms,tt,ua,ud) s)``])); 284 285val CODE_POOL_lpc2set_LEMMA = prove( 286 ``!x y z. (x = z INSERT y) = (z INSERT y) SUBSET x /\ (x DIFF (z INSERT y) = {})``, 287 SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY,IN_DIFF] \\ METIS_TAC []); 288 289val CODE_POOL_lpc2set = store_thm("CODE_POOL_lpc2set", 290 ``CODE_POOL LPC_ROM {(p,c)} (lpc2set' (rs,st,is,ms,tt,ua,ud) s) = 291 ({p+3w;p+2w;p+1w;p} = is) /\ (rs = {}) /\ (st = {}) /\ (ms = {}) /\ (tt = {}) /\ (ua = {}) /\ (ud = {}) /\ 292 (LPC_READ_ROM (p + 0w) s = SOME (( 7 >< 0) c)) /\ 293 (LPC_READ_ROM (p + 1w) s = SOME ((15 >< 8) c)) /\ 294 (LPC_READ_ROM (p + 2w) s = SOME ((23 >< 16) c)) /\ 295 (LPC_READ_ROM (p + 3w) s = SOME ((31 >< 24) c))``, 296 SIMP_TAC bool_ss [CODE_POOL_def,IMAGE_INSERT,IMAGE_EMPTY,BIGUNION_INSERT, 297 BIGUNION_EMPTY,UNION_EMPTY,LPC_ROM_def,CODE_POOL_lpc2set_LEMMA, 298 GSYM DELETE_DEF, INSERT_SUBSET, EMPTY_SUBSET,IN_lpc2set] 299 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ ASM_SIMP_TAC std_ss [] 300 \\ ASM_SIMP_TAC std_ss [DELETE_lpc2set,EMPTY_lpc2set,DIFF_INSERT,WORD_ADD_0] 301 \\ ASM_SIMP_TAC std_ss [GSYM AND_IMP_INTRO,DELETE_lpc2set,EMPTY_lpc2set,DIFF_EMPTY] 302 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 303 \\ ASM_SIMP_TAC std_ss [DELETE_lpc2set,EMPTY_lpc2set]); 304 305val LPC_SPEC_CODE = (RW [GSYM LPC_MODEL_def] o SIMP_RULE std_ss [LPC_MODEL_def] o prove) 306 (``SPEC LPC_MODEL (CODE_POOL (FST (SND (SND LPC_MODEL))) c * p) {} 307 (CODE_POOL (FST (SND (SND LPC_MODEL))) c * q) = 308 SPEC LPC_MODEL p c q``, 309 REWRITE_TAC [SPEC_CODE]); 310 311val IMP_LPC_SPEC_LEMMA = prove( 312 ``!p q. 313 (!s s2 y. 314 p (lpc2set' y s) ==> 315 (?s1. LPC_NEXT s s1) /\ 316 (LPC_NEXT s s2 ==> q (lpc2set' y s2) /\ (lpc2set'' y s = lpc2set'' y s2))) ==> 317 SPEC LPC_MODEL p {} q``, 318 REWRITE_TAC [LPC_SPEC_SEMANTICS] \\ REPEAT STRIP_TAC \\ RES_TAC 319 \\ FULL_SIMP_TAC bool_ss [rel_sequence_def] 320 \\ Q.EXISTS_TAC `SUC 0` \\ METIS_TAC []); 321 322val IMP_LPC_SPEC = save_thm("IMP_LPC_SPEC", 323 (RW1 [STAR_COMM] o RW [LPC_SPEC_CODE] o 324 SPECL [``CODE_POOL LPC_ROM {(p,c)} * p1``, 325 ``CODE_POOL LPC_ROM {(p,c)} * q1``]) IMP_LPC_SPEC_LEMMA); 326 327val lpc2set''_thm = store_thm("lpc2set''_thm", 328 ``(lpc2set'' (rs,st,is,ms,tt,ua,ud) s1 = lpc2set'' (rs,st,is,ms,tt,ua,ud) s2) = 329 (!a. ~(a IN rs) ==> (LPC_READ_REG a s1 = LPC_READ_REG a s2)) /\ 330 (!a. ~(a IN st) ==> (LPC_READ_STATUS a s1 = LPC_READ_STATUS a s2)) /\ 331 (!a. ~(a IN is) ==> (LPC_READ_ROM a s1 = LPC_READ_ROM a s2)) /\ 332 (!a. ~(a IN ms) ==> (LPC_READ_RAM a s1 = LPC_READ_RAM a s2)) /\ 333 (!a. ~(a IN tt) ==> (LPC_READ_TIME s1 = LPC_READ_TIME s2)) /\ 334 (!a. ~(a IN ua) ==> (LPC_READ_UART0 s1 = LPC_READ_UART0 s2)) /\ 335 (!a. ~(a IN ud) ==> (LPC_READ_UNDEF s1 = LPC_READ_UNDEF s2))``, 336 SIMP_TAC std_ss [oneTheory.one] 337 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC 338 \\ FULL_SIMP_TAC std_ss [EXTENSION] 339 THEN1 (Cases \\ ASM_SIMP_TAC std_ss [IN_lpc2set] \\ METIS_TAC []) 340 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tReg a (LPC_READ_REG a s1)`) 341 \\ METIS_TAC [IN_lpc2set]) 342 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tStatus a (LPC_READ_STATUS a s1)`) 343 \\ FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] \\ METIS_TAC []) 344 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tRom a (LPC_READ_ROM a s1)`) 345 \\ FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] \\ METIS_TAC []) 346 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tRam a (LPC_READ_RAM a s1)`) 347 \\ FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] \\ METIS_TAC []) 348 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tTime (LPC_READ_TIME s1)`) 349 \\ FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] \\ METIS_TAC []) 350 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tUart0 (LPC_READ_UART0 s1)`) 351 \\ FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] \\ METIS_TAC []) 352 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tUndef (LPC_READ_UNDEF s1)`) 353 \\ FULL_SIMP_TAC std_ss [IN_lpc2set,oneTheory.one] \\ METIS_TAC [])); 354 355 356val _ = export_theory(); 357