175 where |
175 where |
176 "tinc_b \<equiv> [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4), |
176 "tinc_b \<equiv> [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4), |
177 (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6), |
177 (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6), |
178 (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]" |
178 (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]" |
179 |
179 |
|
180 (* FIXME: doubly defined |
180 text {* |
181 text {* |
181 @{text "tshift tm off"} shifts @{text "tm"} by offset @{text "off"}, leaving |
182 @{text "tshift tm off"} shifts @{text "tm"} by offset @{text "off"}, leaving |
182 instructions concerning state @{text "0"} unchanged, because state @{text "0"} |
183 instructions concerning state @{text "0"} unchanged, because state @{text "0"} |
183 is the end state, which needs not be changed with shift operation. |
184 is the end state, which needs not be changed with shift operation. |
184 *} |
185 *} |
186 fun tshift :: "tprog \<Rightarrow> nat \<Rightarrow> tprog" |
187 fun tshift :: "tprog \<Rightarrow> nat \<Rightarrow> tprog" |
187 where |
188 where |
188 "tshift tp off = (map (\<lambda> (action, state). |
189 "tshift tp off = (map (\<lambda> (action, state). |
189 (action, (if state = 0 then 0 |
190 (action, (if state = 0 then 0 |
190 else state + off))) tp)" |
191 else state + off))) tp)" |
|
192 *) |
191 |
193 |
192 text {* |
194 text {* |
193 @{text "tinc ss n"} returns the TM which simulates the execution of |
195 @{text "tinc ss n"} returns the TM which simulates the execution of |
194 Abacus instruction @{text "Inc n"}, assuming that TM is located at |
196 Abacus instruction @{text "Inc n"}, assuming that TM is located at |
195 location @{text "ss"} in the final TM complied from the whole |
197 location @{text "ss"} in the final TM complied from the whole |