62 inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
62 inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
63 inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
63 inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
64 inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
64 inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
65 inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
65 inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
66 where |
66 where |
67 "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or> |
67 "inv_init0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or> |
68 (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))" |
68 (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))" |
69 | "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)" |
69 | "inv_init1 n (l, r) = ((l, r) = ([], Oc \<up> n))" |
70 | "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)" |
70 | "inv_init2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))" |
71 | "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])" |
71 | "inv_init3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))" |
72 | "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))" |
72 | "inv_init4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))" |
73 |
73 |
74 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool" |
74 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool" |
75 where |
75 where |
76 "inv_init x (s, l, r) = |
76 "inv_init n (s, l, r) = |
77 (if s = 0 then inv_init0 x (l, r) |
77 (if s = 0 then inv_init0 n (l, r) else |
78 else if s = 1 then inv_init1 x (l, r) |
78 if s = 1 then inv_init1 n (l, r) else |
79 else if s = 2 then inv_init2 x (l, r) |
79 if s = 2 then inv_init2 n (l, r) else |
80 else if s = 3 then inv_init3 x (l, r) |
80 if s = 3 then inv_init3 n (l, r) else |
81 else if s = 4 then inv_init4 x (l, r) |
81 if s = 4 then inv_init4 n (l, r) |
82 else False)" |
82 else False)" |
83 |
83 |
84 declare inv_init.simps[simp del] |
|
85 |
84 |
86 |
85 |
87 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
86 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
88 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
87 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
89 apply(rule_tac x = "Suc i" in exI, simp) |
88 apply(rule_tac x = "Suc i" in exI, simp) |
107 apply(rule_tac inv_init_step, simp_all) |
106 apply(rule_tac inv_init_step, simp_all) |
108 done |
107 done |
109 |
108 |
110 fun init_state :: "config \<Rightarrow> nat" |
109 fun init_state :: "config \<Rightarrow> nat" |
111 where |
110 where |
112 "init_state (s, l, r) = (if s = 0 then 0 |
111 "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
113 else 5 - s)" |
|
114 |
112 |
115 fun init_step :: "config \<Rightarrow> nat" |
113 fun init_step :: "config \<Rightarrow> nat" |
116 where |
114 where |
117 "init_step (s, l, r) = (if s = 2 then length r |
115 "init_step (s, l, r) = |
118 else if s = 3 then if r = [] \<or> r = [Bk] then Suc 0 else 0 |
116 (if s = 2 then length r else |
119 else if s = 4 then length l |
117 if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else |
120 else 0)" |
118 if s = 4 then length l |
|
119 else 0)" |
121 |
120 |
122 fun init_measure :: "config \<Rightarrow> nat \<times> nat" |
121 fun init_measure :: "config \<Rightarrow> nat \<times> nat" |
123 where |
122 where |
124 "init_measure c = |
123 "init_measure c = (init_state c, init_step c)" |
125 (init_state c, init_step c)" |
|
126 |
124 |
127 |
125 |
128 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set" |
126 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set" |
129 where |
127 where |
130 "lex_pair \<equiv> less_than <*lex*> less_than" |
128 "lex_pair \<equiv> less_than <*lex*> less_than" |
131 |
129 |
132 definition init_LE :: "(config \<times> config) set" |
130 definition init_LE :: "(config \<times> config) set" |
133 where |
131 where |
134 "init_LE \<equiv> (inv_image lex_pair init_measure)" |
132 "init_LE \<equiv> (inv_image lex_pair init_measure)" |
135 |
133 |
136 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]" |
134 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]" |
137 apply(case_tac r, auto, case_tac a, auto) |
135 by (case_tac r, auto, case_tac a, auto) |
138 done |
136 |
139 |
137 |
140 lemma wf_init_le: "wf init_LE" |
138 lemma wf_init_le: "wf init_LE" |
141 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def) |
139 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def) |
142 |
140 |
143 lemma init_halt: |
141 lemma init_halt: |
162 moreover hence "inv_init x (s, l, r)" |
160 moreover hence "inv_init x (s, l, r)" |
163 using c b by simp |
161 using c b by simp |
164 ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), |
162 ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), |
165 steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE" |
163 steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE" |
166 using a |
164 using a |
167 proof(simp) |
165 proof(simp del: inv_init.simps) |
168 assume "inv_init x (s, l, r)" "0 < s" |
166 assume "inv_init x (s, l, r)" "0 < s" |
169 thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE" |
167 thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE" |
170 apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral |
168 apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_init_def numeral split: if_splits) |
171 split: if_splits) |
|
172 apply(case_tac r, auto, case_tac a, auto) |
169 apply(case_tac r, auto, case_tac a, auto) |
173 done |
170 done |
174 qed |
171 qed |
175 qed |
172 qed |
176 qed |
173 qed |
197 qed |
194 qed |
198 |
195 |
199 |
196 |
200 (* tcopy_loop *) |
197 (* tcopy_loop *) |
201 |
198 |
202 fun inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
199 fun |
203 where |
200 inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
204 "inv_loop1_loop x (l, r) = |
201 inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
205 (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)" |
202 inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
206 |
203 inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
207 fun inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
204 inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
208 where |
205 inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
209 "inv_loop1_exit x (l, r) = |
206 inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
210 (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )" |
207 inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
211 |
208 inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
212 fun inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
209 inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
213 where |
|
214 "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))" |
|
215 |
|
216 fun inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
|
217 where |
|
218 "inv_loop2 x (l, r) = |
|
219 (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)" |
|
220 |
|
221 fun inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
|
222 where |
|
223 "inv_loop3 x (l, r) = |
|
224 (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)" |
|
225 |
|
226 fun inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
|
227 where |
|
228 "inv_loop4 x (l, r) = |
|
229 (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)" |
|
230 |
|
231 fun inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
|
232 where |
210 where |
233 "inv_loop5_loop x (l, r) = |
211 "inv_loop0 x (l, r) = (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )" |
234 (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)" |
212 | "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)" |
235 |
213 | "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)" |
236 fun inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
214 | "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))" |
237 where |
215 | "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)" |
238 "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)" |
216 | "inv_loop3 x (l, r) = |
239 |
217 (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)" |
240 fun inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
218 | "inv_loop4 x (l, r) = |
241 where |
219 (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)" |
242 "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> |
220 | "inv_loop5_loop x (l, r) = |
243 inv_loop5_exit x (l, r))" |
221 (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)" |
|
222 | "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)" |
|
223 | "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))" |
244 |
224 |
245 fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
225 fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
246 where |
226 where |
247 "inv_loop6_loop x (l, r) = |
227 "inv_loop6_loop x (l, r) = |
248 (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)" |
228 (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)" |
253 (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)" |
233 (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)" |
254 |
234 |
255 fun inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
235 fun inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
256 where |
236 where |
257 "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))" |
237 "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))" |
258 |
|
259 fun inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
|
260 where |
|
261 "inv_loop0 x (l, r) = |
|
262 (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )" |
|
263 |
238 |
264 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool" |
239 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool" |
265 where |
240 where |
266 "inv_loop x (s, l, r) = |
241 "inv_loop x (s, l, r) = |
267 (if s = 0 then inv_loop0 x (l, r) |
242 (if s = 0 then inv_loop0 x (l, r) |
275 |
250 |
276 declare inv_loop.simps[simp del] inv_loop1.simps[simp del] |
251 declare inv_loop.simps[simp del] inv_loop1.simps[simp del] |
277 inv_loop2.simps[simp del] inv_loop3.simps[simp del] |
252 inv_loop2.simps[simp del] inv_loop3.simps[simp del] |
278 inv_loop4.simps[simp del] inv_loop5.simps[simp del] |
253 inv_loop4.simps[simp del] inv_loop5.simps[simp del] |
279 inv_loop6.simps[simp del] |
254 inv_loop6.simps[simp del] |
|
255 |
280 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR" |
256 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR" |
281 apply(case_tac t, auto) |
257 by (case_tac t, auto) |
282 done |
|
283 |
|
284 |
258 |
285 lemma [simp]: "inv_loop1 x (b, []) = False" |
259 lemma [simp]: "inv_loop1 x (b, []) = False" |
286 by(simp add: inv_loop1.simps) |
260 by(simp add: inv_loop1.simps) |
287 |
261 |
288 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])" |
262 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])" |
289 apply(auto simp: inv_loop2.simps inv_loop3.simps) |
263 by (auto simp: inv_loop2.simps inv_loop3.simps) |
290 done |
264 |
291 |
265 |
292 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])" |
266 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])" |
293 apply(auto simp: inv_loop3.simps) |
267 by (auto simp: inv_loop3.simps) |
294 done |
268 |
295 |
269 |
296 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])" |
270 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])" |
297 apply(auto simp: inv_loop4.simps inv_loop5.simps) |
271 apply(auto simp: inv_loop4.simps inv_loop5.simps) |
298 apply(rule_tac [!] x = i in exI, |
272 apply(rule_tac [!] x = i in exI, |
299 rule_tac [!] x = "Suc j" in exI, simp_all) |
273 rule_tac [!] x = "Suc j" in exI, simp_all) |
1068 where |
1042 where |
1069 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] " |
1043 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] " |
1070 |
1044 |
1071 (* invariants of dither *) |
1045 (* invariants of dither *) |
1072 abbreviation |
1046 abbreviation |
1073 "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]" |
1047 "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))" |
1074 |
1048 |
1075 abbreviation |
1049 abbreviation |
1076 "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]" |
1050 "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))" |
1077 |
1051 |
1078 lemma dither_loops_aux: |
1052 lemma dither_loops_aux: |
1079 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> |
1053 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> |
1080 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))" |
1054 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))" |
1081 apply(induct stp) |
1055 apply(induct stp) |
1328 lemma tcontra_unhalt: |
1302 lemma tcontra_unhalt: |
1329 assumes "\<not> haltP0 tcontra [code tcontra]" |
1303 assumes "\<not> haltP0 tcontra [code tcontra]" |
1330 shows "False" |
1304 shows "False" |
1331 proof - |
1305 proof - |
1332 (* invariants *) |
1306 (* invariants *) |
1333 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1307 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)" |
1334 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1308 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)" |
1335 def P3 \<equiv> "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]" |
1309 def P3 \<equiv> "\<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))" |
1336 |
1310 |
1337 (* |
1311 (* |
1338 {P1} tcopy {P2} {P2} H {P3} |
1312 {P1} tcopy {P2} {P2} H {P3} |
1339 ---------------------------- |
1313 ---------------------------- |
1340 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1314 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1347 (* {P1} (tcopy |+| H) {P3} *) |
1321 (* {P1} (tcopy |+| H) {P3} *) |
1348 have first: "{P1} (tcopy |+| H) {P3}" |
1322 have first: "{P1} (tcopy |+| H) {P3}" |
1349 proof (cases rule: Hoare_plus_halt_simple) |
1323 proof (cases rule: Hoare_plus_halt_simple) |
1350 case A_halt (* of tcopy *) |
1324 case A_halt (* of tcopy *) |
1351 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1325 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1352 by (rule tcopy_correct2) |
1326 by (simp) (rule tcopy_correct2) |
1353 next |
1327 next |
1354 case B_halt (* of H *) |
1328 case B_halt (* of H *) |
1355 show "{P2} H {P3}" |
1329 show "{P2} H {P3}" |
1356 unfolding P2_def P3_def |
1330 unfolding P2_def P3_def |
1357 using assms by (rule H_halt_inv) |
1331 using assms by (simp) (rule H_halt_inv) |
1358 qed (simp) |
1332 qed (simp) |
1359 |
1333 |
1360 (* {P3} dither {P3} *) |
1334 (* {P3} dither {P3} *) |
1361 have second: "{P3} dither {P3}" unfolding P3_def |
1335 have second: "{P3} dither {P3}" unfolding P3_def |
1362 by (rule dither_halts) |
1336 by (rule dither_halts) |
1382 lemma tcontra_halt: |
1356 lemma tcontra_halt: |
1383 assumes "haltP0 tcontra [code tcontra]" |
1357 assumes "haltP0 tcontra [code tcontra]" |
1384 shows "False" |
1358 shows "False" |
1385 proof - |
1359 proof - |
1386 (* invariants *) |
1360 (* invariants *) |
1387 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1361 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)" |
1388 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1362 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)" |
1389 def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1363 def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))" |
1390 |
1364 |
1391 (* |
1365 (* |
1392 {P1} tcopy {P2} {P2} H {P3} |
1366 {P1} tcopy {P2} {P2} H {P3} |
1393 ---------------------------- |
1367 ---------------------------- |
1394 {P1} (tcopy |+| H) {P3} {P3} dither loops |
1368 {P1} (tcopy |+| H) {P3} {P3} dither loops |
1401 (* {P1} (tcopy |+| H) {P3} *) |
1375 (* {P1} (tcopy |+| H) {P3} *) |
1402 have first: "{P1} (tcopy |+| H) {P3}" |
1376 have first: "{P1} (tcopy |+| H) {P3}" |
1403 proof (cases rule: Hoare_plus_halt_simple) |
1377 proof (cases rule: Hoare_plus_halt_simple) |
1404 case A_halt (* of tcopy *) |
1378 case A_halt (* of tcopy *) |
1405 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1379 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1406 by (rule tcopy_correct2) |
1380 by (simp) (rule tcopy_correct2) |
1407 next |
1381 next |
1408 case B_halt (* of H *) |
1382 case B_halt (* of H *) |
1409 then show "{P2} H {P3}" |
1383 then show "{P2} H {P3}" |
1410 unfolding P2_def P3_def |
1384 unfolding P2_def P3_def |
1411 using assms by (rule H_unhalt_inv) |
1385 using assms by (simp) (rule H_unhalt_inv) |
1412 qed (simp) |
1386 qed (simp) |
1413 |
1387 |
1414 (* {P3} dither loops *) |
1388 (* {P3} dither loops *) |
1415 have second: "{P3} dither \<up>" unfolding P3_def |
1389 have second: "{P3} dither \<up>" unfolding P3_def |
1416 by (rule dither_loops) |
1390 by (rule dither_loops) |