11 |
11 |
12 definition |
12 definition |
13 "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))" |
13 "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))" |
14 |
14 |
15 lemma not_acc_smaller: |
15 lemma not_acc_smaller: |
16 assumes notacc: "\<not> acc R x" |
16 assumes notacc: "\<not> accp R x" |
17 shows "\<exists>y. R y x \<and> \<not> acc R y" |
17 shows "\<exists>y. R y x \<and> \<not> accp R y" |
18 proof (rule classical) |
18 proof (rule classical) |
19 assume "\<not> ?thesis" |
19 assume "\<not> ?thesis" |
20 hence "\<And>y. R y x \<Longrightarrow> acc R y" by blast |
20 hence "\<And>y. R y x \<Longrightarrow> accp R y" by blast |
21 with accI have "acc R x" . |
21 with accp.accI have "accp R x" . |
22 with notacc show ?thesis by contradiction |
22 with notacc show ?thesis by contradiction |
23 qed |
23 qed |
24 |
24 |
25 lemma non_acc_has_idseq: |
25 lemma non_acc_has_idseq: |
26 assumes "\<not> acc R x" |
26 assumes "\<not> accp R x" |
27 shows "\<exists>s. idseq R s x" |
27 shows "\<exists>s. idseq R s x" |
28 proof - |
28 proof - |
29 |
29 |
30 have "\<exists>f. \<forall>x. \<not>acc R x \<longrightarrow> R (f x) x \<and> \<not>acc R (f x)" |
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) |
31 by (rule choice, auto simp:not_acc_smaller) |
32 |
32 |
33 then obtain f where |
33 then obtain f where |
34 in_R: "\<And>x. \<not>acc R x \<Longrightarrow> R (f x) x" |
34 in_R: "\<And>x. \<not>accp R x \<Longrightarrow> R (f x) x" |
35 and nia: "\<And>x. \<not>acc R x \<Longrightarrow> \<not>acc R (f x)" |
35 and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)" |
36 by blast |
36 by blast |
37 |
37 |
38 let ?s = "\<lambda>i. (f ^ i) x" |
38 let ?s = "\<lambda>i. (f ^ i) x" |
39 |
39 |
40 { |
40 { |
41 fix i |
41 fix i |
42 have "\<not>acc R (?s i)" |
42 have "\<not>accp R (?s i)" |
43 by (induct i) (auto simp:nia `\<not>acc R x`) |
43 by (induct i) (auto simp:nia `\<not>accp R x`) |
44 hence "R (f (?s i)) (?s i)" |
44 hence "R (f (?s i)) (?s i)" |
45 by (rule in_R) |
45 by (rule in_R) |
46 } |
46 } |
47 |
47 |
48 hence "idseq R ?s x" |
48 hence "idseq R ?s x" |
279 |
279 |
280 theorem SCT_on_relations: |
280 theorem SCT_on_relations: |
281 assumes R: "R = mk_rel RDs" |
281 assumes R: "R = mk_rel RDs" |
282 assumes sound: "sound_int \<A> RDs M" |
282 assumes sound: "sound_int \<A> RDs M" |
283 assumes "SCT \<A>" |
283 assumes "SCT \<A>" |
284 shows "\<forall>x. acc R x" |
284 shows "\<forall>x. accp R x" |
285 proof (rule, rule classical) |
285 proof (rule, rule classical) |
286 fix x |
286 fix x |
287 assume "\<not> acc R x" |
287 assume "\<not> accp R x" |
288 with non_acc_has_idseq |
288 with non_acc_has_idseq |
289 have "\<exists>s. idseq R s x" . |
289 have "\<exists>s. idseq R s x" . |
290 then obtain s where "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> |
291 hence "\<exists>cs. \<forall>i. cs i \<in> set RDs \<and> |
292 in_cdesc (cs i) (s (Suc i)) (s i)" |
292 in_cdesc (cs i) (s (Suc i)) (s i)" |