1(*---------------------------------------------------------------------------*) 2(* Register machines *) 3(*---------------------------------------------------------------------------*) 4 5open HolKernel bossLib boolLib Parse 6open finite_mapTheory arithmeticTheory pred_setTheory; 7open boolSimps 8 9val _ = new_theory "reg" 10 11(*---------------------------------------------------------------------------*) 12(* Register machines have two instructions: *) 13(* *) 14(* INC r j -- increment register r and goto instruction j *) 15(* TST r i j -- if register r = 0 then goto instr. i else *) 16(* decrement r and goto j *) 17(*---------------------------------------------------------------------------*) 18 19val _ = Hol_datatype 20 `instr = INC of num => num 21 | TST of num => num => num`; 22 23(*---------------------------------------------------------------------------*) 24(* A machine configuration is the current state of the registers and the *) 25(* current instruction index. The final result of a computation will be held *) 26(* in register 0. *) 27(*---------------------------------------------------------------------------*) 28 29val _ = Hol_datatype `config = <| pc : num; regs : num |-> num |>` 30val _ = hide "config" 31 32val saferead_def = Define` 33 saferead f i = case FLOOKUP f i of NONE => 0 | SOME v => v 34`; 35val _ = set_fixity "''" (Infixl 2000) 36val _ = overload_on ("''", ``saferead``) 37 38val reg0_def = Define `reg0 config = config.regs '' 0`; 39 40(*---------------------------------------------------------------------------*) 41(* A step of computation is represented as a relation between configurations.*) 42(* A configuration (Regs,i) holds the contents of the registers and the pc. *) 43(* A program is represented by a finite map from the pc to the instruction *) 44(* to be executed. If the pc is not in the domain of the program, no change *) 45(* is made to the configuration. *) 46(*---------------------------------------------------------------------------*) 47 48val Step_def = Define ` 49 Step prog cfg = 50 case FLOOKUP prog cfg.pc of 51 NONE => cfg 52 | SOME(INC r j) => cfg with <| 53 regs updated_by (\R. R |+ (r, R '' r + 1)); 54 pc := j 55 |> 56 | SOME(TST r a b) => 57 if cfg.regs '' r = 0 then cfg with pc := a 58 else cfg with <| regs updated_by (\R. R |+ (r, R '' r - 1)); 59 pc := b |>`; 60 61(* ---------------------------------------------------------------------- 62 Translate a list into a finite map. 63 ---------------------------------------------------------------------- *) 64 65val fmapOf_def = 66 Define 67 `fmapOf list = FEMPTY |++ GENLIST (��n. (n, EL n list)) (LENGTH list)` 68 69(*---------------------------------------------------------------------------*) 70(* A sequence f is an execution of prog on inputs args starting at pc, just *) 71(* when the first element of f is the initial configuration of the machine, *) 72(* and each subsequent element follows by making a step of computation. An *) 73(* execution is finite just in case some configuration in it has a pc not in *) 74(* the domain of prog. In that case, all subsequent configs are identical. *) 75(* This is distinguishable from an infinite execution where all configs are *) 76(* identical, since each config in the latter will have the pc in the domain *) 77(* of prog. *) 78(*---------------------------------------------------------------------------*) 79 80val isExecution_def = 81 Define 82 `isExecution prog pc args f = 83 (f 0 = <| regs := fmapOf args; pc := pc|>) /\ 84 (!n. f (n+1) = Step prog (f n))`; 85 86val Executions_Exist = store_thm( 87 "Executions_Exist", 88 ``!prog pc args. ?f. isExecution prog pc args f``, 89 RW_TAC arith_ss [isExecution_def] THEN 90 Q.EXISTS_TAC `\n. FUNPOW (Step prog) n <| regs := fmapOf args; pc := pc|>` THEN 91 RW_TAC arith_ss [FUNPOW] THEN RW_TAC arith_ss [GSYM ADD1] THEN 92 RW_TAC arith_ss [FUNPOW_SUC]); 93 94val Executions_Unique = store_thm( 95 "Executions_Unique", 96 ``!prog pc args f1 f2. 97 isExecution prog pc args f1 /\ 98 isExecution prog pc args f2 ==> (f1=f2)``, 99 RW_TAC arith_ss [isExecution_def, FUN_EQ_THM] THEN 100 Induct_on `x` THEN RW_TAC arith_ss [] THEN METIS_TAC [ADD1]); 101 102(*---------------------------------------------------------------------------*) 103(* Execution is deterministic, so we can talk of "the" execution of prog on *) 104(* args starting at pc: *) 105(* *) 106(* |- isExecution prog pc args (execOf prog pc args) *) 107(* *) 108(*---------------------------------------------------------------------------*) 109 110val execOf_def = 111 new_specification 112 ("execOf_def", 113 ["execOf"], 114 SIMP_RULE std_ss [SKOLEM_THM] Executions_Exist); 115 116(*---------------------------------------------------------------------------*) 117(* val execOf_thm = *) 118(* |- !prog pc args. *) 119(* (execOf prog pc args 0 = (fmapOf args,pc)) /\ *) 120(* !n. execOf prog pc args (SUC n) = Step prog (execOf prog pc args n) *) 121(*---------------------------------------------------------------------------*) 122 123val execOf_thm = save_thm( 124 "execOf_thm", 125 SIMP_RULE arith_ss [isExecution_def, GSYM ADD1] execOf_def); 126 127val execOf_recn = store_thm( 128 "execOf_recn", 129 ``execOf prog pc args n = 130 if n=0 then <| regs := fmapOf args; pc := pc|> 131 else Step prog (execOf prog pc args (n-1))``, 132 Cases_on `n` THEN RW_TAC arith_ss [execOf_thm]); 133 134val _ = computeLib.add_funs [execOf_recn,FLOOKUP_DEF]; 135 136(*---------------------------------------------------------------------------*) 137(* The index of the first terminated configuration in a sequence. *) 138(*---------------------------------------------------------------------------*) 139 140val haltedConfig_def = Define ` 141 haltedConfig (prog : num |-> instr) cnfg = cnfg.pc ��� FDOM prog 142` 143 144val haltsAt_def = 145 Define 146 `haltsAt (prog:num |-> instr) (seq:num -> config) = 147 if (?n. haltedConfig prog (seq n)) 148 then SOME (LEAST n. haltedConfig prog (seq n)) 149 else NONE`; 150 151val haltsSuffix = store_thm( 152 "haltsSuffix", 153 ``!prog pc args seq m. 154 isExecution prog pc args seq /\ 155 haltedConfig prog (seq m) ==> 156 !q. m <= q ==> haltedConfig prog (seq q)``, 157 SRW_TAC [][haltedConfig_def,isExecution_def,GSYM ADD1] THEN 158 `?k. q = m + k` by METIS_TAC [LESS_EQUAL_ADD] THEN 159 SRW_TAC [][] THEN POP_ASSUM (K ALL_TAC) THEN 160 Induct_on `k` THEN SRW_TAC [][ADD_CLAUSES] THEN 161 Q.SPEC_THEN `seq (m + k)` FULL_STRUCT_CASES_TAC 162 (theorem "config_literal_nchotomy") THEN 163 SRW_TAC [][Step_def,FLOOKUP_DEF] THEN FULL_SIMP_TAC (srw_ss()) []); 164 165val haltsSuffixThm = store_thm( 166 "haltsSuffixThm", 167 ``!prog pc args m q. 168 haltedConfig prog (execOf prog pc args m) /\ m <= q ==> 169 haltedConfig prog (execOf prog pc args q)``, 170 METIS_TAC [execOf_def,haltsSuffix]); 171 172val Halts_def = 173 Define 174 `Halts prog pc args = ?n. haltsAt prog (execOf prog pc args) = SOME n`; 175 176(*---------------------------------------------------------------------------*) 177(* The function computed by program prog is given by funOf prog. *) 178(*---------------------------------------------------------------------------*) 179 180val funOf_def = Define ` 181 funOf prog args = 182 let seq = execOf prog 1 (0::args) 183 in case haltsAt prog seq of 184 SOME m => SOME (reg0 (seq m)) 185 | NONE => NONE 186`; 187 188(*---------------------------------------------------------------------------*) 189(* Accept/reject inputs. *) 190(*---------------------------------------------------------------------------*) 191 192val Accepts_def = 193 Define 194 `Accepts prog pc args = 195 ?m. (haltsAt prog (execOf prog pc args) = SOME m) /\ 196 (reg0(execOf prog pc args m) = 1)`; 197 198val Rejects_def = 199 Define 200 `Rejects prog pc args = 201 ?m. (haltsAt prog (execOf prog pc args) = SOME m) /\ 202 (reg0(execOf prog pc args m) = 0)`; 203 204(*---------------------------------------------------------------------------*) 205(* The set of computable functions. Needs a notion of arity of the function. *) 206(*---------------------------------------------------------------------------*) 207 208val nComputable_def = 209 Define 210 `nComputable n (f:num list -> num option) = 211 ?prog. !args. (LENGTH args = n) ==> (f args = funOf prog args)`; 212 213val Computable_def = 214 Define 215 `Computable = BIGUNION {nComputable n | n IN UNIV}`; 216 217val IN_Computable = Q.prove 218(`f IN Computable = 219 ?n prog. !args. (LENGTH args = n) ==> (f args = funOf prog args)`, 220 SRW_TAC [] [IN_BIGUNION, Computable_def,EQ_IMP_THM,nComputable_def] THEN 221 METIS_TAC [nComputable_def, SPECIFICATION]); 222 223 224(*---------------------------------------------------------------------------*) 225(* While instruction 0 is not entered, make a Step, thereby updating the *) 226(* registers and the next instruction. By convention, programs start at *) 227(* pc 1. *) 228(*---------------------------------------------------------------------------*) 229 230val Run_def = 231 Define 232 `Run prog args n = 233 FUNPOW (Step prog) n <| regs := fmapOf (0::args); pc := 1|>`; 234 235val whileRun_def = Define` 236 whileRun prog args = 237 WHILE (��c. ��haltedConfig prog c) (Step prog) 238 <| regs := fmapOf (0::args); pc := 1 |> 239` 240 241(*---------------------------------------------------------------------------*) 242(* Example Register program executions. *) 243(*---------------------------------------------------------------------------*) 244 245val predOf_def = Define` 246 predOf P s <=> P s.pc (saferead s.regs) 247` 248 249val firstHaltsAt_def = Define` 250 firstHaltsAt prog n s <=> 251 haltedConfig prog (FUNPOW (Step prog) n s) ��� 252 ���m. m < n ��� ��haltedConfig prog (FUNPOW (Step prog) m s) 253`; 254 255val HOARE_def = Define` 256 HOARE P prog Q <=> 257 ���s0. predOf P s0 ��� 258 ���n. firstHaltsAt prog n s0 ��� 259 predOf Q (FUNPOW (Step prog) n s0) 260` 261 262 263val _ = temp_add_rule {fixity = Infix(NONASSOC, 450), 264 term_name = "HOARE", 265 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 266 paren_style = OnlyIfNecessary, 267 pp_elements = [HardSpace 1, TOK (UTF8.chr 0x22A2), 268 BreakSpace(1,2), TM, BreakSpace(1,0), 269 TOK (UTF8.chr 0x22A3), HardSpace 1]} 270 271 272val saferead_update = store_thm( 273 "saferead_update", 274 ``((fm |+ (k1,v)) '' k1 = v) ��� 275 (k1 ��� k2 ��� ((fm |+ (k1,v)) '' k2 = fm '' k2))``, 276 SRW_TAC [][saferead_def, FLOOKUP_UPDATE]); 277 278val _ = overload_on("RM*", ``��p n s. FUNPOW (Step p) n s``) 279open lcsymtacs 280val haltedConfig_suffix = store_thm( 281 "haltedConfig_suffix", 282 ``haltedConfig p (RM* p m s) ��� m ��� n ��� haltedConfig p (RM* p n s)``, 283 Induct_on `n` >| [ 284 strip_tac >> `m = 0` by decide_tac >> fsrw_tac [][], 285 Cases_on `m = SUC n` >- srw_tac [][] >> 286 strip_tac >> `m ��� n` by decide_tac >> 287 srw_tac [][FUNPOW_SUC] >> 288 `haltedConfig p (RM* p n s)` by METIS_TAC [] >> 289 `(RM* p n s).pc ��� FDOM p` by METIS_TAC [haltedConfig_def] >> 290 srw_tac [][Step_def, FLOOKUP_DEF] 291 ]); 292 293val firstHaltsAt_prefix = store_thm( 294 "firstHaltsAt_prefix", 295 ``���m n plus_mn s0. 296 firstHaltsAt prog n (FUNPOW (Step prog) m s0) ��� 297 ��haltedConfig prog (FUNPOW (Step prog)m s0) ��� (plus_mn = m + n) ��� 298 firstHaltsAt prog (plus_mn) s0``, 299 SIMP_TAC (srw_ss()) [firstHaltsAt_def] THEN SRW_TAC [][] THENL [ 300 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [GSYM FUNPOW_ADD], 301 Cases_on `m' ��� m` >- METIS_TAC [haltedConfig_suffix] >> 302 `m < m'` by decide_tac >> 303 first_x_assum (qspec_then `m' - m` mp_tac) >> 304 srw_tac [ARITH_ss][GSYM FUNPOW_ADD] 305 ]); 306 307val firstHaltsAt_ZERO = store_thm( 308 "firstHaltsAt_ZERO", 309 ``firstHaltsAt p 0 s ��� haltedConfig p s``, 310 srw_tac [][firstHaltsAt_def]); 311val _ = export_rewrites ["firstHaltsAt_ZERO"] 312 313 314val firstHaltsAt_SUC = store_thm( 315 "firstHaltsAt_SUC", 316 ``firstHaltsAt p (SUC n) s ��� 317 firstHaltsAt p n (Step p s) ��� ��haltedConfig p s``, 318 srw_tac [][firstHaltsAt_def, FUNPOW, EQ_IMP_THM] >| [ 319 first_x_assum (qspec_then `SUC m` mp_tac) >> 320 srw_tac [][FUNPOW], 321 first_x_assum (qspec_then `0` mp_tac) >> srw_tac [][], 322 Cases_on `m = 0` >- srw_tac [][] >> 323 `���m���. m = SUC m���` by (Cases_on `m` >> srw_tac [][]) >> 324 fsrw_tac [][FUNPOW] 325 ]); 326 327val firstHaltsAt_ADD = store_thm( 328 "firstHaltsAt_ADD", 329 ``0 < m ��� (firstHaltsAt p (m + n) s ��� firstHaltsAt p m (RM* p n s))``, 330 srw_tac [][firstHaltsAt_def, EQ_IMP_THM, FUNPOW_ADD] >| [ 331 first_x_assum (qspec_then `m' + n` mp_tac) >> 332 srw_tac [][FUNPOW_ADD], 333 Cases_on `n ��� m'` >- 334 (first_x_assum (qspec_then `m' - n` mp_tac) >> 335 srw_tac [ARITH_ss][GSYM FUNPOW_ADD]) >> 336 first_x_assum (qspec_then `0` mp_tac) >> 337 srw_tac [][] >> 338 `m' ��� n` by DECIDE_TAC >> 339 metis_tac [haltedConfig_suffix] 340 ]); 341 342val unused_instructions = store_thm( 343 "unused_instructions", 344 ``���n m s. 345 firstHaltsAt prog��� n s ��� DISJOINT (FDOM prog���) (FDOM prog���) ��� m ��� n ��� 346 (RM* (FUNION prog��� prog���) m s = RM* prog��� m s)``, 347 Induct_on `n` >- srw_tac [][] >> 348 srw_tac [][firstHaltsAt_SUC] >> 349 `(m = 0) ��� ���m���. m = SUC m���` by (Cases_on `m` >> srw_tac [][]) 350 >- srw_tac [][] >> 351 `m��� ��� n` by fsrw_tac [][] >> 352 `s.pc ��� FDOM prog���` by fsrw_tac [][haltedConfig_def] >> 353 `s.pc ��� FDOM prog���` 354 by (fsrw_tac [][DISJOINT_DEF, EXTENSION] >> metis_tac []) >> 355 srw_tac [][FUNPOW] >> 356 `Step (FUNION prog��� prog���) s = Step prog��� s` 357 by srw_tac [][Step_def, FLOOKUP_DEF, FUNION_DEF] >> 358 srw_tac [][]); 359 360val haltedConfig_bigger_prog = store_thm( 361 "haltedConfig_bigger_prog", 362 ``haltedConfig (FUNION p��� p���) s ��� haltedConfig p��� s``, 363 srw_tac [][haltedConfig_def, FUNION_DEF]); 364 365val predOf_AND_def = Define` 366 predOf_AND p q pc rf ��� p pc rf ��� q pc rf 367`; 368 369val _ = set_fixity "&&" (Infixr 400) 370val _ = overload_on("&&", ``predOf_AND``) 371 372val PCNOTIN_def = Define` 373 PCNOTIN s pc rf ��� pc ��� s 374` 375val _ = overload_on("PC���", ``PCNOTIN``) 376 377val predOf_AND_thm = store_thm( 378 "predOf_AND_thm", 379 ``predOf (P && Q) s ��� predOf P s ��� predOf Q s``, 380 srw_tac [][predOf_AND_def, predOf_def]) 381 382val predOf_PCNOTIN = store_thm( 383 "predOf_PCNOTIN", 384 ``predOf (PC��� s) c ��� c.pc ��� s``, 385 srw_tac [][PCNOTIN_def, predOf_def]); 386 387val HOARE_sequence = store_thm( 388 "HOARE_sequence", 389 ``���P Q R. 390 HOARE P prog1 R ��� HOARE R prog2 (Q && PC��� (FDOM prog1)) ��� 391 DISJOINT (FDOM prog1) (FDOM prog2) ��� 392 HOARE P (FUNION prog1 prog2) Q``, 393 SRW_TAC [][HOARE_def] THEN 394 `���n���. firstHaltsAt prog1 n��� s0 ��� predOf R (RM* prog1 n��� s0)` 395 by METIS_TAC [] THEN 396 Q.ABBREV_TAC `s1 = RM* prog1 n��� s0` THEN 397 `���n���. firstHaltsAt prog2 n��� s1 ��� 398 predOf (Q && PC���(FDOM prog1)) (RM* prog2 n��� s1)` 399 by METIS_TAC [] THEN 400 Q.EXISTS_TAC `n��� + n���` THEN ASM_SIMP_TAC (srw_ss()) [FUNPOW_ADD] THEN 401 `���m. m ��� n��� ��� (RM* (FUNION prog1 prog2) m s0 = RM* prog1 m s0)` 402 by metis_tac[unused_instructions] >> 403 asm_simp_tac (srw_ss()) [] >> 404 Cases_on `n��� = 0` >- 405 (fsrw_tac [][firstHaltsAt_def, predOf_AND_thm] >> conj_tac >- 406 fsrw_tac [][haltedConfig_def, FUNION_DEF] >> 407 srw_tac [ARITH_ss][] >> metis_tac [haltedConfig_bigger_prog]) >> 408 `0 < n���` by decide_tac >> 409 asm_simp_tac (srw_ss()) [firstHaltsAt_ADD] >> 410 `FUNION prog1 prog2 = FUNION prog2 prog1` 411 by metis_tac [FUNION_COMM] >> 412 pop_assum SUBST_ALL_TAC >> 413 `���m. m ��� n��� ��� (RM* (FUNION prog2 prog1) m s1 = RM* prog2 m s1)` 414 by metis_tac [DISJOINT_SYM, unused_instructions] >> 415 REVERSE conj_tac >- fsrw_tac [][predOf_AND_thm] >> 416 fsrw_tac [][firstHaltsAt_def] >> conj_tac >- 417 fsrw_tac [][haltedConfig_def, predOf_PCNOTIN, predOf_AND_thm, 418 FUNION_DEF] >> 419 srw_tac [ARITH_ss][] >> metis_tac [haltedConfig_bigger_prog]); 420 421val RPWhile_def = Define` 422 RPWhile reg bi ei pbi p = 423 FUNION (FEMPTY |+ (bi, TST reg ei pbi)) p 424` 425 426val IN_FDOM_RPWhile = store_thm( 427 "IN_FDOM_RPWhile", 428 ``x ��� FDOM (RPWhile reg bi ei pbi p) ��� (x = bi) ��� x ��� FDOM p``, 429 srw_tac [][RPWhile_def, FUNION_DEF]); 430val _ = export_rewrites ["IN_FDOM_RPWhile"] 431 432val rP_def = Define` 433 rP r P pc reg = P (reg r) 434`; 435 436val rP_thm = store_thm( 437 "rP_thm", 438 ``predOf (rP r P) s ��� P (s.regs '' r)``, 439 srw_tac [][predOf_def, rP_def]); 440val _ = augment_srw_ss [rewrites [rP_thm]] 441 442val rP_eq_thm = store_thm( 443 "rP_eq_thm", 444 ``predOf (rP r ((=) v)) s ��� (s.regs '' r = v)``, 445 srw_tac [][] >> metis_tac []) 446val _ = augment_srw_ss [rewrites [rP_eq_thm]] 447 448val PCeq_def = Define` 449 PCeq n pc reg = (pc = n) 450`; 451 452val PCeq_thm = store_thm( 453 "PCeq_thm", 454 ``predOf (PCeq c) s ��� (s.pc = c)``, 455 srw_tac [][predOf_def, PCeq_def]); 456val _ = augment_srw_ss [rewrites [PCeq_thm]] 457 458val PCsub_def = Define` 459 PCsub P v pc reg = P v reg 460` 461 462val PCsub_AND = store_thm( 463 "PCsub_AND", 464 ``PCsub (P && Q) v = PCsub P v && PCsub Q v``, 465 srw_tac [][FUN_EQ_THM, PCsub_def, predOf_AND_def]); 466val _ = augment_srw_ss [rewrites [PCsub_AND]] 467 468val PCsub_PCsub = store_thm( 469 "PCsub_PCsub", 470 ``PCsub (PCsub P v1) v2 = PCsub P v1``, 471 srw_tac [][FUN_EQ_THM, PCsub_def]); 472val _ = augment_srw_ss [rewrites [PCsub_PCsub]] 473 474val PCsub_rP = store_thm( 475 "PCsub_rP", 476 ``PCsub (rP r P) v = rP r P``, 477 srw_tac [][PCsub_def, rP_def, FUN_EQ_THM]); 478val _ = augment_srw_ss [rewrites [PCsub_rP]] 479 480val PCsub_K = store_thm( 481 "PCsub_K", 482 ``PCsub (K P) v = K P``, 483 srw_tac [][PCsub_def, FUN_EQ_THM]); 484val _ = augment_srw_ss [rewrites [PCsub_K]] 485 486val PCsub_PCeq = store_thm( 487 "PCsub_PCeq", 488 ``PCsub (PCeq v1) v2 = K (K (v2 = v1))``, 489 srw_tac [][PCsub_def, PCeq_def, FUN_EQ_THM]); 490val _ = augment_srw_ss [rewrites [PCsub_PCeq]] 491 492val PCsub_PCNOTIN = store_thm( 493 "PCsub_PCNOTIN", 494 ``PCsub (PC��� s) v = K (K (v ��� s))``, 495 srw_tac [][PCsub_def, PCNOTIN_def, FUN_EQ_THM]); 496val _ = augment_srw_ss [rewrites [PCsub_PCNOTIN]] 497 498val PCsub_ABS = store_thm( 499 "PCsub_ABS", 500 ``PCsub (��p:num. f p) v = (��p:num. f v)``, 501 srw_tac [][PCsub_def, FUN_EQ_THM]); 502val _ = augment_srw_ss [rewrites [PCsub_ABS]] 503 504val REGfRsub_def = Define` 505 REGfRsub P r f pc reg = P pc ((r =+ f reg) reg) 506` 507 508val REGfRsub_ABS = store_thm( 509 "REGfRsub_ABS", 510 ``REGfRsub (��p r. f1 p r) rg f = (��p r. f1 p ((rg =+ f r) r))``, 511 srw_tac [][FUN_EQ_THM, REGfRsub_def]); 512 513val REGfRsub_AND = store_thm( 514 "REGfRsub_AND", 515 ``REGfRsub (P && Q) r f = REGfRsub P r f && REGfRsub Q r f``, 516 srw_tac [][predOf_AND_def, REGfRsub_def, FUN_EQ_THM]); 517val _ = augment_srw_ss [rewrites [REGfRsub_AND]] 518 519val REGfRsub_PCsub = store_thm( 520 "REGfRsub_PCsub", 521 ``REGfRsub (PCsub P v) r f = PCsub (REGfRsub P r f) v``, 522 srw_tac [][REGfRsub_def, PCsub_def, FUN_EQ_THM]) 523val _ = augment_srw_ss [rewrites [SYM REGfRsub_PCsub]] 524 525val REGfRsub_rP1 = store_thm( 526 "REGfRsub_rP1", 527 ``REGfRsub (rP r P) r f = K (P o f)``, 528 srw_tac [][FUN_EQ_THM, REGfRsub_def, rP_def, 529 combinTheory.APPLY_UPDATE_THM]); 530 531val REGfRsub_rP2 = store_thm( 532 "REGfRsub_rP2", 533 ``r1 ��� r2 ��� (REGfRsub (rP r1 P) r2 f = rP r1 P)``, 534 srw_tac [][FUN_EQ_THM, REGfRsub_def, rP_def, 535 combinTheory.APPLY_UPDATE_THM]); 536val _ = augment_srw_ss [rewrites [REGfRsub_rP1, REGfRsub_rP2]] 537 538val REGfRsub_PCeq = store_thm( 539 "REGfRsub_PCeq", 540 ``REGfRsub (PCeq v) r f = PCeq v``, 541 srw_tac [][FUN_EQ_THM, PCeq_def, REGfRsub_def]); 542val _ = augment_srw_ss [rewrites [REGfRsub_PCeq]] 543 544val REGfRsub_PCNOTIN = store_thm( 545 "REGfRsub_PCNOTIN", 546 ``REGfRsub (PC��� s) r f = PC��� s``, 547 srw_tac [][REGfRsub_def, PCNOTIN_def, FUN_EQ_THM]); 548val _ = augment_srw_ss [rewrites [REGfRsub_PCNOTIN]] 549 550val RPWhile_rule = store_thm( 551 "RPWhile_rule", 552 ``ei ��� bi ��� bi ��� FDOM p ��� ei ��� FDOM p ��� 553 (���n. HOARE (rP reg ($= n) && REGfRsub (PCsub Inv ei) reg (��r. r reg + 1) && 554 PCeq pbi) 555 p 556 (rP reg (��x. x <= n) && PCsub Inv ei && PCeq bi)) ==> 557 HOARE (PCsub Inv ei && PCeq bi) 558 (RPWhile reg bi ei pbi p) 559 (Inv && rP reg ($= 0) && PCeq ei)``, 560 srw_tac [][HOARE_def] >> 561 pop_assum mp_tac >> qabbrev_tac `v = s0.regs '' reg` >> 562 pop_assum (mp_tac o SYM o REWRITE_RULE [markerTheory.Abbrev_def]) >> 563 map_every qid_spec_tac [`s0`, `v`] >> 564 completeInduct_on `v` >> fsrw_tac [][GSYM RIGHT_FORALL_IMP_THM] >> 565 srw_tac [][] >> 566 pop_assum (mp_tac o 567 SIMP_RULE (srw_ss()) [predOf_def, predOf_AND_thm, PCeq_def, 568 PCsub_def]) >> 569 qabbrev_tac `N = s0.regs '' reg` >> 570 Cases_on `N = 0` >- 571 (strip_tac >> qexists_tac `1` >> 572 `Step (RPWhile reg bi ei pbi p) s0 = s0 with pc := ei` 573 by srw_tac [][RPWhile_def, Step_def, FLOOKUP_UPDATE, 574 FLOOKUP_FUNION] >> 575 asm_simp_tac (srw_ss()) [RPWhile_def, firstHaltsAt_def, predOf_def, 576 predOf_AND_thm, DECIDE ``m < 1 ��� (m = 0)``, 577 PCeq_def, rP_def, haltedConfig_def, 578 FUNION_DEF]) >> 579 strip_tac >> 580 qabbrev_tac 581 `s1 = s0 with <| pc := pbi; regs := s0.regs |+ (reg, N - 1) |>` >> 582 `Step (RPWhile reg bi ei pbi p) s0 = s1` 583 by (srw_tac [][RPWhile_def, Step_def, FLOOKUP_UPDATE, FLOOKUP_FUNION, 584 Abbr`s1`] >> 585 srw_tac [][theorem "config_component_equality"]) >> 586 first_x_assum 587 (qspecl_then [`N - 1`, `s1`] 588 (mp_tac o SIMP_RULE (srw_ss()) 589 [predOf_def, predOf_AND_thm, rP_def, 590 PCsub_def, PCeq_def, REGfRsub_def])) >> 591 `(s1.pc = pbi) ��� (s1.regs = s0.regs |+ (reg,N-1))` 592 by srw_tac [][Abbr`s1`] >> 593 asm_simp_tac (srw_ss() ++ ARITH_ss) [saferead_update]>> 594 qmatch_abbrev_tac `(Inv ei f ==> Q) ==> R` >> 595 `f = (saferead s0.regs)` 596 by (srw_tac [][Abbr`f`, FUN_EQ_THM, combinTheory.APPLY_UPDATE_THM, 597 saferead_update] >> srw_tac [][] >> srw_tac [][]) >> 598 pop_assum SUBST1_TAC >> asm_simp_tac (srw_ss()) [] >> 599 map_every qunabbrev_tac [`Q`, `R`] >> 600 disch_then (Q.X_CHOOSE_THEN `c` strip_assume_tac) >> 601 qabbrev_tac `s2 = RM* p c s1` >> 602 `RM* (RPWhile reg bi ei pbi p) c s1 = s2` 603 by (srw_tac [][RPWhile_def, Abbr`s2`] >> 604 qmatch_abbrev_tac `RM* (FUNION gp p) c s1 = RM* p c s1` >> 605 `DISJOINT (FDOM gp) (FDOM p)` 606 by srw_tac [][Abbr`gp`, DISJOINT_DEF, EXTENSION] >> 607 srw_tac [][Once FUNION_COMM] >> 608 match_mp_tac unused_instructions >> 609 metis_tac [DECIDE ``x ��� x``, DISJOINT_SYM]) >> 610 first_x_assum (qspec_then `s2` mp_tac) >> 611 asm_simp_tac (srw_ss() ++ ARITH_ss) [] >> 612 `predOf (PCsub Inv ei && PCeq bi) s2` 613 by srw_tac [][PCsub_def, PCeq_def, predOf_AND_thm, predOf_def] >> 614 asm_simp_tac (srw_ss()) [] >> 615 disch_then (Q.X_CHOOSE_THEN `M` STRIP_ASSUME_TAC) >> 616 qexists_tac `SUC (M + c)` >> 617 asm_simp_tac (srw_ss()) [firstHaltsAt_SUC, haltedConfig_def] >> 618 asm_simp_tac (srw_ss()) [FUNPOW] >> 619 Cases_on `M = 0` >- fsrw_tac [][haltedConfig_def] >> 620 `0 < M` by decide_tac >> 621 asm_simp_tac (srw_ss()) [FUNPOW_ADD, firstHaltsAt_ADD]); 622 623 624(* 625(* Halt immediately *) 626val prog1 = ``FEMPTY |++ [(1,TST 0 0 0)]``; 627 628(* Add R1 and R2, putting result in R0 and trashing R1 *) 629val prog2 = ``FUNION (RPmove 1 0 1 3) (RPmove 2 0 3 0)`` 630 631EVAL ``reg0(Run ^prog1 [0;1;2] 1)``; 632EVAL ``reg0(Run ^prog2 [3;4] 8)``; 633EVAL ``reg0(Run ^prog2 [3;19] 40)``; 634Count.apply EVAL ``reg0(Run ^prog2 [19;52] 400)``; 635 636Count.apply EVAL ``reg0 (whileRun ^prog2 [19;52])``; 637 638val zero_nb1 = prove( 639 ``~(0 = NUMERAL (BIT1 n))``, 640 REWRITE_TAC [NUMERAL_DEF, BIT1, ADD_CLAUSES, SUC_NOT]); 641val nb12 = prove( 642 ``NUMERAL (BIT1 n) <> NUMERAL (BIT2 m)``, 643 REWRITE_TAC [NUMERAL_DEF, BIT1, BIT2, ADD_CLAUSES, SUC_NOT, 644 prim_recTheory.INV_SUC_EQ] THEN 645 DISCH_THEN (MP_TAC o AP_TERM ``EVEN``) THEN 646 SRW_TAC [][EVEN_ADD, EVEN]); 647 648val keycollapse1 = prove( 649 ``fm |+ (0, v1) |+ (NUMERAL (BIT1 n), v2) |+ (0, v3) = 650 fm |+ (0, v3) |+ (NUMERAL (BIT1 n), v2)``, 651 SRW_TAC [][fmap_EXT, EXTENSION, FAPPLY_FUPDATE_THM, zero_nb1] THEN1 652 PROVE_TAC [] THEN 653 SRW_TAC [][] THEN 654 FULL_SIMP_TAC (srw_ss()) [zero_nb1]); 655 656val keycollapse2 = prove( 657 ``fm |+ (NUMERAL (BIT1 n), v1) |+ (NUMERAL (BIT2 m), v2) 658 |+ (NUMERAL (BIT1 n), v3) = 659 fm |+ (NUMERAL (BIT1 n), v3) |+ (NUMERAL (BIT2 m), v2)``, 660 SRW_TAC [][fmap_EXT, EXTENSION, FAPPLY_FUPDATE_THM, nb12] THEN1 661 PROVE_TAC [] THEN 662 SRW_TAC [][] THEN 663 FULL_SIMP_TAC (srw_ss()) [nb12]); 664 665SIMP_CONV (srw_ss()) [Run_def, FUNION_DEF, numeralTheory.numeral_funpow, Step_def, FLOOKUP_FUNION, RPmove_def, FLOOKUP_UPDATE, fmapOf_def, saferead_def, FUPDATE_LIST_THM, keycollapse1, keycollapse2] ``Run ^prog2 [19;52] 41`` 666 667*) 668 669val RPimp_def = Define` 670 RPimp P Q pc reg ��� (P pc reg ��� Q pc reg) 671` 672 673val _ = set_mapped_fixity {tok = "=R=>", fixity = Infixr 200, 674 term_name = "RPimp"} 675 676val RPimp_thm = store_thm( 677 "RPimp_thm", 678 ``predOf (P =R=> Q) s ��� (predOf P s ==> predOf Q s)``, 679 srw_tac [][RPimp_def, predOf_def]) 680 681val _ = overload_on ("TT", ``K (K T) : num -> (num -> num) -> bool``) 682val RPimp_rwt = store_thm( 683 "RPimp_rwt", 684 ``(P =R=> P) = TT``, 685 srw_tac [][FUN_EQ_THM, RPimp_def]); 686val predOf_KK = store_thm( 687 "predOf_KK", 688 ``predOf (K (K v)) s = v``, 689 srw_tac [][predOf_def]); 690val REGfRsub_KK = store_thm( 691 "REGfRsub_KK", 692 ``REGfRsub (K (K v)) r f = K (K v)``, 693 srw_tac [][REGfRsub_def, FUN_EQ_THM]); 694val pAND_rwt = store_thm( 695 "pAND_rwt", 696 ``(TT && P = P) ��� (P && TT = P)``, 697 srw_tac [][FUN_EQ_THM, predOf_AND_def]); 698val _ = augment_srw_ss [rewrites [RPimp_rwt, predOf_KK, REGfRsub_KK, pAND_rwt]] 699 700 701val prepost_munge = store_thm( 702 "prepost_munge", 703 ``���P Q P' Q'. 704 HOARE P' c Q' ��� 705 (���s. predOf (P =R=> P') s) ��� (���s. predOf (Q' =R=> Q) s) ��� 706 HOARE P c Q``, 707 srw_tac [][HOARE_def, RPimp_def, predOf_def] >> metis_tac []); 708 709(* adjust while rule to have generic conclusion *) 710val RPWhile = save_thm( 711 "RPWhile", 712 RPWhile_rule |> UNDISCH 713 |> MATCH_MP (prepost_munge 714 |> REWRITE_RULE [Once (GSYM AND_IMP_INTRO)]) 715 |> SPEC_ALL |> DISCH_ALL 716 |> REWRITE_RULE [AND_IMP_INTRO] 717 |> (fn th => foldl (fn (v, th) => Q.GEN v th) th 718 [`pbi`, `ei`, `bi`, `p`, `reg`, 719 `Inv`, `Q`, `P`])) 720 721val INC_correct = store_thm( 722 "INC_correct", 723 ``ei ��� bi ��� 724 (���s. predOf (P =R=> PCeq bi && 725 REGfRsub (PCsub Q ei) r (��R. R r + 1)) 726 s) ��� 727 P ��� FEMPTY |+ (bi, INC r ei) ��� Q``, 728 srw_tac [][HOARE_def, predOf_def, PCeq_def, predOf_AND_def, RPimp_def, 729 REGfRsub_def, PCsub_def] >> 730 qexists_tac `1` >> 731 res_tac >> 732 srw_tac [][Step_def, firstHaltsAt_def, FLOOKUP_UPDATE, haltedConfig_def, 733 DECIDE ``m < 1 ��� (m = 0)``] >> 734 pop_assum mp_tac >> 735 qmatch_abbrev_tac `Q ei f1 ��� Q ei f2` >> 736 qsuff_tac `f1 = f2` >> srw_tac [][] >> 737 srw_tac [][Abbr`f2`, Abbr`f1`, saferead_update, 738 combinTheory.APPLY_UPDATE_THM, FUN_EQ_THM] >> 739 srw_tac [][saferead_update]); 740 741(* Implementations of the recursive functions *) 742(* results put into register 0; arguments in registers 1 .. n *) 743 744val zeroRP_def = Define` 745 zeroRP zr bi ei = RPWhile zr bi ei bi FEMPTY 746`; 747 748val zeroRP_correct = store_thm( 749 "zeroRP_correct", 750 ``bi ��� ei ��� 751 (���s. predOf (P =R=> PCeq bi && REGfRsub (PCsub Q ei) zr (K 0)) s) ��� 752 HOARE P (zeroRP zr bi ei) Q``, 753 srw_tac [][zeroRP_def] >> 754 match_mp_tac RPWhile >> 755 qexists_tac `REGfRsub (PCsub Q ei) zr (K 0)` >> 756 srw_tac [][] >| [ 757 srw_tac [][HOARE_def, predOf_AND_def, predOf_def, PCeq_def, rP_def, 758 REGfRsub_def, PCsub_def] >> qexists_tac `0` >> 759 fsrw_tac [][haltedConfig_def, combinTheory.UPDATE_EQ], 760 fsrw_tac [][RPimp_thm, predOf_AND_def, predOf_def, PCsub_def, 761 PCeq_def] >> 762 srw_tac [][predOf_def, PCsub_def, predOf_AND_def] >> 763 fsrw_tac [][REGfRsub_def, PCsub_def], 764 srw_tac [][predOf_def, REGfRsub_def, PCsub_def, predOf_AND_def, 765 RPimp_def, PCeq_def, rP_def] >> 766 metis_tac [combinTheory.APPLY_UPDATE_ID] 767 ]) 768 769val RPmove_def = Define` 770 RPmove src dest basei exiti = 771 RPWhile src basei exiti (basei + 1) 772 (FEMPTY |+ (basei + 1, INC dest basei)) 773` 774 775val SchirmerConseqAux = store_thm( 776 "SchirmerConseqAux", 777 ``���P' Q' P Q. 778 (���Z. P' Z ��� p ��� Q' Z) ��� 779 (���pc reg. P pc reg ��� 780 ���Z. P' Z pc reg ��� ���s. predOf (Q' Z =R=> Q) s) ��� 781 P ��� p ��� Q``, 782 srw_tac [][HOARE_def, predOf_def, RPimp_def] >> metis_tac []); 783 784val move_correct = store_thm( 785 "move_correct", 786 ``exiti ��� basei ��� exiti ��� basei + 1 ��� src ��� dest ��� 787 (���s. predOf 788 (P =R=> PCeq basei && 789 REGfRsub (REGfRsub (PCsub Q exiti) src (K 0)) 790 dest 791 (��r. r dest + r src)) 792 s) ��� 793 P ��� (RPmove src dest basei exiti) ��� Q``, 794 strip_tac >> 795 match_mp_tac (INST_TYPE [alpha |-> ``:num``] SchirmerConseqAux) >> 796 map_every qexists_tac [`��n. P && (��pc reg. reg src + reg dest = n)`, 797 `��n. Q`] >> 798 reverse (srw_tac [][]) 799 >- srw_tac [][predOf_AND_def, predOf_def, RPimp_def] >> 800 srw_tac [][RPmove_def] >> 801 match_mp_tac RPWhile >> 802 asm_simp_tac (srw_ss() ++ ARITH_ss) [] >> 803 qexists_tac `(��pc reg. reg src + reg dest = Z) && 804 REGfRsub (REGfRsub (PCsub Q exiti) src (K 0)) 805 dest 806 (��r. r dest + r src)` >> 807 rpt strip_tac 808 >- (match_mp_tac INC_correct >> 809 srw_tac [ARITH_ss][RPimp_thm, predOf_AND_thm, REGfRsub_ABS, 810 combinTheory.APPLY_UPDATE_THM] >> 811 fsrw_tac [][predOf_def, PCsub_def, REGfRsub_def, 812 combinTheory.APPLY_UPDATE_THM] >> 813 qpat_x_assum `Q exiti f` mp_tac >> 814 asm_simp_tac (srw_ss()) [combinTheory.UPDATE_EQ] >> 815 qpat_x_assum `x + y = z` mp_tac >> 816 asm_simp_tac (srw_ss()) [] >> 817 strip_tac >> 818 asm_simp_tac (srw_ss()) [Once combinTheory.UPDATE_COMMUTES, 819 SimpL ``(==>)``, 820 combinTheory.UPDATE_EQ] >> 821 srw_tac [ARITH_ss][Once combinTheory.UPDATE_COMMUTES]) 822 >- (srw_tac [ARITH_ss][RPimp_thm, predOf_AND_thm] >> 823 fsrw_tac [][predOf_def, RPimp_def] >> res_tac >> 824 fsrw_tac [][predOf_AND_def, PCeq_def]) >> 825 asm_simp_tac (srw_ss() ++ ARITH_ss) [RPimp_thm, predOf_AND_thm] >> 826 srw_tac [] [predOf_def, PCsub_def, REGfRsub_def] >> 827 qpat_x_assum `Q s.pc f` mp_tac >> 828 asm_simp_tac (srw_ss()) [combinTheory.UPDATE_APPLY_IMP_ID]); 829 830val RPcopy_def = Define` 831 RPcopy src dest tmp bi ei = 832 FUNION 833 (RPWhile src bi (bi + 3) (bi + 1) 834 (FUNION 835 (FEMPTY |+ (bi + 1, INC dest (bi + 2))) 836 (FEMPTY |+ (bi + 2, INC tmp bi)))) 837 (RPmove tmp src (bi + 3) ei) 838` 839 840val FDOM_RPWhile = store_thm( 841 "FDOM_RPWhile", 842 ``FDOM (RPWhile src bi ei pbi p) = bi INSERT FDOM p``, 843 srw_tac [][RPWhile_def, FUNION_DEF, EXTENSION]); 844val _ = export_rewrites ["FDOM_RPWhile"] 845 846val FDOM_RPmove = store_thm( 847 "FDOM_RPmove", 848 ``FDOM (RPmove src dest bi ei) = {bi; bi + 1}``, 849 srw_tac [][RPmove_def, FUNION_DEF, FDOM_RPWhile]); 850val _ = export_rewrites ["FDOM_RPmove"] 851 852val FDOM_RPcopy = store_thm( 853 "FDOM_RPcopy", 854 ``FDOM (RPcopy src dest tmp bi ei) = {bi; bi + 1; bi + 2; bi + 3; bi + 4}``, 855 srw_tac [][RPcopy_def, FUNION_DEF, FDOM_RPmove, FDOM_RPWhile] >> 856 srw_tac [ARITH_ss][EXTENSION]); 857val _ = export_rewrites ["FDOM_RPcopy"] 858 859val HOARE_skip = store_thm( 860 "HOARE_skip", 861 ``(���s. predOf (P =R=> Q) s) ==> P ��� FEMPTY ��� Q``, 862 srw_tac [][HOARE_def, predOf_def, RPimp_def] >> 863 qexists_tac `0` >> srw_tac [][haltedConfig_def]); 864 865 866val RPcopy_correct = store_thm( 867 "RPcopy_correct", 868 ``ALL_DISTINCT [src; dest; tmp] ��� 869 ei ��� { bi; bi + 1; bi + 2; bi + 3; bi + 4 } ��� 870 (���s. predOf 871 (P =R=> 872 PCeq bi && rP tmp ((=) 0) && 873 REGfRsub (PCsub Q ei) dest (��r. r dest + r src)) s) ��� 874 P ��� RPcopy src dest tmp bi ei ��� Q``, 875 srw_tac [][RPcopy_def] >> 876 match_mp_tac (GEN_ALL HOARE_sequence) >> 877 asm_simp_tac (srw_ss() ++ ARITH_ss) 878 [FDOM_RPWhile, FUNION_DEF, FDOM_RPmove] >> 879 qexists_tac `PCeq (bi + 3) && 880 REGfRsub (REGfRsub 881 (PCsub (Q && PC��� {bi; bi + 1; bi + 2}) ei) 882 tmp 883 (K 0)) 884 src 885 (��r. r src + r tmp)` >> 886 reverse conj_tac 887 >- (match_mp_tac move_correct >> 888 asm_simp_tac (srw_ss() ++ ARITH_ss) [RPimp_thm, predOf_AND_thm]) >> 889 qmatch_abbrev_tac `P ��� prog ��� (PCeq (bi + 3) && QQ)` >> 890 match_mp_tac (INST_TYPE [alpha |-> ``:num # num``] SchirmerConseqAux) >> 891 map_every qexists_tac [ 892 `��(S0,D0). rP src ((=) S0) && rP dest ((=)D0) && P`, 893 `��SD. PCeq (bi + 3) && QQ` 894 ] >> 895 simp_tac (srw_ss()) [pairTheory.EXISTS_PROD, pairTheory.FORALL_PROD] >> 896 reverse conj_tac 897 >- srw_tac [][rP_def, predOf_AND_def, predOf_def, RPimp_def] >> 898 map_every qx_gen_tac [`S0`, `D0`] >> 899 qunabbrev_tac `prog` >> match_mp_tac RPWhile >> 900 asm_simp_tac (srw_ss() ++ ARITH_ss) [FUNION_DEF] >> 901 qexists_tac ` 902 REGfRsub QQ dest (��r. r dest + r src) && 903 (��pc reg. (reg tmp + reg src = S0) ��� (reg dest + reg src = S0 + D0)) 904 ` >> srw_tac [][] >| [ 905 (* invariant preserved by body *) 906 match_mp_tac (GEN_ALL HOARE_sequence) >> 907 asm_simp_tac (srw_ss()) [] >> 908 qmatch_abbrev_tac `���R. Pre ��� c1 ��� R ��� R ��� c2 ��� Post` >> 909 qexists_tac ` 910 PCeq (bi + 2) && REGfRsub (PCsub Post bi) tmp (��r. r tmp + 1) 911 ` >> 912 reverse conj_tac 913 >- (qunabbrev_tac `c2` >> match_mp_tac INC_correct >> 914 srw_tac [ARITH_ss][]) >> 915 qunabbrev_tac `c1` >> match_mp_tac INC_correct >> 916 srw_tac [ARITH_ss][Abbr`Pre`, Abbr`Post`, Abbr`QQ`, RPimp_thm, 917 predOf_AND_thm, REGfRsub_ABS, 918 combinTheory.APPLY_UPDATE_THM] >> 919 qpat_x_assum `predOf (REGfRsub QQQ rrr fff) s` mp_tac >> 920 asm_simp_tac (srw_ss()) [predOf_def, REGfRsub_def, PCsub_def, 921 combinTheory.APPLY_UPDATE_THM] >> 922 qmatch_abbrev_tac `Q ei f1 ==> Q ei f2` >> 923 qsuff_tac `f1 = f2` >- srw_tac [][] >> 924 srw_tac [ARITH_ss][Abbr`f1`, Abbr`f2`, FUN_EQ_THM, 925 combinTheory.APPLY_UPDATE_THM], 926 927 (* invariant true initially *) 928 fsrw_tac [][RPimp_thm, predOf_AND_thm, Abbr`QQ`] >> strip_tac >> 929 res_tac >> 930 fsrw_tac [ARITH_ss][predOf_def, REGfRsub_def, PCsub_def, 931 combinTheory.APPLY_UPDATE_THM] >> 932 pop_assum mp_tac >> 933 qpat_x_assum `P pccc rrrr` (K ALL_TAC) >> 934 asm_simp_tac (srw_ss()) [combinTheory.UPDATE_APPLY_IMP_ID, 935 combinTheory.APPLY_UPDATE_THM], 936 937 (* post-condition established *) 938 asm_simp_tac (srw_ss()) [RPimp_thm, predOf_AND_thm] >> 939 srw_tac [][REGfRsub_def, predOf_def] >> 940 fsrw_tac [][] >> 941 qpat_x_assum `QQ (bi + 3) f2` mp_tac >> 942 qmatch_abbrev_tac `QQ (bi + 3) f1 ==> QQ (bi + 3) f2` >> 943 qsuff_tac `f1 = f2` >- srw_tac [][] >> 944 srw_tac [][Abbr`f1`, Abbr`f2`, combinTheory.APPLY_UPDATE_THM, 945 combinTheory.UPDATE_APPLY_IMP_ID] 946 ]) 947 948val listpresent_def = Define` 949 listpresent base l pc r ��� 950 ���j. j < LENGTH l ��� (r (j + base) = EL j l) 951`; 952 953val _ = overload_on ("initvec", ``listpresent 1``) 954 955val zeroset_def = Define` 956 zeroset s pc r ��� ���j. j ��� s ��� (r j = 0) 957`; 958 959val PCsub_listpresent = store_thm( 960 "PCsub_listpresent", 961 ``PCsub (listpresent b vec) pcval = listpresent b vec``, 962 srw_tac [][listpresent_def, FUN_EQ_THM, PCsub_def]); 963val _ = augment_srw_ss [rewrites [PCsub_listpresent]] 964 965val PCsub_zeroset = store_thm( 966 "PCsub_zeroset", 967 ``PCsub (zeroset tmps) pcval = zeroset tmps``, 968 srw_tac [][zeroset_def, PCsub_def, FUN_EQ_THM]); 969val _ = augment_srw_ss [rewrites [PCsub_zeroset]] 970 971val zeroset_concrete = store_thm( 972 "zeroset_concrete", 973 ``(zeroset {} = K (K T)) ��� 974 (zeroset (x INSERT s) = rP x ((=) 0) && zeroset s)``, 975 srw_tac [DNF_ss][zeroset_def, FUN_EQ_THM, rP_def, predOf_AND_def] >> 976 metis_tac []); 977val _ = augment_srw_ss [rewrites [zeroset_concrete]] 978 979val EL_LENGTH_LAST = store_thm( 980 "EL_LENGTH_LAST", 981 ``EL (LENGTH t) (h::t) = LAST (h::t)``, 982 qid_spec_tac `h` >> Induct_on `t` >> srw_tac [][]); 983 984val listpresent_concrete = store_thm( 985 "listpresent_concrete", 986 ``(listpresent b [] = K (K T))��� 987 (listpresent b (h::t) = rP b ((=) h) && listpresent (b + 1) t)``, 988 srw_tac [][listpresent_def, FUN_EQ_THM, predOf_AND_def, rP_def, 989 EQ_IMP_THM] >| 990 [ 991 pop_assum (qspec_then `0` mp_tac) >> srw_tac [][], 992 first_x_assum (qspec_then `SUC j` mp_tac) >> srw_tac [ARITH_ss][ADD1], 993 Cases_on `j` >> fsrw_tac [][] >> res_tac >> fsrw_tac [ARITH_ss][ADD1] 994 ]); 995 996val REGfRsub_listpresent = store_thm( 997 "REGfRsub_listpresent", 998 ``r < b ��� b + LENGTH l < r ��� 999 (REGfRsub (listpresent b l) r rf = listpresent b l)``, 1000 srw_tac [ARITH_ss][listpresent_def, FUN_EQ_THM, REGfRsub_def, 1001 combinTheory.APPLY_UPDATE_THM]); 1002val _ = augment_srw_ss [rewrites [REGfRsub_listpresent]] 1003 1004val REGfRsub_zeroset = store_thm( 1005 "REGfRsub_zeroset", 1006 ``i ��� s ��� (REGfRsub (zeroset s) i rf = zeroset s)``, 1007 srw_tac [COND_elim_ss, DNF_ss] 1008 [zeroset_def, REGfRsub_def, FUN_EQ_THM, 1009 combinTheory.APPLY_UPDATE_THM] >> metis_tac []); 1010val _ = augment_srw_ss [rewrites [REGfRsub_zeroset]] 1011 1012val implements_def = Define` 1013 implements rm temps bi ei f i = 1014 ���l. 1015 (LENGTH l = i) ��� (���j. j ��� temps ==> j > i) ==> 1016 (���r. (f l = SOME r) ==> 1017 (initvec l && zeroset temps && rP 0 ((=) 0) && PCeq bi) 1018 ��� 1019 rm 1020 ��� (initvec l && PCeq ei && rP 0 ((=) r))) ��� 1021 ((f l = NONE) ==> 1022 ��((initvec l && zeroset temps && rP 0 ((=) 0) && PCeq bi) ��� 1023 rm 1024 ��� K (K T))) 1025`; 1026 1027open recursivefnsTheory 1028 1029val implements_zero = store_thm( 1030 "implements_zero", 1031 ``implements FEMPTY {} i i (K (SOME 0)) 1``, 1032 srw_tac [][implements_def] >> 1033 match_mp_tac HOARE_skip >> 1034 srw_tac [][predOf_def, RPimp_def, predOf_AND_def]); 1035 1036val implements_SUC = store_thm( 1037 "implements_SUC", 1038 ``implements (FUNION (RPcopy 1 0 i bi (bi + 5)) 1039 (FEMPTY |+ (bi + 5, INC 0 (bi + 6)))) {i} bi (bi + 6) 1040 (SOME o succ) 1``, 1041 srw_tac [][implements_def] >> 1042 Cases_on `l` >> 1043 fsrw_tac [][listpresent_concrete, listTheory.LENGTH_NIL] >> 1044 srw_tac [][] >> 1045 match_mp_tac HOARE_sequence >> 1046 srw_tac [ARITH_ss][FDOM_RPcopy] >> 1047 qmatch_abbrev_tac `���R. P ��� c1 ��� R ��� R ��� c2 ��� Q` >> 1048 qexists_tac 1049 `REGfRsub (PCsub Q (bi + 6)) 0 (��r. r 0 + 1) && PCeq (bi + 5)` >> 1050 reverse conj_tac 1051 >- (srw_tac [][Abbr`c2`] >> 1052 match_mp_tac INC_correct >> 1053 srw_tac [][Abbr`Q`, predOf_def, predOf_AND_def, RPimp_def, 1054 PCsub_def, REGfRsub_def, PCeq_def, PCNOTIN_def, 1055 rP_def]) >> 1056 qunabbrev_tac `c1` >> 1057 match_mp_tac RPcopy_correct >> 1058 srw_tac [ARITH_ss][] >> 1059 srw_tac [ARITH_ss][Abbr`P`, Abbr`Q`] >> 1060 srw_tac [ARITH_ss][predOf_def, predOf_AND_thm, RPimp_thm] >> 1061 fsrw_tac [ARITH_ss][REGfRsub_def, combinTheory.APPLY_UPDATE_THM]); 1062 1063val implements_proj = store_thm( 1064 "implements_proj", 1065 ``i < n ��� implements (RPcopy (i + 1) 0 j bi (bi + 5)) {j} 1066 bi (bi + 5) (SOME o proj i) n``, 1067 srw_tac [][implements_def] >> 1068 match_mp_tac RPcopy_correct >> 1069 srw_tac [ARITH_ss][REGfRsub_def, RPimp_thm, predOf_AND_thm, 1070 combinTheory.APPLY_UPDATE_THM, 1071 primrecfnsTheory.proj_def] >> 1072 fsrw_tac [][predOf_def, listpresent_def]); 1073 1074val usedregs_def = Define` 1075 usedregs rmp = IMAGE (��a. case a of INC r p => r | TST r p1 p2 => r) 1076 (FRANGE rmp) 1077`; 1078 1079val usedregs_thm = store_thm( 1080 "usedregs_thm", 1081 ``(usedregs FEMPTY = {}) ��� 1082 (usedregs (fm |+ (p1, INC r p2)) = r INSERT usedregs (fm \\ p1)) ��� 1083 (usedregs (fm |+ (p1, TST r p2 p3)) = r INSERT usedregs (fm \\ p1)) ��� 1084 (DISJOINT (FDOM fm1) (FDOM fm2) ==> 1085 (usedregs (FUNION fm1 fm2) = usedregs fm1 UNION usedregs fm2))``, 1086 srw_tac [][usedregs_def, FRANGE_FUNION]); 1087val _ = export_rewrites ["usedregs_thm"] 1088 1089val FINITE_usedregs = store_thm( 1090 "FINITE_usedregs", 1091 ``FINITE (usedregs rmp)``, 1092 srw_tac [][usedregs_def]); 1093val _ = export_rewrites ["FINITE_usedregs"] 1094 1095val usedregs_RPwhile = store_thm( 1096 "usedregs_RPwhile", 1097 ``i ��� FDOM p ��� (usedregs (RPWhile tst i j k p) = tst INSERT usedregs p)``, 1098 srw_tac [][RPWhile_def, GSYM INSERT_SING_UNION]); 1099val _ = export_rewrites ["usedregs_RPwhile"] 1100 1101val usedregs_RPmove = store_thm( 1102 "usedregs_RPmove", 1103 ``usedregs (RPmove src dest bi ei) = {src;dest}``, 1104 srw_tac [ARITH_ss][RPmove_def]); 1105val _ = export_rewrites ["usedregs_RPmove"] 1106 1107val usedregs_RPcopy = store_thm( 1108 "usedregs_RPcopy", 1109 ``usedregs (RPcopy src dest tmp bi ei) = {src;dest;tmp}``, 1110 srw_tac [ARITH_ss][RPcopy_def] >> srw_tac [][EXTENSION] >> metis_tac []); 1111val _ = export_rewrites ["usedregs_RPcopy"] 1112 1113val unusedregs_RMstar = store_thm( 1114 "unusedregs_RMstar", 1115 ``r ��� usedregs rmp ��� ((RM* rmp n s).regs '' r = s.regs '' r)``, 1116 strip_tac >> qid_spec_tac `s` >> 1117 Induct_on `n` >> srw_tac [][FUNPOW, Step_def] >> 1118 `(FLOOKUP rmp s.pc = NONE) ��� (���r' p. FLOOKUP rmp s.pc = SOME (INC r' p)) ��� 1119 (���r' p1 p2. FLOOKUP rmp s.pc = SOME (TST r' p1 p2))` 1120 by metis_tac [TypeBase.nchotomy_of ``:'a option``, 1121 TypeBase.nchotomy_of ``:instr``] >> 1122 srw_tac [][] >> 1123 qsuff_tac `r ��� r'` >> srw_tac [][saferead_update] >| [ 1124 `INC r' p ��� FRANGE rmp` by METIS_TAC [FRANGE_FLOOKUP] >> 1125 fsrw_tac [][usedregs_def] >> 1126 first_x_assum (qspec_then `INC r' p` mp_tac) >> srw_tac [][], 1127 1128 `TST r' p1 p2 ��� FRANGE rmp` by METIS_TAC [FRANGE_FLOOKUP] >> 1129 fsrw_tac [][usedregs_def] >> 1130 first_x_assum (qspec_then `TST r' p1 p2` mp_tac) >> srw_tac [][] 1131 ]); 1132 1133val unusedregs_dont_change = store_thm( 1134 "unusedregs_dont_change", 1135 ``���n r. P ��� c ��� Q ��� r ��� usedregs c ��� 1136 (P && rP r ((=) n)) ��� c ��� (Q && rP r ((=) n))``, 1137 srw_tac [][HOARE_def, predOf_def, predOf_AND_def, rP_def] >> 1138 first_x_assum (qspec_then `s0` mp_tac) >> asm_simp_tac (srw_ss()) [] >> 1139 disch_then (Q.X_CHOOSE_THEN `m` strip_assume_tac) >> 1140 qexists_tac `m` >> srw_tac [][unusedregs_RMstar]); 1141 1142val recfn_arity_nonzero = store_thm( 1143 "recfn_arity_nonzero", 1144 ``���f i. recfn f i ��� 0 < i``, 1145 ho_match_mp_tac recfn_ind >> srw_tac [ARITH_ss][] >> 1146 fsrw_tac [][]); 1147 1148(* val theorem1 = store_thm( 1149 "theorem1", 1150 ``���f i. recfn f i ��� 1151 ���bi A. FINITE A ��� DISJOINT A { x | x < i + 1 } ��� 1152 ���ei temps rm. 1153 DISJOINT temps A ��� DISJOINT (usedregs rm) A ��� 1154 usedregs rm ��� temps ��� { x | x < i + 1 } ��� 1155 implements rm temps bi ei f i``, 1156 ho_match_mp_tac recfn_strongind >> rpt conj_tac >| [ 1157 (* zerof *) 1158 srw_tac [][] >> map_every qexists_tac [`bi`, `{}`, `FEMPTY`] >> 1159 srw_tac [][implements_zero], 1160 1161 (* succ *) 1162 srw_tac [][] >> 1163 qabbrev_tac `tmp = MAX_SET (3 INSERT A) + 1` >> 1164 `tmp ��� A ��� 3 < tmp` 1165 by (qunabbrev_tac `tmp` >> DEEP_INTRO_TAC MAX_SET_ELIM >> 1166 srw_tac [][DISJ_IMP_THM, FORALL_AND_THM] >> 1167 fsrw_tac [ARITH_ss][Once MONO_NOT_EQ]) >> 1168 `0 ��� A ��� 1 ��� A` 1169 by (conj_tac >> spose_not_then assume_tac >> 1170 fsrw_tac [][IN_DISJOINT, GSYM IMP_DISJ_THM] >> 1171 res_tac >> fsrw_tac [][]) >> 1172 map_every qexists_tac [`bi + 6`, `{tmp}`, 1173 `FUNION (RPcopy 1 0 tmp bi (bi + 5)) 1174 (FEMPTY |+ (bi + 5, INC 0 (bi + 6)))`] >> 1175 srw_tac [ARITH_ss][implements_SUC], 1176 1177 (* proj *) 1178 map_every qx_gen_tac [`i`, `n`] >> srw_tac [][] >> 1179 qabbrev_tac `tmp = MAX_SET (n INSERT A) + 1` >> 1180 `tmp ��� A ��� n < tmp` 1181 by (qunabbrev_tac `tmp` >> DEEP_INTRO_TAC MAX_SET_ELIM >> 1182 srw_tac [][DISJ_IMP_THM, FORALL_AND_THM] >> 1183 fsrw_tac [ARITH_ss][Once MONO_NOT_EQ]) >> 1184 `���i. i ��� A ��� n < i` 1185 by fsrw_tac [][IN_DISJOINT, GSYM IMP_DISJ_THM, 1186 DECIDE ``~(x < y + 1) <=> y < x``] >> 1187 map_every qexists_tac [`bi + 5`, `{tmp}`, 1188 `RPcopy (i + 1) 0 tmp bi (bi + 5)`] >> 1189 srw_tac [ARITH_ss][implements_proj] >> 1190 strip_tac >> res_tac >> fsrw_tac [ARITH_ss][], 1191 1192 (* composition *) 1193 srw_tac [][listTheory.EVERY_CONJ] >> 1194 ` 1195 1196*) 1197 1198val _ = export_theory(); 1199