|
1 (* Title: thys/Abacus_Mopup.thy |
|
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
|
3 *) |
|
4 |
|
5 header {* Mopup Turing Machine that deletes all "registers", except one *} |
|
6 |
|
7 theory Abacus_Mopup |
|
8 imports Uncomputable |
|
9 begin |
|
10 |
|
11 fun mopup_a :: "nat \<Rightarrow> instr list" |
|
12 where |
|
13 "mopup_a 0 = []" | |
|
14 "mopup_a (Suc n) = mopup_a n @ |
|
15 [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]" |
|
16 |
|
17 definition mopup_b :: "instr list" |
|
18 where |
|
19 "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3), |
|
20 (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]" |
|
21 |
|
22 fun mopup :: "nat \<Rightarrow> instr list" |
|
23 where |
|
24 "mopup n = mopup_a n @ shift mopup_b (2*n)" |
|
25 |
|
26 type_synonym mopup_type = "config \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> cell list \<Rightarrow> bool" |
|
27 |
|
28 fun mopup_stop :: "mopup_type" |
|
29 where |
|
30 "mopup_stop (s, l, r) lm n ires= |
|
31 (\<exists> ln rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = <lm ! n> @ Bk\<up>rn)" |
|
32 |
|
33 fun mopup_bef_erase_a :: "mopup_type" |
|
34 where |
|
35 "mopup_bef_erase_a (s, l, r) lm n ires= |
|
36 (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> |
|
37 r = Oc\<up>m@ Bk # <(drop ((s + 1) div 2) lm)> @ Bk\<up>rn)" |
|
38 |
|
39 fun mopup_bef_erase_b :: "mopup_type" |
|
40 where |
|
41 "mopup_bef_erase_b (s, l, r) lm n ires = |
|
42 (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = Bk # Oc\<up>m @ Bk # |
|
43 <(drop (s div 2) lm)> @ Bk\<up>rn)" |
|
44 |
|
45 fun mopup_jump_over1 :: "mopup_type" |
|
46 where |
|
47 "mopup_jump_over1 (s, l, r) lm n ires = |
|
48 (\<exists> ln m1 m2 rn. m1 + m2 = Suc (lm ! n) \<and> |
|
49 l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> |
|
50 (r = Oc\<up>m2 @ Bk # <(drop (Suc n) lm)> @ Bk\<up>rn \<or> |
|
51 (r = Oc\<up>m2 \<and> (drop (Suc n) lm) = [])))" |
|
52 |
|
53 fun mopup_aft_erase_a :: "mopup_type" |
|
54 where |
|
55 "mopup_aft_erase_a (s, l, r) lm n ires = |
|
56 (\<exists> lnl lnr rn (ml::nat list) m. |
|
57 m = Suc (lm ! n) \<and> l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> |
|
58 (r = <ml> @ Bk\<up>rn))" |
|
59 |
|
60 fun mopup_aft_erase_b :: "mopup_type" |
|
61 where |
|
62 "mopup_aft_erase_b (s, l, r) lm n ires= |
|
63 (\<exists> lnl lnr rn (ml::nat list) m. |
|
64 m = Suc (lm ! n) \<and> |
|
65 l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> |
|
66 (r = Bk # <ml> @ Bk\<up>rn \<or> |
|
67 r = Bk # Bk # <ml> @ Bk\<up>rn))" |
|
68 |
|
69 fun mopup_aft_erase_c :: "mopup_type" |
|
70 where |
|
71 "mopup_aft_erase_c (s, l, r) lm n ires = |
|
72 (\<exists> lnl lnr rn (ml::nat list) m. |
|
73 m = Suc (lm ! n) \<and> |
|
74 l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> |
|
75 (r = <ml> @ Bk\<up>rn \<or> r = Bk # <ml> @ Bk\<up>rn))" |
|
76 |
|
77 fun mopup_left_moving :: "mopup_type" |
|
78 where |
|
79 "mopup_left_moving (s, l, r) lm n ires = |
|
80 (\<exists> lnl lnr rn m. |
|
81 m = Suc (lm ! n) \<and> |
|
82 ((l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Bk\<up>rn) \<or> |
|
83 (l = Oc\<up>(m - 1) @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Oc # Bk\<up>rn)))" |
|
84 |
|
85 fun mopup_jump_over2 :: "mopup_type" |
|
86 where |
|
87 "mopup_jump_over2 (s, l, r) lm n ires = |
|
88 (\<exists> ln rn m1 m2. |
|
89 m1 + m2 = Suc (lm ! n) |
|
90 \<and> r \<noteq> [] |
|
91 \<and> (hd r = Oc \<longrightarrow> (l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> r = Oc\<up>m2 @ Bk\<up>rn)) |
|
92 \<and> (hd r = Bk \<longrightarrow> (l = Bk\<up>ln @ Bk # ires \<and> r = Bk # Oc\<up>(m1+m2)@ Bk\<up>rn)))" |
|
93 |
|
94 |
|
95 fun mopup_inv :: "mopup_type" |
|
96 where |
|
97 "mopup_inv (s, l, r) lm n ires = |
|
98 (if s = 0 then mopup_stop (s, l, r) lm n ires |
|
99 else if s \<le> 2*n then |
|
100 if s mod 2 = 1 then mopup_bef_erase_a (s, l, r) lm n ires |
|
101 else mopup_bef_erase_b (s, l, r) lm n ires |
|
102 else if s = 2*n + 1 then |
|
103 mopup_jump_over1 (s, l, r) lm n ires |
|
104 else if s = 2*n + 2 then mopup_aft_erase_a (s, l, r) lm n ires |
|
105 else if s = 2*n + 3 then mopup_aft_erase_b (s, l, r) lm n ires |
|
106 else if s = 2*n + 4 then mopup_aft_erase_c (s, l, r) lm n ires |
|
107 else if s = 2*n + 5 then mopup_left_moving (s, l, r) lm n ires |
|
108 else if s = 2*n + 6 then mopup_jump_over2 (s, l, r) lm n ires |
|
109 else False)" |
|
110 |
|
111 lemma mopup_fetch_0[simp]: |
|
112 "(fetch (mopup_a n @ shift mopup_b (2 * n)) 0 b) = (Nop, 0)" |
|
113 by(simp add: fetch.simps) |
|
114 |
|
115 lemma mop_bef_length[simp]: "length (mopup_a n) = 4 * n" |
|
116 apply(induct n, simp_all add: mopup_a.simps) |
|
117 done |
|
118 |
|
119 lemma mopup_a_nth: |
|
120 "\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = |
|
121 mopup_a (Suc q) ! ((4 * q) + x)" |
|
122 apply(induct n, simp) |
|
123 apply(case_tac "q < n", simp add: mopup_a.simps, auto) |
|
124 apply(simp add: nth_append) |
|
125 apply(subgoal_tac "q = n", simp) |
|
126 apply(arith) |
|
127 done |
|
128 |
|
129 lemma fetch_bef_erase_a_o[simp]: |
|
130 "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> |
|
131 \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc) = (W0, s + 1)" |
|
132 apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto) |
|
133 apply(subgoal_tac "length (mopup_a n) = 4*n") |
|
134 apply(auto simp: fetch.simps nth_of.simps nth_append) |
|
135 apply(subgoal_tac "mopup_a n ! (4 * q + 1) = |
|
136 mopup_a (Suc q) ! ((4 * q) + 1)", |
|
137 simp add: mopup_a.simps nth_append) |
|
138 apply(rule mopup_a_nth, auto) |
|
139 apply arith |
|
140 done |
|
141 |
|
142 lemma fetch_bef_erase_a_b[simp]: |
|
143 "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> |
|
144 \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s + 2)" |
|
145 apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto) |
|
146 apply(subgoal_tac "length (mopup_a n) = 4*n") |
|
147 apply(auto simp: fetch.simps nth_of.simps nth_append) |
|
148 apply(subgoal_tac "mopup_a n ! (4 * q + 0) = |
|
149 mopup_a (Suc q) ! ((4 * q + 0))", |
|
150 simp add: mopup_a.simps nth_append) |
|
151 apply(rule mopup_a_nth, auto) |
|
152 apply arith |
|
153 done |
|
154 |
|
155 lemma fetch_bef_erase_b_b: |
|
156 "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = 0\<rbrakk> \<Longrightarrow> |
|
157 (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)" |
|
158 apply(subgoal_tac "\<exists> q. s = 2 * q", auto) |
|
159 apply(case_tac qa, simp, simp) |
|
160 apply(auto simp: fetch.simps nth_of.simps nth_append) |
|
161 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = |
|
162 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
|
163 simp add: mopup_a.simps nth_append) |
|
164 apply(rule mopup_a_nth, auto) |
|
165 done |
|
166 |
|
167 lemma fetch_jump_over1_o: |
|
168 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Oc |
|
169 = (R, Suc (2 * n))" |
|
170 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
171 apply(auto simp: fetch.simps nth_of.simps mopup_b_def nth_append |
|
172 shift.simps) |
|
173 done |
|
174 |
|
175 lemma fetch_jump_over1_b: |
|
176 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk |
|
177 = (R, Suc (Suc (2 * n)))" |
|
178 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
179 apply(auto simp: fetch.simps nth_of.simps mopup_b_def |
|
180 nth_append shift.simps) |
|
181 done |
|
182 |
|
183 lemma fetch_aft_erase_a_o: |
|
184 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Oc |
|
185 = (W0, Suc (2 * n + 2))" |
|
186 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
187 apply(auto simp: fetch.simps nth_of.simps mopup_b_def |
|
188 nth_append shift.simps) |
|
189 done |
|
190 |
|
191 lemma fetch_aft_erase_a_b: |
|
192 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk |
|
193 = (L, Suc (2 * n + 4))" |
|
194 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
195 apply(auto simp: fetch.simps nth_of.simps mopup_b_def |
|
196 nth_append shift.simps) |
|
197 done |
|
198 |
|
199 lemma fetch_aft_erase_b_b: |
|
200 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2*n + 3) Bk |
|
201 = (R, Suc (2 * n + 3))" |
|
202 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
203 apply(subgoal_tac "2*n + 3 = Suc (2*n + 2)", simp only: fetch.simps) |
|
204 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
205 done |
|
206 |
|
207 lemma fetch_aft_erase_c_o: |
|
208 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Oc |
|
209 = (W0, Suc (2 * n + 2))" |
|
210 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
211 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) |
|
212 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
213 done |
|
214 |
|
215 lemma fetch_aft_erase_c_b: |
|
216 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk |
|
217 = (R, Suc (2 * n + 1))" |
|
218 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
219 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) |
|
220 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
221 done |
|
222 |
|
223 lemma fetch_left_moving_o: |
|
224 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Oc) |
|
225 = (L, 2*n + 6)" |
|
226 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
227 apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps) |
|
228 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
229 done |
|
230 |
|
231 lemma fetch_left_moving_b: |
|
232 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk) |
|
233 = (L, 2*n + 5)" |
|
234 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
235 apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps) |
|
236 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
237 done |
|
238 |
|
239 lemma fetch_jump_over2_b: |
|
240 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Bk) |
|
241 = (R, 0)" |
|
242 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
243 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) |
|
244 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
245 done |
|
246 |
|
247 lemma fetch_jump_over2_o: |
|
248 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Oc) |
|
249 = (L, 2*n + 6)" |
|
250 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
251 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) |
|
252 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
253 done |
|
254 |
|
255 lemmas mopupfetchs = |
|
256 fetch_bef_erase_a_o fetch_bef_erase_a_b fetch_bef_erase_b_b |
|
257 fetch_jump_over1_o fetch_jump_over1_b fetch_aft_erase_a_o |
|
258 fetch_aft_erase_a_b fetch_aft_erase_b_b fetch_aft_erase_c_o |
|
259 fetch_aft_erase_c_b fetch_left_moving_o fetch_left_moving_b |
|
260 fetch_jump_over2_b fetch_jump_over2_o |
|
261 |
|
262 declare |
|
263 mopup_jump_over2.simps[simp del] mopup_left_moving.simps[simp del] |
|
264 mopup_aft_erase_c.simps[simp del] mopup_aft_erase_b.simps[simp del] |
|
265 mopup_aft_erase_a.simps[simp del] mopup_jump_over1.simps[simp del] |
|
266 mopup_bef_erase_a.simps[simp del] mopup_bef_erase_b.simps[simp del] |
|
267 mopup_stop.simps[simp del] |
|
268 |
|
269 lemma [simp]: |
|
270 "\<lbrakk>mopup_bef_erase_a (s, l, Oc # xs) lm n ires\<rbrakk> \<Longrightarrow> |
|
271 mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires" |
|
272 apply(auto simp: mopup_bef_erase_a.simps mopup_bef_erase_b.simps ) |
|
273 apply(rule_tac x = "m - 1" in exI, rule_tac x = rn in exI) |
|
274 apply(case_tac m, simp, simp add: replicate_Suc) |
|
275 done |
|
276 |
|
277 lemma mopup_false1: |
|
278 "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc s \<le> 2 * n\<rbrakk> |
|
279 \<Longrightarrow> RR" |
|
280 apply(arith) |
|
281 done |
|
282 |
|
283 lemma [simp]: |
|
284 "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; |
|
285 mopup_bef_erase_a (s, l, Oc # xs) lm n ires; r = Oc # xs\<rbrakk> |
|
286 \<Longrightarrow> (Suc s \<le> 2 * n \<longrightarrow> mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires) \<and> |
|
287 (\<not> Suc s \<le> 2 * n \<longrightarrow> mopup_jump_over1 (Suc s, l, Bk # xs) lm n ires) " |
|
288 apply(auto elim: mopup_false1) |
|
289 done |
|
290 |
|
291 lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m) |
|
292 else Oc\<up>(Suc m) @ Bk # <lm>)" |
|
293 apply(case_tac lm, simp_all add: tape_of_nl_abv tape_of_nat_abv split: if_splits) |
|
294 done |
|
295 |
|
296 lemma drop_tape_of_cons: |
|
297 "\<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>" |
|
298 by (metis Suc_lessD append_Cons list.simps(2) nth_drop' replicate_Suc tape_of_nl_cons) |
|
299 |
|
300 lemma erase2jumpover1: |
|
301 "\<lbrakk>q < length list; |
|
302 \<forall>rn. <drop q list> \<noteq> Oc # Oc \<up> (list ! q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> |
|
303 \<Longrightarrow> <drop q list> = Oc # Oc \<up> (list ! q)" |
|
304 apply(erule_tac x = 0 in allE, simp) |
|
305 apply(case_tac "Suc q < length list") |
|
306 apply(erule_tac notE) |
|
307 apply(rule_tac drop_tape_of_cons, simp_all) |
|
308 apply(subgoal_tac "length list = Suc q", auto) |
|
309 apply(subgoal_tac "drop q list = [list ! q]") |
|
310 apply(simp add: tape_of_nl_abv tape_of_nat_abv replicate_Suc) |
|
311 by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI) |
|
312 |
|
313 lemma erase2jumpover2: |
|
314 "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> |
|
315 Oc # Oc \<up> (list ! q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> |
|
316 \<Longrightarrow> RR" |
|
317 apply(case_tac "Suc q < length list") |
|
318 apply(erule_tac x = "Suc n" in allE, simp) |
|
319 apply(erule_tac notE, simp add: replicate_Suc) |
|
320 apply(rule_tac drop_tape_of_cons, simp_all) |
|
321 apply(subgoal_tac "length list = Suc q", auto) |
|
322 apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv) |
|
323 by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons) |
|
324 |
|
325 lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))" |
|
326 by arith |
|
327 |
|
328 declare replicate_Suc[simp] |
|
329 |
|
330 lemma mopup_bef_erase_a_2_jump_over[simp]: |
|
331 "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; |
|
332 mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> (Suc (Suc s) \<le> 2 * n)\<rbrakk> |
|
333 \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires" |
|
334 apply(auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps) |
|
335 apply(case_tac m, auto simp: mod_ex1) |
|
336 apply(subgoal_tac "n = Suc q", auto) |
|
337 apply(rule_tac x = "Suc ln" in exI, rule_tac x = 0 in exI, auto) |
|
338 apply(case_tac [!] lm, simp_all) |
|
339 apply(case_tac [!] rn, auto elim: erase2jumpover1 erase2jumpover2) |
|
340 apply(erule_tac x = 0 in allE, simp) |
|
341 apply(rule_tac classical, simp) |
|
342 apply(erule_tac notE) |
|
343 apply(rule_tac drop_tape_of_cons, simp_all) |
|
344 done |
|
345 |
|
346 lemma Suc_Suc_div: "\<lbrakk>0 < s; s mod 2 = Suc 0; Suc (Suc s) \<le> 2 * n\<rbrakk> |
|
347 \<Longrightarrow> (Suc (Suc (s div 2))) \<le> n" |
|
348 apply(arith) |
|
349 done |
|
350 |
|
351 lemma mopup_bef_erase_a_2_a[simp]: |
|
352 "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; |
|
353 mopup_bef_erase_a (s, l, Bk # xs) lm n ires; |
|
354 Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> |
|
355 mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires" |
|
356 apply(auto simp: mopup_bef_erase_a.simps) |
|
357 apply(subgoal_tac "drop (Suc (Suc (s div 2))) lm \<noteq> []") |
|
358 apply(case_tac m, simp_all) |
|
359 apply(rule_tac x = "Suc ln" in exI, simp) |
|
360 apply arith |
|
361 apply(case_tac m, simp_all) |
|
362 apply(rule_tac x = "Suc (lm ! (Suc s div 2))" in exI, simp) |
|
363 apply(rule_tac x = rn in exI, simp) |
|
364 apply(rule_tac drop_tape_of_cons, simp, auto) |
|
365 done |
|
366 |
|
367 lemma mopup_false2: |
|
368 "\<lbrakk>0 < s; s \<le> 2 * n; |
|
369 s mod 2 = Suc 0; Suc s \<noteq> 2 * n; |
|
370 \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> RR" |
|
371 apply(arith) |
|
372 done |
|
373 |
|
374 lemma [simp]: "mopup_bef_erase_a (s, l, []) lm n ires \<Longrightarrow> |
|
375 mopup_bef_erase_a (s, l, [Bk]) lm n ires" |
|
376 apply(auto simp: mopup_bef_erase_a.simps) |
|
377 done |
|
378 |
|
379 lemma [simp]: |
|
380 "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc (Suc s) \<le> 2 *n; |
|
381 mopup_bef_erase_a (s, l, []) lm n ires\<rbrakk> |
|
382 \<Longrightarrow> mopup_jump_over1 (s', Bk # l, []) lm n ires" |
|
383 by auto |
|
384 |
|
385 lemma "mopup_bef_erase_b (s, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
386 apply(auto simp: mopup_bef_erase_b.simps) |
|
387 done |
|
388 |
|
389 lemma [simp]: "mopup_bef_erase_b (s, l, Oc # xs) lm n ires = False" |
|
390 apply(auto simp: mopup_bef_erase_b.simps ) |
|
391 done |
|
392 |
|
393 lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> |
|
394 (s - Suc 0) mod 2 = Suc 0" |
|
395 apply(arith) |
|
396 done |
|
397 |
|
398 lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> |
|
399 s - Suc 0 \<le> 2 * n" |
|
400 apply(simp) |
|
401 done |
|
402 |
|
403 lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> \<not> s \<le> Suc 0" |
|
404 apply(arith) |
|
405 done |
|
406 |
|
407 lemma [simp]: "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; |
|
408 s mod 2 \<noteq> Suc 0; |
|
409 mopup_bef_erase_b (s, l, Bk # xs) lm n ires; r = Bk # xs\<rbrakk> |
|
410 \<Longrightarrow> mopup_bef_erase_a (s - Suc 0, Bk # l, xs) lm n ires" |
|
411 apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps) |
|
412 apply(rule_tac x = "Suc ln" in exI, simp) |
|
413 done |
|
414 |
|
415 lemma [simp]: "\<lbrakk>mopup_bef_erase_b (s, l, []) lm n ires\<rbrakk> \<Longrightarrow> |
|
416 mopup_bef_erase_a (s - Suc 0, Bk # l, []) lm n ires" |
|
417 apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps) |
|
418 done |
|
419 |
|
420 lemma [simp]: |
|
421 "\<lbrakk>n < length lm; |
|
422 mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires; |
|
423 r = Oc # xs\<rbrakk> |
|
424 \<Longrightarrow> mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires" |
|
425 apply(auto simp: mopup_jump_over1.simps) |
|
426 apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI, |
|
427 rule_tac x = "m2 - 1" in exI, simp) |
|
428 apply(case_tac "m2", simp, simp) |
|
429 apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI, |
|
430 rule_tac x = "m2 - 1" in exI) |
|
431 apply(case_tac m2, simp, simp) |
|
432 done |
|
433 |
|
434 lemma mopup_jump_over1_2_aft_erase_a[simp]: |
|
435 "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires\<rbrakk> |
|
436 \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires" |
|
437 apply(simp only: mopup_jump_over1.simps mopup_aft_erase_a.simps) |
|
438 apply(erule_tac exE)+ |
|
439 apply(rule_tac x = ln in exI, rule_tac x = "Suc 0" in exI) |
|
440 apply(case_tac m2, simp) |
|
441 apply(rule_tac x = rn in exI, rule_tac x = "drop (Suc n) lm" in exI, |
|
442 simp) |
|
443 apply(simp) |
|
444 done |
|
445 |
|
446 lemma [simp]: |
|
447 "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, []) lm n ires\<rbrakk> \<Longrightarrow> |
|
448 mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires" |
|
449 apply(rule mopup_jump_over1_2_aft_erase_a, simp) |
|
450 apply(auto simp: mopup_jump_over1.simps) |
|
451 apply(rule_tac x = ln in exI, rule_tac x = "Suc (lm ! n)" in exI, |
|
452 rule_tac x = 0 in exI, simp add: tape_of_nl_abv ) |
|
453 done |
|
454 |
|
455 lemma [simp]: "<[]> = []" |
|
456 apply(simp add: tape_of_nl_abv) |
|
457 done |
|
458 |
|
459 lemma [simp]: |
|
460 "\<lbrakk>n < length lm; |
|
461 mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires\<rbrakk> |
|
462 \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires" |
|
463 apply(auto simp: mopup_aft_erase_a.simps mopup_aft_erase_b.simps ) |
|
464 apply(case_tac ml) |
|
465 apply(simp_all add: tape_of_nl_cons split: if_splits) |
|
466 apply(case_tac rn, simp_all) |
|
467 apply(case_tac a, simp_all) |
|
468 apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) |
|
469 apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp) |
|
470 apply(case_tac a, simp, simp add: tape_of_nl_abv tape_of_nat_abv) |
|
471 apply(case_tac a, simp_all) |
|
472 apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp) |
|
473 apply(rule_tac x = rn in exI, simp) |
|
474 apply(rule_tac x = "nat # list" in exI, simp add: tape_of_nl_cons) |
|
475 done |
|
476 |
|
477 lemma [simp]: |
|
478 "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
479 apply(auto simp: mopup_aft_erase_a.simps) |
|
480 done |
|
481 |
|
482 lemma [simp]: |
|
483 "\<lbrakk>n < length lm; |
|
484 mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires\<rbrakk> |
|
485 \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires" |
|
486 apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps) |
|
487 apply(erule exE)+ |
|
488 apply(case_tac lnr, simp) |
|
489 apply(case_tac ml, auto simp: tape_of_nl_cons) |
|
490 apply(case_tac ml, auto simp: tape_of_nl_cons) |
|
491 apply(rule_tac x = "Suc rn" in exI, simp) |
|
492 done |
|
493 |
|
494 lemma [simp]: |
|
495 "mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires \<Longrightarrow> l \<noteq> []" |
|
496 apply(simp only: mopup_aft_erase_a.simps) |
|
497 apply(erule exE)+ |
|
498 apply(auto) |
|
499 done |
|
500 |
|
501 lemma [simp]: |
|
502 "\<lbrakk>n < length lm; mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires\<rbrakk> |
|
503 \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires" |
|
504 apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps) |
|
505 apply(erule exE)+ |
|
506 apply(subgoal_tac "ml = [] \<and> rn = 0", erule conjE, erule conjE, simp) |
|
507 apply(case_tac lnr, simp) |
|
508 apply(rule_tac x = lnl in exI, auto) |
|
509 apply(rule_tac x = 1 in exI, simp) |
|
510 apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits) |
|
511 done |
|
512 |
|
513 lemma [simp]: "mopup_aft_erase_b (2 * n + 3, l, Oc # xs) lm n ires = False" |
|
514 apply(auto simp: mopup_aft_erase_b.simps ) |
|
515 done |
|
516 |
|
517 lemma tape_of_ex1[intro]: |
|
518 "\<exists>rna ml. Oc \<up> a @ Bk \<up> rn = <ml::nat list> @ Bk \<up> rna \<or> Oc \<up> a @ Bk \<up> rn = Bk # <ml> @ Bk \<up> rna" |
|
519 apply(case_tac a, simp_all) |
|
520 apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) |
|
521 apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp) |
|
522 apply(simp add: tape_of_nl_abv tape_of_nat_abv) |
|
523 done |
|
524 |
|
525 lemma [intro]: "\<exists>rna ml. Oc \<up> a @ Bk # <list::nat list> @ Bk \<up> rn = |
|
526 <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml::nat list> @ Bk \<up> rna" |
|
527 apply(case_tac "list = []", simp add: replicate_Suc[THEN sym] del: replicate_Suc) |
|
528 apply(rule_tac rn = "Suc rn" in tape_of_ex1) |
|
529 apply(case_tac a, simp) |
|
530 apply(rule_tac x = rn in exI, rule_tac x = list in exI, simp) |
|
531 apply(rule_tac x = rn in exI, rule_tac x = "nat # list" in exI) |
|
532 apply(simp add: tape_of_nl_cons) |
|
533 done |
|
534 |
|
535 lemma [simp]: |
|
536 "\<lbrakk>n < length lm; |
|
537 mopup_aft_erase_c (2 * n + 4, l, Oc # xs) lm n ires\<rbrakk> |
|
538 \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires" |
|
539 apply(auto simp: mopup_aft_erase_c.simps mopup_aft_erase_b.simps ) |
|
540 apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits, auto) |
|
541 apply(case_tac rn, simp_all) |
|
542 done |
|
543 |
|
544 lemma mopup_aft_erase_c_aft_erase_a[simp]: |
|
545 "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, Bk # xs) lm n ires\<rbrakk> |
|
546 \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires" |
|
547 apply(simp only: mopup_aft_erase_c.simps mopup_aft_erase_a.simps ) |
|
548 apply(erule_tac exE)+ |
|
549 apply(erule conjE, erule conjE, erule disjE) |
|
550 apply(subgoal_tac "ml = []", simp, case_tac rn, |
|
551 simp, simp, rule conjI) |
|
552 apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp) |
|
553 apply(rule_tac x = nat in exI, rule_tac x = "[]" in exI, simp) |
|
554 apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits) |
|
555 apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp) |
|
556 apply(rule_tac x = rn in exI, rule_tac x = "ml" in exI, simp) |
|
557 done |
|
558 |
|
559 lemma [simp]: |
|
560 "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, []) lm n ires\<rbrakk> |
|
561 \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires" |
|
562 apply(rule mopup_aft_erase_c_aft_erase_a, simp) |
|
563 apply(simp only: mopup_aft_erase_c.simps) |
|
564 apply(erule exE)+ |
|
565 apply(rule_tac x = lnl in exI, rule_tac x = lnr in exI, simp add: ) |
|
566 apply(rule_tac x = 0 in exI, rule_tac x = "[]" in exI, simp) |
|
567 done |
|
568 |
|
569 lemma mopup_aft_erase_b_2_aft_erase_c[simp]: |
|
570 "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires\<rbrakk> |
|
571 \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires" |
|
572 apply(auto simp: mopup_aft_erase_b.simps mopup_aft_erase_c.simps) |
|
573 apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp) |
|
574 apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp) |
|
575 done |
|
576 |
|
577 lemma [simp]: |
|
578 "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, []) lm n ires\<rbrakk> |
|
579 \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, []) lm n ires" |
|
580 apply(rule_tac mopup_aft_erase_b_2_aft_erase_c, simp) |
|
581 apply(simp add: mopup_aft_erase_b.simps) |
|
582 done |
|
583 |
|
584 lemma [simp]: |
|
585 "mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
586 apply(auto simp: mopup_left_moving.simps) |
|
587 done |
|
588 |
|
589 lemma exp_ind: "a\<up>(Suc x) = a\<up>x @ [a]" |
|
590 apply(induct x, auto) |
|
591 done |
|
592 |
|
593 lemma [simp]: |
|
594 "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires\<rbrakk> |
|
595 \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires" |
|
596 apply(simp only: mopup_left_moving.simps mopup_jump_over2.simps) |
|
597 apply(erule_tac exE)+ |
|
598 apply(erule conjE, erule disjE, erule conjE) |
|
599 apply(case_tac rn, simp, simp add: ) |
|
600 apply(case_tac "hd l", simp add: ) |
|
601 apply(case_tac "lm ! n", simp) |
|
602 apply(rule_tac x = "lnl" in exI, rule_tac x = rn in exI, |
|
603 rule_tac x = "Suc 0" in exI, rule_tac x = 0 in exI) |
|
604 apply(case_tac lnl, simp,simp, simp add: exp_ind[THEN sym]) |
|
605 apply(case_tac "lm ! n", simp) |
|
606 apply(case_tac lnl, simp, simp) |
|
607 apply(rule_tac x = lnl in exI, rule_tac x = rn in exI, auto) |
|
608 apply(case_tac "lm ! n", simp) |
|
609 apply(case_tac lnl, simp_all add: numeral_2_eq_2) |
|
610 done |
|
611 |
|
612 lemma [simp]: "mopup_left_moving (2 * n + 5, l, xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
613 apply(auto simp: mopup_left_moving.simps) |
|
614 done |
|
615 |
|
616 lemma [simp]: |
|
617 "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Bk # xs) lm n ires\<rbrakk> |
|
618 \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, hd l # Bk # xs) lm n ires" |
|
619 apply(simp only: mopup_left_moving.simps) |
|
620 apply(erule exE)+ |
|
621 apply(case_tac lnr, auto) |
|
622 apply(rule_tac x = "Suc rn" in exI, simp) |
|
623 done |
|
624 |
|
625 lemma [simp]: |
|
626 "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, []) lm n ires\<rbrakk> |
|
627 \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, [hd l]) lm n ires" |
|
628 apply(simp only: mopup_left_moving.simps) |
|
629 apply(erule exE)+ |
|
630 apply(case_tac lnr, auto) |
|
631 apply(rule_tac x = 1 in exI, simp) |
|
632 done |
|
633 |
|
634 |
|
635 lemma [simp]: |
|
636 "mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
637 apply(auto simp: mopup_jump_over2.simps ) |
|
638 done |
|
639 |
|
640 lemma [simp]: |
|
641 "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires\<rbrakk> |
|
642 \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires" |
|
643 apply(simp only: mopup_jump_over2.simps) |
|
644 apply(erule_tac exE)+ |
|
645 apply(simp add: , erule conjE, erule_tac conjE) |
|
646 apply(case_tac m1, simp) |
|
647 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, |
|
648 rule_tac x = 0 in exI, simp) |
|
649 apply(case_tac ln, simp, simp, simp only: exp_ind[THEN sym], simp) |
|
650 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, |
|
651 rule_tac x = nat in exI, rule_tac x = "Suc m2" in exI, simp) |
|
652 done |
|
653 |
|
654 lemma [simp]: |
|
655 "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\<rbrakk> |
|
656 \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires" |
|
657 apply(auto simp: mopup_jump_over2.simps mopup_stop.simps) |
|
658 apply(simp_all add: tape_of_nat_abv exp_ind[THEN sym]) |
|
659 done |
|
660 |
|
661 lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False" |
|
662 apply(simp only: mopup_jump_over2.simps, simp) |
|
663 done |
|
664 |
|
665 declare fetch.simps[simp del] |
|
666 lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)" |
|
667 by arith |
|
668 |
|
669 (* |
|
670 lemma [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0) " |
|
671 by arith |
|
672 |
|
673 lemma [simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0) " |
|
674 by arith |
|
675 |
|
676 |
|
677 lemma [simp]: "(2*q - Suc 0) div 2 = (q - 1)" |
|
678 by arith |
|
679 |
|
680 lemma [simp]: "(Suc (2*q)) div 2 = q" |
|
681 by arith |
|
682 *) |
|
683 lemma mod_2: "x mod 2 = 0 \<or> x mod 2 = Suc 0" |
|
684 by arith |
|
685 |
|
686 lemma mopup_inv_step: |
|
687 "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> |
|
688 \<Longrightarrow> mopup_inv (step (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)) lm n ires" |
|
689 apply(case_tac r, case_tac [2] a) |
|
690 apply(auto split:if_splits simp add:step.simps) |
|
691 apply(simp_all add: mopupfetchs) |
|
692 apply(drule_tac mopup_false2, simp_all) |
|
693 apply(drule_tac mopup_false2, simp_all) |
|
694 by (metis Suc_n_not_n mod2_Suc_Suc mod_ex1 mod_mult_self1_is_0) |
|
695 |
|
696 declare mopup_inv.simps[simp del] |
|
697 lemma mopup_inv_steps: |
|
698 "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> |
|
699 mopup_inv (steps (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp) lm n ires" |
|
700 apply(induct_tac stp, simp add: steps.simps) |
|
701 apply(simp add: step_red) |
|
702 apply(case_tac "steps (s, l, r) |
|
703 (mopup_a n @ shift mopup_b (2 * n), 0) na", simp) |
|
704 apply(rule_tac mopup_inv_step, simp, simp) |
|
705 done |
|
706 |
|
707 fun abc_mopup_stage1 :: "config \<Rightarrow> nat \<Rightarrow> nat" |
|
708 where |
|
709 "abc_mopup_stage1 (s, l, r) n = |
|
710 (if s > 0 \<and> s \<le> 2*n then 6 |
|
711 else if s = 2*n + 1 then 4 |
|
712 else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then 3 |
|
713 else if s = 2*n + 5 then 2 |
|
714 else if s = 2*n + 6 then 1 |
|
715 else 0)" |
|
716 |
|
717 fun abc_mopup_stage2 :: "config \<Rightarrow> nat \<Rightarrow> nat" |
|
718 where |
|
719 "abc_mopup_stage2 (s, l, r) n = |
|
720 (if s > 0 \<and> s \<le> 2*n then length r |
|
721 else if s = 2*n + 1 then length r |
|
722 else if s = 2*n + 5 then length l |
|
723 else if s = 2*n + 6 then length l |
|
724 else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then length r |
|
725 else 0)" |
|
726 |
|
727 fun abc_mopup_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat" |
|
728 where |
|
729 "abc_mopup_stage3 (s, l, r) n = |
|
730 (if s > 0 \<and> s \<le> 2*n then |
|
731 if hd r = Bk then 0 |
|
732 else 1 |
|
733 else if s = 2*n + 2 then 1 |
|
734 else if s = 2*n + 3 then 0 |
|
735 else if s = 2*n + 4 then 2 |
|
736 else 0)" |
|
737 |
|
738 definition |
|
739 "abc_mopup_measure = measures [\<lambda>(c, n). abc_mopup_stage1 c n, |
|
740 \<lambda>(c, n). abc_mopup_stage2 c n, |
|
741 \<lambda>(c, n). abc_mopup_stage3 c n]" |
|
742 |
|
743 lemma wf_abc_mopup_measure: |
|
744 shows "wf abc_mopup_measure" |
|
745 unfolding abc_mopup_measure_def |
|
746 by auto |
|
747 |
|
748 lemma abc_mopup_measure_induct [case_names Step]: |
|
749 "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> abc_mopup_measure\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
750 using wf_abc_mopup_measure |
|
751 by (metis wf_iff_no_infinite_down_chain) |
|
752 |
|
753 lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False" |
|
754 apply(auto simp: mopup_bef_erase_a.simps) |
|
755 done |
|
756 |
|
757 lemma [simp]: "mopup_bef_erase_b (a, aa, []) lm n ires = False" |
|
758 apply(auto simp: mopup_bef_erase_b.simps) |
|
759 done |
|
760 |
|
761 lemma [simp]: "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False" |
|
762 apply(auto simp: mopup_aft_erase_b.simps) |
|
763 done |
|
764 |
|
765 declare mopup_inv.simps[simp del] |
|
766 |
|
767 lemma [simp]: |
|
768 "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> |
|
769 (fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk) = (R, 2*q - 1)" |
|
770 apply(case_tac q, simp, simp) |
|
771 apply(auto simp: fetch.simps nth_of.simps nth_append) |
|
772 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = |
|
773 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
|
774 simp add: mopup_a.simps nth_append) |
|
775 apply(rule mopup_a_nth, auto) |
|
776 done |
|
777 |
|
778 lemma [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0) " |
|
779 by arith |
|
780 |
|
781 lemma mopup_halt: |
|
782 assumes |
|
783 less: "n < length lm" |
|
784 and inv: "mopup_inv (Suc 0, l, r) lm n ires" |
|
785 and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" |
|
786 and P: "P = (\<lambda> (c, n). is_final c)" |
|
787 shows "\<exists> stp. P (f stp)" |
|
788 proof (induct rule: abc_mopup_measure_induct) |
|
789 case (Step na) |
|
790 have h: "\<not> P (f na)" by fact |
|
791 show "(f (Suc na), f na) \<in> abc_mopup_measure" |
|
792 proof(simp add: f) |
|
793 obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)" |
|
794 apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto) |
|
795 done |
|
796 then have "mopup_inv (a, b, c) lm n ires" |
|
797 using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na] |
|
798 apply(simp) |
|
799 done |
|
800 moreover have "a > 0" |
|
801 using h g |
|
802 apply(simp add: f P) |
|
803 done |
|
804 ultimately |
|
805 have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure" |
|
806 apply(case_tac c, case_tac [2] aa) |
|
807 apply(auto split:if_splits simp add:step.simps mopup_inv.simps) |
|
808 apply(simp_all add: mopupfetchs abc_mopup_measure_def) |
|
809 done |
|
810 thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) |
|
811 (mopup_a n @ shift mopup_b (2 * n), 0), n), |
|
812 steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) |
|
813 \<in> abc_mopup_measure" |
|
814 using g by simp |
|
815 qed |
|
816 qed |
|
817 |
|
818 lemma mopup_inv_start: |
|
819 "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" |
|
820 apply(auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps) |
|
821 apply(case_tac [!] am, auto split: if_splits simp: tape_of_nl_cons) |
|
822 apply(rule_tac x = "Suc a" in exI, rule_tac x = k in exI, simp) |
|
823 apply(case_tac [!] n, auto) |
|
824 apply(case_tac k, auto) |
|
825 done |
|
826 |
|
827 lemma mopup_correct: |
|
828 assumes less: "n < length (am::nat list)" |
|
829 and rs: "am ! n = rs" |
|
830 shows "\<exists> stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp) |
|
831 = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" |
|
832 using less |
|
833 proof - |
|
834 have a: "mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" |
|
835 using less |
|
836 apply(simp add: mopup_inv_start) |
|
837 done |
|
838 then have "\<exists> stp. is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)" |
|
839 using less mopup_halt[of n am "Bk # Bk # ires" "<am> @ Bk \<up> k" ires |
|
840 "(\<lambda>stp. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" |
|
841 "(\<lambda>(c, n). is_final c)"] |
|
842 apply(simp) |
|
843 done |
|
844 from this obtain stp where b: |
|
845 "is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)" .. |
|
846 from a b have |
|
847 "mopup_inv (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp) |
|
848 am n ires" |
|
849 apply(rule_tac mopup_inv_steps, simp_all add: less) |
|
850 done |
|
851 from b and this show "?thesis" |
|
852 apply(rule_tac x = stp in exI, simp) |
|
853 apply(case_tac "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) |
|
854 (mopup_a n @ shift mopup_b (2 * n), 0) stp") |
|
855 apply(simp add: mopup_inv.simps mopup_stop.simps rs) |
|
856 using rs |
|
857 apply(simp add: tape_of_nat_abv) |
|
858 done |
|
859 qed |
|
860 |
|
861 (*we can use Hoare_plus here*) |
|
862 |
|
863 lemma wf_mopup[intro]: "tm_wf (mopup n, 0)" |
|
864 apply(induct n, simp add: mopup.simps shift.simps mopup_b_def tm_wf.simps) |
|
865 apply(auto simp: mopup.simps shift.simps mopup_b_def tm_wf.simps) |
|
866 done |
|
867 |
|
868 end |