1328 apply(erule disj_forward, auto) |
1328 apply(erule disj_forward, auto) |
1329 done |
1329 done |
1330 |
1330 |
1331 lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m) |
1331 lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m) |
1332 else Oc\<up>(Suc m) @ Bk # <lm>)" |
1332 else Oc\<up>(Suc m) @ Bk # <lm>)" |
1333 apply(case_tac lm, simp_all add: tape_of_nl_abv split: if_splits) |
1333 apply(case_tac lm, simp_all add: tape_of_nl_abv tape_of_nat_abv split: if_splits) |
1334 done |
1334 done |
1335 |
1335 |
1336 |
1336 |
1337 lemma locate_a_2_locate_a[simp]: "inv_locate_a (as, am) (q, aaa, Bk # xs) ires |
1337 lemma locate_a_2_locate_a[simp]: "inv_locate_a (as, am) (q, aaa, Bk # xs) ires |
1338 \<Longrightarrow> inv_locate_a (as, am) (q, aaa, Oc # xs) ires" |
1338 \<Longrightarrow> inv_locate_a (as, am) (q, aaa, Oc # xs) ires" |
1950 \<Longrightarrow> inv_check_left_moving_on_leftmost (as, lm) |
1950 \<Longrightarrow> inv_check_left_moving_on_leftmost (as, lm) |
1951 (s', list, Bk # Bk # r) ires" |
1951 (s', list, Bk # Bk # r) ires" |
1952 apply(auto simp: inv_on_left_moving_in_middle_B.simps |
1952 apply(auto simp: inv_on_left_moving_in_middle_B.simps |
1953 inv_check_left_moving_on_leftmost.simps split: if_splits) |
1953 inv_check_left_moving_on_leftmost.simps split: if_splits) |
1954 apply(case_tac [!] "rev lm1", simp_all) |
1954 apply(case_tac [!] "rev lm1", simp_all) |
1955 apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_list.simps) |
1955 apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps) |
1956 done |
1956 done |
1957 |
1957 |
1958 lemma [simp]: |
1958 lemma [simp]: |
1959 "inv_check_left_moving_in_middle (as, lm) (s, l, Bk # r) ires= False" |
1959 "inv_check_left_moving_in_middle (as, lm) (s, l, Bk # r) ires= False" |
1960 by(auto simp: inv_check_left_moving_in_middle.simps ) |
1960 by(auto simp: inv_check_left_moving_in_middle.simps ) |
2018 apply(simp only: inv_check_left_moving_in_middle.simps |
2018 apply(simp only: inv_check_left_moving_in_middle.simps |
2019 inv_on_left_moving_in_middle_B.simps) |
2019 inv_on_left_moving_in_middle_B.simps) |
2020 apply(erule_tac exE)+ |
2020 apply(erule_tac exE)+ |
2021 apply(rule_tac x = "rev (tl (rev lm1))" in exI, |
2021 apply(rule_tac x = "rev (tl (rev lm1))" in exI, |
2022 rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto) |
2022 rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto) |
2023 apply(case_tac [!] "rev lm1",simp_all add: tape_of_nl_abv tape_of_nat_list.simps) |
2023 apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_abv tape_of_nl_abv tape_of_nat_list.simps) |
2024 apply(case_tac [!] a, simp_all) |
2024 apply(case_tac [!] a, simp_all) |
2025 apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps, auto) |
2025 apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto) |
2026 apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps, auto) |
2026 apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto) |
2027 apply(case_tac [!] lista, simp_all add: tape_of_nat_list.simps) |
2027 apply(case_tac [!] lista, simp_all add: tape_of_nat_abv tape_of_nat_list.simps) |
2028 done |
2028 done |
2029 |
2029 |
2030 lemma [simp]: |
2030 lemma [simp]: |
2031 "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires\<Longrightarrow> |
2031 "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires\<Longrightarrow> |
2032 inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires" |
2032 inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires" |
4293 apply(case_tac "Suc q < length list") |
4293 apply(case_tac "Suc q < length list") |
4294 apply(erule_tac notE) |
4294 apply(erule_tac notE) |
4295 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) |
4295 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) |
4296 apply(subgoal_tac "length list = Suc q", auto) |
4296 apply(subgoal_tac "length list = Suc q", auto) |
4297 apply(subgoal_tac "drop q list = [list ! q]") |
4297 apply(subgoal_tac "drop q list = [list ! q]") |
4298 apply(simp add: tape_of_nl_abv) |
4298 apply(simp add: tape_of_nl_abv tape_of_nat_abv) |
4299 by (metis append_Nil2 append_eq_conv_conj lessI nth_drop') |
4299 by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI) |
4300 |
4300 |
4301 lemma erase2jumpover2: |
4301 lemma erase2jumpover2: |
4302 "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> |
4302 "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> |
4303 Oc # Oc \<up> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> |
4303 Oc # Oc \<up> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> |
4304 \<Longrightarrow> RR" |
4304 \<Longrightarrow> RR" |
4305 apply(case_tac "Suc q < length list") |
4305 apply(case_tac "Suc q < length list") |
4306 apply(erule_tac x = "Suc n" in allE, simp) |
4306 apply(erule_tac x = "Suc n" in allE, simp) |
4307 apply(erule_tac notE) |
4307 apply(erule_tac notE) |
4308 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) |
4308 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) |
4309 apply(subgoal_tac "length list = Suc q", auto) |
4309 apply(subgoal_tac "length list = Suc q", auto) |
4310 apply(erule_tac x = "n" in allE, simp) |
4310 apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv) |
4311 by (metis append_Nil2 append_eq_conv_conj lessI nth_drop' |
4311 by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons) |
4312 replicate_Suc tape_of_nat_list.simps(2) tape_of_nl_abv) |
|
4313 |
4312 |
4314 lemma mopup_bef_erase_a_2_jump_over[simp]: |
4313 lemma mopup_bef_erase_a_2_jump_over[simp]: |
4315 "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; |
4314 "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; |
4316 mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> (Suc (Suc s) \<le> 2 * n)\<rbrakk> |
4315 mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> (Suc (Suc s) \<le> 2 * n)\<rbrakk> |
4317 \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires" |
4316 \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires" |
4722 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = |
4721 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = |
4723 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
4722 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
4724 simp add: mopup_a.simps nth_append) |
4723 simp add: mopup_a.simps nth_append) |
4725 apply(rule mopup_a_nth, auto) |
4724 apply(rule mopup_a_nth, auto) |
4726 done |
4725 done |
|
4726 |
|
4727 (* FIXME: is also in uncomputable *) |
|
4728 lemma halt_lemma: |
|
4729 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
4730 by (metis wf_iff_no_infinite_down_chain) |
|
4731 |
4727 |
4732 |
4728 lemma mopup_halt: |
4733 lemma mopup_halt: |
4729 assumes |
4734 assumes |
4730 less: "n < length lm" |
4735 less: "n < length lm" |
4731 and inv: "mopup_inv (Suc 0, l, r) lm n ires" |
4736 and inv: "mopup_inv (Suc 0, l, r) lm n ires" |