3754 (Nop, 0)" |
3757 (Nop, 0)" |
3755 apply(case_tac b) |
3758 apply(case_tac b) |
3756 apply(simp_all add: start_of.simps fetch.simps nth_append) |
3759 apply(simp_all add: start_of.simps fetch.simps nth_append) |
3757 done |
3760 done |
3758 |
3761 |
3759 (********for mopup***********) |
|
3760 fun mopup_a :: "nat \<Rightarrow> instr list" |
|
3761 where |
|
3762 "mopup_a 0 = []" | |
|
3763 "mopup_a (Suc n) = mopup_a n @ |
|
3764 [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]" |
|
3765 |
|
3766 definition mopup_b :: "instr list" |
|
3767 where |
|
3768 "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3), |
|
3769 (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]" |
|
3770 |
|
3771 fun mopup :: "nat \<Rightarrow> instr list" |
|
3772 where |
|
3773 "mopup n = mopup_a n @ shift mopup_b (2*n)" |
|
3774 (****) |
|
3775 |
|
3776 type_synonym mopup_type = "config \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> cell list \<Rightarrow> bool" |
|
3777 |
|
3778 fun mopup_stop :: "mopup_type" |
|
3779 where |
|
3780 "mopup_stop (s, l, r) lm n ires= |
|
3781 (\<exists> ln rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = <abc_lm_v lm n> @ Bk\<up>rn)" |
|
3782 |
|
3783 fun mopup_bef_erase_a :: "mopup_type" |
|
3784 where |
|
3785 "mopup_bef_erase_a (s, l, r) lm n ires= |
|
3786 (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> |
|
3787 r = Oc\<up>m@ Bk # <(drop ((s + 1) div 2) lm)> @ Bk\<up>rn)" |
|
3788 |
|
3789 fun mopup_bef_erase_b :: "mopup_type" |
|
3790 where |
|
3791 "mopup_bef_erase_b (s, l, r) lm n ires = |
|
3792 (\<exists> ln m rn. l = Bk\<up>ln @ Bk # Bk # ires \<and> r = Bk # Oc\<up>m @ Bk # |
|
3793 <(drop (s div 2) lm)> @ Bk\<up>rn)" |
|
3794 |
|
3795 fun mopup_jump_over1 :: "mopup_type" |
|
3796 where |
|
3797 "mopup_jump_over1 (s, l, r) lm n ires = |
|
3798 (\<exists> ln m1 m2 rn. m1 + m2 = Suc (abc_lm_v lm n) \<and> |
|
3799 l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> |
|
3800 (r = Oc\<up>m2 @ Bk # <(drop (Suc n) lm)> @ Bk\<up>rn \<or> |
|
3801 (r = Oc\<up>m2 \<and> (drop (Suc n) lm) = [])))" |
|
3802 |
|
3803 fun mopup_aft_erase_a :: "mopup_type" |
|
3804 where |
|
3805 "mopup_aft_erase_a (s, l, r) lm n ires = |
|
3806 (\<exists> lnl lnr rn (ml::nat list) m. |
|
3807 m = Suc (abc_lm_v lm n) \<and> l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> |
|
3808 (r = <ml> @ Bk\<up>rn))" |
|
3809 |
|
3810 fun mopup_aft_erase_b :: "mopup_type" |
|
3811 where |
|
3812 "mopup_aft_erase_b (s, l, r) lm n ires= |
|
3813 (\<exists> lnl lnr rn (ml::nat list) m. |
|
3814 m = Suc (abc_lm_v lm n) \<and> |
|
3815 l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> |
|
3816 (r = Bk # <ml> @ Bk\<up>rn \<or> |
|
3817 r = Bk # Bk # <ml> @ Bk\<up>rn))" |
|
3818 |
|
3819 fun mopup_aft_erase_c :: "mopup_type" |
|
3820 where |
|
3821 "mopup_aft_erase_c (s, l, r) lm n ires = |
|
3822 (\<exists> lnl lnr rn (ml::nat list) m. |
|
3823 m = Suc (abc_lm_v lm n) \<and> |
|
3824 l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> |
|
3825 (r = <ml> @ Bk\<up>rn \<or> r = Bk # <ml> @ Bk\<up>rn))" |
|
3826 |
|
3827 fun mopup_left_moving :: "mopup_type" |
|
3828 where |
|
3829 "mopup_left_moving (s, l, r) lm n ires = |
|
3830 (\<exists> lnl lnr rn m. |
|
3831 m = Suc (abc_lm_v lm n) \<and> |
|
3832 ((l = Bk\<up>lnr @ Oc\<up>m @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Bk\<up>rn) \<or> |
|
3833 (l = Oc\<up>(m - 1) @ Bk\<up>lnl @ Bk # Bk # ires \<and> r = Oc # Bk\<up>rn)))" |
|
3834 |
|
3835 fun mopup_jump_over2 :: "mopup_type" |
|
3836 where |
|
3837 "mopup_jump_over2 (s, l, r) lm n ires = |
|
3838 (\<exists> ln rn m1 m2. |
|
3839 m1 + m2 = Suc (abc_lm_v lm n) |
|
3840 \<and> r \<noteq> [] |
|
3841 \<and> (hd r = Oc \<longrightarrow> (l = Oc\<up>m1 @ Bk\<up>ln @ Bk # Bk # ires \<and> r = Oc\<up>m2 @ Bk\<up>rn)) |
|
3842 \<and> (hd r = Bk \<longrightarrow> (l = Bk\<up>ln @ Bk # ires \<and> r = Bk # Oc\<up>(m1+m2)@ Bk\<up>rn)))" |
|
3843 |
|
3844 |
|
3845 fun mopup_inv :: "mopup_type" |
|
3846 where |
|
3847 "mopup_inv (s, l, r) lm n ires = |
|
3848 (if s = 0 then mopup_stop (s, l, r) lm n ires |
|
3849 else if s \<le> 2*n then |
|
3850 if s mod 2 = 1 then mopup_bef_erase_a (s, l, r) lm n ires |
|
3851 else mopup_bef_erase_b (s, l, r) lm n ires |
|
3852 else if s = 2*n + 1 then |
|
3853 mopup_jump_over1 (s, l, r) lm n ires |
|
3854 else if s = 2*n + 2 then mopup_aft_erase_a (s, l, r) lm n ires |
|
3855 else if s = 2*n + 3 then mopup_aft_erase_b (s, l, r) lm n ires |
|
3856 else if s = 2*n + 4 then mopup_aft_erase_c (s, l, r) lm n ires |
|
3857 else if s = 2*n + 5 then mopup_left_moving (s, l, r) lm n ires |
|
3858 else if s = 2*n + 6 then mopup_jump_over2 (s, l, r) lm n ires |
|
3859 else False)" |
|
3860 |
|
3861 lemma mopup_fetch_0[simp]: |
|
3862 "(fetch (mopup_a n @ shift mopup_b (2 * n)) 0 b) = (Nop, 0)" |
|
3863 by(simp add: fetch.simps) |
|
3864 |
|
3865 lemma mop_bef_length[simp]: "length (mopup_a n) = 4 * n" |
|
3866 apply(induct n, simp_all add: mopup_a.simps) |
|
3867 done |
|
3868 |
|
3869 lemma mopup_a_nth: |
|
3870 "\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = |
|
3871 mopup_a (Suc q) ! ((4 * q) + x)" |
|
3872 apply(induct n, simp) |
|
3873 apply(case_tac "q < n", simp add: mopup_a.simps, auto) |
|
3874 apply(simp add: nth_append) |
|
3875 apply(subgoal_tac "q = n", simp) |
|
3876 apply(arith) |
|
3877 done |
|
3878 |
|
3879 lemma fetch_bef_erase_a_o[simp]: |
|
3880 "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> |
|
3881 \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc) = (W0, s + 1)" |
|
3882 apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto) |
|
3883 apply(subgoal_tac "length (mopup_a n) = 4*n") |
|
3884 apply(auto simp: fetch.simps nth_of.simps nth_append) |
|
3885 apply(subgoal_tac "mopup_a n ! (4 * q + 1) = |
|
3886 mopup_a (Suc q) ! ((4 * q) + 1)", |
|
3887 simp add: mopup_a.simps nth_append) |
|
3888 apply(rule mopup_a_nth, auto) |
|
3889 apply arith |
|
3890 done |
|
3891 |
|
3892 lemma fetch_bef_erase_a_b[simp]: |
|
3893 "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> |
|
3894 \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s + 2)" |
|
3895 apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto) |
|
3896 apply(subgoal_tac "length (mopup_a n) = 4*n") |
|
3897 apply(auto simp: fetch.simps nth_of.simps nth_append) |
|
3898 apply(subgoal_tac "mopup_a n ! (4 * q + 0) = |
|
3899 mopup_a (Suc q) ! ((4 * q + 0))", |
|
3900 simp add: mopup_a.simps nth_append) |
|
3901 apply(rule mopup_a_nth, auto) |
|
3902 apply arith |
|
3903 done |
|
3904 |
|
3905 lemma fetch_bef_erase_b_b: |
|
3906 "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = 0\<rbrakk> \<Longrightarrow> |
|
3907 (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)" |
|
3908 apply(subgoal_tac "\<exists> q. s = 2 * q", auto) |
|
3909 apply(case_tac qa, simp, simp) |
|
3910 apply(auto simp: fetch.simps nth_of.simps nth_append) |
|
3911 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = |
|
3912 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
|
3913 simp add: mopup_a.simps nth_append) |
|
3914 apply(rule mopup_a_nth, auto) |
|
3915 done |
|
3916 |
|
3917 lemma fetch_jump_over1_o: |
|
3918 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Oc |
|
3919 = (R, Suc (2 * n))" |
|
3920 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3921 apply(auto simp: fetch.simps nth_of.simps mopup_b_def nth_append |
|
3922 shift.simps) |
|
3923 done |
|
3924 |
|
3925 lemma fetch_jump_over1_b: |
|
3926 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk |
|
3927 = (R, Suc (Suc (2 * n)))" |
|
3928 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3929 apply(auto simp: fetch.simps nth_of.simps mopup_b_def |
|
3930 nth_append shift.simps) |
|
3931 done |
|
3932 |
|
3933 lemma fetch_aft_erase_a_o: |
|
3934 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Oc |
|
3935 = (W0, Suc (2 * n + 2))" |
|
3936 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3937 apply(auto simp: fetch.simps nth_of.simps mopup_b_def |
|
3938 nth_append shift.simps) |
|
3939 done |
|
3940 |
|
3941 lemma fetch_aft_erase_a_b: |
|
3942 "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk |
|
3943 = (L, Suc (2 * n + 4))" |
|
3944 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3945 apply(auto simp: fetch.simps nth_of.simps mopup_b_def |
|
3946 nth_append shift.simps) |
|
3947 done |
|
3948 |
|
3949 lemma fetch_aft_erase_b_b: |
|
3950 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2*n + 3) Bk |
|
3951 = (R, Suc (2 * n + 3))" |
|
3952 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3953 apply(subgoal_tac "2*n + 3 = Suc (2*n + 2)", simp only: fetch.simps) |
|
3954 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
3955 done |
|
3956 |
|
3957 lemma fetch_aft_erase_c_o: |
|
3958 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Oc |
|
3959 = (W0, Suc (2 * n + 2))" |
|
3960 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3961 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) |
|
3962 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
3963 done |
|
3964 |
|
3965 lemma fetch_aft_erase_c_b: |
|
3966 "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk |
|
3967 = (R, Suc (2 * n + 1))" |
|
3968 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3969 apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps) |
|
3970 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
3971 done |
|
3972 |
|
3973 lemma fetch_left_moving_o: |
|
3974 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Oc) |
|
3975 = (L, 2*n + 6)" |
|
3976 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3977 apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps) |
|
3978 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
3979 done |
|
3980 |
|
3981 lemma fetch_left_moving_b: |
|
3982 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk) |
|
3983 = (L, 2*n + 5)" |
|
3984 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3985 apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps) |
|
3986 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
3987 done |
|
3988 |
|
3989 lemma fetch_jump_over2_b: |
|
3990 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Bk) |
|
3991 = (R, 0)" |
|
3992 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
3993 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) |
|
3994 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
3995 done |
|
3996 |
|
3997 lemma fetch_jump_over2_o: |
|
3998 "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Oc) |
|
3999 = (L, 2*n + 6)" |
|
4000 apply(subgoal_tac "length (mopup_a n) = 4 * n") |
|
4001 apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps) |
|
4002 apply(auto simp: nth_of.simps mopup_b_def nth_append shift.simps) |
|
4003 done |
|
4004 |
|
4005 lemmas mopupfetchs = |
|
4006 fetch_bef_erase_a_o fetch_bef_erase_a_b fetch_bef_erase_b_b |
|
4007 fetch_jump_over1_o fetch_jump_over1_b fetch_aft_erase_a_o |
|
4008 fetch_aft_erase_a_b fetch_aft_erase_b_b fetch_aft_erase_c_o |
|
4009 fetch_aft_erase_c_b fetch_left_moving_o fetch_left_moving_b |
|
4010 fetch_jump_over2_b fetch_jump_over2_o |
|
4011 |
|
4012 declare |
|
4013 mopup_jump_over2.simps[simp del] mopup_left_moving.simps[simp del] |
|
4014 mopup_aft_erase_c.simps[simp del] mopup_aft_erase_b.simps[simp del] |
|
4015 mopup_aft_erase_a.simps[simp del] mopup_jump_over1.simps[simp del] |
|
4016 mopup_bef_erase_a.simps[simp del] mopup_bef_erase_b.simps[simp del] |
|
4017 mopup_stop.simps[simp del] |
|
4018 |
|
4019 lemma [simp]: |
|
4020 "\<lbrakk>mopup_bef_erase_a (s, l, Oc # xs) lm n ires\<rbrakk> \<Longrightarrow> |
|
4021 mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires" |
|
4022 apply(auto simp: mopup_bef_erase_a.simps mopup_bef_erase_b.simps ) |
|
4023 apply(rule_tac x = "m - 1" in exI, rule_tac x = rn in exI) |
|
4024 apply(case_tac m, simp, simp) |
|
4025 done |
|
4026 |
|
4027 lemma mopup_false1: |
|
4028 "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc s \<le> 2 * n\<rbrakk> |
|
4029 \<Longrightarrow> RR" |
|
4030 apply(arith) |
|
4031 done |
|
4032 |
|
4033 lemma [simp]: |
|
4034 "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; |
|
4035 mopup_bef_erase_a (s, l, Oc # xs) lm n ires; r = Oc # xs\<rbrakk> |
|
4036 \<Longrightarrow> (Suc s \<le> 2 * n \<longrightarrow> mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires) \<and> |
|
4037 (\<not> Suc s \<le> 2 * n \<longrightarrow> mopup_jump_over1 (Suc s, l, Bk # xs) lm n ires) " |
|
4038 apply(auto elim: mopup_false1) |
|
4039 done |
|
4040 |
|
4041 lemma drop_tape_of_cons: |
|
4042 "\<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>" |
|
4043 by (metis Suc_lessD append_Cons list.simps(2) nth_drop' replicate_Suc tape_of_nl_cons) |
|
4044 |
|
4045 lemma erase2jumpover1: |
|
4046 "\<lbrakk>q < length list; |
|
4047 \<forall>rn. <drop q list> \<noteq> Oc # Oc \<up> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> |
|
4048 \<Longrightarrow> <drop q list> = Oc # Oc \<up> abc_lm_v (a # list) (Suc q)" |
|
4049 apply(erule_tac x = 0 in allE, simp) |
|
4050 apply(case_tac "Suc q < length list") |
|
4051 apply(erule_tac notE) |
|
4052 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) |
|
4053 apply(subgoal_tac "length list = Suc q", auto) |
|
4054 apply(subgoal_tac "drop q list = [list ! q]") |
|
4055 apply(simp add: tape_of_nl_abv tape_of_nat_abv) |
|
4056 by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI) |
|
4057 |
|
4058 lemma erase2jumpover2: |
|
4059 "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> |
|
4060 Oc # Oc \<up> abc_lm_v (a # list) (Suc q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> |
|
4061 \<Longrightarrow> RR" |
|
4062 apply(case_tac "Suc q < length list") |
|
4063 apply(erule_tac x = "Suc n" in allE, simp) |
|
4064 apply(erule_tac notE) |
|
4065 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) |
|
4066 apply(subgoal_tac "length list = Suc q", auto) |
|
4067 apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv) |
|
4068 by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons) |
|
4069 |
|
4070 lemma mopup_bef_erase_a_2_jump_over[simp]: |
|
4071 "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; s \<le> 2 * n; |
|
4072 mopup_bef_erase_a (s, l, Bk # xs) lm n ires; \<not> (Suc (Suc s) \<le> 2 * n)\<rbrakk> |
|
4073 \<Longrightarrow> mopup_jump_over1 (s', Bk # l, xs) lm n ires" |
|
4074 apply(auto simp: mopup_bef_erase_a.simps mopup_jump_over1.simps) |
|
4075 apply(case_tac m, auto simp: mod_ex1) |
|
4076 apply(subgoal_tac "n = Suc q", auto) |
|
4077 apply(rule_tac x = "Suc ln" in exI, rule_tac x = 0 in exI, auto) |
|
4078 apply(case_tac [!] lm, simp_all) |
|
4079 apply(case_tac [!] rn, auto elim: erase2jumpover1 erase2jumpover2) |
|
4080 apply(erule_tac x = 0 in allE, simp) |
|
4081 apply(rule_tac classical, simp) |
|
4082 apply(erule_tac notE) |
|
4083 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps) |
|
4084 done |
|
4085 |
|
4086 lemma Suc_Suc_div: "\<lbrakk>0 < s; s mod 2 = Suc 0; Suc (Suc s) \<le> 2 * n\<rbrakk> |
|
4087 \<Longrightarrow> (Suc (Suc (s div 2))) \<le> n" |
|
4088 apply(arith) |
|
4089 done |
|
4090 |
|
4091 lemma mopup_bef_erase_a_2_a[simp]: |
|
4092 "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0; |
|
4093 mopup_bef_erase_a (s, l, Bk # xs) lm n ires; |
|
4094 Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> |
|
4095 mopup_bef_erase_a (Suc (Suc s), Bk # l, xs) lm n ires" |
|
4096 apply(auto simp: mopup_bef_erase_a.simps) |
|
4097 apply(subgoal_tac "drop (Suc (Suc (s div 2))) lm \<noteq> []") |
|
4098 apply(case_tac m, simp_all) |
|
4099 apply(rule_tac x = "Suc (abc_lm_v lm (Suc (s div 2)))" in exI, |
|
4100 rule_tac x = rn in exI, auto simp: mod_ex1) |
|
4101 apply(rule_tac drop_tape_of_cons) |
|
4102 apply arith |
|
4103 apply(simp add: abc_lm_v.simps) |
|
4104 done |
|
4105 |
|
4106 lemma mopup_false2: |
|
4107 "\<lbrakk>0 < s; s \<le> 2 * n; |
|
4108 s mod 2 = Suc 0; Suc s \<noteq> 2 * n; |
|
4109 \<not> Suc (Suc s) \<le> 2 * n\<rbrakk> \<Longrightarrow> RR" |
|
4110 apply(arith) |
|
4111 done |
|
4112 |
|
4113 lemma [simp]: "mopup_bef_erase_a (s, l, []) lm n ires \<Longrightarrow> |
|
4114 mopup_bef_erase_a (s, l, [Bk]) lm n ires" |
|
4115 apply(auto simp: mopup_bef_erase_a.simps) |
|
4116 done |
|
4117 |
|
4118 lemma [simp]: |
|
4119 "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc (Suc s) \<le> 2 *n; |
|
4120 mopup_bef_erase_a (s, l, []) lm n ires\<rbrakk> |
|
4121 \<Longrightarrow> mopup_jump_over1 (s', Bk # l, []) lm n ires" |
|
4122 by auto |
|
4123 |
|
4124 lemma "mopup_bef_erase_b (s, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
4125 apply(auto simp: mopup_bef_erase_b.simps) |
|
4126 done |
|
4127 |
|
4128 lemma [simp]: "mopup_bef_erase_b (s, l, Oc # xs) lm n ires = False" |
|
4129 apply(auto simp: mopup_bef_erase_b.simps ) |
|
4130 done |
|
4131 |
|
4132 lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> |
|
4133 (s - Suc 0) mod 2 = Suc 0" |
|
4134 apply(arith) |
|
4135 done |
|
4136 |
|
4137 lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> |
|
4138 s - Suc 0 \<le> 2 * n" |
|
4139 apply(simp) |
|
4140 done |
|
4141 |
|
4142 lemma [simp]: "\<lbrakk>0 < s; s \<le> 2 *n; s mod 2 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> \<not> s \<le> Suc 0" |
|
4143 apply(arith) |
|
4144 done |
|
4145 |
|
4146 lemma [simp]: "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; |
|
4147 s mod 2 \<noteq> Suc 0; |
|
4148 mopup_bef_erase_b (s, l, Bk # xs) lm n ires; r = Bk # xs\<rbrakk> |
|
4149 \<Longrightarrow> mopup_bef_erase_a (s - Suc 0, Bk # l, xs) lm n ires" |
|
4150 apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps) |
|
4151 done |
|
4152 |
|
4153 lemma [simp]: "\<lbrakk>mopup_bef_erase_b (s, l, []) lm n ires\<rbrakk> \<Longrightarrow> |
|
4154 mopup_bef_erase_a (s - Suc 0, Bk # l, []) lm n ires" |
|
4155 apply(auto simp: mopup_bef_erase_b.simps mopup_bef_erase_a.simps) |
|
4156 done |
|
4157 |
|
4158 lemma [simp]: |
|
4159 "\<lbrakk>n < length lm; |
|
4160 mopup_jump_over1 (Suc (2 * n), l, Oc # xs) lm n ires; |
|
4161 r = Oc # xs\<rbrakk> |
|
4162 \<Longrightarrow> mopup_jump_over1 (Suc (2 * n), Oc # l, xs) lm n ires" |
|
4163 apply(auto simp: mopup_jump_over1.simps) |
|
4164 apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI, |
|
4165 rule_tac x = "m2 - 1" in exI, simp) |
|
4166 apply(case_tac "m2", simp, simp) |
|
4167 apply(rule_tac x = ln in exI, rule_tac x = "Suc m1" in exI, |
|
4168 rule_tac x = "m2 - 1" in exI) |
|
4169 apply(case_tac m2, simp, simp) |
|
4170 done |
|
4171 |
|
4172 lemma mopup_jump_over1_2_aft_erase_a[simp]: |
|
4173 "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, Bk # xs) lm n ires\<rbrakk> |
|
4174 \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires" |
|
4175 apply(simp only: mopup_jump_over1.simps mopup_aft_erase_a.simps) |
|
4176 apply(erule_tac exE)+ |
|
4177 apply(rule_tac x = ln in exI, rule_tac x = "Suc 0" in exI) |
|
4178 apply(case_tac m2, simp) |
|
4179 apply(rule_tac x = rn in exI, rule_tac x = "drop (Suc n) lm" in exI, |
|
4180 simp) |
|
4181 apply(simp) |
|
4182 done |
|
4183 |
|
4184 lemma [simp]: |
|
4185 "\<lbrakk>n < length lm; mopup_jump_over1 (Suc (2 * n), l, []) lm n ires\<rbrakk> \<Longrightarrow> |
|
4186 mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires" |
|
4187 apply(rule mopup_jump_over1_2_aft_erase_a, simp) |
|
4188 apply(auto simp: mopup_jump_over1.simps) |
|
4189 apply(rule_tac x = ln in exI, rule_tac x = "Suc (abc_lm_v lm n)" in exI, |
|
4190 rule_tac x = 0 in exI, simp add: ) |
|
4191 done |
|
4192 |
|
4193 |
|
4194 lemma [simp]: |
|
4195 "\<lbrakk>n < length lm; |
|
4196 mopup_aft_erase_a (Suc (Suc (2 * n)), l, Oc # xs) lm n ires\<rbrakk> |
|
4197 \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires" |
|
4198 apply(auto simp: mopup_aft_erase_a.simps mopup_aft_erase_b.simps ) |
|
4199 apply(case_tac ml) |
|
4200 apply(simp_all add: tape_of_nl_cons split: if_splits) |
|
4201 apply(case_tac a, simp_all) |
|
4202 apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) |
|
4203 apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp) |
|
4204 apply(case_tac a, simp_all) |
|
4205 apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp) |
|
4206 apply(rule_tac x = rn in exI) |
|
4207 apply(rule_tac x = "nat # list" in exI, simp add: tape_of_nl_cons) |
|
4208 done |
|
4209 |
|
4210 lemma [simp]: |
|
4211 "mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
4212 apply(auto simp: mopup_aft_erase_a.simps) |
|
4213 done |
|
4214 |
|
4215 lemma [simp]: |
|
4216 "\<lbrakk>n < length lm; |
|
4217 mopup_aft_erase_a (Suc (Suc (2 * n)), l, Bk # xs) lm n ires\<rbrakk> |
|
4218 \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, hd l # Bk # xs) lm n ires" |
|
4219 apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps) |
|
4220 apply(erule exE)+ |
|
4221 apply(case_tac lnr, simp) |
|
4222 apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits) |
|
4223 apply(auto) |
|
4224 apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits) |
|
4225 apply(rule_tac x = "Suc rn" in exI, simp) |
|
4226 done |
|
4227 |
|
4228 lemma [simp]: |
|
4229 "mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires \<Longrightarrow> l \<noteq> []" |
|
4230 apply(simp only: mopup_aft_erase_a.simps) |
|
4231 apply(erule exE)+ |
|
4232 apply(auto) |
|
4233 done |
|
4234 |
|
4235 lemma [simp]: |
|
4236 "\<lbrakk>n < length lm; mopup_aft_erase_a (Suc (Suc (2 * n)), l, []) lm n ires\<rbrakk> |
|
4237 \<Longrightarrow> mopup_left_moving (5 + 2 * n, tl l, [hd l]) lm n ires" |
|
4238 apply(simp only: mopup_aft_erase_a.simps mopup_left_moving.simps) |
|
4239 apply(erule exE)+ |
|
4240 apply(subgoal_tac "ml = [] \<and> rn = 0", erule conjE, erule conjE, simp) |
|
4241 apply(case_tac lnr, simp) |
|
4242 apply(rule_tac x = lnl in exI, simp) |
|
4243 apply(rule_tac x = 1 in exI, simp) |
|
4244 apply(case_tac ml, simp, simp) |
|
4245 done |
|
4246 |
|
4247 |
|
4248 lemma [simp]: "mopup_aft_erase_b (2 * n + 3, l, Oc # xs) lm n ires = False" |
|
4249 apply(auto simp: mopup_aft_erase_b.simps ) |
|
4250 done |
|
4251 |
|
4252 lemma tape_of_ex1[intro]: |
|
4253 "\<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" |
|
4254 apply(case_tac a, simp_all) |
|
4255 apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp) |
|
4256 apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp) |
|
4257 done |
|
4258 |
|
4259 lemma [intro]: "\<exists>rna ml. Oc \<up> a @ Bk # <list::nat list> @ Bk \<up> rn = |
|
4260 <ml> @ Bk \<up> rna \<or> Oc \<up> a @ Bk # <list> @ Bk \<up> rn = Bk # <ml::nat list> @ Bk \<up> rna" |
|
4261 apply(case_tac "list = []", simp add: replicate_Suc[THEN sym] del: replicate_Suc) |
|
4262 apply(rule_tac rn = "Suc rn" in tape_of_ex1) |
|
4263 apply(case_tac a, simp) |
|
4264 apply(rule_tac x = rn in exI, rule_tac x = list in exI, simp) |
|
4265 apply(rule_tac x = rn in exI, rule_tac x = "nat # list" in exI) |
|
4266 apply(simp add: tape_of_nl_cons) |
|
4267 done |
|
4268 |
|
4269 lemma [simp]: |
|
4270 "\<lbrakk>n < length lm; |
|
4271 mopup_aft_erase_c (2 * n + 4, l, Oc # xs) lm n ires\<rbrakk> |
|
4272 \<Longrightarrow> mopup_aft_erase_b (Suc (Suc (Suc (2 * n))), l, Bk # xs) lm n ires" |
|
4273 apply(auto simp: mopup_aft_erase_c.simps mopup_aft_erase_b.simps ) |
|
4274 apply(case_tac ml, simp_all add: tape_of_nl_cons split: if_splits, auto) |
|
4275 done |
|
4276 |
|
4277 lemma mopup_aft_erase_c_aft_erase_a[simp]: |
|
4278 "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, Bk # xs) lm n ires\<rbrakk> |
|
4279 \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, xs) lm n ires" |
|
4280 apply(simp only: mopup_aft_erase_c.simps mopup_aft_erase_a.simps ) |
|
4281 apply(erule_tac exE)+ |
|
4282 apply(erule conjE, erule conjE, erule disjE) |
|
4283 apply(subgoal_tac "ml = []", simp, case_tac rn, |
|
4284 simp, simp, rule conjI) |
|
4285 apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp) |
|
4286 apply(rule_tac x = nat in exI, rule_tac x = "[]" in exI, simp) |
|
4287 apply(case_tac ml, simp, simp add: tape_of_nl_cons split: if_splits) |
|
4288 apply(rule_tac x = lnl in exI, rule_tac x = "Suc lnr" in exI, simp) |
|
4289 apply(rule_tac x = rn in exI, rule_tac x = "ml" in exI, simp) |
|
4290 done |
|
4291 |
|
4292 lemma [simp]: |
|
4293 "\<lbrakk>n < length lm; mopup_aft_erase_c (2 * n + 4, l, []) lm n ires\<rbrakk> |
|
4294 \<Longrightarrow> mopup_aft_erase_a (Suc (Suc (2 * n)), Bk # l, []) lm n ires" |
|
4295 apply(rule mopup_aft_erase_c_aft_erase_a, simp) |
|
4296 apply(simp only: mopup_aft_erase_c.simps) |
|
4297 apply(erule exE)+ |
|
4298 apply(rule_tac x = lnl in exI, rule_tac x = lnr in exI, simp add: ) |
|
4299 apply(rule_tac x = 0 in exI, rule_tac x = "[]" in exI, simp) |
|
4300 done |
|
4301 |
|
4302 lemma mopup_aft_erase_b_2_aft_erase_c[simp]: |
|
4303 "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, Bk # xs) lm n ires\<rbrakk> |
|
4304 \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, xs) lm n ires" |
|
4305 apply(auto simp: mopup_aft_erase_b.simps mopup_aft_erase_c.simps) |
|
4306 apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp) |
|
4307 apply(rule_tac x = "lnl" in exI, rule_tac x = "Suc lnr" in exI, simp) |
|
4308 done |
|
4309 |
|
4310 lemma [simp]: |
|
4311 "\<lbrakk>n < length lm; mopup_aft_erase_b (2 * n + 3, l, []) lm n ires\<rbrakk> |
|
4312 \<Longrightarrow> mopup_aft_erase_c (4 + 2 * n, Bk # l, []) lm n ires" |
|
4313 apply(rule_tac mopup_aft_erase_b_2_aft_erase_c, simp) |
|
4314 apply(simp add: mopup_aft_erase_b.simps) |
|
4315 done |
|
4316 |
|
4317 lemma [simp]: |
|
4318 "mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
4319 apply(auto simp: mopup_left_moving.simps) |
|
4320 done |
|
4321 |
|
4322 lemma [simp]: |
|
4323 "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Oc # xs) lm n ires\<rbrakk> |
|
4324 \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires" |
|
4325 apply(simp only: mopup_left_moving.simps mopup_jump_over2.simps) |
|
4326 apply(erule_tac exE)+ |
|
4327 apply(erule conjE, erule disjE, erule conjE) |
|
4328 apply(case_tac rn, simp, simp add: ) |
|
4329 apply(case_tac "hd l", simp add: ) |
|
4330 apply(case_tac "abc_lm_v lm n", simp) |
|
4331 apply(rule_tac x = "lnl" in exI, rule_tac x = rn in exI, |
|
4332 rule_tac x = "Suc 0" in exI, rule_tac x = 0 in exI) |
|
4333 apply(case_tac lnl, simp, simp, simp add: exp_ind[THEN sym], simp) |
|
4334 apply(case_tac "abc_lm_v lm n", simp) |
|
4335 apply(case_tac lnl, simp, simp) |
|
4336 apply(rule_tac x = lnl in exI, rule_tac x = rn in exI) |
|
4337 apply(rule_tac x = nat in exI, rule_tac x = "Suc (Suc 0)" in exI, simp) |
|
4338 done |
|
4339 |
|
4340 lemma [simp]: "mopup_left_moving (2 * n + 5, l, xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
4341 apply(auto simp: mopup_left_moving.simps) |
|
4342 done |
|
4343 |
|
4344 lemma [simp]: |
|
4345 "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, Bk # xs) lm n ires\<rbrakk> |
|
4346 \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, hd l # Bk # xs) lm n ires" |
|
4347 apply(simp only: mopup_left_moving.simps) |
|
4348 apply(erule exE)+ |
|
4349 apply(case_tac lnr, simp) |
|
4350 apply(rule_tac x = lnl in exI, rule_tac x = nat in exI, simp) |
|
4351 apply(rule_tac x = "Suc rn" in exI, simp) |
|
4352 done |
|
4353 |
|
4354 lemma [simp]: |
|
4355 "\<lbrakk>n < length lm; mopup_left_moving (2 * n + 5, l, []) lm n ires\<rbrakk> |
|
4356 \<Longrightarrow> mopup_left_moving (2 * n + 5, tl l, [hd l]) lm n ires" |
|
4357 apply(simp only: mopup_left_moving.simps) |
|
4358 apply(erule exE)+ |
|
4359 apply(case_tac lnr, auto) |
|
4360 done |
|
4361 |
|
4362 |
|
4363 lemma [simp]: |
|
4364 "mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires \<Longrightarrow> l \<noteq> []" |
|
4365 apply(auto simp: mopup_jump_over2.simps ) |
|
4366 done |
|
4367 |
|
4368 lemma [simp]: |
|
4369 "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Oc # xs) lm n ires\<rbrakk> |
|
4370 \<Longrightarrow> mopup_jump_over2 (2 * n + 6, tl l, hd l # Oc # xs) lm n ires" |
|
4371 apply(simp only: mopup_jump_over2.simps) |
|
4372 apply(erule_tac exE)+ |
|
4373 apply(simp add: , erule conjE, erule_tac conjE) |
|
4374 apply(case_tac m1, simp) |
|
4375 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, |
|
4376 rule_tac x = 0 in exI, simp) |
|
4377 apply(case_tac ln, simp, simp, simp only: exp_ind[THEN sym], simp) |
|
4378 apply(rule_tac x = ln in exI, rule_tac x = rn in exI, |
|
4379 rule_tac x = nat in exI, rule_tac x = "Suc m2" in exI, simp) |
|
4380 done |
|
4381 |
|
4382 lemma [simp]: |
|
4383 "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\<rbrakk> |
|
4384 \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires" |
|
4385 apply(auto simp: mopup_jump_over2.simps mopup_stop.simps) |
|
4386 apply(simp_all add: tape_of_nat_abv exp_ind[THEN sym]) |
|
4387 done |
|
4388 |
|
4389 lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False" |
|
4390 apply(simp only: mopup_jump_over2.simps, simp) |
|
4391 done |
|
4392 |
|
4393 lemma mopup_inv_step: |
|
4394 "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> |
|
4395 \<Longrightarrow> mopup_inv (step (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0)) lm n ires" |
|
4396 apply(case_tac r, case_tac [2] a) |
|
4397 apply(auto split:if_splits simp add:step.simps) |
|
4398 apply(simp_all add: mopupfetchs) |
|
4399 done |
|
4400 |
|
4401 declare mopup_inv.simps[simp del] |
|
4402 lemma mopup_inv_steps: |
|
4403 "\<lbrakk>n < length lm; mopup_inv (s, l, r) lm n ires\<rbrakk> \<Longrightarrow> |
|
4404 mopup_inv (steps (s, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp) lm n ires" |
|
4405 apply(induct_tac stp, simp add: steps.simps) |
|
4406 apply(simp add: step_red) |
|
4407 apply(case_tac "steps (s, l, r) |
|
4408 (mopup_a n @ shift mopup_b (2 * n), 0) na", simp) |
|
4409 apply(rule_tac mopup_inv_step, simp, simp) |
|
4410 done |
|
4411 |
|
4412 fun abc_mopup_stage1 :: "config \<Rightarrow> nat \<Rightarrow> nat" |
|
4413 where |
|
4414 "abc_mopup_stage1 (s, l, r) n = |
|
4415 (if s > 0 \<and> s \<le> 2*n then 6 |
|
4416 else if s = 2*n + 1 then 4 |
|
4417 else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then 3 |
|
4418 else if s = 2*n + 5 then 2 |
|
4419 else if s = 2*n + 6 then 1 |
|
4420 else 0)" |
|
4421 |
|
4422 fun abc_mopup_stage2 :: "config \<Rightarrow> nat \<Rightarrow> nat" |
|
4423 where |
|
4424 "abc_mopup_stage2 (s, l, r) n = |
|
4425 (if s > 0 \<and> s \<le> 2*n then length r |
|
4426 else if s = 2*n + 1 then length r |
|
4427 else if s = 2*n + 5 then length l |
|
4428 else if s = 2*n + 6 then length l |
|
4429 else if s \<ge> 2*n + 2 \<and> s \<le> 2*n + 4 then length r |
|
4430 else 0)" |
|
4431 |
|
4432 fun abc_mopup_stage3 :: "config \<Rightarrow> nat \<Rightarrow> nat" |
|
4433 where |
|
4434 "abc_mopup_stage3 (s, l, r) n = |
|
4435 (if s > 0 \<and> s \<le> 2*n then |
|
4436 if hd r = Bk then 0 |
|
4437 else 1 |
|
4438 else if s = 2*n + 2 then 1 |
|
4439 else if s = 2*n + 3 then 0 |
|
4440 else if s = 2*n + 4 then 2 |
|
4441 else 0)" |
|
4442 |
|
4443 definition |
|
4444 "abc_mopup_measure = measures [\<lambda>(c, n). abc_mopup_stage1 c n, |
|
4445 \<lambda>(c, n). abc_mopup_stage2 c n, |
|
4446 \<lambda>(c, n). abc_mopup_stage3 c n]" |
|
4447 |
|
4448 lemma wf_abc_mopup_measure: |
|
4449 shows "wf abc_mopup_measure" |
|
4450 unfolding abc_mopup_measure_def |
|
4451 by auto |
|
4452 |
|
4453 lemma abc_mopup_measure_induct [case_names Step]: |
|
4454 "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> abc_mopup_measure\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
4455 using wf_abc_mopup_measure |
|
4456 by (metis wf_iff_no_infinite_down_chain) |
|
4457 |
|
4458 lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False" |
|
4459 apply(auto simp: mopup_bef_erase_a.simps) |
|
4460 done |
|
4461 |
|
4462 lemma [simp]: "mopup_bef_erase_b (a, aa, []) lm n ires = False" |
|
4463 apply(auto simp: mopup_bef_erase_b.simps) |
|
4464 done |
|
4465 |
|
4466 lemma [simp]: "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False" |
|
4467 apply(auto simp: mopup_aft_erase_b.simps) |
|
4468 done |
|
4469 |
|
4470 declare mopup_inv.simps[simp del] |
|
4471 |
|
4472 lemma [simp]: |
|
4473 "\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow> |
|
4474 (fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk) = (R, 2*q - 1)" |
|
4475 apply(case_tac q, simp, simp) |
|
4476 apply(auto simp: fetch.simps nth_of.simps nth_append) |
|
4477 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = |
|
4478 mopup_a (Suc nat) ! ((4 * nat) + 2)", |
|
4479 simp add: mopup_a.simps nth_append) |
|
4480 apply(rule mopup_a_nth, auto) |
|
4481 done |
|
4482 |
|
4483 lemma mopup_halt: |
|
4484 assumes |
|
4485 less: "n < length lm" |
|
4486 and inv: "mopup_inv (Suc 0, l, r) lm n ires" |
|
4487 and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" |
|
4488 and P: "P = (\<lambda> (c, n). is_final c)" |
|
4489 shows "\<exists> stp. P (f stp)" |
|
4490 proof (induct rule: abc_mopup_measure_induct) |
|
4491 case (Step na) |
|
4492 have h: "\<not> P (f na)" by fact |
|
4493 show "(f (Suc na), f na) \<in> abc_mopup_measure" |
|
4494 proof(simp add: f) |
|
4495 obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)" |
|
4496 apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto) |
|
4497 done |
|
4498 then have "mopup_inv (a, b, c) lm n ires" |
|
4499 using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na] |
|
4500 apply(simp) |
|
4501 done |
|
4502 moreover have "a > 0" |
|
4503 using h g |
|
4504 apply(simp add: f P) |
|
4505 done |
|
4506 ultimately |
|
4507 have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure" |
|
4508 apply(case_tac c, case_tac [2] aa) |
|
4509 apply(auto split:if_splits simp add:step.simps mopup_inv.simps) |
|
4510 apply(simp_all add: mopupfetchs abc_mopup_measure_def lex_triple_def lex_pair_def ) |
|
4511 done |
|
4512 thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) |
|
4513 (mopup_a n @ shift mopup_b (2 * n), 0), n), |
|
4514 steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n) |
|
4515 \<in> abc_mopup_measure" |
|
4516 using g by simp |
|
4517 qed |
|
4518 qed |
|
4519 |
|
4520 lemma mopup_inv_start: |
|
4521 "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" |
|
4522 apply(auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps) |
|
4523 apply(case_tac [!] am, auto split: if_splits simp: tape_of_nl_cons) |
|
4524 apply(rule_tac x = "Suc a" in exI, rule_tac x = k in exI, simp) |
|
4525 apply(case_tac [!] n, simp_all add: abc_lm_v.simps) |
|
4526 apply(case_tac k, simp, simp_all) |
|
4527 done |
|
4528 |
|
4529 lemma mopup_correct: |
|
4530 assumes less: "n < length (am::nat list)" |
|
4531 and rs: "abc_lm_v am n = rs" |
|
4532 shows "\<exists> stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp) |
|
4533 = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)" |
|
4534 using less |
|
4535 proof - |
|
4536 have a: "mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires" |
|
4537 using less |
|
4538 apply(simp add: mopup_inv_start) |
|
4539 done |
|
4540 then have "\<exists> stp. is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)" |
|
4541 using less mopup_halt[of n am "Bk # Bk # ires" "<am> @ Bk \<up> k" ires |
|
4542 "(\<lambda>stp. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))" |
|
4543 "(\<lambda>(c, n). is_final c)"] |
|
4544 apply(simp) |
|
4545 done |
|
4546 from this obtain stp where b: |
|
4547 "is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)" .. |
|
4548 from a b have |
|
4549 "mopup_inv (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp) |
|
4550 am n ires" |
|
4551 apply(rule_tac mopup_inv_steps, simp_all add: less) |
|
4552 done |
|
4553 from b and this show "?thesis" |
|
4554 apply(rule_tac x = stp in exI, simp) |
|
4555 apply(case_tac "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) |
|
4556 (mopup_a n @ shift mopup_b (2 * n), 0) stp") |
|
4557 apply(simp add: mopup_inv.simps mopup_stop.simps rs) |
|
4558 using rs |
|
4559 apply(simp add: tape_of_nat_abv) |
|
4560 done |
|
4561 qed |
|
4562 |
|
4563 (*we can use Hoare_plus here*) |
|
4564 |
|
4565 lemma wf_mopup[intro]: "tm_wf (mopup n, 0)" |
|
4566 apply(induct n, simp add: mopup.simps shift.simps mopup_b_def tm_wf.simps) |
|
4567 apply(auto simp: mopup.simps shift.simps mopup_b_def tm_wf.simps) |
|
4568 done |
|
4569 |
|
4570 lemma length_tp: |
3762 lemma length_tp: |
4571 "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> |
3763 "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> |
4572 start_of ly (length ap) = Suc (length tp div 2)" |
3764 start_of ly (length ap) = Suc (length tp div 2)" |
4573 apply(frule_tac length_tp', simp_all) |
3765 apply(frule_tac length_tp', simp_all) |
4574 apply(simp add: start_of.simps) |
3766 apply(simp add: start_of.simps) |