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