12 imports Transitive_Closure |
12 imports Transitive_Closure |
13 begin |
13 begin |
14 |
14 |
15 subsection \<open>Basic Definitions\<close> |
15 subsection \<open>Basic Definitions\<close> |
16 |
16 |
17 definition wf :: "('a * 'a) set => bool" where |
17 definition wf :: "('a \<times> 'a) set \<Rightarrow> bool" |
18 "wf r \<longleftrightarrow> (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))" |
18 where "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))" |
19 |
19 |
20 definition wfP :: "('a => 'a => bool) => bool" where |
20 definition wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
21 "wfP r \<longleftrightarrow> wf {(x, y). r x y}" |
21 where "wfP r \<longleftrightarrow> wf {(x, y). r x y}" |
22 |
22 |
23 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r" |
23 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r" |
24 by (simp add: wfP_def) |
24 by (simp add: wfP_def) |
25 |
25 |
26 lemma wfUNIVI: |
26 lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r" |
27 "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)" |
|
28 unfolding wf_def by blast |
27 unfolding wf_def by blast |
29 |
28 |
30 lemmas wfPUNIVI = wfUNIVI [to_pred] |
29 lemmas wfPUNIVI = wfUNIVI [to_pred] |
31 |
30 |
32 text\<open>Restriction to domain @{term A} and range @{term B}. If @{term r} is |
31 text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>. |
33 well-founded over their intersection, then @{term "wf r"}\<close> |
32 If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close> |
34 lemma wfI: |
33 lemma wfI: |
35 "[| r \<subseteq> A \<times> B; |
34 assumes "r \<subseteq> A \<times> B" |
36 !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x; x : A; x : B |] ==> P x |] |
35 and "\<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x; x \<in> A; x \<in> B\<rbrakk> \<Longrightarrow> P x" |
37 ==> wf r" |
36 shows "wf r" |
38 unfolding wf_def by blast |
37 using assms unfolding wf_def by blast |
39 |
38 |
40 lemma wf_induct: |
39 lemma wf_induct: |
41 "[| wf(r); |
40 assumes "wf r" |
42 !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) |
41 and "\<And>x. \<forall>y. (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x" |
43 |] ==> P(a)" |
42 shows "P a" |
44 unfolding wf_def by blast |
43 using assms unfolding wf_def by blast |
45 |
44 |
46 lemmas wfP_induct = wf_induct [to_pred] |
45 lemmas wfP_induct = wf_induct [to_pred] |
47 |
46 |
48 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
47 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
49 |
48 |
50 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] |
49 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] |
51 |
50 |
52 lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r" |
51 lemma wf_not_sym: "wf r \<Longrightarrow> (a, x) \<in> r \<Longrightarrow> (x, a) \<notin> r" |
53 by (induct a arbitrary: x set: wf) blast |
52 by (induct a arbitrary: x set: wf) blast |
54 |
53 |
55 lemma wf_asym: |
54 lemma wf_asym: |
56 assumes "wf r" "(a, x) \<in> r" |
55 assumes "wf r" "(a, x) \<in> r" |
57 obtains "(x, a) \<notin> r" |
56 obtains "(x, a) \<notin> r" |
58 by (drule wf_not_sym[OF assms]) |
57 by (drule wf_not_sym[OF assms]) |
59 |
58 |
60 lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r" |
59 lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r" |
61 by (blast elim: wf_asym) |
60 by (blast elim: wf_asym) |
62 |
61 |
63 lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r" |
62 lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r" |
64 by (drule wf_not_refl[OF assms]) |
63 by (drule wf_not_refl[OF assms]) |
65 |
64 |
66 lemma wf_wellorderI: |
65 lemma wf_wellorderI: |
67 assumes wf: "wf {(x::'a::ord, y). x < y}" |
66 assumes wf: "wf {(x::'a::ord, y). x < y}" |
68 assumes lin: "OFCLASS('a::ord, linorder_class)" |
67 assumes lin: "OFCLASS('a::ord, linorder_class)" |
69 shows "OFCLASS('a::ord, wellorder_class)" |
68 shows "OFCLASS('a::ord, wellorder_class)" |
70 using lin by (rule wellorder_class.intro) |
69 using lin |
71 (rule class.wellorder_axioms.intro, rule wf_induct_rule [OF wf], simp) |
70 apply (rule wellorder_class.intro) |
72 |
71 apply (rule class.wellorder_axioms.intro) |
73 lemma (in wellorder) wf: |
72 apply (rule wf_induct_rule [OF wf]) |
74 "wf {(x, y). x < y}" |
73 apply simp |
75 unfolding wf_def by (blast intro: less_induct) |
74 done |
|
75 |
|
76 lemma (in wellorder) wf: "wf {(x, y). x < y}" |
|
77 unfolding wf_def by (blast intro: less_induct) |
76 |
78 |
77 |
79 |
78 subsection \<open>Basic Results\<close> |
80 subsection \<open>Basic Results\<close> |
79 |
81 |
80 text \<open>Point-free characterization of well-foundedness\<close> |
82 text \<open>Point-free characterization of well-foundedness\<close> |
118 |
120 |
119 lemma wfI_min: |
121 lemma wfI_min: |
120 assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q" |
122 assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q" |
121 shows "wf R" |
123 shows "wf R" |
122 proof (rule wfI_pf) |
124 proof (rule wfI_pf) |
123 fix A assume b: "A \<subseteq> R `` A" |
125 fix A |
124 { fix x assume "x \<in> A" |
126 assume b: "A \<subseteq> R `` A" |
125 from a[OF this] b have "False" by blast |
127 have False if "x \<in> A" for x |
126 } |
128 using a[OF that] b by blast |
127 thus "A = {}" by blast |
129 then show "A = {}" by blast |
128 qed |
130 qed |
129 |
131 |
130 lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))" |
132 lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))" |
131 apply auto |
133 apply auto |
132 apply (erule wfE_min, assumption, blast) |
134 apply (erule wfE_min, assumption, blast) |
133 apply (rule wfI_min, auto) |
135 apply (rule wfI_min, auto) |
134 done |
136 done |
135 |
137 |
136 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] |
138 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] |
137 |
139 |
138 text\<open>Well-foundedness of transitive closure\<close> |
140 |
|
141 subsubsection \<open>Well-foundedness of transitive closure\<close> |
139 |
142 |
140 lemma wf_trancl: |
143 lemma wf_trancl: |
141 assumes "wf r" |
144 assumes "wf r" |
142 shows "wf (r^+)" |
145 shows "wf (r\<^sup>+)" |
143 proof - |
146 proof - |
144 { |
147 have "P x" if induct_step: "\<And>x. (\<And>y. (y, x) \<in> r\<^sup>+ \<Longrightarrow> P y) \<Longrightarrow> P x" for P x |
145 fix P and x |
148 proof (rule induct_step) |
146 assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x" |
149 show "P y" if "(y, x) \<in> r\<^sup>+" for y |
147 have "P x" |
150 using \<open>wf r\<close> and that |
148 proof (rule induct_step) |
151 proof (induct x arbitrary: y) |
149 fix y assume "(y, x) : r^+" |
152 case (less x) |
150 with \<open>wf r\<close> show "P y" |
153 note hyp = \<open>\<And>x' y'. (x', x) \<in> r \<Longrightarrow> (y', x') \<in> r\<^sup>+ \<Longrightarrow> P y'\<close> |
151 proof (induct x arbitrary: y) |
154 from \<open>(y, x) \<in> r\<^sup>+\<close> show "P y" |
152 case (less x) |
155 proof cases |
153 note hyp = \<open>\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'\<close> |
156 case base |
154 from \<open>(y, x) : r^+\<close> show "P y" |
157 show "P y" |
155 proof cases |
158 proof (rule induct_step) |
156 case base |
159 fix y' |
157 show "P y" |
160 assume "(y', y) \<in> r\<^sup>+" |
158 proof (rule induct_step) |
161 with \<open>(y, x) \<in> r\<close> show "P y'" |
159 fix y' assume "(y', y) : r^+" |
162 by (rule hyp [of y y']) |
160 with \<open>(y, x) : r\<close> show "P y'" by (rule hyp [of y y']) |
|
161 qed |
|
162 next |
|
163 case step |
|
164 then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp |
|
165 then show "P y" by (rule hyp [of x' y]) |
|
166 qed |
163 qed |
|
164 next |
|
165 case step |
|
166 then obtain x' where "(x', x) \<in> r" and "(y, x') \<in> r\<^sup>+" |
|
167 by simp |
|
168 then show "P y" by (rule hyp [of x' y]) |
167 qed |
169 qed |
168 qed |
170 qed |
169 } then show ?thesis unfolding wf_def by blast |
171 qed |
|
172 then show ?thesis unfolding wf_def by blast |
170 qed |
173 qed |
171 |
174 |
172 lemmas wfP_trancl = wf_trancl [to_pred] |
175 lemmas wfP_trancl = wf_trancl [to_pred] |
173 |
176 |
174 lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)" |
177 lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)" |
175 apply (subst trancl_converse [symmetric]) |
178 apply (subst trancl_converse [symmetric]) |
176 apply (erule wf_trancl) |
179 apply (erule wf_trancl) |
177 done |
180 done |
178 |
181 |
179 text \<open>Well-foundedness of subsets\<close> |
182 text \<open>Well-foundedness of subsets\<close> |
180 |
183 |
181 lemma wf_subset: "[| wf(r); p<=r |] ==> wf(p)" |
184 lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p" |
182 apply (simp (no_asm_use) add: wf_eq_minimal) |
185 apply (simp add: wf_eq_minimal) |
183 apply fast |
186 apply fast |
184 done |
187 done |
185 |
188 |
186 lemmas wfP_subset = wf_subset [to_pred] |
189 lemmas wfP_subset = wf_subset [to_pred] |
187 |
190 |
219 show "A = {}" by (rule wfE_pf) |
222 show "A = {}" by (rule wfE_pf) |
220 qed |
223 qed |
221 |
224 |
222 text \<open>Well-foundedness of insert\<close> |
225 text \<open>Well-foundedness of insert\<close> |
223 |
226 |
224 lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)" |
227 lemma wf_insert [iff]: "wf (insert (y, x) r) \<longleftrightarrow> wf r \<and> (x, y) \<notin> r\<^sup>*" |
225 apply (rule iffI) |
228 apply (rule iffI) |
226 apply (blast elim: wf_trancl [THEN wf_irrefl] |
229 apply (blast elim: wf_trancl [THEN wf_irrefl] |
227 intro: rtrancl_into_trancl1 wf_subset |
230 intro: rtrancl_into_trancl1 wf_subset |
228 rtrancl_mono [THEN [2] rev_subsetD]) |
231 rtrancl_mono [THEN [2] rev_subsetD]) |
229 apply (simp add: wf_eq_minimal, safe) |
232 apply (simp add: wf_eq_minimal, safe) |
230 apply (rule allE, assumption, erule impE, blast) |
233 apply (rule allE, assumption, erule impE, blast) |
231 apply (erule bexE) |
234 apply (erule bexE) |
232 apply (rename_tac "a", case_tac "a = x") |
235 apply (rename_tac "a", case_tac "a = x") |
233 prefer 2 |
236 prefer 2 |
234 apply blast |
237 apply blast |
235 apply (case_tac "y:Q") |
238 apply (case_tac "y \<in> Q") |
236 prefer 2 apply blast |
239 prefer 2 apply blast |
237 apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE) |
240 apply (rule_tac x = "{z. z \<in> Q \<and> (z,y) \<in> r\<^sup>*}" in allE) |
238 apply assumption |
241 apply assumption |
239 apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl) |
242 apply (erule_tac V = "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> P Q" for P in thin_rl) |
240 \<comment>\<open>essential for speed\<close> |
243 (*essential for speed*) |
241 txt\<open>Blast with new substOccur fails\<close> |
244 (*blast with new substOccur fails*) |
242 apply (fast intro: converse_rtrancl_into_rtrancl) |
245 apply (fast intro: converse_rtrancl_into_rtrancl) |
243 done |
246 done |
244 |
247 |
245 text\<open>Well-foundedness of image\<close> |
248 |
246 |
249 subsubsection \<open>Well-foundedness of image\<close> |
247 lemma wf_map_prod_image: "[| wf r; inj f |] ==> wf (map_prod f f ` r)" |
250 |
|
251 lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)" |
248 apply (simp only: wf_eq_minimal, clarify) |
252 apply (simp only: wf_eq_minimal, clarify) |
249 apply (case_tac "EX p. f p : Q") |
253 apply (case_tac "\<exists>p. f p \<in> Q") |
250 apply (erule_tac x = "{p. f p : Q}" in allE) |
254 apply (erule_tac x = "{p. f p \<in> Q}" in allE) |
251 apply (fast dest: inj_onD, blast) |
255 apply (fast dest: inj_onD, blast) |
252 done |
256 done |
253 |
257 |
254 |
258 |
255 subsection \<open>Well-Foundedness Results for Unions\<close> |
259 subsection \<open>Well-Foundedness Results for Unions\<close> |
257 lemma wf_union_compatible: |
261 lemma wf_union_compatible: |
258 assumes "wf R" "wf S" |
262 assumes "wf R" "wf S" |
259 assumes "R O S \<subseteq> R" |
263 assumes "R O S \<subseteq> R" |
260 shows "wf (R \<union> S)" |
264 shows "wf (R \<union> S)" |
261 proof (rule wfI_min) |
265 proof (rule wfI_min) |
262 fix x :: 'a and Q |
266 fix x :: 'a and Q |
263 let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}" |
267 let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}" |
264 assume "x \<in> Q" |
268 assume "x \<in> Q" |
265 obtain a where "a \<in> ?Q'" |
269 obtain a where "a \<in> ?Q'" |
266 by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast |
270 by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast |
267 with \<open>wf S\<close> |
271 with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" |
268 obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min) |
272 by (erule wfE_min) |
269 { |
273 { |
270 fix y assume "(y, z) \<in> S" |
274 fix y assume "(y, z) \<in> S" |
271 then have "y \<notin> ?Q'" by (rule zmin) |
275 then have "y \<notin> ?Q'" by (rule zmin) |
272 |
|
273 have "y \<notin> Q" |
276 have "y \<notin> Q" |
274 proof |
277 proof |
275 assume "y \<in> Q" |
278 assume "y \<in> Q" |
276 with \<open>y \<notin> ?Q'\<close> |
279 with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto |
277 obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto |
|
278 from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI) |
280 from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI) |
279 with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" .. |
281 with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" .. |
280 with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast |
282 with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast |
281 with \<open>w \<in> Q\<close> show False by contradiction |
283 with \<open>w \<in> Q\<close> show False by contradiction |
282 qed |
284 qed |
283 } |
285 } |
284 with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast |
286 with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast |
285 qed |
287 qed |
286 |
288 |
287 |
289 |
288 text \<open>Well-foundedness of indexed union with disjoint domains and ranges\<close> |
290 text \<open>Well-foundedness of indexed union with disjoint domains and ranges\<close> |
289 |
291 |
290 lemma wf_UN: "[| ALL i:I. wf(r i); |
292 lemma wf_UN: |
291 ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} |
293 assumes "\<forall>i\<in>I. wf (r i)" |
292 |] ==> wf(UN i:I. r i)" |
294 and "\<forall>i\<in>I. \<forall>j\<in>I. r i \<noteq> r j \<longrightarrow> Domain (r i) \<inter> Range (r j) = {}" |
293 apply (simp only: wf_eq_minimal, clarify) |
295 shows "wf (\<Union>i\<in>I. r i)" |
294 apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i") |
296 using assms |
295 prefer 2 |
297 apply (simp only: wf_eq_minimal) |
296 apply force |
298 apply clarify |
297 apply clarify |
299 apply (rename_tac A a, case_tac "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i") |
298 apply (drule bspec, assumption) |
300 prefer 2 |
299 apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE) |
301 apply force |
300 apply (blast elim!: allE) |
302 apply clarify |
301 done |
303 apply (drule bspec, assumption) |
|
304 apply (erule_tac x="{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }" in allE) |
|
305 apply (blast elim!: allE) |
|
306 done |
302 |
307 |
303 lemma wfP_SUP: |
308 lemma wfP_SUP: |
304 "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPREMUM UNIV r)" |
309 "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPREMUM UNIV r)" |
305 apply (rule wf_UN[to_pred]) |
310 apply (rule wf_UN[to_pred]) |
306 apply simp_all |
311 apply simp_all |
307 done |
312 done |
308 |
313 |
309 lemma wf_Union: |
314 lemma wf_Union: |
310 "[| ALL r:R. wf r; |
315 assumes "\<forall>r\<in>R. wf r" |
311 ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} |
316 and "\<forall>r\<in>R. \<forall>s\<in>R. r \<noteq> s \<longrightarrow> Domain r \<inter> Range s = {}" |
312 |] ==> wf (\<Union> R)" |
317 shows "wf (\<Union>R)" |
313 using wf_UN[of R "\<lambda>i. i"] by simp |
318 using assms wf_UN[of R "\<lambda>i. i"] by simp |
314 |
319 |
315 (*Intuition: we find an (R u S)-min element of a nonempty subset A |
320 (*Intuition: we find an (R u S)-min element of a nonempty subset A |
316 by case distinction. |
321 by case distinction. |
317 1. There is a step a -R-> b with a,b : A. |
322 1. There is a step a -R-> b with a,b : A. |
318 Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}. |
323 Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}. |
321 have an S-successor and is thus S-min in A as well. |
326 have an S-successor and is thus S-min in A as well. |
322 2. There is no such step. |
327 2. There is no such step. |
323 Pick an S-min element of A. In this case it must be an R-min |
328 Pick an S-min element of A. In this case it must be an R-min |
324 element of A as well. |
329 element of A as well. |
325 *) |
330 *) |
326 lemma wf_Un: |
331 lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)" |
327 "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)" |
332 using wf_union_compatible[of s r] |
328 using wf_union_compatible[of s r] |
|
329 by (auto simp: Un_ac) |
333 by (auto simp: Un_ac) |
330 |
334 |
331 lemma wf_union_merge: |
335 lemma wf_union_merge: "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" |
332 "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" (is "wf ?A = wf ?B") |
336 (is "wf ?A = wf ?B") |
333 proof |
337 proof |
334 assume "wf ?A" |
338 assume "wf ?A" |
335 with wf_trancl have wfT: "wf (?A^+)" . |
339 with wf_trancl have wfT: "wf (?A\<^sup>+)" . |
336 moreover have "?B \<subseteq> ?A^+" |
340 moreover have "?B \<subseteq> ?A\<^sup>+" |
337 by (subst trancl_unfold, subst trancl_unfold) blast |
341 by (subst trancl_unfold, subst trancl_unfold) blast |
338 ultimately show "wf ?B" by (rule wf_subset) |
342 ultimately show "wf ?B" by (rule wf_subset) |
339 next |
343 next |
340 assume "wf ?B" |
344 assume "wf ?B" |
341 |
345 |
342 show "wf ?A" |
346 show "wf ?A" |
343 proof (rule wfI_min) |
347 proof (rule wfI_min) |
344 fix Q :: "'a set" and x |
348 fix Q :: "'a set" and x |
345 assume "x \<in> Q" |
349 assume "x \<in> Q" |
346 |
350 |
347 with \<open>wf ?B\<close> |
351 with \<open>wf ?B\<close> |
348 obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" |
352 obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" |
349 by (erule wfE_min) |
353 by (erule wfE_min) |
350 then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" |
354 then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" |
351 and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" |
355 and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" |
352 and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" |
356 and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" |
353 by auto |
357 by auto |
354 |
358 |
355 show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q" |
359 show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q" |
356 proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q") |
360 proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q") |
357 case True |
361 case True |
358 with \<open>z \<in> Q\<close> A3 show ?thesis by blast |
362 with \<open>z \<in> Q\<close> A3 show ?thesis by blast |
359 next |
363 next |
360 case False |
364 case False |
361 then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast |
365 then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast |
362 |
|
363 have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q" |
366 have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q" |
364 proof (intro allI impI) |
367 proof (intro allI impI) |
365 fix y assume "(y, z') \<in> ?A" |
368 fix y assume "(y, z') \<in> ?A" |
366 then show "y \<notin> Q" |
369 then show "y \<notin> Q" |
367 proof |
370 proof |
368 assume "(y, z') \<in> R" |
371 assume "(y, z') \<in> R" |
369 then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> .. |
372 then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> .. |
370 with A1 show "y \<notin> Q" . |
373 with A1 show "y \<notin> Q" . |
371 next |
374 next |
372 assume "(y, z') \<in> S" |
375 assume "(y, z') \<in> S" |
373 then have "(y, z) \<in> S O R" using \<open>(z', z) \<in> R\<close> .. |
376 then have "(y, z) \<in> S O R" using \<open>(z', z) \<in> R\<close> .. |
374 with A2 show "y \<notin> Q" . |
377 with A2 show "y \<notin> Q" . |
375 qed |
378 qed |
376 qed |
379 qed |
377 with \<open>z' \<in> Q\<close> show ?thesis .. |
380 with \<open>z' \<in> Q\<close> show ?thesis .. |
475 have "acyclic r" |
479 have "acyclic r" |
476 using \<open>irrefl r\<close> and \<open>trans r\<close> by (simp add: irrefl_def acyclic_irrefl) |
480 using \<open>irrefl r\<close> and \<open>trans r\<close> by (simp add: irrefl_def acyclic_irrefl) |
477 with \<open>finite r\<close> show ?thesis by (rule finite_acyclic_wf_converse) |
481 with \<open>finite r\<close> show ?thesis by (rule finite_acyclic_wf_converse) |
478 qed |
482 qed |
479 |
483 |
480 lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r" |
484 lemma wf_iff_acyclic_if_finite: "finite r \<Longrightarrow> wf r = acyclic r" |
481 by (blast intro: finite_acyclic_wf wf_acyclic) |
485 by (blast intro: finite_acyclic_wf wf_acyclic) |
482 |
486 |
483 |
487 |
484 subsection \<open>@{typ nat} is well-founded\<close> |
488 subsection \<open>@{typ nat} is well-founded\<close> |
485 |
489 |
486 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++" |
490 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+" |
487 proof (rule ext, rule ext, rule iffI) |
491 proof (rule ext, rule ext, rule iffI) |
488 fix n m :: nat |
492 fix n m :: nat |
489 assume "m < n" |
493 show "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n" |
490 then show "(\<lambda>m n. n = Suc m)^++ m n" |
494 using that |
491 proof (induct n) |
495 proof (induct n) |
492 case 0 then show ?case by auto |
496 case 0 |
|
497 then show ?case by auto |
493 next |
498 next |
494 case (Suc n) then show ?case |
499 case (Suc n) |
|
500 then show ?case |
495 by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) |
501 by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) |
496 qed |
502 qed |
497 next |
503 show "m < n" if "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" |
498 fix n m :: nat |
504 using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less) |
499 assume "(\<lambda>m n. n = Suc m)^++ m n" |
505 qed |
500 then show "m < n" |
506 |
501 by (induct n) |
507 definition pred_nat :: "(nat \<times> nat) set" |
502 (simp_all add: less_Suc_eq_le reflexive le_less) |
508 where "pred_nat = {(m, n). n = Suc m}" |
503 qed |
509 |
504 |
510 definition less_than :: "(nat \<times> nat) set" |
505 definition |
511 where "less_than = pred_nat\<^sup>+" |
506 pred_nat :: "(nat * nat) set" where |
512 |
507 "pred_nat = {(m, n). n = Suc m}" |
513 lemma less_eq: "(m, n) \<in> pred_nat\<^sup>+ \<longleftrightarrow> m < n" |
508 |
|
509 definition |
|
510 less_than :: "(nat * nat) set" where |
|
511 "less_than = pred_nat^+" |
|
512 |
|
513 lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n" |
|
514 unfolding less_nat_rel pred_nat_def trancl_def by simp |
514 unfolding less_nat_rel pred_nat_def trancl_def by simp |
515 |
515 |
516 lemma pred_nat_trancl_eq_le: |
516 lemma pred_nat_trancl_eq_le: "(m, n) \<in> pred_nat\<^sup>* \<longleftrightarrow> m \<le> n" |
517 "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n" |
|
518 unfolding less_eq rtrancl_eq_or_trancl by auto |
517 unfolding less_eq rtrancl_eq_or_trancl by auto |
519 |
518 |
520 lemma wf_pred_nat: "wf pred_nat" |
519 lemma wf_pred_nat: "wf pred_nat" |
521 apply (unfold wf_def pred_nat_def, clarify) |
520 apply (unfold wf_def pred_nat_def, clarify) |
522 apply (induct_tac x, blast+) |
521 apply (induct_tac x, blast+) |
526 by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) |
525 by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) |
527 |
526 |
528 lemma trans_less_than [iff]: "trans less_than" |
527 lemma trans_less_than [iff]: "trans less_than" |
529 by (simp add: less_than_def) |
528 by (simp add: less_than_def) |
530 |
529 |
531 lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)" |
530 lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)" |
532 by (simp add: less_than_def less_eq) |
531 by (simp add: less_than_def less_eq) |
533 |
532 |
534 lemma wf_less: "wf {(x, y::nat). x < y}" |
533 lemma wf_less: "wf {(x, y::nat). x < y}" |
535 by (rule Wellfounded.wellorder_class.wf) |
534 by (rule Wellfounded.wellorder_class.wf) |
536 |
535 |
537 |
536 |
538 subsection \<open>Accessible Part\<close> |
537 subsection \<open>Accessible Part\<close> |
539 |
538 |
540 text \<open> |
539 text \<open> |
541 Inductive definition of the accessible part @{term "acc r"} of a |
540 Inductive definition of the accessible part \<open>acc r\<close> of a |
542 relation; see also @{cite "paulin-tlca"}. |
541 relation; see also @{cite "paulin-tlca"}. |
543 \<close> |
542 \<close> |
544 |
543 |
545 inductive_set |
544 inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set" |
546 acc :: "('a * 'a) set => 'a set" |
545 where accI: "(\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" |
547 for r :: "('a * 'a) set" |
546 |
548 where |
547 abbreviation termip :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
549 accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r" |
548 where "termip r \<equiv> accp (r\<inverse>\<inverse>)" |
550 |
549 |
551 abbreviation |
550 abbreviation termi :: "('a \<times> 'a) set \<Rightarrow> 'a set" |
552 termip :: "('a => 'a => bool) => 'a => bool" where |
551 where "termi r \<equiv> acc (r\<inverse>)" |
553 "termip r \<equiv> accp (r\<inverse>\<inverse>)" |
|
554 |
|
555 abbreviation |
|
556 termi :: "('a * 'a) set => 'a set" where |
|
557 "termi r \<equiv> acc (r\<inverse>)" |
|
558 |
552 |
559 lemmas accpI = accp.accI |
553 lemmas accpI = accp.accI |
560 |
554 |
561 lemma accp_eq_acc [code]: |
555 lemma accp_eq_acc [code]: "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})" |
562 "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})" |
|
563 by (simp add: acc_def) |
556 by (simp add: acc_def) |
564 |
557 |
565 |
558 |
566 text \<open>Induction rules\<close> |
559 text \<open>Induction rules\<close> |
567 |
560 |
568 theorem accp_induct: |
561 theorem accp_induct: |
569 assumes major: "accp r a" |
562 assumes major: "accp r a" |
570 assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x" |
563 assumes hyp: "\<And>x. accp r x \<Longrightarrow> \<forall>y. r y x \<longrightarrow> P y \<Longrightarrow> P x" |
571 shows "P a" |
564 shows "P a" |
572 apply (rule major [THEN accp.induct]) |
565 apply (rule major [THEN accp.induct]) |
573 apply (rule hyp) |
566 apply (rule hyp) |
574 apply (rule accp.accI) |
567 apply (rule accp.accI) |
575 apply fast |
568 apply fast |
576 apply fast |
569 apply fast |
577 done |
570 done |
578 |
571 |
579 lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp] |
572 lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp] |
580 |
573 |
581 theorem accp_downward: "accp r b ==> r a b ==> accp r a" |
574 theorem accp_downward: "accp r b \<Longrightarrow> r a b \<Longrightarrow> accp r a" |
582 apply (erule accp.cases) |
575 apply (erule accp.cases) |
583 apply fast |
576 apply fast |
584 done |
577 done |
585 |
578 |
586 lemma not_accp_down: |
579 lemma not_accp_down: |
587 assumes na: "\<not> accp R x" |
580 assumes na: "\<not> accp R x" |
588 obtains z where "R z x" and "\<not> accp R z" |
581 obtains z where "R z x" and "\<not> accp R z" |
589 proof - |
582 proof - |
590 assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis" |
583 assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis" |
591 |
|
592 show thesis |
584 show thesis |
593 proof (cases "\<forall>z. R z x \<longrightarrow> accp R z") |
585 proof (cases "\<forall>z. R z x \<longrightarrow> accp R z") |
594 case True |
586 case True |
595 hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto |
587 then have "\<And>z. R z x \<Longrightarrow> accp R z" by auto |
596 hence "accp R x" |
588 then have "accp R x" by (rule accp.accI) |
597 by (rule accp.accI) |
|
598 with na show thesis .. |
589 with na show thesis .. |
599 next |
590 next |
600 case False then obtain z where "R z x" and "\<not> accp R z" |
591 case False then obtain z where "R z x" and "\<not> accp R z" |
601 by auto |
592 by auto |
602 with a show thesis . |
593 with a show thesis . |
603 qed |
594 qed |
604 qed |
595 qed |
605 |
596 |
606 lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b" |
597 lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r a \<longrightarrow> accp r b" |
607 apply (erule rtranclp_induct) |
598 apply (erule rtranclp_induct) |
608 apply blast |
599 apply blast |
609 apply (blast dest: accp_downward) |
600 apply (blast dest: accp_downward) |
610 done |
601 done |
611 |
602 |
612 theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b" |
603 theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b" |
613 apply (blast dest: accp_downwards_aux) |
604 apply (blast dest: accp_downwards_aux) |
614 done |
605 done |
615 |
606 |
616 theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r" |
607 theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r" |
617 apply (rule wfPUNIVI) |
608 apply (rule wfPUNIVI) |
618 apply (rule_tac P=P in accp_induct) |
609 apply (rule_tac P=P in accp_induct) |
619 apply blast |
610 apply blast |
620 apply blast |
611 apply blast |
621 done |
612 done |
622 |
613 |
623 theorem accp_wfPD: "wfP r ==> accp r x" |
614 theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x" |
624 apply (erule wfP_induct_rule) |
615 apply (erule wfP_induct_rule) |
625 apply (rule accp.accI) |
616 apply (rule accp.accI) |
626 apply blast |
617 apply blast |
627 done |
618 done |
628 |
619 |
697 |
688 |
698 subsection \<open>Tools for building wellfounded relations\<close> |
689 subsection \<open>Tools for building wellfounded relations\<close> |
699 |
690 |
700 text \<open>Inverse Image\<close> |
691 text \<open>Inverse Image\<close> |
701 |
692 |
702 lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))" |
693 lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)" for f :: "'a \<Rightarrow> 'b" |
703 apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal) |
694 apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal) |
704 apply clarify |
695 apply clarify |
705 apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }") |
696 apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}") |
706 prefer 2 apply (blast del: allE) |
697 prefer 2 apply (blast del: allE) |
707 apply (erule allE) |
698 apply (erule allE) |
708 apply (erule (1) notE impE) |
699 apply (erule (1) notE impE) |
709 apply blast |
700 apply blast |
710 done |
701 done |
711 |
702 |
712 text \<open>Measure functions into @{typ nat}\<close> |
703 text \<open>Measure functions into @{typ nat}\<close> |
713 |
704 |
714 definition measure :: "('a => nat) => ('a * 'a)set" |
705 definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set" |
715 where "measure = inv_image less_than" |
706 where "measure = inv_image less_than" |
716 |
707 |
717 lemma in_measure[simp, code_unfold]: "((x,y) : measure f) = (f x < f y)" |
708 lemma in_measure[simp, code_unfold]: "(x, y) \<in> measure f \<longleftrightarrow> f x < f y" |
718 by (simp add:measure_def) |
709 by (simp add:measure_def) |
719 |
710 |
720 lemma wf_measure [iff]: "wf (measure f)" |
711 lemma wf_measure [iff]: "wf (measure f)" |
721 apply (unfold measure_def) |
712 apply (unfold measure_def) |
722 apply (rule wf_less_than [THEN wf_inv_image]) |
713 apply (rule wf_less_than [THEN wf_inv_image]) |
723 done |
714 done |
724 |
715 |
725 lemma wf_if_measure: fixes f :: "'a \<Rightarrow> nat" |
716 lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}" |
726 shows "(!!x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}" |
717 for f :: "'a \<Rightarrow> nat" |
727 apply(insert wf_measure[of f]) |
718 apply(insert wf_measure[of f]) |
728 apply(simp only: measure_def inv_image_def less_than_def less_eq) |
719 apply(simp only: measure_def inv_image_def less_than_def less_eq) |
729 apply(erule wf_subset) |
720 apply(erule wf_subset) |
730 apply auto |
721 apply auto |
731 done |
722 done |
732 |
723 |
733 |
724 |
734 text\<open>Lexicographic combinations\<close> |
725 subsubsection \<open>Lexicographic combinations\<close> |
735 |
726 |
736 definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where |
727 definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" |
737 "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}" |
728 (infixr "<*lex*>" 80) |
738 |
729 where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}" |
739 lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)" |
730 |
740 apply (unfold wf_def lex_prod_def) |
731 lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)" |
|
732 apply (unfold wf_def lex_prod_def) |
741 apply (rule allI, rule impI) |
733 apply (rule allI, rule impI) |
742 apply (simp (no_asm_use) only: split_paired_All) |
734 apply (simp (no_asm_use) only: split_paired_All) |
743 apply (drule spec, erule mp) |
735 apply (drule spec, erule mp) |
744 apply (rule allI, rule impI) |
736 apply (rule allI, rule impI) |
745 apply (drule spec, erule mp, blast) |
737 apply (drule spec, erule mp, blast) |
746 done |
738 done |
747 |
739 |
748 lemma in_lex_prod[simp]: |
740 lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s" |
749 "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))" |
|
750 by (auto simp:lex_prod_def) |
741 by (auto simp:lex_prod_def) |
751 |
742 |
752 text\<open>@{term "op <*lex*>"} preserves transitivity\<close> |
743 text \<open>\<open><*lex*>\<close> preserves transitivity\<close> |
753 |
744 lemma trans_lex_prod [intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)" |
754 lemma trans_lex_prod [intro!]: |
745 unfolding trans_def lex_prod_def by blast |
755 "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)" |
746 |
756 by (unfold trans_def lex_prod_def, blast) |
|
757 |
747 |
758 text \<open>lexicographic combinations with measure functions\<close> |
748 text \<open>lexicographic combinations with measure functions\<close> |
759 |
749 |
760 definition |
750 definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80) |
761 mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80) |
751 where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))" |
762 where |
|
763 "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))" |
|
764 |
752 |
765 lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)" |
753 lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)" |
766 unfolding mlex_prod_def |
754 unfolding mlex_prod_def |
767 by auto |
755 by auto |
768 |
756 |
769 lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R" |
757 lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R" |
770 unfolding mlex_prod_def by simp |
758 unfolding mlex_prod_def by simp |
771 |
759 |
772 lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R" |
760 lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R" |
773 unfolding mlex_prod_def by auto |
761 unfolding mlex_prod_def by auto |
774 |
762 |
775 text \<open>proper subset relation on finite sets\<close> |
763 text \<open>proper subset relation on finite sets\<close> |
776 |
764 |
777 definition finite_psubset :: "('a set * 'a set) set" |
765 definition finite_psubset :: "('a set \<times> 'a set) set" |
778 where "finite_psubset = {(A,B). A < B & finite B}" |
766 where "finite_psubset = {(A,B). A < B \<and> finite B}" |
779 |
767 |
780 lemma wf_finite_psubset[simp]: "wf(finite_psubset)" |
768 lemma wf_finite_psubset[simp]: "wf finite_psubset" |
781 apply (unfold finite_psubset_def) |
769 apply (unfold finite_psubset_def) |
782 apply (rule wf_measure [THEN wf_subset]) |
770 apply (rule wf_measure [THEN wf_subset]) |
783 apply (simp add: measure_def inv_image_def less_than_def less_eq) |
771 apply (simp add: measure_def inv_image_def less_than_def less_eq) |
784 apply (fast elim!: psubset_card_mono) |
772 apply (fast elim!: psubset_card_mono) |
785 done |
773 done |
786 |
774 |
787 lemma trans_finite_psubset: "trans finite_psubset" |
775 lemma trans_finite_psubset: "trans finite_psubset" |
788 by (simp add: finite_psubset_def less_le trans_def, blast) |
776 by (auto simp add: finite_psubset_def less_le trans_def) |
789 |
777 |
790 lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)" |
778 lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A < B \<and> finite B" |
791 unfolding finite_psubset_def by auto |
779 unfolding finite_psubset_def by auto |
792 |
780 |
793 text \<open>max- and min-extension of order to finite sets\<close> |
781 text \<open>max- and min-extension of order to finite sets\<close> |
794 |
782 |
795 inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" |
783 inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" |
796 for R :: "('a \<times> 'a) set" |
784 for R :: "('a \<times> 'a) set" |
797 where |
785 where |
798 max_extI[intro]: "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R" |
786 max_extI[intro]: "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R" |
799 |
787 |
800 lemma max_ext_wf: |
788 lemma max_ext_wf: |
801 assumes wf: "wf r" |
789 assumes wf: "wf r" |
802 shows "wf (max_ext r)" |
790 shows "wf (max_ext r)" |
803 proof (rule acc_wfI, intro allI) |
791 proof (rule acc_wfI, intro allI) |
804 fix M show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") |
792 fix M |
|
793 show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") |
805 proof cases |
794 proof cases |
806 assume "finite M" |
795 assume "finite M" |
807 thus ?thesis |
796 then show ?thesis |
808 proof (induct M) |
797 proof (induct M) |
809 show "{} \<in> ?W" |
798 show "{} \<in> ?W" |
810 by (rule accI) (auto elim: max_ext.cases) |
799 by (rule accI) (auto elim: max_ext.cases) |
811 next |
800 next |
812 fix M a assume "M \<in> ?W" "finite M" |
801 fix M a assume "M \<in> ?W" "finite M" |
813 with wf show "insert a M \<in> ?W" |
802 with wf show "insert a M \<in> ?W" |
814 proof (induct arbitrary: M) |
803 proof (induct arbitrary: M) |
815 fix M a |
804 fix M a |
816 assume "M \<in> ?W" and [intro]: "finite M" |
805 assume "M \<in> ?W" and [intro]: "finite M" |
817 assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W" |
806 assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W" |
818 { |
807 have add_less: "\<lbrakk>M \<in> ?W ; (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r)\<rbrakk> \<Longrightarrow> N \<union> M \<in> ?W" |
819 fix N M :: "'a set" |
808 if "finite N" "finite M" for N M :: "'a set" |
820 assume "finite N" "finite M" |
809 using that by (induct N arbitrary: M) (auto simp: hyp) |
821 then |
810 |
822 have "\<lbrakk>M \<in> ?W ; (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r)\<rbrakk> \<Longrightarrow> N \<union> M \<in> ?W" |
|
823 by (induct N arbitrary: M) (auto simp: hyp) |
|
824 } |
|
825 note add_less = this |
|
826 |
|
827 show "insert a M \<in> ?W" |
811 show "insert a M \<in> ?W" |
828 proof (rule accI) |
812 proof (rule accI) |
829 fix N assume Nless: "(N, insert a M) \<in> max_ext r" |
813 fix N |
830 hence asm1: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)" |
814 assume Nless: "(N, insert a M) \<in> max_ext r" |
|
815 then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)" |
831 by (auto elim!: max_ext.cases) |
816 by (auto elim!: max_ext.cases) |
832 |
817 |
833 let ?N1 = "{ n \<in> N. (n, a) \<in> r }" |
818 let ?N1 = "{n \<in> N. (n, a) \<in> r}" |
834 let ?N2 = "{ n \<in> N. (n, a) \<notin> r }" |
819 let ?N2 = "{n \<in> N. (n, a) \<notin> r}" |
835 have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto |
820 have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto |
836 from Nless have "finite N" by (auto elim: max_ext.cases) |
821 from Nless have "finite N" by (auto elim: max_ext.cases) |
837 then have finites: "finite ?N1" "finite ?N2" by auto |
822 then have finites: "finite ?N1" "finite ?N2" by auto |
838 |
823 |
839 have "?N2 \<in> ?W" |
824 have "?N2 \<in> ?W" |
840 proof cases |
825 proof cases |
841 assume [simp]: "M = {}" |
826 assume [simp]: "M = {}" |
842 have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases) |
827 have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases) |
843 |
828 |
844 from asm1 have "?N2 = {}" by auto |
829 from * have "?N2 = {}" by auto |
845 with Mw show "?N2 \<in> ?W" by (simp only:) |
830 with Mw show "?N2 \<in> ?W" by (simp only:) |
846 next |
831 next |
847 assume "M \<noteq> {}" |
832 assume "M \<noteq> {}" |
848 from asm1 finites have N2: "(?N2, M) \<in> max_ext r" |
833 from * finites have N2: "(?N2, M) \<in> max_ext r" |
849 by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto |
834 by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto |
850 |
|
851 with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward) |
835 with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward) |
852 qed |
836 qed |
853 with finites have "?N1 \<union> ?N2 \<in> ?W" |
837 with finites have "?N1 \<union> ?N2 \<in> ?W" |
854 by (rule add_less) simp |
838 by (rule add_less) simp |
855 then show "N \<in> ?W" by (simp only: N) |
839 then show "N \<in> ?W" by (simp only: N) |
856 qed |
840 qed |
857 qed |
841 qed |
858 qed |
842 qed |
861 show ?thesis |
845 show ?thesis |
862 by (rule accI) (auto elim: max_ext.cases) |
846 by (rule accI) (auto elim: max_ext.cases) |
863 qed |
847 qed |
864 qed |
848 qed |
865 |
849 |
866 lemma max_ext_additive: |
850 lemma max_ext_additive: |
867 "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> |
851 "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> |
868 (A \<union> C, B \<union> D) \<in> max_ext R" |
852 (A \<union> C, B \<union> D) \<in> max_ext R" |
869 by (force elim!: max_ext.cases) |
853 by (force elim!: max_ext.cases) |
870 |
854 |
871 |
855 |
872 definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" where |
856 definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" |
873 "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}" |
857 where "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}" |
874 |
858 |
875 lemma min_ext_wf: |
859 lemma min_ext_wf: |
876 assumes "wf r" |
860 assumes "wf r" |
877 shows "wf (min_ext r)" |
861 shows "wf (min_ext r)" |
878 proof (rule wfI_min) |
862 proof (rule wfI_min) |
879 fix Q :: "'a set set" |
863 show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q" |
880 fix x |
864 for Q :: "'a set set" and x |
881 assume nonempty: "x \<in> Q" |
865 proof (cases "Q = {{}}") |
882 show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" |
866 case True |
883 proof cases |
867 then show ?thesis by (simp add: min_ext_def) |
884 assume "Q = {{}}" thus ?thesis by (simp add: min_ext_def) |
|
885 next |
868 next |
886 assume "Q \<noteq> {{}}" |
869 case False |
887 with nonempty |
870 with nonempty obtain e x where "x \<in> Q" "e \<in> x" by force |
888 obtain e x where "x \<in> Q" "e \<in> x" by force |
|
889 then have eU: "e \<in> \<Union>Q" by auto |
871 then have eU: "e \<in> \<Union>Q" by auto |
890 with \<open>wf r\<close> |
872 with \<open>wf r\<close> |
891 obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" |
873 obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" |
892 by (erule wfE_min) |
874 by (erule wfE_min) |
893 from z obtain m where "m \<in> Q" "z \<in> m" by auto |
875 from z obtain m where "m \<in> Q" "z \<in> m" by auto |
894 from \<open>m \<in> Q\<close> |
876 from \<open>m \<in> Q\<close> |
895 show ?thesis |
877 show ?thesis |
896 proof (rule, intro bexI allI impI) |
878 proof (rule, intro bexI allI impI) |
897 fix n |
879 fix n |
898 assume smaller: "(n, m) \<in> min_ext r" |
880 assume smaller: "(n, m) \<in> min_ext r" |
899 with \<open>z \<in> m\<close> obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def) |
881 with \<open>z \<in> m\<close> obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def) |
900 then show "n \<notin> Q" using z(2) by auto |
882 then show "n \<notin> Q" using z(2) by auto |
901 qed |
883 qed |
902 qed |
884 qed |
903 qed |
885 qed |
904 |
886 |
905 text\<open>Bounded increase must terminate:\<close> |
887 |
|
888 subsubsection \<open>Bounded increase must terminate\<close> |
906 |
889 |
907 lemma wf_bounded_measure: |
890 lemma wf_bounded_measure: |
908 fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat" |
891 fixes ub :: "'a \<Rightarrow> nat" |
909 assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a \<ge> f b & f b > f a" |
892 and f :: "'a \<Rightarrow> nat" |
910 shows "wf r" |
893 assumes "\<And>a b. (b, a) \<in> r \<Longrightarrow> ub b \<le> ub a \<and> ub a \<ge> f b \<and> f b > f a" |
911 apply(rule wf_subset[OF wf_measure[of "%a. ub a - f a"]]) |
894 shows "wf r" |
912 apply (auto dest: assms) |
895 apply (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]]) |
913 done |
896 apply (auto dest: assms) |
|
897 done |
914 |
898 |
915 lemma wf_bounded_set: |
899 lemma wf_bounded_set: |
916 fixes ub :: "'a \<Rightarrow> 'b set" and f :: "'a \<Rightarrow> 'b set" |
900 fixes ub :: "'a \<Rightarrow> 'b set" |
917 assumes "!!a b. (b,a) : r \<Longrightarrow> |
901 and f :: "'a \<Rightarrow> 'b set" |
918 finite(ub a) & ub b \<subseteq> ub a & ub a \<supseteq> f b & f b \<supset> f a" |
902 assumes "\<And>a b. (b,a) \<in> r \<Longrightarrow> finite (ub a) \<and> ub b \<subseteq> ub a \<and> ub a \<supseteq> f b \<and> f b \<supset> f a" |
919 shows "wf r" |
903 shows "wf r" |
920 apply(rule wf_bounded_measure[of r "%a. card(ub a)" "%a. card(f a)"]) |
904 apply(rule wf_bounded_measure[of r "\<lambda>a. card(ub a)" "\<lambda>a. card(f a)"]) |
921 apply(drule assms) |
905 apply(drule assms) |
922 apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) |
906 apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) |
923 done |
907 done |
924 |
908 |
925 lemma finite_subset_wf: |
909 lemma finite_subset_wf: |
926 assumes "finite A" |
910 assumes "finite A" |
927 shows "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" |
911 shows "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" |
928 proof (intro finite_acyclic_wf) |
912 proof (intro finite_acyclic_wf) |
929 have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A" by blast |
913 have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A" by blast |
930 thus "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" |
914 then show "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" |
931 by (rule finite_subset) (auto simp: assms finite_cartesian_product) |
915 by (rule finite_subset) (auto simp: assms finite_cartesian_product) |
932 next |
916 next |
933 have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}" |
917 have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}" |
934 by (intro trancl_id transI) blast |
918 by (intro trancl_id transI) blast |
935 also have " \<forall>x. (x, x) \<notin> \<dots>" by blast |
919 also have " \<forall>x. (x, x) \<notin> \<dots>" by blast |