equal
deleted
inserted
replaced
709 |
709 |
710 lemma [simp]: "a\<up>(Suc 0) = [a]" |
710 lemma [simp]: "a\<up>(Suc 0) = [a]" |
711 by(simp) |
711 by(simp) |
712 |
712 |
713 lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<up>(Suc a) @ Bk # (<xs@ [b]>))" |
713 lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<up>(Suc a) @ Bk # (<xs@ [b]>))" |
714 apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps) |
714 apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) |
715 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps) |
715 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) |
716 done |
716 done |
717 |
717 |
718 lemma bl_bin_bk_oc[simp]: |
718 lemma bl_bin_bk_oc[simp]: |
719 "bl_bin (xs @ [Bk, Oc]) = |
719 "bl_bin (xs @ [Bk, Oc]) = |
720 bl_bin xs + 2*2^(length xs)" |
720 bl_bin xs + 2*2^(length xs)" |
1229 using h |
1229 using h |
1230 apply(simp add: abc_twice_def) |
1230 apply(simp add: abc_twice_def) |
1231 done |
1231 done |
1232 qed |
1232 qed |
1233 thus "?thesis" |
1233 thus "?thesis" |
1234 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps) |
1234 apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv) |
1235 done |
1235 done |
1236 qed |
1236 qed |
1237 |
1237 |
1238 |
1238 |
1239 lemma adjust_fetch0: |
1239 lemma adjust_fetch0: |