equal
deleted
inserted
replaced
664 |
664 |
665 declare fetch.simps[simp del] |
665 declare fetch.simps[simp del] |
666 lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)" |
666 lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)" |
667 by arith |
667 by arith |
668 |
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" |
669 lemma mod_2: "x mod 2 = 0 \<or> x mod 2 = Suc 0" |
684 by arith |
670 by arith |
685 |
671 |
686 lemma mopup_inv_step: |
672 lemma mopup_inv_step: |
687 "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> |
673 "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> |
856 using rs |
842 using rs |
857 apply(simp add: tape_of_nat_abv) |
843 apply(simp add: tape_of_nat_abv) |
858 done |
844 done |
859 qed |
845 qed |
860 |
846 |
861 (*we can use Hoare_plus here*) |
|
862 |
|
863 lemma wf_mopup[intro]: "tm_wf (mopup n, 0)" |
847 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) |
848 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) |
849 apply(auto simp: mopup.simps shift.simps mopup_b_def tm_wf.simps) |
866 done |
850 done |
867 |
851 |