61 | "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))" |
61 | "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))" |
62 | "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))" |
62 | "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))" |
63 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))" |
63 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))" |
64 | "inv_begin4 n (l, r) = (n > 0 \<and> (l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc]))" |
64 | "inv_begin4 n (l, r) = (n > 0 \<and> (l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc]))" |
65 |
65 |
|
66 |
|
67 |
66 fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool" |
68 fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool" |
67 where |
69 where |
68 "inv_begin n (s, l, r) = |
70 "inv_begin n (s, tp) = |
69 (if s = 0 then inv_begin0 n (l, r) else |
71 (if s = 0 then inv_begin0 n tp else |
70 if s = 1 then inv_begin1 n (l, r) else |
72 if s = 1 then inv_begin1 n tp else |
71 if s = 2 then inv_begin2 n (l, r) else |
73 if s = 2 then inv_begin2 n tp else |
72 if s = 3 then inv_begin3 n (l, r) else |
74 if s = 3 then inv_begin3 n tp else |
73 if s = 4 then inv_begin4 n (l, r) |
75 if s = 4 then inv_begin4 n tp |
74 else False)" |
76 else False)" |
75 |
77 |
76 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
78 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
77 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
79 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
78 by (rule_tac x = "Suc i" in exI, simp) |
80 by (rule_tac x = "Suc i" in exI, simp) |
118 "begin_LE = measures [measure_begin_state, measure_begin_step]" |
120 "begin_LE = measures [measure_begin_state, measure_begin_step]" |
119 |
121 |
120 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]" |
122 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]" |
121 by (case_tac r, auto, case_tac a, auto) |
123 by (case_tac r, auto, case_tac a, auto) |
122 |
124 |
|
125 |
|
126 lemma halt_lemma: |
|
127 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
128 by (metis wf_iff_no_infinite_down_chain) |
|
129 |
123 lemma begin_halt: |
130 lemma begin_halt: |
124 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)" |
131 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)" |
125 proof(rule_tac LE = begin_LE in halt_lemma) |
132 proof(rule_tac LE = begin_LE in halt_lemma) |
126 show "wf begin_LE" unfolding begin_LE_def by (auto) |
133 show "wf begin_LE" unfolding begin_LE_def by (auto) |
127 next |
134 next |
128 assume h: "0 < x" |
135 assume h: "0 < x" |
129 show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
136 show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
153 qed |
160 qed |
154 qed |
161 qed |
155 qed |
162 qed |
156 |
163 |
157 lemma begin_correct: |
164 lemma begin_correct: |
158 "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}" |
165 "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}" |
159 proof(rule_tac Hoare_haltI) |
166 proof(rule_tac Hoare_haltI) |
160 fix l r |
167 fix l r |
161 assume h: "0 < x" "inv_begin1 x (l, r)" |
168 assume h: "0 < n" "inv_begin1 n (l, r)" |
162 hence "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)" |
169 then have "\<exists> stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)" |
163 by (rule_tac begin_halt) |
170 by (rule_tac begin_halt) |
164 then obtain stp where "is_final (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)" .. |
171 then obtain stp where "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)" .. |
165 moreover have "inv_begin x (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)" |
172 moreover have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)" |
166 apply(rule_tac inv_begin_steps) |
173 apply(rule_tac inv_begin_steps) |
167 using h by(simp_all add: inv_begin.simps) |
174 using h by(simp_all add: inv_begin.simps) |
168 ultimately show |
175 ultimately show |
169 "\<exists>n. is_final (steps (1, l, r) (tcopy_begin, 0) n) \<and> |
176 "\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and> |
170 inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 0) n" |
177 inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp" |
171 using h |
178 using h |
172 apply(rule_tac x = stp in exI) |
179 apply(rule_tac x = stp in exI) |
173 apply(case_tac "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps) |
180 apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps) |
174 done |
181 done |
175 qed |
182 qed |
176 |
183 |
177 declare tm_comp.simps [simp del] |
184 declare tm_comp.simps [simp del] |
178 declare adjust.simps[simp del] |
185 declare adjust.simps[simp del] |
891 moreover |
898 moreover |
892 have "{inv_loop1 x} tcopy_loop {inv_loop0 x}" |
899 have "{inv_loop1 x} tcopy_loop {inv_loop0 x}" |
893 by (metis assms loop_correct) |
900 by (metis assms loop_correct) |
894 moreover |
901 moreover |
895 have "inv_begin0 x \<mapsto> inv_loop1 x" |
902 have "inv_begin0 x \<mapsto> inv_loop1 x" |
896 by (auto simp: inv_begin0.simps inv_loop1.simps assert_imp_def) |
903 unfolding assert_imp_def |
897 (rule_tac x = "Suc 0" in exI, auto) |
904 unfolding inv_begin0.simps inv_loop1.simps |
|
905 unfolding inv_loop1_loop.simps inv_loop1_exit.simps |
|
906 apply(auto simp add: numeral Cons_eq_append_conv) |
|
907 by (rule_tac x = "Suc 0" in exI, auto) |
898 ultimately |
908 ultimately |
899 have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}" |
909 have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}" |
900 by (rule_tac Hoare_plus_halt) (auto) |
910 by (rule_tac Hoare_plus_halt) (auto) |
901 moreover |
911 moreover |
902 have "{inv_end1 x} tcopy_end {inv_end0 x}" |
912 have "{inv_end1 x} tcopy_end {inv_end0 x}" |
920 proof - |
930 proof - |
921 have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}" |
931 have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}" |
922 by (rule tcopy_correct1) (simp) |
932 by (rule tcopy_correct1) (simp) |
923 moreover |
933 moreover |
924 have "pre_tcopy n = inv_begin1 (Suc n)" |
934 have "pre_tcopy n = inv_begin1 (Suc n)" |
925 by (auto simp add: tape_of_nl_abv) |
935 by (auto simp add: tape_of_nl_abv tape_of_nat_abv) |
926 moreover |
936 moreover |
927 have "inv_end0 (Suc n) = post_tcopy n" |
937 have "inv_end0 (Suc n) = post_tcopy n" |
928 by (auto simp add: inv_end0.simps tape_of_nl_abv) |
938 by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nl_abv) |
929 ultimately |
939 ultimately |
930 show "{pre_tcopy n} tcopy {post_tcopy n}" |
940 show "{pre_tcopy n} tcopy {post_tcopy n}" |
931 by simp |
941 by simp |
932 qed |
942 qed |
933 |
943 |