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