15 text {* |
15 text {* |
16 Inductive definition of the accessible part @{term "acc r"} of a |
16 Inductive definition of the accessible part @{term "acc r"} of a |
17 relation; see also \cite{paulin-tlca}. |
17 relation; see also \cite{paulin-tlca}. |
18 *} |
18 *} |
19 |
19 |
20 inductive2 |
20 inductive_set |
21 acc :: "('a => 'a => bool) => 'a => bool" |
21 acc :: "('a * 'a) set => 'a set" |
22 for r :: "'a => 'a => bool" |
22 for r :: "('a * 'a) set" |
23 where |
23 where |
24 accI: "(!!y. r y x ==> acc r y) ==> acc r x" |
24 accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r" |
25 |
25 |
26 abbreviation |
26 abbreviation |
27 termi :: "('a => 'a => bool) => 'a => bool" where |
27 termip :: "('a => 'a => bool) => 'a => bool" where |
28 "termi r == acc (r\<inverse>\<inverse>)" |
28 "termip r == accp (r\<inverse>\<inverse>)" |
|
29 |
|
30 abbreviation |
|
31 termi :: "('a * 'a) set => 'a set" where |
|
32 "termi r == acc (r\<inverse>)" |
29 |
33 |
30 |
34 |
31 subsection {* Induction rules *} |
35 subsection {* Induction rules *} |
32 |
36 |
33 theorem acc_induct: |
37 theorem accp_induct: |
34 assumes major: "acc r a" |
38 assumes major: "accp r a" |
35 assumes hyp: "!!x. acc r x ==> \<forall>y. r y x --> P y ==> P x" |
39 assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x" |
36 shows "P a" |
40 shows "P a" |
37 apply (rule major [THEN acc.induct]) |
41 apply (rule major [THEN accp.induct]) |
38 apply (rule hyp) |
42 apply (rule hyp) |
39 apply (rule accI) |
43 apply (rule accp.accI) |
40 apply fast |
44 apply fast |
41 apply fast |
45 apply fast |
42 done |
46 done |
43 |
47 |
44 theorems acc_induct_rule = acc_induct [rule_format, induct set: acc] |
48 theorems accp_induct_rule = accp_induct [rule_format, induct set: accp] |
45 |
49 |
46 theorem acc_downward: "acc r b ==> r a b ==> acc r a" |
50 theorem accp_downward: "accp r b ==> r a b ==> accp r a" |
47 apply (erule acc.cases) |
51 apply (erule accp.cases) |
48 apply fast |
52 apply fast |
49 done |
53 done |
50 |
54 |
51 lemma not_acc_down: |
55 lemma not_accp_down: |
52 assumes na: "\<not> acc R x" |
56 assumes na: "\<not> accp R x" |
53 obtains z where "R z x" and "\<not> acc R z" |
57 obtains z where "R z x" and "\<not> accp R z" |
54 proof - |
58 proof - |
55 assume a: "\<And>z. \<lbrakk>R z x; \<not> acc R z\<rbrakk> \<Longrightarrow> thesis" |
59 assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis" |
56 |
60 |
57 show thesis |
61 show thesis |
58 proof (cases "\<forall>z. R z x \<longrightarrow> acc R z") |
62 proof (cases "\<forall>z. R z x \<longrightarrow> accp R z") |
59 case True |
63 case True |
60 hence "\<And>z. R z x \<Longrightarrow> acc R z" by auto |
64 hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto |
61 hence "acc R x" |
65 hence "accp R x" |
62 by (rule accI) |
66 by (rule accp.accI) |
63 with na show thesis .. |
67 with na show thesis .. |
64 next |
68 next |
65 case False then obtain z where "R z x" and "\<not> acc R z" |
69 case False then obtain z where "R z x" and "\<not> accp R z" |
66 by auto |
70 by auto |
67 with a show thesis . |
71 with a show thesis . |
68 qed |
72 qed |
69 qed |
73 qed |
70 |
74 |
71 lemma acc_downwards_aux: "r\<^sup>*\<^sup>* b a ==> acc r a --> acc r b" |
75 lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b" |
72 apply (erule rtrancl_induct') |
76 apply (erule rtranclp_induct) |
73 apply blast |
77 apply blast |
74 apply (blast dest: acc_downward) |
78 apply (blast dest: accp_downward) |
75 done |
79 done |
76 |
80 |
77 theorem acc_downwards: "acc r a ==> r\<^sup>*\<^sup>* b a ==> acc r b" |
81 theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b" |
78 apply (blast dest: acc_downwards_aux) |
82 apply (blast dest: accp_downwards_aux) |
79 done |
83 done |
80 |
84 |
81 theorem acc_wfI: "\<forall>x. acc r x ==> wfP r" |
85 theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r" |
82 apply (rule wfPUNIVI) |
86 apply (rule wfPUNIVI) |
83 apply (induct_tac P x rule: acc_induct) |
87 apply (induct_tac P x rule: accp_induct) |
84 apply blast |
88 apply blast |
85 apply blast |
89 apply blast |
86 done |
90 done |
87 |
91 |
88 theorem acc_wfD: "wfP r ==> acc r x" |
92 theorem accp_wfPD: "wfP r ==> accp r x" |
89 apply (erule wfP_induct_rule) |
93 apply (erule wfP_induct_rule) |
90 apply (rule accI) |
94 apply (rule accp.accI) |
91 apply blast |
95 apply blast |
92 done |
96 done |
93 |
97 |
94 theorem wf_acc_iff: "wfP r = (\<forall>x. acc r x)" |
98 theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)" |
95 apply (blast intro: acc_wfI dest: acc_wfD) |
99 apply (blast intro: accp_wfPI dest: accp_wfPD) |
96 done |
100 done |
97 |
101 |
98 |
102 |
99 text {* Smaller relations have bigger accessible parts: *} |
103 text {* Smaller relations have bigger accessible parts: *} |
100 |
104 |
101 lemma acc_subset: |
105 lemma accp_subset: |
102 assumes sub: "R1 \<le> R2" |
106 assumes sub: "R1 \<le> R2" |
103 shows "acc R2 \<le> acc R1" |
107 shows "accp R2 \<le> accp R1" |
104 proof |
108 proof |
105 fix x assume "acc R2 x" |
109 fix x assume "accp R2 x" |
106 then show "acc R1 x" |
110 then show "accp R1 x" |
107 proof (induct x) |
111 proof (induct x) |
108 fix x |
112 fix x |
109 assume ih: "\<And>y. R2 y x \<Longrightarrow> acc R1 y" |
113 assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y" |
110 with sub show "acc R1 x" |
114 with sub show "accp R1 x" |
111 by (blast intro: accI) |
115 by (blast intro: accp.accI) |
112 qed |
116 qed |
113 qed |
117 qed |
114 |
118 |
115 |
119 |
116 text {* This is a generalized induction theorem that works on |
120 text {* This is a generalized induction theorem that works on |
117 subsets of the accessible part. *} |
121 subsets of the accessible part. *} |
118 |
122 |
119 lemma acc_subset_induct: |
123 lemma accp_subset_induct: |
120 assumes subset: "D \<le> acc R" |
124 assumes subset: "D \<le> accp R" |
121 and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z" |
125 and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z" |
122 and "D x" |
126 and "D x" |
123 and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x" |
127 and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x" |
124 shows "P x" |
128 shows "P x" |
125 proof - |
129 proof - |
126 from subset and `D x` |
130 from subset and `D x` |
127 have "acc R x" .. |
131 have "accp R x" .. |
128 then show "P x" using `D x` |
132 then show "P x" using `D x` |
129 proof (induct x) |
133 proof (induct x) |
130 fix x |
134 fix x |
131 assume "D x" |
135 assume "D x" |
132 and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y" |
136 and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y" |
133 with dcl and istep show "P x" by blast |
137 with dcl and istep show "P x" by blast |
134 qed |
138 qed |
135 qed |
139 qed |
136 |
140 |
|
141 |
|
142 text {* Set versions of the above theorems *} |
|
143 |
|
144 lemmas acc_induct = accp_induct [to_set] |
|
145 |
|
146 lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] |
|
147 |
|
148 lemmas acc_downward = accp_downward [to_set] |
|
149 |
|
150 lemmas not_acc_down = not_accp_down [to_set] |
|
151 |
|
152 lemmas acc_downwards_aux = accp_downwards_aux [to_set] |
|
153 |
|
154 lemmas acc_downwards = accp_downwards [to_set] |
|
155 |
|
156 lemmas acc_wfI = accp_wfPI [to_set] |
|
157 |
|
158 lemmas acc_wfD = accp_wfPD [to_set] |
|
159 |
|
160 lemmas wf_acc_iff = wfP_accp_iff [to_set] |
|
161 |
|
162 lemmas acc_subset = accp_subset [to_set] |
|
163 |
|
164 lemmas acc_subset_induct = accp_subset_induct [to_set] |
|
165 |
137 end |
166 end |