1open HolKernel Parse boolLib bossLib; 2open arithmeticTheory; 3open combinTheory; 4open whileTheory; 5open indexedListsTheory; 6open numeralTheory; 7open primrecfnsTheory; 8open listTheory; 9open mp_then; 10open boolTheory; 11open numpairTheory; 12open pred_setTheory; 13 14val _ = new_theory "rmModel"; 15 16 17Type reg = ���:num���; 18Type state = ���:num���; 19 20Datatype: 21 action = Inc num (state option) | Dec num (state option) (state option) 22End 23 24(* regOf :: action -> reg num *) 25Definition regOf_def[simp]: 26 regOf (Inc r _) = r ��� regOf (Dec r _ _) = r 27End 28 29(* inst_Val :: action -> value -> updated value *) 30Definition inst_Val_def[simp]: 31 inst_Val (Inc _ _) v = v + 1 /\ 32 inst_Val (Dec _ _ _) v = if v = 0 then 0 else v - 1 33End 34 35(* inst_Dest :: action -> value -> next state *) 36Definition inst_Dest_def[simp]: 37 inst_Dest (Inc _ s) v = s ��� 38 inst_Dest (Dec _ s1 s2) v = if v = 0 then s2 else s1 39End 40 41(* 42 ---------------------------------- 43 ----- Register Machine Model ----- 44 ---------------------------------- 45*) 46 47 48(* 49 Q : state set (each one represented with a number); 50 tf : state -> action (returns the action inside the state); 51 q0 : state (initial state); 52 I : reg list (input regs); 53 O : reg (output register); 54*) 55Datatype: 56 rm = <| 57 Q : state set; 58 tf : state -> action ; 59 q0 : state ; 60 In : reg list ; 61 Out : reg 62 |> 63End 64 65(* Initialise *) 66val init_machine_def = Define ` 67 init_machine m i = 68 ((��n. if findi n m.In = LENGTH m.In then 0 69 else EL (findi n m.In) i) 70 , 71 SOME m.q0) 72`; 73 74 75(* run machine :: machine -> (registers, state option) -> (registers, state option) *) 76val run_machine_1_def = Define ` 77 (run_machine_1 m (rs, NONE) = (rs, NONE)) 78 ��� 79 (run_machine_1 m (rs, SOME s) = if s ��� m.Q then (rs, NONE) 80 else case m.tf s of 81 | Inc r so => ( rs (| r |-> rs r + 1 |), so ) 82 | Dec r so1 so2 => if rs r > 0 then ( rs (| r |-> rs r - 1 |) , so1) 83 else ( rs, so2)) 84`; 85 86Theorem run_machine_1_alt: 87 (run_machine_1 m (rs, NONE) = (rs, NONE)) ��� 88 (run_machine_1 m (rs, SOME s) = if s ��� m.Q then (rs, NONE) 89 else let i = m.tf s; 90 r = regOf i 91 in (rs(|r |-> inst_Val i (rs r)|), inst_Dest i (rs r))) 92Proof 93 rw[run_machine_1_def] >> Cases_on`m.tf s` >> rw[] >> fs[] >> 94 rw[APPLY_UPDATE_THM, FUN_EQ_THM] >> rw[] >> rw[] 95QED 96 97val run_machine_def = Define ` 98 (run_machine m = WHILE (��(rs, so). so ��� NONE) (run_machine_1 m)) 99`; 100 101val rsf_def = Define ` 102 rsf m i = FST (run_machine m (init_machine m i)) 103`; 104 105val RUN_def = Define ` 106 RUN m i = FST (run_machine m (init_machine m i)) m.Out 107`; 108 109Definition conv_def: 110 (conv (SOME s) = s+1) ��� 111 (conv NONE = 0) 112End 113 114Definition strip_state_def: 115 strip_state action = case action of 116 | Inc _ so => [conv so] 117 | Dec _ so1 so2 => conv so1::[conv so2] 118End 119 120Definition opt_to_set_def[simp]: 121 opt_to_set (SOME q) = {q} ��� 122 opt_to_set NONE = {} 123End 124 125Definition action_states_def[simp]: 126 action_states (Inc r qopt) = opt_to_set qopt ��� 127 action_states (Dec r qopt1 qopt2) = opt_to_set qopt1 ��� opt_to_set qopt2 128End 129 130(* Definition of wellformedness of a register machine : 131 Has finite states initial state(q0) is in that machine's set of all states(Q), 132 and a valid state only transits to a valid state or NONE. 133*) 134val wfrm_def = Define ` 135 wfrm m ��� 136 FINITE m.Q ��� 137 m.q0 ��� m.Q ��� 138 (���s. s ��� m.Q ��� action_states (m.tf s) ��� m.Q) 139`; 140 141val rm_component_equality = theorem "rm_component_equality" 142 143val _ = export_theory () 144