203 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
203 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
204 where |
204 where |
205 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
205 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
206 |
206 |
207 fun |
207 fun |
208 adjust :: "instr list \<Rightarrow> instr list" |
208 adjust :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
209 where |
209 where |
210 "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p" |
210 "adjust p e = map (\<lambda> (a, s). (a, if s = 0 then e else s)) p" |
|
211 |
|
212 abbreviation |
|
213 "adjust0 p \<equiv> adjust p (Suc (length p div 2))" |
211 |
214 |
212 lemma length_shift [simp]: |
215 lemma length_shift [simp]: |
213 shows "length (shift p n) = length p" |
216 shows "length (shift p n) = length p" |
214 by simp |
217 by simp |
215 |
218 |
216 lemma length_adjust [simp]: |
219 lemma length_adjust [simp]: |
217 shows "length (adjust p) = length p" |
220 shows "length (adjust p n) = length p" |
218 by (induct p) (auto) |
221 by (induct p) (auto) |
219 |
222 |
220 |
223 |
221 (* composition of two Turing machines *) |
224 (* composition of two Turing machines *) |
222 fun |
225 fun |
223 tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100) |
226 tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100) |
224 where |
227 where |
225 "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))" |
228 "tm_comp p1 p2 = ((adjust0 p1) @ (shift p2 (length p1 div 2)))" |
226 |
229 |
227 lemma tm_comp_length: |
230 lemma tm_comp_length: |
228 shows "length (A |+| B) = length A + length B" |
231 shows "length (A |+| B) = length A + length B" |
229 by auto |
232 by auto |
230 |
233 |