|
1 theory SCT_Interpretation |
|
2 imports Main SCT_Misc SCT_Definition |
|
3 begin |
|
4 |
|
5 |
|
6 definition |
|
7 "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))" |
|
8 |
|
9 lemma not_acc_smaller: |
|
10 assumes notacc: "\<not> acc R x" |
|
11 shows "\<exists>y. R y x \<and> \<not> acc R y" |
|
12 proof (rule classical) |
|
13 assume "\<not> ?thesis" |
|
14 hence "\<And>y. R y x \<Longrightarrow> acc R y" by blast |
|
15 with accI have "acc R x" . |
|
16 with notacc show ?thesis by contradiction |
|
17 qed |
|
18 |
|
19 lemma non_acc_has_idseq: |
|
20 assumes "\<not> acc R x" |
|
21 shows "\<exists>s. idseq R s x" |
|
22 proof - |
|
23 |
|
24 have "\<exists>f. \<forall>x. \<not>acc R x \<longrightarrow> R (f x) x \<and> \<not>acc R (f x)" |
|
25 by (rule choice, auto simp:not_acc_smaller) |
|
26 |
|
27 then obtain f where |
|
28 in_R: "\<And>x. \<not>acc R x \<Longrightarrow> R (f x) x" |
|
29 and nia: "\<And>x. \<not>acc R x \<Longrightarrow> \<not>acc R (f x)" |
|
30 by blast |
|
31 |
|
32 let ?s = "\<lambda>i. (f ^ i) x" |
|
33 |
|
34 { |
|
35 fix i |
|
36 have "\<not>acc R (?s i)" |
|
37 by (induct i) (auto simp:nia `\<not>acc R x`) |
|
38 hence "R (f (?s i)) (?s i)" |
|
39 by (rule in_R) |
|
40 } |
|
41 |
|
42 hence "idseq R ?s x" |
|
43 unfolding idseq_def |
|
44 by auto |
|
45 |
|
46 thus ?thesis by auto |
|
47 qed |
|
48 |
|
49 |
|
50 |
|
51 |
|
52 |
|
53 types ('a, 'q) cdesc = |
|
54 "('q \<Rightarrow> bool) \<times> ('q \<Rightarrow> 'a) \<times>('q \<Rightarrow> 'a)" |
|
55 |
|
56 |
|
57 fun in_cdesc :: "('a, 'q) cdesc \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
58 where |
|
59 "in_cdesc (\<Gamma>, r, l) x y = (\<exists>q. x = r q \<and> y = l q \<and> \<Gamma> q)" |
|
60 |
|
61 fun mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
62 where |
|
63 "mk_rel [] x y = False" |
|
64 "mk_rel (c#cs) x y = |
|
65 (in_cdesc c x y \<or> mk_rel cs x y)" |
|
66 |
|
67 |
|
68 lemma some_rd: |
|
69 assumes "mk_rel rds x y" |
|
70 shows "\<exists>rd\<in>set rds. in_cdesc rd x y" |
|
71 using prems |
|
72 by (induct rds) (auto simp:in_cdesc_def) |
|
73 |
|
74 (* from a value sequence, get a sequence of rds *) |
|
75 |
|
76 lemma ex_cs: |
|
77 assumes idseq: "idseq (mk_rel rds) s x" |
|
78 shows "\<exists>cs. \<forall>i. cs i \<in> set rds \<and> in_cdesc (cs i) (s (Suc i)) (s i)" |
|
79 proof - |
|
80 from idseq |
|
81 have a: "\<forall>i. \<exists>rd \<in> set rds. in_cdesc rd (s (Suc i)) (s i)" |
|
82 by (auto simp:idseq_def intro:some_rd) |
|
83 |
|
84 show ?thesis |
|
85 by (rule choice) (insert a, blast) |
|
86 qed |
|
87 |
|
88 |
|
89 |
|
90 types ('q, 'a) interpr = "('a, 'q) cdesc \<times> (nat \<Rightarrow> 'a \<Rightarrow> nat)" |
|
91 types 'a measures = "nat \<Rightarrow> 'a \<Rightarrow> nat" |
|
92 |
|
93 |
|
94 fun stepP :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> |
|
95 ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> bool" |
|
96 where |
|
97 "stepP (\<Gamma>1,r1,l1) (\<Gamma>2,r2,l2) m1 m2 R |
|
98 = (\<forall>q\<^isub>1 q\<^isub>2. \<Gamma>1 q\<^isub>1 \<and> \<Gamma>2 q\<^isub>2 \<and> r1 q\<^isub>1 = l2 q\<^isub>2 |
|
99 \<longrightarrow> R (m2 (l2 q\<^isub>2)) ((m1 (l1 q\<^isub>1))))" |
|
100 |
|
101 |
|
102 definition |
|
103 decr :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> |
|
104 ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" |
|
105 where |
|
106 "decr c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op <)" |
|
107 |
|
108 definition |
|
109 decreq :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> |
|
110 ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool" |
|
111 where |
|
112 "decreq c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op \<le>)" |
|
113 |
|
114 definition |
|
115 no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool" |
|
116 where |
|
117 "no_step c1 c2 = stepP c1 c2 (\<lambda>x. 0) (\<lambda>x. 0) (\<lambda>x y. False)" |
|
118 |
|
119 |
|
120 |
|
121 lemma decr_in_cdesc: |
|
122 assumes "in_cdesc RD1 y x" |
|
123 assumes "in_cdesc RD2 z y" |
|
124 assumes "decr RD1 RD2 m1 m2" |
|
125 shows "m2 y < m1 x" |
|
126 using prems |
|
127 by (cases RD1, cases RD2, auto simp:decr_def) |
|
128 |
|
129 lemma decreq_in_cdesc: |
|
130 assumes "in_cdesc RD1 y x" |
|
131 assumes "in_cdesc RD2 z y" |
|
132 assumes "decreq RD1 RD2 m1 m2" |
|
133 shows "m2 y \<le> m1 x" |
|
134 using prems |
|
135 by (cases RD1, cases RD2, auto simp:decreq_def) |
|
136 |
|
137 |
|
138 lemma no_inf_desc_nat_sequence: |
|
139 fixes s :: "nat \<Rightarrow> nat" |
|
140 assumes leq: "\<And>i. n \<le> i \<Longrightarrow> s (Suc i) \<le> s i" |
|
141 assumes less: "\<exists>\<^sub>\<infinity>i. s (Suc i) < s i" |
|
142 shows False |
|
143 proof - |
|
144 { |
|
145 fix i j:: nat |
|
146 assume "n \<le> i" |
|
147 assume "i \<le> j" |
|
148 { |
|
149 fix k |
|
150 have "s (i + k) \<le> s i" |
|
151 proof (induct k) |
|
152 case 0 thus ?case by simp |
|
153 next |
|
154 case (Suc k) |
|
155 with leq[of "i + k"] `n \<le> i` |
|
156 show ?case by simp |
|
157 qed |
|
158 } |
|
159 from this[of "j - i"] `n \<le> i` `i \<le> j` |
|
160 have "s j \<le> s i" by auto |
|
161 } |
|
162 note decr = this |
|
163 |
|
164 let ?min = "LEAST x. x \<in> range (\<lambda>i. s (n + i))" |
|
165 have "?min \<in> range (\<lambda>i. s (n + i))" |
|
166 by (rule LeastI) auto |
|
167 then obtain k where min: "?min = s (n + k)" by auto |
|
168 |
|
169 from less |
|
170 obtain k' where "n + k < k'" |
|
171 and "s (Suc k') < s k'" |
|
172 unfolding INF_nat by auto |
|
173 |
|
174 with decr[of "n + k" k'] min |
|
175 have "s (Suc k') < ?min" by auto |
|
176 moreover from `n + k < k'` |
|
177 have "s (Suc k') = s (n + (Suc k' - n))" by simp |
|
178 ultimately |
|
179 show False using not_less_Least by blast |
|
180 qed |
|
181 |
|
182 |
|
183 |
|
184 definition |
|
185 approx :: "scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc |
|
186 \<Rightarrow> 'a measures \<Rightarrow> 'a measures \<Rightarrow> bool" |
|
187 where |
|
188 "approx G C C' M M' |
|
189 = (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j)) |
|
190 \<and>(eq G i j \<longrightarrow> decreq C C' (M i) (M' j)))" |
|
191 |
|
192 |
|
193 |
|
194 |
|
195 (* Unfolding "approx" for finite graphs *) |
|
196 |
|
197 lemma approx_empty: |
|
198 "approx (Graph {}) c1 c2 ms1 ms2" |
|
199 unfolding approx_def has_edge_def dest_graph.simps by simp |
|
200 |
|
201 lemma approx_less: |
|
202 assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)" |
|
203 assumes "approx (Graph Es) c1 c2 ms1 ms2" |
|
204 shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2" |
|
205 using prems |
|
206 unfolding approx_def has_edge_def dest_graph.simps decr_def |
|
207 by auto |
|
208 |
|
209 lemma approx_leq: |
|
210 assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)" |
|
211 assumes "approx (Graph Es) c1 c2 ms1 ms2" |
|
212 shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2" |
|
213 using prems |
|
214 unfolding approx_def has_edge_def dest_graph.simps decreq_def |
|
215 by auto |
|
216 |
|
217 |
|
218 lemma "approx (Graph {(1, \<down>, 2),(2, \<Down>, 3)}) c1 c2 ms1 ms2" |
|
219 apply (intro approx_less approx_leq approx_empty) |
|
220 oops |
|
221 |
|
222 |
|
223 (* |
|
224 fun |
|
225 no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool" |
|
226 where |
|
227 "no_step (\<Gamma>1, r1, l1) (\<Gamma>2, r2, l2) = |
|
228 (\<forall>q\<^isub>1 q\<^isub>2. \<Gamma>1 q\<^isub>1 \<and> \<Gamma>2 q\<^isub>2 \<and> r1 q\<^isub>1 = l2 q\<^isub>2 \<longrightarrow> False)" |
|
229 *) |
|
230 |
|
231 lemma no_stepI: |
|
232 "stepP c1 c2 m1 m2 (\<lambda>x y. False) |
|
233 \<Longrightarrow> no_step c1 c2" |
|
234 by (cases c1, cases c2) (auto simp: no_step_def) |
|
235 |
|
236 definition |
|
237 sound_int :: "acg \<Rightarrow> ('a, 'q) cdesc list |
|
238 \<Rightarrow> 'a measures list \<Rightarrow> bool" |
|
239 where |
|
240 "sound_int \<A> RDs M = |
|
241 (\<forall>n<length RDs. \<forall>m<length RDs. |
|
242 no_step (RDs ! n) (RDs ! m) \<or> |
|
243 (\<exists>G. (\<A> \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m) \<and> approx G (RDs ! n) (RDs ! m) (M ! n) (M ! m)))" |
|
244 |
|
245 |
|
246 (* The following are uses by the tactics *) |
|
247 lemma length_simps: "length [] = 0" "length (x#xs) = Suc (length xs)" |
|
248 by auto |
|
249 |
|
250 lemma all_less_zero: "\<forall>n<(0::nat). P n" |
|
251 by simp |
|
252 |
|
253 lemma all_less_Suc: |
|
254 assumes Pk: "P k" |
|
255 assumes Pn: "\<forall>n<k. P n" |
|
256 shows "\<forall>n<Suc k. P n" |
|
257 proof (intro allI impI) |
|
258 fix n assume "n < Suc k" |
|
259 show "P n" |
|
260 proof (cases "n < k") |
|
261 case True with Pn show ?thesis by simp |
|
262 next |
|
263 case False with `n < Suc k` have "n = k" by simp |
|
264 with Pk show ?thesis by simp |
|
265 qed |
|
266 qed |
|
267 |
|
268 |
|
269 lemma step_witness: |
|
270 assumes "in_cdesc RD1 y x" |
|
271 assumes "in_cdesc RD2 z y" |
|
272 shows "\<not> no_step RD1 RD2" |
|
273 using prems |
|
274 by (cases RD1, cases RD2) (auto simp:no_step_def) |
|
275 |
|
276 |
|
277 theorem SCT_on_relations: |
|
278 assumes R: "R = mk_rel RDs" |
|
279 assumes sound: "sound_int \<A> RDs M" |
|
280 assumes "SCT \<A>" |
|
281 shows "\<forall>x. acc R x" |
|
282 proof (rule, rule classical) |
|
283 fix x |
|
284 assume "\<not> acc R x" |
|
285 with non_acc_has_idseq |
|
286 have "\<exists>s. idseq R s x" . |
|
287 then obtain s where "idseq R s x" .. |
|
288 hence "\<exists>cs. \<forall>i. cs i \<in> set RDs \<and> |
|
289 in_cdesc (cs i) (s (Suc i)) (s i)" |
|
290 unfolding R by (rule ex_cs) |
|
291 then obtain cs where |
|
292 [simp]: "\<And>i. cs i \<in> set RDs" |
|
293 and ird[simp]: "\<And>i. in_cdesc (cs i) (s (Suc i)) (s i)" |
|
294 by blast |
|
295 |
|
296 let ?cis = "\<lambda>i. index_of RDs (cs i)" |
|
297 have "\<forall>i. \<exists>G. (\<A> \<turnstile> ?cis i \<leadsto>\<^bsup>G\<^esup> (?cis (Suc i))) |
|
298 \<and> approx G (RDs ! ?cis i) (RDs ! ?cis (Suc i)) |
|
299 (M ! ?cis i) (M ! ?cis (Suc i))" (is "\<forall>i. \<exists>G. ?P i G") |
|
300 proof |
|
301 fix i |
|
302 let ?n = "?cis i" and ?n' = "?cis (Suc i)" |
|
303 |
|
304 have "in_cdesc (RDs ! ?n) (s (Suc i)) (s i)" |
|
305 "in_cdesc (RDs ! ?n') (s (Suc (Suc i))) (s (Suc i))" |
|
306 by (simp_all add:index_of_member) |
|
307 with step_witness |
|
308 have "\<not> no_step (RDs ! ?n) (RDs ! ?n')" . |
|
309 moreover have |
|
310 "?n < length RDs" |
|
311 "?n' < length RDs" |
|
312 by (simp_all add:index_of_length[symmetric]) |
|
313 ultimately |
|
314 obtain G |
|
315 where "\<A> \<turnstile> ?n \<leadsto>\<^bsup>G\<^esup> ?n'" |
|
316 and "approx G (RDs ! ?n) (RDs ! ?n') (M ! ?n) (M ! ?n')" |
|
317 using sound |
|
318 unfolding sound_int_def by auto |
|
319 |
|
320 thus "\<exists>G. ?P i G" by blast |
|
321 qed |
|
322 with choice |
|
323 have "\<exists>Gs. \<forall>i. ?P i (Gs i)" . |
|
324 then obtain Gs where |
|
325 A: "\<And>i. \<A> \<turnstile> ?cis i \<leadsto>\<^bsup>(Gs i)\<^esup> (?cis (Suc i))" |
|
326 and B: "\<And>i. approx (Gs i) (RDs ! ?cis i) (RDs ! ?cis (Suc i)) |
|
327 (M ! ?cis i) (M ! ?cis (Suc i))" |
|
328 by blast |
|
329 |
|
330 let ?p = "\<lambda>i. (?cis i, Gs i)" |
|
331 |
|
332 from A have "has_ipath \<A> ?p" |
|
333 unfolding has_ipath_def |
|
334 by auto |
|
335 |
|
336 with `SCT \<A>` SCT_def |
|
337 obtain th where "is_desc_thread th ?p" |
|
338 by auto |
|
339 |
|
340 then obtain n |
|
341 where fr: "\<forall>i\<ge>n. eqlat ?p th i" |
|
342 and inf: "\<exists>\<^sub>\<infinity>i. descat ?p th i" |
|
343 unfolding is_desc_thread_def by auto |
|
344 |
|
345 from B |
|
346 have approx: |
|
347 "\<And>i. approx (Gs i) (cs i) (cs (Suc i)) |
|
348 (M ! ?cis i) (M ! ?cis (Suc i))" |
|
349 by (simp add:index_of_member) |
|
350 |
|
351 let ?seq = "\<lambda>i. (M ! ?cis i) (th i) (s i)" |
|
352 |
|
353 have "\<And>i. n < i \<Longrightarrow> ?seq (Suc i) \<le> ?seq i" |
|
354 proof - |
|
355 fix i |
|
356 let ?q1 = "th i" and ?q2 = "th (Suc i)" |
|
357 assume "n < i" |
|
358 |
|
359 with fr have "eqlat ?p th i" by simp |
|
360 hence "dsc (Gs i) ?q1 ?q2 \<or> eq (Gs i) ?q1 ?q2" |
|
361 by simp |
|
362 thus "?seq (Suc i) \<le> ?seq i" |
|
363 proof |
|
364 assume "dsc (Gs i) ?q1 ?q2" |
|
365 |
|
366 with approx |
|
367 have a:"decr (cs i) (cs (Suc i)) |
|
368 ((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" |
|
369 unfolding approx_def by auto |
|
370 |
|
371 show ?thesis |
|
372 apply (rule less_imp_le) |
|
373 apply (rule decr_in_cdesc[of _ "s (Suc i)" "s i"]) |
|
374 by (rule ird a)+ |
|
375 next |
|
376 assume "eq (Gs i) ?q1 ?q2" |
|
377 |
|
378 with approx |
|
379 have a:"decreq (cs i) (cs (Suc i)) |
|
380 ((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" |
|
381 unfolding approx_def by auto |
|
382 |
|
383 show ?thesis |
|
384 apply (rule decreq_in_cdesc[of _ "s (Suc i)" "s i"]) |
|
385 by (rule ird a)+ |
|
386 qed |
|
387 qed |
|
388 moreover have "\<exists>\<^sub>\<infinity>i. ?seq (Suc i) < ?seq i" unfolding INF_nat |
|
389 proof |
|
390 fix i |
|
391 from inf obtain j where "i < j" and d: "descat ?p th j" |
|
392 unfolding INF_nat by auto |
|
393 let ?q1 = "th j" and ?q2 = "th (Suc j)" |
|
394 from d have "dsc (Gs j) ?q1 ?q2" by auto |
|
395 |
|
396 with approx |
|
397 have a:"decr (cs j) (cs (Suc j)) |
|
398 ((M ! ?cis j) ?q1) ((M ! ?cis (Suc j)) ?q2)" |
|
399 unfolding approx_def by auto |
|
400 |
|
401 have "?seq (Suc j) < ?seq j" |
|
402 apply (rule decr_in_cdesc[of _ "s (Suc j)" "s j"]) |
|
403 by (rule ird a)+ |
|
404 with `i < j` |
|
405 show "\<exists>j. i < j \<and> ?seq (Suc j) < ?seq j" by auto |
|
406 qed |
|
407 ultimately have False |
|
408 by (rule no_inf_desc_nat_sequence[of "Suc n"]) simp |
|
409 thus "acc R x" .. |
|
410 qed |
|
411 |
|
412 |
|
413 end |