computability/register/register_machineScript.sml

16 val _ = Datatype `RegMachine = <| insts : instruction list; regs : num |-> num; pc : num |>`;
22 val reg_val_def = Define`reg_val regs n = case FLOOKUP regs n of NONE => 0n | SOME x => x `;
24 val upd_reg_def = Define`upd_reg f n regs = regs |+ (n,f (reg_val regs n))`;
29               Inc n => rm with <|regs updated_by upd_reg SUC n;pc updated_by SUC |>
30            |  Dec n => rm with <|regs updated_by upd_reg PRE n;pc updated_by SUC |>
31            | JZ n i b => if reg_val rm.regs n = 0 then rm with
33                              regs updated_by upd_reg (��x. x) n|>
44                   regs :=init_regs 2 input_list; pc := 0 |>`
64    ==> ���k. run_reg k rm = rm with <| pc := LENGTH pre + 3; regs := rm.regs |+(n,0) |>`,
65 Induct_on `reg_val rm.regs n` >> rw[]
66   >- (`reg_val rm.regs n = 0` by simp[] >> fs[] >> qexists_tac `SUC 0` >>
84 `��� args. (run_reg 2 (initial_reg succ_inst args)).regs ' 2 = succ args`,
88           >- (`�� (is_halted (<|insts := [Inc 2]; regs := FEMPTY; pc := 0|>))`
96 `��� args. if args = [] then (run_reg 2 (initial_reg zerof_inst args)).regs ' 2 = zerof args
97          else (run_reg (3 * HD args) (initial_reg zerof_inst args)).regs ' 2 = zerof args`,
114 EVAL ``(run_reg 11 (initial_reg (proj_inst 4) [1;2;3;4])).regs ' 2``;
119           ( (run_reg (11*LENGTH args) (initial_reg (proj_inst i) args)).regs ' 2 = proj i args)`,
123 `��� args. OPTION_MAP ((reg_fun Cn_inst args).regs 2) = Cn [nlist_of args]`,
127 `��� args. OPTION_MAP ((reg_fun Pr_inst args).regs 2) = Pr [nlist_of args]`,
131 `��� args. OPTION_MAP ((reg_fun min_inst args).regs 2) = min [nlist_of args]`,
137 `���f. ���inst. (��� args. OPTION_MAP ((reg_fun inst args).regs 2) = f args)`,