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