47 where |
47 where |
48 "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4), |
48 "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4), |
49 (R, 2), (R, 2), (L, 5), (W0, 4), |
49 (R, 2), (R, 2), (L, 5), (W0, 4), |
50 (R, 0), (L, 5)]" |
50 (R, 0), (L, 5)]" |
51 |
51 |
52 definition |
52 idefinition |
53 tcopy :: "instr list" |
53 tcopy :: "instr list" |
54 where |
54 where |
55 "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end" |
55 "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end" |
56 |
56 |
57 |
57 |
79 if s = 2 then inv_begin2 n (l, r) else |
79 if s = 2 then inv_begin2 n (l, r) else |
80 if s = 3 then inv_begin3 n (l, r) else |
80 if s = 3 then inv_begin3 n (l, r) else |
81 if s = 4 then inv_begin4 n (l, r) |
81 if s = 4 then inv_begin4 n (l, r) |
82 else False)" |
82 else False)" |
83 |
83 |
84 |
|
85 |
|
86 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
84 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
87 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
85 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
88 apply(rule_tac x = "Suc i" in exI, simp) |
86 apply(rule_tac x = "Suc i" in exI, simp) |
89 done |
87 done |
90 |
88 |
91 lemma inv_begin_step: |
89 lemma inv_begin_step: |
92 "\<lbrakk>inv_begin x cf; x > 0\<rbrakk> |
90 "\<lbrakk>inv_begin x cf; x > 0\<rbrakk> \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))" |
93 \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))" |
|
94 unfolding tcopy_begin_def |
91 unfolding tcopy_begin_def |
95 apply(case_tac cf) |
92 apply(case_tac cf) |
96 apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits) |
93 apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits) |
97 apply(case_tac "hd c", auto simp: inv_begin.simps) |
94 apply(case_tac "hd c", auto simp: inv_begin.simps) |
98 apply(case_tac c, simp_all) |
95 apply(case_tac c, simp_all) |
137 |
134 |
138 lemma wf_begin_le: "wf init_LE" |
135 lemma wf_begin_le: "wf init_LE" |
139 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def) |
136 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def) |
140 |
137 |
141 lemma init_halt: |
138 lemma init_halt: |
142 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" |
139 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)" |
143 proof(rule_tac LE = init_LE in halt_lemma) |
140 proof(rule_tac LE = init_LE in halt_lemma) |
144 show "wf init_LE" by(simp add: wf_begin_le) |
141 show "wf init_LE" by(simp add: wf_begin_le) |
145 next |
142 next |
146 assume h: "0 < x" |
143 assume h: "0 < x" |
147 show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
144 show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
171 qed |
168 qed |
172 qed |
169 qed |
173 qed |
170 qed |
174 |
171 |
175 lemma init_correct: |
172 lemma init_correct: |
176 "x > 0 \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}" |
173 "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}" |
177 proof(rule_tac Hoare_haltI) |
174 proof(rule_tac Hoare_haltI) |
178 fix l r |
175 fix l r |
179 assume h: "0 < x" |
176 assume h: "0 < x" "inv_begin1 x (l, r)" |
180 "inv_begin1 x (l, r)" |
177 hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)" |
181 hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" |
178 by (rule_tac init_halt) |
182 by(erule_tac init_halt) |
|
183 then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" .. |
179 then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" .. |
184 moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" |
180 moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" |
185 apply(rule_tac inv_begin_steps) |
181 apply(rule_tac inv_begin_steps) |
186 using h by(simp_all add: inv_begin.simps) |
182 using h by(simp_all add: inv_begin.simps) |
187 ultimately show |
183 ultimately show |
1002 apply(auto simp add: numeral tape_of_nat_abv) |
998 apply(auto simp add: numeral tape_of_nat_abv) |
1003 by (metis Suc_neq_Zero is_final_eq) |
999 by (metis Suc_neq_Zero is_final_eq) |
1004 |
1000 |
1005 |
1001 |
1006 lemma dither_halts_aux: |
1002 lemma dither_halts_aux: |
1007 shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 3 = (0, Bk \<up> m, [Oc, Oc])" |
1003 shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])" |
1008 unfolding dither_def |
1004 unfolding dither_def |
1009 by (simp add: steps.simps step.simps numeral) |
1005 by (simp add: steps.simps step.simps numeral) |
1010 |
1006 |
1011 lemma dither_halts: |
1007 lemma dither_halts: |
1012 shows "{dither_halt_inv} dither {dither_halt_inv}" |
1008 shows "{dither_halt_inv} dither {dither_halt_inv}" |