equal
deleted
inserted
replaced
1437 apply(simp add: t_wcode_main_def nth_append fetch.simps t_wcode_main_first_part_def |
1437 apply(simp add: t_wcode_main_def nth_append fetch.simps t_wcode_main_first_part_def |
1438 nth_of.simps t_twice_len_def, auto) |
1438 nth_of.simps t_twice_len_def, auto) |
1439 apply(simp add: t_twice_def t_twice_compile_def) |
1439 apply(simp add: t_twice_def t_twice_compile_def) |
1440 using mopup_mod2[of 1] |
1440 using mopup_mod2[of 1] |
1441 apply(simp) |
1441 apply(simp) |
1442 by arith |
1442 done |
1443 |
1443 |
1444 lemma wcode_jump1: |
1444 lemma wcode_jump1: |
1445 "\<exists> stp ln rn. steps0 (Suc (t_twice_len) + length t_wcode_main_first_part div 2, |
1445 "\<exists> stp ln rn. steps0 (Suc (t_twice_len) + length t_wcode_main_first_part div 2, |
1446 Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(n)) |
1446 Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(n)) |
1447 t_wcode_main stp |
1447 t_wcode_main stp |
2067 by metis |
2067 by metis |
2068 qed |
2068 qed |
2069 |
2069 |
2070 lemma [intro]: "length t_twice mod 2 = 0" |
2070 lemma [intro]: "length t_twice mod 2 = 0" |
2071 apply(auto simp: t_twice_def t_twice_compile_def) |
2071 apply(auto simp: t_twice_def t_twice_compile_def) |
2072 done |
2072 by (metis mopup_mod2) |
2073 |
2073 |
2074 lemma t_fourtimes_append_pre: |
2074 lemma t_fourtimes_append_pre: |
2075 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_fourtimes stp |
2075 "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_fourtimes stp |
2076 = (Suc t_fourtimes_len, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn)) |
2076 = (Suc t_fourtimes_len, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn)) |
2077 \<Longrightarrow> steps0 (Suc 0 + length (t_wcode_main_first_part @ |
2077 \<Longrightarrow> steps0 (Suc 0 + length (t_wcode_main_first_part @ |
2129 apply(simp add: t_wcode_main_def) |
2129 apply(simp add: t_wcode_main_def) |
2130 done |
2130 done |
2131 |
2131 |
2132 lemma even_twice_len: "length t_twice mod 2 = 0" |
2132 lemma even_twice_len: "length t_twice mod 2 = 0" |
2133 apply(auto simp: t_twice_def t_twice_compile_def) |
2133 apply(auto simp: t_twice_def t_twice_compile_def) |
2134 done |
2134 by (metis mopup_mod2) |
2135 |
2135 |
2136 lemma even_fourtimes_len: "length t_fourtimes mod 2 = 0" |
2136 lemma even_fourtimes_len: "length t_fourtimes mod 2 = 0" |
2137 apply(auto simp: t_fourtimes_def t_fourtimes_compile_def) |
2137 apply(auto simp: t_fourtimes_def t_fourtimes_compile_def) |
2138 done |
2138 by (metis mopup_mod2) |
2139 |
2139 |
2140 lemma [simp]: "2 * (length t_twice div 2) = length t_twice" |
2140 lemma [simp]: "2 * (length t_twice div 2) = length t_twice" |
2141 using even_twice_len |
2141 using even_twice_len |
2142 by arith |
2142 by arith |
2143 |
2143 |