93 |
93 |
94 lemma steps_add [simp]: |
94 lemma steps_add [simp]: |
95 shows "steps c p (m + n) = steps (steps c p m) p n" |
95 shows "steps c p (m + n) = steps (steps c p m) p n" |
96 by (induct m arbitrary: c) (auto) |
96 by (induct m arbitrary: c) (auto) |
97 |
97 |
98 fun |
|
99 tm_wf :: "tprog \<Rightarrow> bool" |
|
100 where |
|
101 "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> |
|
102 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))" |
|
103 |
|
104 lemma halt_lemma: |
|
105 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
106 by (metis wf_iff_no_infinite_down_chain) |
|
107 |
|
108 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
|
109 where "x \<up> n == replicate n x" |
|
110 |
|
111 consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100) |
|
112 |
|
113 fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" |
|
114 where |
|
115 "tape_of_nat_list [] = []" | |
|
116 "tape_of_nat_list [n] = Oc\<up>(Suc n)" | |
|
117 "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)" |
|
118 |
|
119 defs (overloaded) |
|
120 tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am" |
|
121 tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)" |
|
122 |
|
123 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool" |
|
124 where |
|
125 "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)" |
|
126 |
|
127 fun |
|
128 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
|
129 where |
|
130 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
|
131 |
|
132 fun |
|
133 adjust :: "instr list \<Rightarrow> instr list" |
|
134 where |
|
135 "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p" |
|
136 |
|
137 lemma length_shift [simp]: |
|
138 "length (shift p n) = length p" |
|
139 by simp |
|
140 |
|
141 lemma length_adjust[simp]: |
|
142 shows "length (adjust p) = length p" |
|
143 by (induct p) (auto) |
|
144 |
|
145 fun |
|
146 tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100) |
|
147 where |
|
148 "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))" |
|
149 |
|
150 lemma step_0 [simp]: |
98 lemma step_0 [simp]: |
151 shows "step (0, (l, r)) p = (0, (l, r))" |
99 shows "step (0, (l, r)) p = (0, (l, r))" |
152 by (case_tac p, simp) |
100 by (case_tac p, simp) |
153 |
101 |
154 lemma steps_0 [simp]: |
102 lemma steps_0 [simp]: |
155 shows "steps (0, (l, r)) p n = (0, (l, r))" |
103 shows "steps (0, (l, r)) p n = (0, (l, r))" |
156 by (induct n) (simp_all) |
104 by (induct n) (simp_all) |
157 |
105 |
|
106 |
|
107 |
158 fun |
108 fun |
159 is_final :: "config \<Rightarrow> bool" |
109 is_final :: "config \<Rightarrow> bool" |
160 where |
110 where |
161 "is_final (s, l, r) = (s = 0)" |
111 "is_final (s, l, r) = (s = 0)" |
|
112 |
|
113 lemma is_final_eq: |
|
114 shows "is_final (s, tp) = (s = 0)" |
|
115 by (case_tac tp) (auto) |
162 |
116 |
163 lemma is_final_steps: |
117 lemma is_final_steps: |
164 assumes "is_final (s, l, r)" |
118 assumes "is_final (s, l, r)" |
165 shows "is_final (steps (s, l, r) (p, off) n)" |
119 shows "is_final (steps (s, l, r) (p, off) n)" |
166 using assms by (induct n) (auto) |
120 using assms |
167 |
121 by (induct n) (auto) |
168 |
122 |
169 |
123 |
170 (* if the machine is in the halting state, there must have |
124 (* if the machine is in the halting state, there must have |
171 been a state just before the halting state *) |
125 been a state just before the halting state *) |
172 lemma before_final: |
126 lemma before_final: |
197 using asm cases by simp |
151 using asm cases by simp |
198 then show ?thesis by auto |
152 then show ?thesis by auto |
199 qed |
153 qed |
200 qed |
154 qed |
201 |
155 |
202 |
156 (* well-formedness of Turing machine programs *) |
203 lemma length_comp: |
157 fun |
|
158 tm_wf :: "tprog \<Rightarrow> bool" |
|
159 where |
|
160 "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> |
|
161 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))" |
|
162 |
|
163 lemma halt_lemma: |
|
164 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
165 by (metis wf_iff_no_infinite_down_chain) |
|
166 |
|
167 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
|
168 where "x \<up> n == replicate n x" |
|
169 |
|
170 consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100) |
|
171 |
|
172 fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" |
|
173 where |
|
174 "tape_of_nat_list [] = []" | |
|
175 "tape_of_nat_list [n] = Oc\<up>(Suc n)" | |
|
176 "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)" |
|
177 |
|
178 defs (overloaded) |
|
179 tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am" |
|
180 tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)" |
|
181 |
|
182 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool" |
|
183 where |
|
184 "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)" |
|
185 |
|
186 fun |
|
187 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
|
188 where |
|
189 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
|
190 |
|
191 fun |
|
192 adjust :: "instr list \<Rightarrow> instr list" |
|
193 where |
|
194 "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p" |
|
195 |
|
196 lemma length_shift [simp]: |
|
197 shows "length (shift p n) = length p" |
|
198 by simp |
|
199 |
|
200 lemma length_adjust [simp]: |
|
201 shows "length (adjust p) = length p" |
|
202 by (induct p) (auto) |
|
203 |
|
204 |
|
205 (* composition of two Turing machines *) |
|
206 fun |
|
207 tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100) |
|
208 where |
|
209 "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))" |
|
210 |
|
211 lemma tm_comp_length: |
204 shows "length (A |+| B) = length A + length B" |
212 shows "length (A |+| B) = length A + length B" |
205 by auto |
213 by auto |
206 |
214 |
207 declare steps.simps[simp del] |
215 lemma tm_comp_fetch_in_first: |
208 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
|
209 |
|
210 |
|
211 lemma tmcomp_fetch_in_first: |
|
212 assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0" |
216 assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0" |
213 shows "fetch (A |+| B) a x = fetch A a x" |
217 shows "fetch (A |+| B) a x = fetch A a x" |
214 using assms |
218 using assms |
215 apply(case_tac a, case_tac [!] x, |
219 apply(case_tac a) |
216 auto simp: length_comp tm_comp.simps length_adjust nth_append) |
220 apply(case_tac [!] x) |
217 apply(simp_all add: adjust.simps) |
221 apply(auto simp: tm_comp_length nth_append) |
218 done |
|
219 |
|
220 |
|
221 lemma is_final_eq: "is_final (ba, tp) = (ba = 0)" |
|
222 apply(case_tac tp, simp add: is_final.simps) |
|
223 done |
222 done |
224 |
223 |
225 lemma t_merge_pre_eq_step: |
224 lemma t_merge_pre_eq_step: |
226 assumes step: "step (a, b, c) (A, 0) = cf" |
225 assumes step: "step0 (s, l, r) A = cf" |
227 and tm_wf: "tm_wf (A, 0)" |
226 and tm_wf: "tm_wf (A, 0)" |
228 and unfinal: "\<not> is_final cf" |
227 and unfinal: "\<not> is_final cf" |
229 shows "step (a, b, c) (A |+| B, 0) = cf" |
228 shows "step0 (s, l, r) (A |+| B) = cf" |
230 proof - |
229 proof - |
231 have "fetch (A |+| B) a (read c) = fetch A a (read c)" |
230 from step unfinal |
232 proof(rule_tac tmcomp_fetch_in_first) |
231 have "\<not> is_final (step0 (s, l, r) A)" by simp |
233 from step and unfinal show "case fetch A a (read c) of (ac, ns) \<Rightarrow> ns \<noteq> 0" |
232 then have "fetch (A |+| B) s (read r) = fetch A s (read r)" |
234 apply(auto simp: is_final.simps) |
233 by (rule_tac tm_comp_fetch_in_first) (auto simp add: is_final_eq) |
235 apply(case_tac "fetch A a (read c)", simp_all add: is_final_eq) |
234 then show ?thesis |
236 done |
235 using step by auto |
237 qed |
236 qed |
238 thus "?thesis" |
237 |
239 using step |
238 declare steps.simps[simp del] |
240 apply(auto simp: step.simps is_final.simps) |
239 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
241 done |
|
242 qed |
|
243 |
|
244 declare tm_wf.simps[simp del] step.simps[simp del] |
240 declare tm_wf.simps[simp del] step.simps[simp del] |
245 |
241 |
246 lemma t_merge_pre_eq: |
242 lemma t_merge_pre_eq: |
247 "\<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> |
243 "\<lbrakk>steps0 (Suc 0, tp) A stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> |
248 \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf" |
244 \<Longrightarrow> steps0 (Suc 0, tp) (A |+| B) stp = cf" |
249 proof(induct stp arbitrary: cf, simp add: steps.simps) |
245 proof(induct stp arbitrary: cf, simp add: steps.simps) |
250 fix stp cf |
246 fix stp cf |
251 assume ind: "\<And>cf. \<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> |
247 assume ind: "\<And>cf. \<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> |
252 \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf" |
248 \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf" |
253 and h: "steps (Suc 0, tp) (A, 0) (Suc stp) = cf" |
249 and h: "steps (Suc 0, tp) (A, 0) (Suc stp) = cf" |
374 lemma tm_comp_fetch_second_zero: |
370 lemma tm_comp_fetch_second_zero: |
375 "\<lbrakk>fetch B sa' x = (a, 0); tm_wf (A, 0); tm_wf (B, 0); sa' > 0\<rbrakk> |
371 "\<lbrakk>fetch B sa' x = (a, 0); tm_wf (A, 0); tm_wf (B, 0); sa' > 0\<rbrakk> |
376 \<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)" |
372 \<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)" |
377 apply(case_tac x) |
373 apply(case_tac x) |
378 apply(case_tac [!] sa', |
374 apply(case_tac [!] sa', |
379 auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps |
375 auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps |
380 tm_wf.simps shift.simps split: if_splits) |
376 tm_wf.simps shift.simps split: if_splits) |
381 done |
377 done |
382 |
378 |
383 lemma tm_comp_fetch_second_inst: |
379 lemma tm_comp_fetch_second_inst: |
384 "\<lbrakk>sa > 0; s > 0; tm_wf (A, 0); tm_wf (B, 0); fetch B sa x = (a, s)\<rbrakk> |
380 "\<lbrakk>sa > 0; s > 0; tm_wf (A, 0); tm_wf (B, 0); fetch B sa x = (a, s)\<rbrakk> |
385 \<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)" |
381 \<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)" |
386 apply(case_tac x) |
382 apply(case_tac x) |
387 apply(case_tac [!] sa, |
383 apply(case_tac [!] sa, |
388 auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps |
384 auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps |
389 tm_wf.simps shift.simps split: if_splits) |
385 tm_wf.simps shift.simps split: if_splits) |
390 done |
386 done |
391 |
387 |
392 lemma t_merge_second_same: |
388 lemma t_merge_second_same: |
393 assumes a_wf: "tm_wf (A, 0)" |
389 assumes a_wf: "tm_wf (A, 0)" |