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