154 |
154 |
155 lemma fetch_bef_erase_b_b: |
155 lemma fetch_bef_erase_b_b: |
156 "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = 0\<rbrakk> \<Longrightarrow> |
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)" |
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) |
158 apply(subgoal_tac "\<exists> q. s = 2 * q", auto) |
159 apply(case_tac qa, simp, simp) |
159 apply(case_tac q, simp, simp) |
160 apply(auto simp: fetch.simps nth_of.simps nth_append) |
160 apply(auto simp: fetch.simps nth_of.simps nth_append) |
161 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = |
161 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = |
162 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
162 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
163 simp add: mopup_a.simps nth_append) |
163 simp add: mopup_a.simps nth_append) |
164 apply(rule mopup_a_nth, auto) |
164 apply(rule mopup_a_nth, auto) |
288 apply(auto elim: mopup_false1) |
288 apply(auto elim: mopup_false1) |
289 done |
289 done |
290 |
290 |
291 lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m) |
291 lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m) |
292 else Oc\<up>(Suc m) @ Bk # <lm>)" |
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) |
293 by(case_tac lm, simp_all add: tape_of_list_def tape_of_nat_def split: if_splits) |
294 done |
|
295 |
294 |
296 lemma drop_tape_of_cons: |
295 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>" |
296 "\<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) |
297 using Suc_lessD append_Cons list.simps(2) Cons_nth_drop_Suc replicate_Suc tape_of_nl_cons |
|
298 by metis |
299 |
299 |
300 lemma erase2jumpover1: |
300 lemma erase2jumpover1: |
301 "\<lbrakk>q < length list; |
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> |
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)" |
303 \<Longrightarrow> <drop q list> = Oc # Oc \<up> (list ! q)" |
305 apply(case_tac "Suc q < length list") |
305 apply(case_tac "Suc q < length list") |
306 apply(erule_tac notE) |
306 apply(erule_tac notE) |
307 apply(rule_tac drop_tape_of_cons, simp_all) |
307 apply(rule_tac drop_tape_of_cons, simp_all) |
308 apply(subgoal_tac "length list = Suc q", auto) |
308 apply(subgoal_tac "length list = Suc q", auto) |
309 apply(subgoal_tac "drop q list = [list ! q]") |
309 apply(subgoal_tac "drop q list = [list ! q]") |
310 apply(simp add: tape_of_nl_abv tape_of_nat_abv replicate_Suc) |
310 apply(simp add: tape_of_nat_def tape_of_list_def replicate_Suc) |
311 by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI) |
311 by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI) |
312 |
312 |
313 lemma erase2jumpover2: |
313 lemma erase2jumpover2: |
314 "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> |
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> |
315 Oc # Oc \<up> (list ! q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> |
316 \<Longrightarrow> RR" |
316 \<Longrightarrow> RR" |
317 apply(case_tac "Suc q < length list") |
317 apply(case_tac "Suc q < length list") |
318 apply(erule_tac x = "Suc n" in allE, simp) |
318 apply(erule_tac x = "Suc n" in allE, simp) |
319 apply(erule_tac notE, simp add: replicate_Suc) |
319 apply(erule_tac notE, simp add: replicate_Suc) |
320 apply(rule_tac drop_tape_of_cons, simp_all) |
320 apply(rule_tac drop_tape_of_cons, simp_all) |
321 apply(subgoal_tac "length list = Suc q", auto) |
321 apply(subgoal_tac "length list = Suc q", auto) |
322 apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv) |
322 apply(erule_tac x = "n" in allE, simp add: tape_of_list_def) |
323 by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons) |
323 by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI replicate_Suc tape_of_list_def tape_of_nl_cons) |
324 |
324 |
325 lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))" |
325 lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))" |
326 by arith |
326 by arith |
327 |
327 |
328 declare replicate_Suc[simp] |
328 declare replicate_Suc[simp] |
447 "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, []) lm n ires\<rbrakk> \<Longrightarrow> |
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" |
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) |
449 apply(rule mopup_jump_over1_2_aft_erase_a, simp) |
450 apply(auto simp: mopup_jump_over1.simps) |
450 apply(auto simp: mopup_jump_over1.simps) |
451 apply(rule_tac x = ln in exI, rule_tac x = "Suc (lm ! n)" in exI, |
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 ) |
452 rule_tac x = 0 in exI, simp add: tape_of_list_def ) |
453 done |
453 done |
454 |
454 |
455 lemma [simp]: "<[]> = []" |
455 lemma [simp]: "<[]> = []" by(simp add: tape_of_list_def) |
456 apply(simp add: tape_of_nl_abv) |
|
457 done |
|
458 |
456 |
459 lemma [simp]: |
457 lemma [simp]: |
460 "\<lbrakk>n < length lm; |
458 "\<lbrakk>n < length lm; |
461 mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires\<rbrakk> |
459 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" |
460 \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires" |
465 apply(simp_all add: tape_of_nl_cons split: if_splits) |
463 apply(simp_all add: tape_of_nl_cons split: if_splits) |
466 apply(case_tac rn, simp_all) |
464 apply(case_tac rn, simp_all) |
467 apply(case_tac a, simp_all) |
465 apply(case_tac a, simp_all) |
468 apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) |
466 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) |
467 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) |
468 apply(case_tac a, simp, simp add: tape_of_list_def tape_of_nat_def) |
471 apply(case_tac a, simp_all) |
469 apply(case_tac a, simp_all) |
472 apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp) |
470 apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp) |
473 apply(rule_tac x = rn in exI, simp) |
471 apply(rule_tac x = rn in exI, simp) |
474 apply(rule_tac x = "nat # list" in exI, simp add: tape_of_nl_cons) |
472 apply(rule_tac x = "nat # list" in exI, simp add: tape_of_nl_cons) |
475 done |
473 done |
517 lemma tape_of_ex1[intro]: |
515 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" |
516 "\<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) |
517 apply(case_tac a, simp_all) |
520 apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) |
518 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) |
519 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) |
520 apply(simp add: tape_of_list_def tape_of_nat_def) |
523 done |
521 done |
524 |
522 |
525 lemma [intro]: "\<exists>rna ml. Oc \<up> a @ Bk # <list::nat list> @ Bk \<up> rn = |
523 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" |
524 <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) |
525 apply(case_tac "list = []", simp add: replicate_Suc[THEN sym] del: replicate_Suc) |
653 |
651 |
654 lemma [simp]: |
652 lemma [simp]: |
655 "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\<rbrakk> |
653 "\<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" |
654 \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires" |
657 apply(auto simp: mopup_jump_over2.simps mopup_stop.simps) |
655 apply(auto simp: mopup_jump_over2.simps mopup_stop.simps) |
658 apply(simp_all add: tape_of_nat_abv exp_ind[THEN sym]) |
656 apply(simp_all add: tape_of_nat_def exp_ind[THEN sym]) |
659 done |
657 done |
660 |
658 |
661 lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False" |
659 lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False" |
662 apply(simp only: mopup_jump_over2.simps, simp) |
660 apply(simp only: mopup_jump_over2.simps, simp) |
663 done |
661 done |
789 done |
787 done |
790 ultimately |
788 ultimately |
791 have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure" |
789 have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure" |
792 apply(case_tac c, case_tac [2] aa) |
790 apply(case_tac c, case_tac [2] aa) |
793 apply(auto split:if_splits simp add:step.simps mopup_inv.simps) |
791 apply(auto split:if_splits simp add:step.simps mopup_inv.simps) |
794 apply(simp_all add: mopupfetchs abc_mopup_measure_def) |
792 by (auto split:if_splits simp: mopupfetchs abc_mopup_measure_def) |
795 done |
|
796 thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) |
793 thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) |
797 (mopup_a n @ shift mopup_b (2 * n), 0), n), |
794 (mopup_a n @ shift mopup_b (2 * n), 0), n), |
798 steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) |
795 steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) |
799 \<in> abc_mopup_measure" |
796 \<in> abc_mopup_measure" |
800 using g by simp |
797 using g by simp |
838 apply(rule_tac x = stp in exI, simp) |
835 apply(rule_tac x = stp in exI, simp) |
839 apply(case_tac "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) |
836 apply(case_tac "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) |
840 (mopup_a n @ shift mopup_b (2 * n), 0) stp") |
837 (mopup_a n @ shift mopup_b (2 * n), 0) stp") |
841 apply(simp add: mopup_inv.simps mopup_stop.simps rs) |
838 apply(simp add: mopup_inv.simps mopup_stop.simps rs) |
842 using rs |
839 using rs |
843 apply(simp add: tape_of_nat_abv) |
840 apply(simp add: tape_of_nat_def) |
844 done |
841 done |
845 qed |
842 qed |
846 |
843 |
847 lemma wf_mopup[intro]: "tm_wf (mopup n, 0)" |
844 lemma wf_mopup[intro]: "tm_wf (mopup n, 0)" |
848 apply(induct n, simp add: mopup.simps shift.simps mopup_b_def tm_wf.simps) |
845 apply(induct n, simp add: mopup.simps shift.simps mopup_b_def tm_wf.simps) |