author | wenzelm |
Fri, 05 Aug 2016 18:14:28 +0200 | |
changeset 63612 | 7195acc2fe93 |
parent 63572 | c0cbfd2b5a45 |
child 63915 | bab633745c7f |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
1 |
(* Title: HOL/Wellfounded.thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
2 |
Author: Tobias Nipkow |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
3 |
Author: Lawrence C Paulson |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
4 |
Author: Konrad Slind |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
5 |
Author: Alexander Krauss |
55027 | 6 |
Author: Andrei Popescu, TU Muenchen |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
7 |
*) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
8 |
|
60758 | 9 |
section \<open>Well-founded Recursion\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
10 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
11 |
theory Wellfounded |
63572 | 12 |
imports Transitive_Closure |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
13 |
begin |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
14 |
|
60758 | 15 |
subsection \<open>Basic Definitions\<close> |
26976 | 16 |
|
63108 | 17 |
definition wf :: "('a \<times> 'a) set \<Rightarrow> bool" |
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))" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
19 |
|
63108 | 20 |
definition wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
21 |
where "wfP r \<longleftrightarrow> wf {(x, y). r x y}" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
22 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
23 |
lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
24 |
by (simp add: wfP_def) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
25 |
|
63108 | 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" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
27 |
unfolding wf_def by blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
28 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
29 |
lemmas wfPUNIVI = wfUNIVI [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
30 |
|
63108 | 31 |
text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>. |
32 |
If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close> |
|
33 |
lemma wfI: |
|
34 |
assumes "r \<subseteq> A \<times> B" |
|
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" |
|
36 |
shows "wf r" |
|
37 |
using assms unfolding wf_def by blast |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
38 |
|
63108 | 39 |
lemma wf_induct: |
40 |
assumes "wf r" |
|
41 |
and "\<And>x. \<forall>y. (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x" |
|
42 |
shows "P a" |
|
43 |
using assms unfolding wf_def by blast |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
44 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
45 |
lemmas wfP_induct = wf_induct [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
46 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
47 |
lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
48 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
49 |
lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
50 |
|
63108 | 51 |
lemma wf_not_sym: "wf r \<Longrightarrow> (a, x) \<in> r \<Longrightarrow> (x, a) \<notin> r" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
52 |
by (induct a arbitrary: x set: wf) blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
53 |
|
33215
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset
|
54 |
lemma wf_asym: |
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset
|
55 |
assumes "wf r" "(a, x) \<in> r" |
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset
|
56 |
obtains "(x, a) \<notin> r" |
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset
|
57 |
by (drule wf_not_sym[OF assms]) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
58 |
|
63108 | 59 |
lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
60 |
by (blast elim: wf_asym) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
61 |
|
63572 | 62 |
lemma wf_irrefl: |
63 |
assumes "wf r" |
|
64 |
obtains "(a, a) \<notin> r" |
|
63108 | 65 |
by (drule wf_not_refl[OF assms]) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
66 |
|
27823 | 67 |
lemma wf_wellorderI: |
68 |
assumes wf: "wf {(x::'a::ord, y). x < y}" |
|
63572 | 69 |
and lin: "OFCLASS('a::ord, linorder_class)" |
27823 | 70 |
shows "OFCLASS('a::ord, wellorder_class)" |
63108 | 71 |
using lin |
72 |
apply (rule wellorder_class.intro) |
|
73 |
apply (rule class.wellorder_axioms.intro) |
|
74 |
apply (rule wf_induct_rule [OF wf]) |
|
75 |
apply simp |
|
76 |
done |
|
27823 | 77 |
|
63108 | 78 |
lemma (in wellorder) wf: "wf {(x, y). x < y}" |
79 |
unfolding wf_def by (blast intro: less_induct) |
|
27823 | 80 |
|
81 |
||
60758 | 82 |
subsection \<open>Basic Results\<close> |
26976 | 83 |
|
60758 | 84 |
text \<open>Point-free characterization of well-foundedness\<close> |
33216 | 85 |
|
86 |
lemma wfE_pf: |
|
87 |
assumes wf: "wf R" |
|
63572 | 88 |
and a: "A \<subseteq> R `` A" |
33216 | 89 |
shows "A = {}" |
90 |
proof - |
|
63108 | 91 |
from wf have "x \<notin> A" for x |
92 |
proof induct |
|
93 |
fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A" |
|
94 |
then have "x \<notin> R `` A" by blast |
|
95 |
with a show "x \<notin> A" by blast |
|
96 |
qed |
|
97 |
then show ?thesis by auto |
|
33216 | 98 |
qed |
99 |
||
100 |
lemma wfI_pf: |
|
101 |
assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}" |
|
102 |
shows "wf R" |
|
103 |
proof (rule wfUNIVI) |
|
104 |
fix P :: "'a \<Rightarrow> bool" and x |
|
105 |
let ?A = "{x. \<not> P x}" |
|
106 |
assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x" |
|
107 |
then have "?A \<subseteq> R `` ?A" by blast |
|
108 |
with a show "P x" by blast |
|
109 |
qed |
|
110 |
||
63108 | 111 |
|
112 |
subsubsection \<open>Minimal-element characterization of well-foundedness\<close> |
|
33216 | 113 |
|
114 |
lemma wfE_min: |
|
115 |
assumes wf: "wf R" and Q: "x \<in> Q" |
|
116 |
obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q" |
|
117 |
using Q wfE_pf[OF wf, of Q] by blast |
|
118 |
||
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
119 |
lemma wfE_min': |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
120 |
"wf R \<Longrightarrow> Q \<noteq> {} \<Longrightarrow> (\<And>z. z \<in> Q \<Longrightarrow> (\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q) \<Longrightarrow> thesis) \<Longrightarrow> thesis" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
121 |
using wfE_min[of R _ Q] by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
122 |
|
33216 | 123 |
lemma wfI_min: |
124 |
assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q" |
|
125 |
shows "wf R" |
|
126 |
proof (rule wfI_pf) |
|
63108 | 127 |
fix A |
128 |
assume b: "A \<subseteq> R `` A" |
|
129 |
have False if "x \<in> A" for x |
|
130 |
using a[OF that] b by blast |
|
131 |
then show "A = {}" by blast |
|
33216 | 132 |
qed |
133 |
||
63108 | 134 |
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))" |
63572 | 135 |
apply auto |
136 |
apply (erule wfE_min) |
|
137 |
apply assumption |
|
138 |
apply blast |
|
139 |
apply (rule wfI_min) |
|
140 |
apply auto |
|
141 |
done |
|
33216 | 142 |
|
143 |
lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] |
|
144 |
||
63108 | 145 |
|
146 |
subsubsection \<open>Well-foundedness of transitive closure\<close> |
|
33216 | 147 |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
148 |
lemma wf_trancl: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
149 |
assumes "wf r" |
63108 | 150 |
shows "wf (r\<^sup>+)" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
151 |
proof - |
63108 | 152 |
have "P x" if induct_step: "\<And>x. (\<And>y. (y, x) \<in> r\<^sup>+ \<Longrightarrow> P y) \<Longrightarrow> P x" for P x |
153 |
proof (rule induct_step) |
|
154 |
show "P y" if "(y, x) \<in> r\<^sup>+" for y |
|
155 |
using \<open>wf r\<close> and that |
|
156 |
proof (induct x arbitrary: y) |
|
157 |
case (less x) |
|
158 |
note hyp = \<open>\<And>x' y'. (x', x) \<in> r \<Longrightarrow> (y', x') \<in> r\<^sup>+ \<Longrightarrow> P y'\<close> |
|
159 |
from \<open>(y, x) \<in> r\<^sup>+\<close> show "P y" |
|
160 |
proof cases |
|
161 |
case base |
|
162 |
show "P y" |
|
163 |
proof (rule induct_step) |
|
164 |
fix y' |
|
165 |
assume "(y', y) \<in> r\<^sup>+" |
|
166 |
with \<open>(y, x) \<in> r\<close> show "P y'" |
|
167 |
by (rule hyp [of y y']) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
168 |
qed |
63108 | 169 |
next |
170 |
case step |
|
171 |
then obtain x' where "(x', x) \<in> r" and "(y, x') \<in> r\<^sup>+" |
|
172 |
by simp |
|
173 |
then show "P y" by (rule hyp [of x' y]) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
174 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
175 |
qed |
63108 | 176 |
qed |
177 |
then show ?thesis unfolding wf_def by blast |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
178 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
179 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
180 |
lemmas wfP_trancl = wf_trancl [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
181 |
|
63108 | 182 |
lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
183 |
apply (subst trancl_converse [symmetric]) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
184 |
apply (erule wf_trancl) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
185 |
done |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
186 |
|
60758 | 187 |
text \<open>Well-foundedness of subsets\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
188 |
|
63108 | 189 |
lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p" |
63612 | 190 |
by (simp add: wf_eq_minimal) fast |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
191 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
192 |
lemmas wfP_subset = wf_subset [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
193 |
|
60758 | 194 |
text \<open>Well-foundedness of the empty relation\<close> |
33216 | 195 |
|
196 |
lemma wf_empty [iff]: "wf {}" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
197 |
by (simp add: wf_def) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
198 |
|
63612 | 199 |
lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)" |
32205 | 200 |
proof - |
63612 | 201 |
have "wfP bot" |
202 |
by (fact wf_empty [to_pred bot_empty_eq2]) |
|
203 |
then show ?thesis |
|
204 |
by (simp add: bot_fun_def) |
|
32205 | 205 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
206 |
|
63572 | 207 |
lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')" |
208 |
by (erule wf_subset) (rule Int_lower1) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
209 |
|
63572 | 210 |
lemma wf_Int2: "wf r \<Longrightarrow> wf (r' \<inter> r)" |
211 |
by (erule wf_subset) (rule Int_lower2) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
212 |
|
63572 | 213 |
text \<open>Exponentiation.\<close> |
33216 | 214 |
lemma wf_exp: |
215 |
assumes "wf (R ^^ n)" |
|
216 |
shows "wf R" |
|
217 |
proof (rule wfI_pf) |
|
218 |
fix A assume "A \<subseteq> R `` A" |
|
63612 | 219 |
then have "A \<subseteq> (R ^^ n) `` A" |
220 |
by (induct n) force+ |
|
221 |
with \<open>wf (R ^^ n)\<close> show "A = {}" |
|
222 |
by (rule wfE_pf) |
|
33216 | 223 |
qed |
224 |
||
63572 | 225 |
text \<open>Well-foundedness of \<open>insert\<close>.\<close> |
63108 | 226 |
lemma wf_insert [iff]: "wf (insert (y, x) r) \<longleftrightarrow> wf r \<and> (x, y) \<notin> r\<^sup>*" |
63572 | 227 |
apply (rule iffI) |
228 |
apply (blast elim: wf_trancl [THEN wf_irrefl] |
|
229 |
intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN [2] rev_subsetD]) |
|
230 |
apply (simp add: wf_eq_minimal) |
|
231 |
apply safe |
|
232 |
apply (rule allE) |
|
233 |
apply assumption |
|
234 |
apply (erule impE) |
|
235 |
apply blast |
|
236 |
apply (erule bexE) |
|
237 |
apply (rename_tac a, case_tac "a = x") |
|
238 |
prefer 2 |
|
239 |
apply blast |
|
240 |
apply (case_tac "y \<in> Q") |
|
241 |
prefer 2 |
|
242 |
apply blast |
|
243 |
apply (rule_tac x = "{z. z \<in> Q \<and> (z,y) \<in> r\<^sup>*}" in allE) |
|
244 |
apply assumption |
|
245 |
apply (erule_tac V = "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> P Q" for P in thin_rl) |
|
63108 | 246 |
(*essential for speed*) |
63572 | 247 |
(*blast with new substOccur fails*) |
248 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
|
249 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
250 |
|
63108 | 251 |
|
252 |
subsubsection \<open>Well-foundedness of image\<close> |
|
33216 | 253 |
|
63108 | 254 |
lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)" |
63572 | 255 |
apply (simp only: wf_eq_minimal) |
256 |
apply clarify |
|
257 |
apply (case_tac "\<exists>p. f p \<in> Q") |
|
258 |
apply (erule_tac x = "{p. f p \<in> Q}" in allE) |
|
259 |
apply (fast dest: inj_onD) |
|
63612 | 260 |
apply blast |
63572 | 261 |
done |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
262 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
263 |
|
60758 | 264 |
subsection \<open>Well-Foundedness Results for Unions\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
265 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
266 |
lemma wf_union_compatible: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
267 |
assumes "wf R" "wf S" |
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
32205
diff
changeset
|
268 |
assumes "R O S \<subseteq> R" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
269 |
shows "wf (R \<union> S)" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
270 |
proof (rule wfI_min) |
63108 | 271 |
fix x :: 'a and Q |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
272 |
let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
273 |
assume "x \<in> Q" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
274 |
obtain a where "a \<in> ?Q'" |
60758 | 275 |
by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast |
63108 | 276 |
with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" |
277 |
by (erule wfE_min) |
|
63572 | 278 |
have "y \<notin> Q" if "(y, z) \<in> S" for y |
279 |
proof |
|
280 |
from that have "y \<notin> ?Q'" by (rule zmin) |
|
281 |
assume "y \<in> Q" |
|
282 |
with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto |
|
283 |
from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI) |
|
284 |
with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" .. |
|
285 |
with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast |
|
286 |
with \<open>w \<in> Q\<close> show False by contradiction |
|
287 |
qed |
|
60758 | 288 |
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 |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
289 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
290 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
291 |
|
63572 | 292 |
text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
293 |
|
63108 | 294 |
lemma wf_UN: |
295 |
assumes "\<forall>i\<in>I. wf (r i)" |
|
296 |
and "\<forall>i\<in>I. \<forall>j\<in>I. r i \<noteq> r j \<longrightarrow> Domain (r i) \<inter> Range (r j) = {}" |
|
297 |
shows "wf (\<Union>i\<in>I. r i)" |
|
298 |
using assms |
|
299 |
apply (simp only: wf_eq_minimal) |
|
300 |
apply clarify |
|
301 |
apply (rename_tac A a, case_tac "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i") |
|
302 |
prefer 2 |
|
303 |
apply force |
|
304 |
apply clarify |
|
305 |
apply (drule bspec, assumption) |
|
306 |
apply (erule_tac x="{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }" in allE) |
|
307 |
apply (blast elim!: allE) |
|
308 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
309 |
|
32263 | 310 |
lemma wfP_SUP: |
63572 | 311 |
"\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> |
312 |
wfP (SUPREMUM UNIV r)" |
|
313 |
by (rule wf_UN[to_pred]) simp_all |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
314 |
|
63108 | 315 |
lemma wf_Union: |
316 |
assumes "\<forall>r\<in>R. wf r" |
|
317 |
and "\<forall>r\<in>R. \<forall>s\<in>R. r \<noteq> s \<longrightarrow> Domain r \<inter> Range s = {}" |
|
318 |
shows "wf (\<Union>R)" |
|
319 |
using assms wf_UN[of R "\<lambda>i. i"] by simp |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
320 |
|
63109 | 321 |
text \<open> |
322 |
Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction. |
|
323 |
\<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>. |
|
324 |
Pick an \<open>R\<close>-min element \<open>z\<close> of the (nonempty) set \<open>{a\<in>A | \<exists>b\<in>A. a \<midarrow>R\<rightarrow> b}\<close>. |
|
325 |
By definition, there is \<open>z' \<in> A\<close> s.t. \<open>z \<midarrow>R\<rightarrow> z'\<close>. Because \<open>z\<close> is \<open>R\<close>-min in the |
|
326 |
subset, \<open>z'\<close> must be \<open>R\<close>-min in \<open>A\<close>. Because \<open>z'\<close> has an \<open>R\<close>-predecessor, it cannot |
|
327 |
have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well. |
|
328 |
\<^enum> There is no such step. |
|
329 |
Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min |
|
330 |
element of \<open>A\<close> as well. |
|
331 |
\<close> |
|
63108 | 332 |
lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)" |
333 |
using wf_union_compatible[of s r] |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
334 |
by (auto simp: Un_ac) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
335 |
|
63108 | 336 |
lemma wf_union_merge: "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" |
337 |
(is "wf ?A = wf ?B") |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
338 |
proof |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
339 |
assume "wf ?A" |
63108 | 340 |
with wf_trancl have wfT: "wf (?A\<^sup>+)" . |
341 |
moreover have "?B \<subseteq> ?A\<^sup>+" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
342 |
by (subst trancl_unfold, subst trancl_unfold) blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
343 |
ultimately show "wf ?B" by (rule wf_subset) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
344 |
next |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
345 |
assume "wf ?B" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
346 |
show "wf ?A" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
347 |
proof (rule wfI_min) |
63108 | 348 |
fix Q :: "'a set" and x |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
349 |
assume "x \<in> Q" |
63109 | 350 |
with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
351 |
by (erule wfE_min) |
63109 | 352 |
then have 1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" |
353 |
and 2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" |
|
354 |
and 3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
355 |
by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
356 |
show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
357 |
proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q") |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
358 |
case True |
63109 | 359 |
with \<open>z \<in> Q\<close> 3 show ?thesis by blast |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
360 |
next |
63108 | 361 |
case False |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
362 |
then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
363 |
have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
364 |
proof (intro allI impI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
365 |
fix y assume "(y, z') \<in> ?A" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
366 |
then show "y \<notin> Q" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
367 |
proof |
63108 | 368 |
assume "(y, z') \<in> R" |
60758 | 369 |
then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> .. |
63109 | 370 |
with 1 show "y \<notin> Q" . |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
371 |
next |
63108 | 372 |
assume "(y, z') \<in> S" |
60758 | 373 |
then have "(y, z) \<in> S O R" using \<open>(z', z) \<in> R\<close> .. |
63109 | 374 |
with 2 show "y \<notin> Q" . |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
375 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
376 |
qed |
60758 | 377 |
with \<open>z' \<in> Q\<close> show ?thesis .. |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
378 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
379 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
380 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
381 |
|
63612 | 382 |
lemma wf_comp_self: "wf R \<longleftrightarrow> wf (R O R)" \<comment> \<open>special case\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
383 |
by (rule wf_union_merge [where S = "{}", simplified]) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
384 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
385 |
|
60758 | 386 |
subsection \<open>Well-Foundedness of Composition\<close> |
60148 | 387 |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
388 |
text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close> |
60148 | 389 |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
390 |
lemma qc_wf_relto_iff: |
61799 | 391 |
assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close> |
63109 | 392 |
shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" |
63612 | 393 |
(is "wf ?S \<longleftrightarrow> _") |
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
394 |
proof |
63109 | 395 |
show "wf R" if "wf ?S" |
396 |
proof - |
|
397 |
have "R \<subseteq> ?S" by auto |
|
63612 | 398 |
with wf_subset [of ?S] that show "wf R" |
399 |
by auto |
|
63109 | 400 |
qed |
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
401 |
next |
63109 | 402 |
show "wf ?S" if "wf R" |
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
403 |
proof (rule wfI_pf) |
63109 | 404 |
fix A |
405 |
assume A: "A \<subseteq> ?S `` A" |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
406 |
let ?X = "(R \<union> S)\<^sup>* `` A" |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
407 |
have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" |
63109 | 408 |
proof - |
409 |
have "(x, z) \<in> (R \<union> S)\<^sup>* O R" if "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R" for x y z |
|
410 |
using that |
|
411 |
proof (induct y z) |
|
412 |
case rtrancl_refl |
|
413 |
then show ?case by auto |
|
414 |
next |
|
415 |
case (rtrancl_into_rtrancl a b c) |
|
416 |
then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" |
|
417 |
using assms by blast |
|
418 |
then show ?case by simp |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
419 |
qed |
63109 | 420 |
then show ?thesis by auto |
421 |
qed |
|
422 |
then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" |
|
423 |
using rtrancl_Un_subset by blast |
|
424 |
then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" |
|
425 |
by (simp add: relcomp_mono rtrancl_mono) |
|
426 |
also have "\<dots> = (R \<union> S)\<^sup>* O R" |
|
427 |
by (simp add: O_assoc[symmetric]) |
|
428 |
finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*" |
|
429 |
by (simp add: O_assoc[symmetric] relcomp_mono) |
|
430 |
also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" |
|
431 |
using * by (simp add: relcomp_mono) |
|
432 |
finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" |
|
433 |
by (simp add: O_assoc[symmetric]) |
|
434 |
then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" |
|
435 |
by (simp add: Image_mono) |
|
436 |
moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" |
|
437 |
using A by (auto simp: relcomp_Image) |
|
438 |
ultimately have "?X \<subseteq> R `` ?X" |
|
439 |
by (auto simp: relcomp_Image) |
|
440 |
then have "?X = {}" |
|
441 |
using \<open>wf R\<close> by (simp add: wfE_pf) |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
442 |
moreover have "A \<subseteq> ?X" by auto |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
443 |
ultimately show "A = {}" by simp |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
444 |
qed |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
445 |
qed |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
446 |
|
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
447 |
corollary wf_relcomp_compatible: |
60148 | 448 |
assumes "wf R" and "R O S \<subseteq> S O R" |
449 |
shows "wf (S O R)" |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
450 |
proof - |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
451 |
have "R O S \<subseteq> (R \<union> S)\<^sup>* O R" |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
452 |
using assms by blast |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
453 |
then have "wf (S\<^sup>* O R O S\<^sup>*)" |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
454 |
by (simp add: assms qc_wf_relto_iff) |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
455 |
then show ?thesis |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
456 |
by (rule Wellfounded.wf_subset) blast |
60148 | 457 |
qed |
458 |
||
459 |
||
60758 | 460 |
subsection \<open>Acyclic relations\<close> |
33217 | 461 |
|
63108 | 462 |
lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r" |
63572 | 463 |
by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl]) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
464 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
465 |
lemmas wfP_acyclicP = wf_acyclic [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
466 |
|
63108 | 467 |
|
468 |
subsubsection \<open>Wellfoundedness of finite acyclic relations\<close> |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
469 |
|
63108 | 470 |
lemma finite_acyclic_wf [rule_format]: "finite r \<Longrightarrow> acyclic r \<longrightarrow> wf r" |
63572 | 471 |
apply (erule finite_induct) |
472 |
apply blast |
|
473 |
apply (simp add: split_tupled_all) |
|
474 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
475 |
|
63108 | 476 |
lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)" |
63572 | 477 |
apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) |
478 |
apply (erule acyclic_converse [THEN iffD2]) |
|
479 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
480 |
|
63088
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
481 |
text \<open> |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
482 |
Observe that the converse of an irreflexive, transitive, |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
483 |
and finite relation is again well-founded. Thus, we may |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
484 |
employ it for well-founded induction. |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
485 |
\<close> |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
486 |
lemma wf_converse: |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
487 |
assumes "irrefl r" and "trans r" and "finite r" |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
488 |
shows "wf (r\<inverse>)" |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
489 |
proof - |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
490 |
have "acyclic r" |
63572 | 491 |
using \<open>irrefl r\<close> and \<open>trans r\<close> |
492 |
by (simp add: irrefl_def acyclic_irrefl) |
|
493 |
with \<open>finite r\<close> show ?thesis |
|
494 |
by (rule finite_acyclic_wf_converse) |
|
63088
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
495 |
qed |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
496 |
|
63108 | 497 |
lemma wf_iff_acyclic_if_finite: "finite r \<Longrightarrow> wf r = acyclic r" |
63572 | 498 |
by (blast intro: finite_acyclic_wf wf_acyclic) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
499 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
500 |
|
60758 | 501 |
subsection \<open>@{typ nat} is well-founded\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
502 |
|
63108 | 503 |
lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
504 |
proof (rule ext, rule ext, rule iffI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
505 |
fix n m :: nat |
63108 | 506 |
show "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n" |
507 |
using that |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
508 |
proof (induct n) |
63108 | 509 |
case 0 |
510 |
then show ?case by auto |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
511 |
next |
63108 | 512 |
case (Suc n) |
513 |
then show ?case |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
514 |
by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
515 |
qed |
63108 | 516 |
show "m < n" if "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" |
517 |
using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
518 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
519 |
|
63108 | 520 |
definition pred_nat :: "(nat \<times> nat) set" |
521 |
where "pred_nat = {(m, n). n = Suc m}" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
522 |
|
63108 | 523 |
definition less_than :: "(nat \<times> nat) set" |
524 |
where "less_than = pred_nat\<^sup>+" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
525 |
|
63108 | 526 |
lemma less_eq: "(m, n) \<in> pred_nat\<^sup>+ \<longleftrightarrow> m < n" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
527 |
unfolding less_nat_rel pred_nat_def trancl_def by simp |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
528 |
|
63108 | 529 |
lemma pred_nat_trancl_eq_le: "(m, n) \<in> pred_nat\<^sup>* \<longleftrightarrow> m \<le> n" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
530 |
unfolding less_eq rtrancl_eq_or_trancl by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
531 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
532 |
lemma wf_pred_nat: "wf pred_nat" |
63572 | 533 |
apply (unfold wf_def pred_nat_def) |
534 |
apply clarify |
|
535 |
apply (induct_tac x) |
|
536 |
apply blast+ |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
537 |
done |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
538 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
539 |
lemma wf_less_than [iff]: "wf less_than" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
540 |
by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
541 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
542 |
lemma trans_less_than [iff]: "trans less_than" |
35216 | 543 |
by (simp add: less_than_def) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
544 |
|
63108 | 545 |
lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
546 |
by (simp add: less_than_def less_eq) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
547 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
548 |
lemma wf_less: "wf {(x, y::nat). x < y}" |
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
549 |
by (rule Wellfounded.wellorder_class.wf) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
550 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
551 |
|
60758 | 552 |
subsection \<open>Accessible Part\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
553 |
|
60758 | 554 |
text \<open> |
63108 | 555 |
Inductive definition of the accessible part \<open>acc r\<close> of a |
556 |
relation; see also @{cite "paulin-tlca"}. |
|
60758 | 557 |
\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
558 |
|
63108 | 559 |
inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set" |
560 |
where accI: "(\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
561 |
|
63108 | 562 |
abbreviation termip :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
563 |
where "termip r \<equiv> accp (r\<inverse>\<inverse>)" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
564 |
|
63108 | 565 |
abbreviation termi :: "('a \<times> 'a) set \<Rightarrow> 'a set" |
566 |
where "termi r \<equiv> acc (r\<inverse>)" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
567 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
568 |
lemmas accpI = accp.accI |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
569 |
|
63108 | 570 |
lemma accp_eq_acc [code]: "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})" |
54295 | 571 |
by (simp add: acc_def) |
572 |
||
573 |
||
60758 | 574 |
text \<open>Induction rules\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
575 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
576 |
theorem accp_induct: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
577 |
assumes major: "accp r a" |
63108 | 578 |
assumes hyp: "\<And>x. accp r x \<Longrightarrow> \<forall>y. r y x \<longrightarrow> P y \<Longrightarrow> P x" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
579 |
shows "P a" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
580 |
apply (rule major [THEN accp.induct]) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
581 |
apply (rule hyp) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
582 |
apply (rule accp.accI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
583 |
apply fast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
584 |
apply fast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
585 |
done |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
586 |
|
61337 | 587 |
lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp] |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
588 |
|
63108 | 589 |
theorem accp_downward: "accp r b \<Longrightarrow> r a b \<Longrightarrow> accp r a" |
63572 | 590 |
by (cases rule: accp.cases) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
591 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
592 |
lemma not_accp_down: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
593 |
assumes na: "\<not> accp R x" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
594 |
obtains z where "R z x" and "\<not> accp R z" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
595 |
proof - |
63572 | 596 |
assume a: "\<And>z. R z x \<Longrightarrow> \<not> accp R z \<Longrightarrow> thesis" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
597 |
show thesis |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
598 |
proof (cases "\<forall>z. R z x \<longrightarrow> accp R z") |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
599 |
case True |
63108 | 600 |
then have "\<And>z. R z x \<Longrightarrow> accp R z" by auto |
601 |
then have "accp R x" by (rule accp.accI) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
602 |
with na show thesis .. |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
603 |
next |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
604 |
case False then obtain z where "R z x" and "\<not> accp R z" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
605 |
by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
606 |
with a show thesis . |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
607 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
608 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
609 |
|
63108 | 610 |
lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r a \<longrightarrow> accp r b" |
63612 | 611 |
by (erule rtranclp_induct) (blast dest: accp_downward)+ |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
612 |
|
63108 | 613 |
theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b" |
63572 | 614 |
by (blast dest: accp_downwards_aux) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
615 |
|
63108 | 616 |
theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
617 |
apply (rule wfPUNIVI) |
63572 | 618 |
apply (rule_tac P = P in accp_induct) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
619 |
apply blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
620 |
apply blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
621 |
done |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
622 |
|
63108 | 623 |
theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
624 |
apply (erule wfP_induct_rule) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
625 |
apply (rule accp.accI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
626 |
apply blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
627 |
done |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
628 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
629 |
theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)" |
63572 | 630 |
by (blast intro: accp_wfPI dest: accp_wfPD) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
631 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
632 |
|
60758 | 633 |
text \<open>Smaller relations have bigger accessible parts:\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
634 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
635 |
lemma accp_subset: |
63572 | 636 |
assumes "R1 \<le> R2" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
637 |
shows "accp R2 \<le> accp R1" |
26803
0af0f674845d
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
berghofe
parents:
26748
diff
changeset
|
638 |
proof (rule predicate1I) |
63572 | 639 |
fix x |
640 |
assume "accp R2 x" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
641 |
then show "accp R1 x" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
642 |
proof (induct x) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
643 |
fix x |
63572 | 644 |
assume "\<And>y. R2 y x \<Longrightarrow> accp R1 y" |
645 |
with assms show "accp R1 x" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
646 |
by (blast intro: accp.accI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
647 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
648 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
649 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
650 |
|
60758 | 651 |
text \<open>This is a generalized induction theorem that works on |
652 |
subsets of the accessible part.\<close> |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
653 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
654 |
lemma accp_subset_induct: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
655 |
assumes subset: "D \<le> accp R" |
63572 | 656 |
and dcl: "\<And>x z. D x \<Longrightarrow> R z x \<Longrightarrow> D z" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
657 |
and "D x" |
63572 | 658 |
and istep: "\<And>x. D x \<Longrightarrow> (\<And>z. R z x \<Longrightarrow> P z) \<Longrightarrow> P x" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
659 |
shows "P x" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
660 |
proof - |
60758 | 661 |
from subset and \<open>D x\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
662 |
have "accp R x" .. |
60758 | 663 |
then show "P x" using \<open>D x\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
664 |
proof (induct x) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
665 |
fix x |
63572 | 666 |
assume "D x" and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
667 |
with dcl and istep show "P x" by blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
668 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
669 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
670 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
671 |
|
60758 | 672 |
text \<open>Set versions of the above theorems\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
673 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
674 |
lemmas acc_induct = accp_induct [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
675 |
lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
676 |
lemmas acc_downward = accp_downward [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
677 |
lemmas not_acc_down = not_accp_down [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
678 |
lemmas acc_downwards_aux = accp_downwards_aux [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
679 |
lemmas acc_downwards = accp_downwards [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
680 |
lemmas acc_wfI = accp_wfPI [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
681 |
lemmas acc_wfD = accp_wfPD [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
682 |
lemmas wf_acc_iff = wfP_accp_iff [to_set] |
46177
adac34829e10
pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
berghofe
parents:
45970
diff
changeset
|
683 |
lemmas acc_subset = accp_subset [to_set] |
adac34829e10
pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
berghofe
parents:
45970
diff
changeset
|
684 |
lemmas acc_subset_induct = accp_subset_induct [to_set] |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
685 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
686 |
|
60758 | 687 |
subsection \<open>Tools for building wellfounded relations\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
688 |
|
60758 | 689 |
text \<open>Inverse Image\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
690 |
|
63572 | 691 |
lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)" |
63612 | 692 |
for f :: "'a \<Rightarrow> 'b" |
63572 | 693 |
apply (simp add: inv_image_def wf_eq_minimal) |
694 |
apply clarify |
|
695 |
apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}") |
|
696 |
prefer 2 |
|
697 |
apply (blast del: allE) |
|
698 |
apply (erule allE) |
|
699 |
apply (erule (1) notE impE) |
|
700 |
apply blast |
|
701 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
702 |
|
60758 | 703 |
text \<open>Measure functions into @{typ nat}\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
704 |
|
63108 | 705 |
definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set" |
706 |
where "measure = inv_image less_than" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
707 |
|
63108 | 708 |
lemma in_measure[simp, code_unfold]: "(x, y) \<in> measure f \<longleftrightarrow> f x < f y" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
709 |
by (simp add:measure_def) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
710 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
711 |
lemma wf_measure [iff]: "wf (measure f)" |
63572 | 712 |
unfolding measure_def by (rule wf_less_than [THEN wf_inv_image]) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
713 |
|
63108 | 714 |
lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}" |
715 |
for f :: "'a \<Rightarrow> nat" |
|
63572 | 716 |
apply (insert wf_measure[of f]) |
717 |
apply (simp only: measure_def inv_image_def less_than_def less_eq) |
|
718 |
apply (erule wf_subset) |
|
719 |
apply auto |
|
720 |
done |
|
41720 | 721 |
|
722 |
||
63108 | 723 |
subsubsection \<open>Lexicographic combinations\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
724 |
|
63108 | 725 |
definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" |
726 |
(infixr "<*lex*>" 80) |
|
727 |
where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
728 |
|
63108 | 729 |
lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)" |
63572 | 730 |
apply (unfold wf_def lex_prod_def) |
731 |
apply (rule allI) |
|
732 |
apply (rule impI) |
|
733 |
apply (simp only: split_paired_All) |
|
734 |
apply (drule spec) |
|
735 |
apply (erule mp) |
|
736 |
apply (rule allI) |
|
737 |
apply (rule impI) |
|
738 |
apply (drule spec) |
|
739 |
apply (erule mp) |
|
740 |
apply blast |
|
741 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
742 |
|
63108 | 743 |
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" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
744 |
by (auto simp:lex_prod_def) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
745 |
|
63108 | 746 |
text \<open>\<open><*lex*>\<close> preserves transitivity\<close> |
747 |
lemma trans_lex_prod [intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)" |
|
748 |
unfolding trans_def lex_prod_def by blast |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
749 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
750 |
|
60758 | 751 |
text \<open>lexicographic combinations with measure functions\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
752 |
|
63108 | 753 |
definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80) |
754 |
where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
755 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
756 |
lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)" |
63572 | 757 |
by (auto simp: mlex_prod_def) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
758 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
759 |
lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R" |
63572 | 760 |
by (simp add: mlex_prod_def) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
761 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
762 |
lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R" |
63572 | 763 |
by (auto simp: mlex_prod_def) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
764 |
|
63572 | 765 |
text \<open>Proper subset relation on finite sets.\<close> |
63108 | 766 |
definition finite_psubset :: "('a set \<times> 'a set) set" |
63572 | 767 |
where "finite_psubset = {(A, B). A \<subset> B \<and> finite B}" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
768 |
|
63108 | 769 |
lemma wf_finite_psubset[simp]: "wf finite_psubset" |
770 |
apply (unfold finite_psubset_def) |
|
771 |
apply (rule wf_measure [THEN wf_subset]) |
|
772 |
apply (simp add: measure_def inv_image_def less_than_def less_eq) |
|
773 |
apply (fast elim!: psubset_card_mono) |
|
774 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
775 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
776 |
lemma trans_finite_psubset: "trans finite_psubset" |
63612 | 777 |
by (auto simp: finite_psubset_def less_le trans_def) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
778 |
|
63572 | 779 |
lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A \<subset> B \<and> finite B" |
63108 | 780 |
unfolding finite_psubset_def by auto |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
781 |
|
60758 | 782 |
text \<open>max- and min-extension of order to finite sets\<close> |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
783 |
|
63108 | 784 |
inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" |
785 |
for R :: "('a \<times> 'a) set" |
|
63572 | 786 |
where max_extI[intro]: |
787 |
"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" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
788 |
|
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
789 |
lemma max_ext_wf: |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
790 |
assumes wf: "wf r" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
791 |
shows "wf (max_ext r)" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
792 |
proof (rule acc_wfI, intro allI) |
63108 | 793 |
fix M |
794 |
show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") |
|
63572 | 795 |
proof (cases "finite M") |
796 |
case True |
|
63108 | 797 |
then show ?thesis |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
798 |
proof (induct M) |
63572 | 799 |
case empty |
800 |
show ?case |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
801 |
by (rule accI) (auto elim: max_ext.cases) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
802 |
next |
63572 | 803 |
case (insert a M) |
804 |
from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
805 |
proof (induct arbitrary: M) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
806 |
fix M a |
63572 | 807 |
assume "M \<in> ?W" |
808 |
assume [intro]: "finite M" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
809 |
assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W" |
63572 | 810 |
have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W" |
63108 | 811 |
if "finite N" "finite M" for N M :: "'a set" |
812 |
using that by (induct N arbitrary: M) (auto simp: hyp) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
813 |
show "insert a M \<in> ?W" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
814 |
proof (rule accI) |
63108 | 815 |
fix N |
816 |
assume Nless: "(N, insert a M) \<in> max_ext r" |
|
817 |
then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
818 |
by (auto elim!: max_ext.cases) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
819 |
|
63108 | 820 |
let ?N1 = "{n \<in> N. (n, a) \<in> r}" |
821 |
let ?N2 = "{n \<in> N. (n, a) \<notin> r}" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
37767
diff
changeset
|
822 |
have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
823 |
from Nless have "finite N" by (auto elim: max_ext.cases) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
824 |
then have finites: "finite ?N1" "finite ?N2" by auto |
63108 | 825 |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
826 |
have "?N2 \<in> ?W" |
63572 | 827 |
proof (cases "M = {}") |
828 |
case [simp]: True |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
829 |
have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases) |
63108 | 830 |
from * have "?N2 = {}" by auto |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
831 |
with Mw show "?N2 \<in> ?W" by (simp only:) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
832 |
next |
63572 | 833 |
case False |
63108 | 834 |
from * finites have N2: "(?N2, M) \<in> max_ext r" |
60758 | 835 |
by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto |
836 |
with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
837 |
qed |
63108 | 838 |
with finites have "?N1 \<union> ?N2 \<in> ?W" |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
839 |
by (rule add_less) simp |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
840 |
then show "N \<in> ?W" by (simp only: N) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
841 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
842 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
843 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
844 |
next |
63572 | 845 |
case [simp]: False |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
846 |
show ?thesis |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
847 |
by (rule accI) (auto elim: max_ext.cases) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
848 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
849 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
850 |
|
63572 | 851 |
lemma max_ext_additive: "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> (A \<union> C, B \<union> D) \<in> max_ext R" |
63108 | 852 |
by (force elim!: max_ext.cases) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28845
diff
changeset
|
853 |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
854 |
|
63108 | 855 |
definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" |
856 |
where "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
857 |
|
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
858 |
lemma min_ext_wf: |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
859 |
assumes "wf r" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
860 |
shows "wf (min_ext r)" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
861 |
proof (rule wfI_min) |
63108 | 862 |
show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q" |
863 |
for Q :: "'a set set" and x |
|
864 |
proof (cases "Q = {{}}") |
|
865 |
case True |
|
866 |
then show ?thesis by (simp add: min_ext_def) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
867 |
next |
63108 | 868 |
case False |
869 |
with nonempty obtain e x where "x \<in> Q" "e \<in> x" by force |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
870 |
then have eU: "e \<in> \<Union>Q" by auto |
63108 | 871 |
with \<open>wf r\<close> |
872 |
obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
873 |
by (erule wfE_min) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
874 |
from z obtain m where "m \<in> Q" "z \<in> m" by auto |
63572 | 875 |
from \<open>m \<in> Q\<close> show ?thesis |
876 |
proof (intro rev_bexI allI impI) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
877 |
fix n |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
878 |
assume smaller: "(n, m) \<in> min_ext r" |
63572 | 879 |
with \<open>z \<in> m\<close> obtain y where "y \<in> n" "(y, z) \<in> r" |
880 |
by (auto simp: min_ext_def) |
|
881 |
with z(2) show "n \<notin> Q" by auto |
|
63108 | 882 |
qed |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
883 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
884 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
885 |
|
63108 | 886 |
|
887 |
subsubsection \<open>Bounded increase must terminate\<close> |
|
43137 | 888 |
|
889 |
lemma wf_bounded_measure: |
|
63108 | 890 |
fixes ub :: "'a \<Rightarrow> nat" |
891 |
and f :: "'a \<Rightarrow> nat" |
|
892 |
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" |
|
893 |
shows "wf r" |
|
63572 | 894 |
by (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]]) (auto dest: assms) |
43137 | 895 |
|
896 |
lemma wf_bounded_set: |
|
63108 | 897 |
fixes ub :: "'a \<Rightarrow> 'b set" |
898 |
and f :: "'a \<Rightarrow> 'b set" |
|
899 |
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" |
|
900 |
shows "wf r" |
|
63572 | 901 |
apply (rule wf_bounded_measure[of r "\<lambda>a. card (ub a)" "\<lambda>a. card (f a)"]) |
902 |
apply (drule assms) |
|
63108 | 903 |
apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) |
904 |
done |
|
43137 | 905 |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
906 |
lemma finite_subset_wf: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
907 |
assumes "finite A" |
63572 | 908 |
shows "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
909 |
proof (intro finite_acyclic_wf) |
63572 | 910 |
have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A" |
911 |
by blast |
|
63108 | 912 |
then show "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
913 |
by (rule finite_subset) (auto simp: assms finite_cartesian_product) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
914 |
next |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
915 |
have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
916 |
by (intro trancl_id transI) blast |
63572 | 917 |
also have " \<forall>x. (x, x) \<notin> \<dots>" |
918 |
by blast |
|
919 |
finally show "acyclic {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" |
|
920 |
by (rule acyclicI) |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
921 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
922 |
|
54295 | 923 |
hide_const (open) acc accp |
924 |
||
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
925 |
end |