equal
deleted
inserted
replaced
149 assumes "n = 1" |
149 assumes "n = 1" |
150 shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))" |
150 shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))" |
151 using assms by auto |
151 using assms by auto |
152 |
152 |
153 |
153 |
|
154 lemma layout: |
|
155 shows "layout_of [] = []" |
|
156 and "layout_of ((Inc R\<iota>)#os) = (2 * R\<iota> + 9)#(layout_of os)" |
|
157 and "layout_of ((Dec R\<iota> o\<iota>)#os) = (2 * R\<iota> + 16)#(layout_of os)" |
|
158 and "layout_of ((Goto o\<iota>)#os) = 1#(layout_of os)" |
|
159 by(auto simp add: layout_of.simps length_of.simps) |
|
160 |
|
161 |
154 (*>*) |
162 (*>*) |
155 |
163 |
156 section {* Introduction *} |
164 section {* Introduction *} |
157 |
165 |
158 |
166 |
1160 Turing machines, we fetch statements from an abacus program such |
1168 Turing machines, we fetch statements from an abacus program such |
1161 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1169 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1162 this way it is easy to define a function @{term steps} that |
1170 this way it is easy to define a function @{term steps} that |
1163 executes @{term n} statements of an abacus program. |
1171 executes @{term n} statements of an abacus program. |
1164 |
1172 |
|
1173 The main point of abacus programs is to be able to translate them to |
|
1174 Turing machine programs. Because of the jumps in abacus programs, it |
|
1175 seems difficult to build Turing machine programs using @{text "\<oplus>"}. |
|
1176 To overcome this difficulty we calculate a \emph{layout} as follows |
|
1177 |
|
1178 \begin{center} |
|
1179 @{thm layout} |
|
1180 \end{center} |
|
1181 |
1165 |
1182 |
1166 |
1183 |
1167 %Running an abacus program means to start |
1184 %Running an abacus program means to start |
1168 %A \emph{program} of an abacus machine is a list of such |
1185 %A \emph{program} of an abacus machine is a list of such |
1169 %statements. |
1186 %statements. |