author | paulson <lp15@cam.ac.uk> |
Sat, 20 Apr 2024 12:08:01 +0100 | |
changeset 80138 | a30a1385f7d0 |
parent 80046 | 38803a6b3357 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
1 |
(* Title: HOL/Wellfounded.thy |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
2 |
Author: Tobias Nipkow |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
3 |
Author: Lawrence C Paulson |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
4 |
Author: Konrad Slind |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
5 |
Author: Alexander Krauss |
55027 | 6 |
Author: Andrei Popescu, TU Muenchen |
80046
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
7 |
Author: Martin Desharnais, MPI-INF Saarbruecken |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
8 |
*) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
9 |
|
60758 | 10 |
section \<open>Well-founded Recursion\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
11 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
12 |
theory Wellfounded |
63572 | 13 |
imports Transitive_Closure |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
14 |
begin |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
15 |
|
60758 | 16 |
subsection \<open>Basic Definitions\<close> |
26976 | 17 |
|
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
18 |
definition wf_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
19 |
"wf_on A r \<longleftrightarrow> (\<forall>P. (\<forall>x \<in> A. (\<forall>y \<in> A. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x \<in> A. P x))" |
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
20 |
|
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
21 |
abbreviation wf :: "('a \<times> 'a) set \<Rightarrow> bool" where |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
22 |
"wf \<equiv> wf_on UNIV" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
23 |
|
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
24 |
definition wfp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
25 |
"wfp_on A R \<longleftrightarrow> (\<forall>P. (\<forall>x \<in> A. (\<forall>y \<in> A. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x \<in> A. P x))" |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
26 |
|
79965
233d70cad0cf
redefined wfP as an abbreviation for "wfp_on UNIV"
desharna
parents:
79963
diff
changeset
|
27 |
abbreviation wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
233d70cad0cf
redefined wfP as an abbreviation for "wfp_on UNIV"
desharna
parents:
79963
diff
changeset
|
28 |
"wfP \<equiv> wfp_on UNIV" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
29 |
|
79924 | 30 |
alias wfp = wfP |
31 |
||
32 |
text \<open>We keep old name \<^const>\<open>wfP\<close> for backward compatibility, but offer new name \<^const>\<open>wfp\<close> to be |
|
33 |
consistent with similar predicates, e.g., \<^const>\<open>asymp\<close>, \<^const>\<open>transp\<close>, \<^const>\<open>totalp\<close>.\<close> |
|
34 |
||
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
35 |
|
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
36 |
subsection \<open>Equivalence of Definitions\<close> |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
37 |
|
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
38 |
lemma wfp_on_wf_on_eq[pred_set_conv]: "wfp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> wf_on A r" |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
39 |
by (simp add: wfp_on_def wf_on_def) |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
40 |
|
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
41 |
lemma wf_def: "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))" |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
42 |
unfolding wf_on_def by simp |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
43 |
|
79965
233d70cad0cf
redefined wfP as an abbreviation for "wfp_on UNIV"
desharna
parents:
79963
diff
changeset
|
44 |
lemma wfP_def: "wfP r \<longleftrightarrow> wf {(x, y). r x y}" |
233d70cad0cf
redefined wfP as an abbreviation for "wfp_on UNIV"
desharna
parents:
79963
diff
changeset
|
45 |
unfolding wf_def wfp_on_def by simp |
233d70cad0cf
redefined wfP as an abbreviation for "wfp_on UNIV"
desharna
parents:
79963
diff
changeset
|
46 |
|
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
47 |
lemma wfP_wf_eq: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r" |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
48 |
using wfp_on_wf_on_eq . |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
49 |
|
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
50 |
|
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
51 |
subsection \<open>Induction Principles\<close> |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
52 |
|
79996
4f803ae64781
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
desharna
parents:
79971
diff
changeset
|
53 |
lemma wf_on_induct[consumes 1, case_names in_set less, induct set: wf_on]: |
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
54 |
assumes "wf_on A r" and "x \<in> A" and "\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> P y) \<Longrightarrow> P x" |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
55 |
shows "P x" |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
56 |
using assms(2,3) by (auto intro: \<open>wf_on A r\<close>[unfolded wf_on_def, rule_format]) |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
57 |
|
79996
4f803ae64781
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
desharna
parents:
79971
diff
changeset
|
58 |
lemma wfp_on_induct[consumes 1, case_names in_set less, induct pred: wfp_on]: |
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
59 |
assumes "wfp_on A r" and "x \<in> A" and "\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> r y x \<Longrightarrow> P y) \<Longrightarrow> P x" |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
60 |
shows "P x" |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
61 |
using assms by (fact wf_on_induct[to_pred]) |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
62 |
|
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
63 |
lemma wf_induct: |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
64 |
assumes "wf r" |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
65 |
and "\<And>x. \<forall>y. (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x" |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
66 |
shows "P a" |
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
67 |
using assms by (auto intro: wf_on_induct[of UNIV]) |
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
68 |
|
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
69 |
lemmas wfP_induct = wf_induct [to_pred] |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
70 |
|
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
71 |
lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
72 |
|
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
73 |
lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
74 |
|
79997 | 75 |
lemma wf_on_iff_wf: "wf_on A r \<longleftrightarrow> wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}" |
76 |
proof (rule iffI) |
|
77 |
assume wf: "wf_on A r" |
|
78 |
show "wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}" |
|
79 |
unfolding wf_def |
|
80 |
proof (intro allI impI ballI) |
|
81 |
fix P x |
|
82 |
assume IH: "\<forall>x. (\<forall>y. (y, x) \<in> {(x, y). (x, y) \<in> r \<and> x \<in> A \<and> y \<in> A} \<longrightarrow> P y) \<longrightarrow> P x" |
|
83 |
show "P x" |
|
84 |
proof (cases "x \<in> A") |
|
85 |
case True |
|
86 |
show ?thesis |
|
87 |
using wf |
|
88 |
proof (induction x rule: wf_on_induct) |
|
89 |
case in_set |
|
90 |
thus ?case |
|
91 |
using True . |
|
92 |
next |
|
93 |
case (less x) |
|
94 |
thus ?case |
|
95 |
by (auto intro: IH[rule_format]) |
|
96 |
qed |
|
97 |
next |
|
98 |
case False |
|
99 |
then show ?thesis |
|
100 |
by (auto intro: IH[rule_format]) |
|
101 |
qed |
|
102 |
qed |
|
103 |
next |
|
104 |
assume wf: "wf {(x, y). (x, y) \<in> r \<and> x \<in> A \<and> y \<in> A}" |
|
105 |
show "wf_on A r" |
|
106 |
unfolding wf_on_def |
|
107 |
proof (intro allI impI ballI) |
|
108 |
fix P x |
|
109 |
assume IH: "\<forall>x\<in>A. (\<forall>y\<in>A. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x" and "x \<in> A" |
|
110 |
show "P x" |
|
111 |
using wf \<open>x \<in> A\<close> |
|
112 |
proof (induction x rule: wf_on_induct) |
|
113 |
case in_set |
|
114 |
show ?case |
|
115 |
by simp |
|
116 |
next |
|
117 |
case (less y) |
|
118 |
hence "\<And>z. (z, y) \<in> r \<Longrightarrow> z \<in> A \<Longrightarrow> P z" |
|
119 |
by simp |
|
120 |
thus ?case |
|
121 |
using IH[rule_format, OF \<open>y \<in> A\<close>] by simp |
|
122 |
qed |
|
123 |
qed |
|
124 |
qed |
|
125 |
||
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
126 |
|
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
127 |
subsection \<open>Introduction Rules\<close> |
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
128 |
|
63108 | 129 |
lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
130 |
unfolding wf_def by blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
131 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
132 |
lemmas wfPUNIVI = wfUNIVI [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
133 |
|
63108 | 134 |
text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>. |
135 |
If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close> |
|
136 |
lemma wfI: |
|
137 |
assumes "r \<subseteq> A \<times> B" |
|
138 |
and "\<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x; x \<in> A; x \<in> B\<rbrakk> \<Longrightarrow> P x" |
|
139 |
shows "wf r" |
|
140 |
using assms unfolding wf_def by blast |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
141 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
142 |
|
79917
d0205dde00bb
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
desharna
parents:
77172
diff
changeset
|
143 |
subsection \<open>Ordering Properties\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
144 |
|
63108 | 145 |
lemma wf_not_sym: "wf r \<Longrightarrow> (a, x) \<in> r \<Longrightarrow> (x, a) \<notin> r" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
146 |
by (induct a arbitrary: x set: wf) blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
147 |
|
33215
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset
|
148 |
lemma wf_asym: |
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset
|
149 |
assumes "wf r" "(a, x) \<in> r" |
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset
|
150 |
obtains "(x, a) \<notin> r" |
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset
|
151 |
by (drule wf_not_sym[OF assms]) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
152 |
|
74971
16eaa56f69f7
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
desharna
parents:
74868
diff
changeset
|
153 |
lemma wf_imp_asym: "wf r \<Longrightarrow> asym r" |
16eaa56f69f7
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
desharna
parents:
74868
diff
changeset
|
154 |
by (auto intro: asymI elim: wf_asym) |
16eaa56f69f7
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
desharna
parents:
74868
diff
changeset
|
155 |
|
16eaa56f69f7
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
desharna
parents:
74868
diff
changeset
|
156 |
lemma wfP_imp_asymp: "wfP r \<Longrightarrow> asymp r" |
16eaa56f69f7
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
desharna
parents:
74868
diff
changeset
|
157 |
by (rule wf_imp_asym[to_pred]) |
16eaa56f69f7
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
desharna
parents:
74868
diff
changeset
|
158 |
|
63108 | 159 |
lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
160 |
by (blast elim: wf_asym) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
161 |
|
63572 | 162 |
lemma wf_irrefl: |
163 |
assumes "wf r" |
|
164 |
obtains "(a, a) \<notin> r" |
|
63108 | 165 |
by (drule wf_not_refl[OF assms]) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
166 |
|
72170
7fa9605b226c
Another go with lex: now lexordp back in class ord
paulson <lp15@cam.ac.uk>
parents:
72168
diff
changeset
|
167 |
lemma wf_imp_irrefl: |
7fa9605b226c
Another go with lex: now lexordp back in class ord
paulson <lp15@cam.ac.uk>
parents:
72168
diff
changeset
|
168 |
assumes "wf r" shows "irrefl r" |
7fa9605b226c
Another go with lex: now lexordp back in class ord
paulson <lp15@cam.ac.uk>
parents:
72168
diff
changeset
|
169 |
using wf_irrefl [OF assms] by (auto simp add: irrefl_def) |
7fa9605b226c
Another go with lex: now lexordp back in class ord
paulson <lp15@cam.ac.uk>
parents:
72168
diff
changeset
|
170 |
|
74971
16eaa56f69f7
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
desharna
parents:
74868
diff
changeset
|
171 |
lemma wfP_imp_irreflp: "wfP r \<Longrightarrow> irreflp r" |
76588
82a36e3d1b55
rewrite proofs using to_pred attribute on existing lemmas
desharna
parents:
76559
diff
changeset
|
172 |
by (rule wf_imp_irrefl[to_pred]) |
74971
16eaa56f69f7
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
desharna
parents:
74868
diff
changeset
|
173 |
|
27823 | 174 |
lemma wf_wellorderI: |
175 |
assumes wf: "wf {(x::'a::ord, y). x < y}" |
|
63572 | 176 |
and lin: "OFCLASS('a::ord, linorder_class)" |
27823 | 177 |
shows "OFCLASS('a::ord, wellorder_class)" |
71410 | 178 |
apply (rule wellorder_class.intro [OF lin]) |
179 |
apply (simp add: wellorder_class.intro class.wellorder_axioms.intro wf_induct_rule [OF wf]) |
|
63108 | 180 |
done |
27823 | 181 |
|
63108 | 182 |
lemma (in wellorder) wf: "wf {(x, y). x < y}" |
183 |
unfolding wf_def by (blast intro: less_induct) |
|
27823 | 184 |
|
74868
2741ef11ccf6
added wfP_less to wellorder and wfP_less_multiset
desharna
parents:
72184
diff
changeset
|
185 |
lemma (in wellorder) wfP_less[simp]: "wfP (<)" |
2741ef11ccf6
added wfP_less to wellorder and wfP_less_multiset
desharna
parents:
72184
diff
changeset
|
186 |
by (simp add: wf wfP_def) |
2741ef11ccf6
added wfP_less to wellorder and wfP_less_multiset
desharna
parents:
72184
diff
changeset
|
187 |
|
79963 | 188 |
lemma (in wellorder) wfp_on_less[simp]: "wfp_on A (<)" |
189 |
unfolding wfp_on_def |
|
190 |
proof (intro allI impI ballI) |
|
191 |
fix P x |
|
192 |
assume hyps: "\<forall>x\<in>A. (\<forall>y\<in>A. y < x \<longrightarrow> P y) \<longrightarrow> P x" |
|
193 |
show "x \<in> A \<Longrightarrow> P x" |
|
194 |
proof (induction x rule: less_induct) |
|
195 |
case (less x) |
|
196 |
show ?case |
|
197 |
proof (rule hyps[rule_format]) |
|
198 |
show "x \<in> A" |
|
199 |
using \<open>x \<in> A\<close> . |
|
200 |
next |
|
201 |
show "\<And>y. y \<in> A \<Longrightarrow> y < x \<Longrightarrow> P y" |
|
202 |
using less.IH . |
|
203 |
qed |
|
204 |
qed |
|
205 |
qed |
|
206 |
||
27823 | 207 |
|
60758 | 208 |
subsection \<open>Basic Results\<close> |
26976 | 209 |
|
60758 | 210 |
text \<open>Point-free characterization of well-foundedness\<close> |
33216 | 211 |
|
79919
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
212 |
lemma wf_onE_pf: |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
213 |
assumes wf: "wf_on A r" and "B \<subseteq> A" and "B \<subseteq> r `` B" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
214 |
shows "B = {}" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
215 |
proof - |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
216 |
have "x \<notin> B" if "x \<in> A" for x |
79996
4f803ae64781
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
desharna
parents:
79971
diff
changeset
|
217 |
using wf |
79919
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
218 |
proof (induction x rule: wf_on_induct) |
79996
4f803ae64781
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
desharna
parents:
79971
diff
changeset
|
219 |
case in_set |
4f803ae64781
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
desharna
parents:
79971
diff
changeset
|
220 |
show ?case |
4f803ae64781
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
desharna
parents:
79971
diff
changeset
|
221 |
using that . |
4f803ae64781
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
desharna
parents:
79971
diff
changeset
|
222 |
next |
79919
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
223 |
case (less x) |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
224 |
have "x \<notin> r `` B" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
225 |
using less.IH \<open>B \<subseteq> A\<close> by blast |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
226 |
thus ?case |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
227 |
using \<open>B \<subseteq> r `` B\<close> by blast |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
228 |
qed |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
229 |
with \<open>B \<subseteq> A\<close> show ?thesis |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
230 |
by blast |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
231 |
qed |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
232 |
|
79920 | 233 |
lemma wfE_pf: "wf R \<Longrightarrow> A \<subseteq> R `` A \<Longrightarrow> A = {}" |
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
234 |
using wf_onE_pf[of UNIV, simplified] . |
33216 | 235 |
|
79919
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
236 |
lemma wf_onI_pf: |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
237 |
assumes "\<And>B. B \<subseteq> A \<Longrightarrow> B \<subseteq> R `` B \<Longrightarrow> B = {}" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
238 |
shows "wf_on A R" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
239 |
unfolding wf_on_def |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
240 |
proof (intro allI impI ballI) |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
241 |
fix P :: "'a \<Rightarrow> bool" and x :: 'a |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
242 |
let ?B = "{x \<in> A. \<not> P x}" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
243 |
assume "\<forall>x\<in>A. (\<forall>y\<in>A. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
244 |
hence "?B \<subseteq> R `` ?B" by blast |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
245 |
hence "{x \<in> A. \<not> P x} = {}" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
246 |
using assms(1)[of ?B] by simp |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
247 |
moreover assume "x \<in> A" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
248 |
ultimately show "P x" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
249 |
by simp |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
250 |
qed |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
251 |
|
79920 | 252 |
lemma wfI_pf: "(\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}) \<Longrightarrow> wf R" |
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
253 |
using wf_onI_pf[of UNIV, simplified] . |
33216 | 254 |
|
63108 | 255 |
|
256 |
subsubsection \<open>Minimal-element characterization of well-foundedness\<close> |
|
33216 | 257 |
|
79919
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
258 |
lemma wf_on_iff_ex_minimal: "wf_on A R \<longleftrightarrow> (\<forall>B \<subseteq> A. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> B))" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
259 |
proof (intro iffI allI impI) |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
260 |
fix B |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
261 |
assume "wf_on A R" and "B \<subseteq> A" and "B \<noteq> {}" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
262 |
show "\<exists>z \<in> B. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> B" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
263 |
using wf_onE_pf[OF \<open>wf_on A R\<close> \<open>B \<subseteq> A\<close>] \<open>B \<noteq> {}\<close> by blast |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
264 |
next |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
265 |
assume ex_min: "\<forall>B\<subseteq>A. B \<noteq> {} \<longrightarrow> (\<exists>z\<in>B. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> B)" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
266 |
show "wf_on A R " |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
267 |
proof (rule wf_onI_pf) |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
268 |
fix B |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
269 |
assume "B \<subseteq> A" and "B \<subseteq> R `` B" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
270 |
have False if "B \<noteq> {}" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
271 |
using ex_min[rule_format, OF \<open>B \<subseteq> A\<close> \<open>B \<noteq> {}\<close>] |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
272 |
using \<open>B \<subseteq> R `` B\<close> by blast |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
273 |
thus "B = {}" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
274 |
by blast |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
275 |
qed |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
276 |
qed |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
277 |
|
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
278 |
lemma wf_iff_ex_minimal: "wf R \<longleftrightarrow> (\<forall>B. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> B))" |
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
279 |
using wf_on_iff_ex_minimal[of UNIV, simplified] . |
79919
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
280 |
|
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
281 |
lemma wfp_on_iff_ex_minimal: "wfp_on A R \<longleftrightarrow> (\<forall>B \<subseteq> A. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B))" |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
282 |
using wf_on_iff_ex_minimal[of A, to_pred] by simp |
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
283 |
|
80019
991557e01814
renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal
desharna
parents:
79999
diff
changeset
|
284 |
lemma wfp_iff_ex_minimal: "wfp R \<longleftrightarrow> (\<forall>B. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B))" |
79965
233d70cad0cf
redefined wfP as an abbreviation for "wfp_on UNIV"
desharna
parents:
79963
diff
changeset
|
285 |
using wfp_on_iff_ex_minimal[of UNIV, simplified] . |
79919
65e0682cca63
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
desharna
parents:
79917
diff
changeset
|
286 |
|
33216 | 287 |
lemma wfE_min: |
288 |
assumes wf: "wf R" and Q: "x \<in> Q" |
|
289 |
obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q" |
|
290 |
using Q wfE_pf[OF wf, of Q] by blast |
|
291 |
||
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
292 |
lemma wfE_min': |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
293 |
"wf R \<Longrightarrow> Q \<noteq> {} \<Longrightarrow> (\<And>z. z \<in> Q \<Longrightarrow> (\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q) \<Longrightarrow> thesis) \<Longrightarrow> thesis" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
294 |
using wfE_min[of R _ Q] by blast |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
295 |
|
33216 | 296 |
lemma wfI_min: |
297 |
assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q" |
|
298 |
shows "wf R" |
|
299 |
proof (rule wfI_pf) |
|
63108 | 300 |
fix A |
301 |
assume b: "A \<subseteq> R `` A" |
|
302 |
have False if "x \<in> A" for x |
|
303 |
using a[OF that] b by blast |
|
304 |
then show "A = {}" by blast |
|
33216 | 305 |
qed |
306 |
||
63108 | 307 |
lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))" |
79920 | 308 |
unfolding wf_iff_ex_minimal by blast |
33216 | 309 |
|
310 |
lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] |
|
311 |
||
63108 | 312 |
|
79922
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
313 |
subsubsection \<open>Antimonotonicity\<close> |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
314 |
|
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
315 |
lemma wf_on_antimono_strong: |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
316 |
assumes "wf_on B r" and "A \<subseteq> B" and "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (x, y) \<in> r)" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
317 |
shows "wf_on A q" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
318 |
unfolding wf_on_iff_ex_minimal |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
319 |
proof (intro allI impI) |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
320 |
fix AA assume "AA \<subseteq> A" and "AA \<noteq> {}" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
321 |
hence "\<exists>z\<in>AA. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> AA" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
322 |
using \<open>wf_on B r\<close> \<open>A \<subseteq> B\<close> |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
323 |
by (simp add: wf_on_iff_ex_minimal) |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
324 |
then show "\<exists>z\<in>AA. \<forall>y. (y, z) \<in> q \<longrightarrow> y \<notin> AA" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
325 |
using \<open>AA \<subseteq> A\<close> assms(3) by blast |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
326 |
qed |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
327 |
|
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
328 |
lemma wfp_on_antimono_strong: |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
329 |
"wfp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> R x y) \<Longrightarrow> wfp_on A Q" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
330 |
using wf_on_antimono_strong[of B _ A, to_pred] . |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
331 |
|
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
332 |
lemma wf_on_antimono: "A \<subseteq> B \<Longrightarrow> q \<subseteq> r \<Longrightarrow> wf_on B r \<le> wf_on A q" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
333 |
using wf_on_antimono_strong[of B r A q] by auto |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
334 |
|
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
335 |
lemma wfp_on_antimono: "A \<subseteq> B \<Longrightarrow> Q \<le> R \<Longrightarrow> wfp_on B R \<le> wfp_on A Q" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
336 |
using wfp_on_antimono_strong[of B R A Q] by auto |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
337 |
|
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
338 |
lemma wf_on_subset: "wf_on B r \<Longrightarrow> A \<subseteq> B \<Longrightarrow> wf_on A r" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
339 |
using wf_on_antimono_strong . |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
340 |
|
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
341 |
lemma wfp_on_subset: "wfp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> wfp_on A R" |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
342 |
using wfp_on_antimono_strong . |
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
343 |
|
caa9dbffd712
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
desharna
parents:
79920
diff
changeset
|
344 |
|
63108 | 345 |
subsubsection \<open>Well-foundedness of transitive closure\<close> |
33216 | 346 |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
347 |
lemma wf_trancl: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
348 |
assumes "wf r" |
63108 | 349 |
shows "wf (r\<^sup>+)" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
350 |
proof - |
63108 | 351 |
have "P x" if induct_step: "\<And>x. (\<And>y. (y, x) \<in> r\<^sup>+ \<Longrightarrow> P y) \<Longrightarrow> P x" for P x |
352 |
proof (rule induct_step) |
|
353 |
show "P y" if "(y, x) \<in> r\<^sup>+" for y |
|
354 |
using \<open>wf r\<close> and that |
|
355 |
proof (induct x arbitrary: y) |
|
356 |
case (less x) |
|
357 |
note hyp = \<open>\<And>x' y'. (x', x) \<in> r \<Longrightarrow> (y', x') \<in> r\<^sup>+ \<Longrightarrow> P y'\<close> |
|
358 |
from \<open>(y, x) \<in> r\<^sup>+\<close> show "P y" |
|
359 |
proof cases |
|
360 |
case base |
|
361 |
show "P y" |
|
362 |
proof (rule induct_step) |
|
363 |
fix y' |
|
364 |
assume "(y', y) \<in> r\<^sup>+" |
|
365 |
with \<open>(y, x) \<in> r\<close> show "P y'" |
|
366 |
by (rule hyp [of y y']) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32704
diff
changeset
|
367 |
qed |
63108 | 368 |
next |
369 |
case step |
|
370 |
then obtain x' where "(x', x) \<in> r" and "(y, x') \<in> r\<^sup>+" |
|
371 |
by simp |
|
372 |
then show "P y" by (rule hyp [of x' y]) |
|
26748
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 |
63108 | 375 |
qed |
376 |
then show ?thesis unfolding wf_def by blast |
|
26748
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 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
379 |
lemmas wfP_trancl = wf_trancl [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
380 |
|
63108 | 381 |
lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
382 |
apply (subst trancl_converse [symmetric]) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
383 |
apply (erule wf_trancl) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
384 |
done |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
385 |
|
60758 | 386 |
text \<open>Well-foundedness of subsets\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
387 |
|
63108 | 388 |
lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p" |
63612 | 389 |
by (simp add: wf_eq_minimal) fast |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
390 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
391 |
lemmas wfP_subset = wf_subset [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
392 |
|
60758 | 393 |
text \<open>Well-foundedness of the empty relation\<close> |
33216 | 394 |
|
395 |
lemma wf_empty [iff]: "wf {}" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
396 |
by (simp add: wf_def) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
397 |
|
63612 | 398 |
lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)" |
32205 | 399 |
proof - |
63612 | 400 |
have "wfP bot" |
66952 | 401 |
by (fact wf_empty[to_pred bot_empty_eq2]) |
63612 | 402 |
then show ?thesis |
403 |
by (simp add: bot_fun_def) |
|
32205 | 404 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
405 |
|
63572 | 406 |
lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')" |
407 |
by (erule wf_subset) (rule Int_lower1) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
408 |
|
63572 | 409 |
lemma wf_Int2: "wf r \<Longrightarrow> wf (r' \<inter> r)" |
410 |
by (erule wf_subset) (rule Int_lower2) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
411 |
|
63572 | 412 |
text \<open>Exponentiation.\<close> |
33216 | 413 |
lemma wf_exp: |
414 |
assumes "wf (R ^^ n)" |
|
415 |
shows "wf R" |
|
416 |
proof (rule wfI_pf) |
|
417 |
fix A assume "A \<subseteq> R `` A" |
|
63612 | 418 |
then have "A \<subseteq> (R ^^ n) `` A" |
419 |
by (induct n) force+ |
|
420 |
with \<open>wf (R ^^ n)\<close> show "A = {}" |
|
421 |
by (rule wfE_pf) |
|
33216 | 422 |
qed |
423 |
||
63572 | 424 |
text \<open>Well-foundedness of \<open>insert\<close>.\<close> |
68646 | 425 |
lemma wf_insert [iff]: "wf (insert (y,x) r) \<longleftrightarrow> wf r \<and> (x,y) \<notin> r\<^sup>*" (is "?lhs = ?rhs") |
426 |
proof |
|
427 |
assume ?lhs then show ?rhs |
|
428 |
by (blast elim: wf_trancl [THEN wf_irrefl] |
|
429 |
intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN subsetD]) |
|
430 |
next |
|
71410 | 431 |
assume R: ?rhs |
68646 | 432 |
then have R': "Q \<noteq> {} \<Longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)" for Q |
433 |
by (auto simp: wf_eq_minimal) |
|
434 |
show ?lhs |
|
435 |
unfolding wf_eq_minimal |
|
436 |
proof clarify |
|
437 |
fix Q :: "'a set" and q |
|
438 |
assume "q \<in> Q" |
|
439 |
then obtain a where "a \<in> Q" and a: "\<And>y. (y, a) \<in> r \<Longrightarrow> y \<notin> Q" |
|
440 |
using R by (auto simp: wf_eq_minimal) |
|
441 |
show "\<exists>z\<in>Q. \<forall>y'. (y', z) \<in> insert (y, x) r \<longrightarrow> y' \<notin> Q" |
|
442 |
proof (cases "a=x") |
|
443 |
case True |
|
444 |
show ?thesis |
|
445 |
proof (cases "y \<in> Q") |
|
446 |
case True |
|
447 |
then obtain z where "z \<in> Q" "(z, y) \<in> r\<^sup>*" |
|
448 |
"\<And>z'. (z', z) \<in> r \<longrightarrow> z' \<in> Q \<longrightarrow> (z', y) \<notin> r\<^sup>*" |
|
449 |
using R' [of "{z \<in> Q. (z,y) \<in> r\<^sup>*}"] by auto |
|
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
450 |
then have "\<forall>y'. (y', z) \<in> insert (y, x) r \<longrightarrow> y' \<notin> Q" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
451 |
using R by(blast intro: rtrancl_trans)+ |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
452 |
then show ?thesis |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
453 |
by (rule bexI) fact |
68646 | 454 |
next |
455 |
case False |
|
456 |
then show ?thesis |
|
457 |
using a \<open>a \<in> Q\<close> by blast |
|
458 |
qed |
|
459 |
next |
|
460 |
case False |
|
461 |
with a \<open>a \<in> Q\<close> show ?thesis |
|
462 |
by blast |
|
463 |
qed |
|
464 |
qed |
|
465 |
qed |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
466 |
|
63108 | 467 |
|
468 |
subsubsection \<open>Well-foundedness of image\<close> |
|
33216 | 469 |
|
68259
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
470 |
lemma wf_map_prod_image_Dom_Ran: |
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
471 |
fixes r:: "('a \<times> 'a) set" |
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
472 |
and f:: "'a \<Rightarrow> 'b" |
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
473 |
assumes wf_r: "wf r" |
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
474 |
and inj: "\<And> a a'. a \<in> Domain r \<Longrightarrow> a' \<in> Range r \<Longrightarrow> f a = f a' \<Longrightarrow> a = a'" |
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
475 |
shows "wf (map_prod f f ` r)" |
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
476 |
proof (unfold wf_eq_minimal, clarify) |
68262 | 477 |
fix B :: "'b set" and b::"'b" |
478 |
assume "b \<in> B" |
|
479 |
define A where "A = f -` B \<inter> Domain r" |
|
480 |
show "\<exists>z\<in>B. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> B" |
|
481 |
proof (cases "A = {}") |
|
68259
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
482 |
case False |
68262 | 483 |
then obtain a0 where "a0 \<in> A" and "\<forall>a. (a, a0) \<in> r \<longrightarrow> a \<notin> A" |
68259
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
484 |
using wfE_min[OF wf_r] by auto |
71410 | 485 |
thus ?thesis |
68262 | 486 |
using inj unfolding A_def |
487 |
by (intro bexI[of _ "f a0"]) auto |
|
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
488 |
qed (use \<open>b \<in> B\<close> in \<open>unfold A_def, auto\<close>) |
68259
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
489 |
qed |
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
490 |
|
63108 | 491 |
lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)" |
68259
80df7c90e315
By Andrei Popescu based on an initial version by Kasper F. Brandt
nipkow
parents:
67399
diff
changeset
|
492 |
by(rule wf_map_prod_image_Dom_Ran) (auto dest: inj_onD) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
493 |
|
80046
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
494 |
lemma wfp_on_image: "wfp_on (f ` A) R \<longleftrightarrow> wfp_on A (\<lambda>a b. R (f a) (f b))" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
495 |
proof (rule iffI) |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
496 |
assume hyp: "wfp_on (f ` A) R" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
497 |
show "wfp_on A (\<lambda>a b. R (f a) (f b))" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
498 |
unfolding wfp_on_iff_ex_minimal |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
499 |
proof (intro allI impI) |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
500 |
fix B |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
501 |
assume "B \<subseteq> A" and "B \<noteq> {}" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
502 |
hence "f ` B \<subseteq> f ` A" and "f ` B \<noteq> {}" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
503 |
unfolding atomize_conj image_is_empty |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
504 |
using image_mono by iprover |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
505 |
hence "\<exists>z\<in>f ` B. \<forall>y. R y z \<longrightarrow> y \<notin> f ` B" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
506 |
using hyp[unfolded wfp_on_iff_ex_minimal, rule_format] by iprover |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
507 |
then obtain fz where "fz \<in> f ` B" and fz_max: "\<forall>y. R y fz \<longrightarrow> y \<notin> f ` B" .. |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
508 |
|
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
509 |
obtain z where "z \<in> B" and "fz = f z" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
510 |
using \<open>fz \<in> f ` B\<close> unfolding image_iff .. |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
511 |
|
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
512 |
show "\<exists>z\<in>B. \<forall>y. R (f y) (f z) \<longrightarrow> y \<notin> B" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
513 |
proof (intro bexI allI impI) |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
514 |
show "z \<in> B" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
515 |
using \<open>z \<in> B\<close> . |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
516 |
next |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
517 |
fix y assume "R (f y) (f z)" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
518 |
hence "f y \<notin> f ` B" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
519 |
using fz_max \<open>fz = f z\<close> by iprover |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
520 |
thus "y \<notin> B" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
521 |
by (rule contrapos_nn) (rule imageI) |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
522 |
qed |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
523 |
qed |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
524 |
next |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
525 |
assume hyp: "wfp_on A (\<lambda>a b. R (f a) (f b))" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
526 |
show "wfp_on (f ` A) R" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
527 |
unfolding wfp_on_iff_ex_minimal |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
528 |
proof (intro allI impI) |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
529 |
fix fA |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
530 |
assume "fA \<subseteq> f ` A" and "fA \<noteq> {}" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
531 |
then obtain A' where "A' \<subseteq> A" and "A' \<noteq> {}" and "fA = f ` A'" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
532 |
by (auto simp only: subset_image_iff) |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
533 |
|
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
534 |
obtain z where "z \<in> A'" and z_max: "\<forall>y. R (f y) (f z) \<longrightarrow> y \<notin> A'" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
535 |
using hyp[unfolded wfp_on_iff_ex_minimal, rule_format, OF \<open>A' \<subseteq> A\<close> \<open>A' \<noteq> {}\<close>] by blast |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
536 |
|
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
537 |
show "\<exists>z\<in>fA. \<forall>y. R y z \<longrightarrow> y \<notin> fA" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
538 |
proof (intro bexI allI impI) |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
539 |
show "f z \<in> fA" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
540 |
unfolding \<open>fA = f ` A'\<close> |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
541 |
using imageI[OF \<open>z \<in> A'\<close>] . |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
542 |
next |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
543 |
show "\<And>y. R y (f z) \<Longrightarrow> y \<notin> fA" |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
544 |
unfolding \<open>fA = f ` A'\<close> |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
545 |
using z_max by auto |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
546 |
qed |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
547 |
qed |
38803a6b3357
added lemma wfp_on_image and author name to theory
desharna
parents:
80019
diff
changeset
|
548 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
549 |
|
60758 | 550 |
subsection \<open>Well-Foundedness Results for Unions\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
551 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
552 |
lemma wf_union_compatible: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
553 |
assumes "wf R" "wf S" |
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
32205
diff
changeset
|
554 |
assumes "R O S \<subseteq> R" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
555 |
shows "wf (R \<union> S)" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
556 |
proof (rule wfI_min) |
63108 | 557 |
fix x :: 'a and Q |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
558 |
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
|
559 |
assume "x \<in> Q" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
560 |
obtain a where "a \<in> ?Q'" |
60758 | 561 |
by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast |
63108 | 562 |
with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" |
563 |
by (erule wfE_min) |
|
63572 | 564 |
have "y \<notin> Q" if "(y, z) \<in> S" for y |
565 |
proof |
|
566 |
from that have "y \<notin> ?Q'" by (rule zmin) |
|
567 |
assume "y \<in> Q" |
|
568 |
with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto |
|
569 |
from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI) |
|
570 |
with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" .. |
|
571 |
with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast |
|
572 |
with \<open>w \<in> Q\<close> show False by contradiction |
|
573 |
qed |
|
60758 | 574 |
with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
575 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
576 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
577 |
|
63572 | 578 |
text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
579 |
|
63108 | 580 |
lemma wf_UN: |
68646 | 581 |
assumes r: "\<And>i. i \<in> I \<Longrightarrow> wf (r i)" |
582 |
and disj: "\<And>i j. \<lbrakk>i \<in> I; j \<in> I; r i \<noteq> r j\<rbrakk> \<Longrightarrow> Domain (r i) \<inter> Range (r j) = {}" |
|
63108 | 583 |
shows "wf (\<Union>i\<in>I. r i)" |
68646 | 584 |
unfolding wf_eq_minimal |
585 |
proof clarify |
|
586 |
fix A and a :: "'b" |
|
587 |
assume "a \<in> A" |
|
69275 | 588 |
show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> \<Union>(r ` I) \<longrightarrow> y \<notin> A" |
68646 | 589 |
proof (cases "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i") |
590 |
case True |
|
591 |
then obtain i b c where ibc: "i \<in> I" "b \<in> A" "c \<in> A" "(c,b) \<in> r i" |
|
592 |
by blast |
|
593 |
have ri: "\<And>Q. Q \<noteq> {} \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r i \<longrightarrow> y \<notin> Q" |
|
594 |
using r [OF \<open>i \<in> I\<close>] unfolding wf_eq_minimal by auto |
|
595 |
show ?thesis |
|
71410 | 596 |
using ri [of "{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }"] ibc disj |
68646 | 597 |
by blast |
598 |
next |
|
599 |
case False |
|
600 |
with \<open>a \<in> A\<close> show ?thesis |
|
601 |
by blast |
|
602 |
qed |
|
603 |
qed |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
604 |
|
32263 | 605 |
lemma wfP_SUP: |
64632 | 606 |
"\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow> |
69275 | 607 |
wfP (\<Squnion>(range r))" |
63572 | 608 |
by (rule wf_UN[to_pred]) simp_all |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
609 |
|
63108 | 610 |
lemma wf_Union: |
611 |
assumes "\<forall>r\<in>R. wf r" |
|
612 |
and "\<forall>r\<in>R. \<forall>s\<in>R. r \<noteq> s \<longrightarrow> Domain r \<inter> Range s = {}" |
|
613 |
shows "wf (\<Union>R)" |
|
614 |
using assms wf_UN[of R "\<lambda>i. i"] by simp |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
615 |
|
63109 | 616 |
text \<open> |
617 |
Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction. |
|
618 |
\<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>. |
|
619 |
Pick an \<open>R\<close>-min element \<open>z\<close> of the (nonempty) set \<open>{a\<in>A | \<exists>b\<in>A. a \<midarrow>R\<rightarrow> b}\<close>. |
|
620 |
By definition, there is \<open>z' \<in> A\<close> s.t. \<open>z \<midarrow>R\<rightarrow> z'\<close>. Because \<open>z\<close> is \<open>R\<close>-min in the |
|
621 |
subset, \<open>z'\<close> must be \<open>R\<close>-min in \<open>A\<close>. Because \<open>z'\<close> has an \<open>R\<close>-predecessor, it cannot |
|
622 |
have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well. |
|
623 |
\<^enum> There is no such step. |
|
624 |
Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min |
|
625 |
element of \<open>A\<close> as well. |
|
626 |
\<close> |
|
63108 | 627 |
lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)" |
628 |
using wf_union_compatible[of s r] |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
629 |
by (auto simp: Un_ac) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
630 |
|
63108 | 631 |
lemma wf_union_merge: "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" |
632 |
(is "wf ?A = wf ?B") |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
633 |
proof |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
634 |
assume "wf ?A" |
63108 | 635 |
with wf_trancl have wfT: "wf (?A\<^sup>+)" . |
636 |
moreover have "?B \<subseteq> ?A\<^sup>+" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
637 |
by (subst trancl_unfold, subst trancl_unfold) blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
638 |
ultimately show "wf ?B" by (rule wf_subset) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
639 |
next |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
640 |
assume "wf ?B" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
641 |
show "wf ?A" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
642 |
proof (rule wfI_min) |
63108 | 643 |
fix Q :: "'a set" and x |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
644 |
assume "x \<in> Q" |
63109 | 645 |
with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
646 |
by (erule wfE_min) |
63109 | 647 |
then have 1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" |
648 |
and 2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" |
|
649 |
and 3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
650 |
by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
651 |
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
|
652 |
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
|
653 |
case True |
63109 | 654 |
with \<open>z \<in> Q\<close> 3 show ?thesis by blast |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
655 |
next |
63108 | 656 |
case False |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
657 |
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
|
658 |
have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
659 |
proof (intro allI impI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
660 |
fix y assume "(y, z') \<in> ?A" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
661 |
then show "y \<notin> Q" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
662 |
proof |
63108 | 663 |
assume "(y, z') \<in> R" |
60758 | 664 |
then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> .. |
63109 | 665 |
with 1 show "y \<notin> Q" . |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
666 |
next |
63108 | 667 |
assume "(y, z') \<in> S" |
60758 | 668 |
then have "(y, z) \<in> S O R" using \<open>(z', z) \<in> R\<close> .. |
63109 | 669 |
with 2 show "y \<notin> Q" . |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
670 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
671 |
qed |
60758 | 672 |
with \<open>z' \<in> Q\<close> show ?thesis .. |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
673 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
674 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
675 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
676 |
|
63612 | 677 |
lemma wf_comp_self: "wf R \<longleftrightarrow> wf (R O R)" \<comment> \<open>special case\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
678 |
by (rule wf_union_merge [where S = "{}", simplified]) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
679 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
680 |
|
60758 | 681 |
subsection \<open>Well-Foundedness of Composition\<close> |
60148 | 682 |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
683 |
text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close> |
60148 | 684 |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
685 |
lemma qc_wf_relto_iff: |
61799 | 686 |
assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close> |
63109 | 687 |
shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" |
63612 | 688 |
(is "wf ?S \<longleftrightarrow> _") |
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
689 |
proof |
63109 | 690 |
show "wf R" if "wf ?S" |
691 |
proof - |
|
692 |
have "R \<subseteq> ?S" by auto |
|
63612 | 693 |
with wf_subset [of ?S] that show "wf R" |
694 |
by auto |
|
63109 | 695 |
qed |
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
696 |
next |
63109 | 697 |
show "wf ?S" if "wf R" |
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
698 |
proof (rule wfI_pf) |
63109 | 699 |
fix A |
700 |
assume A: "A \<subseteq> ?S `` A" |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
701 |
let ?X = "(R \<union> S)\<^sup>* `` A" |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
702 |
have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" |
63109 | 703 |
proof - |
704 |
have "(x, z) \<in> (R \<union> S)\<^sup>* O R" if "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R" for x y z |
|
705 |
using that |
|
706 |
proof (induct y z) |
|
707 |
case rtrancl_refl |
|
708 |
then show ?case by auto |
|
709 |
next |
|
710 |
case (rtrancl_into_rtrancl a b c) |
|
711 |
then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" |
|
712 |
using assms by blast |
|
713 |
then show ?case by simp |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
714 |
qed |
63109 | 715 |
then show ?thesis by auto |
716 |
qed |
|
717 |
then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" |
|
718 |
using rtrancl_Un_subset by blast |
|
719 |
then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" |
|
720 |
by (simp add: relcomp_mono rtrancl_mono) |
|
721 |
also have "\<dots> = (R \<union> S)\<^sup>* O R" |
|
722 |
by (simp add: O_assoc[symmetric]) |
|
723 |
finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*" |
|
724 |
by (simp add: O_assoc[symmetric] relcomp_mono) |
|
725 |
also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" |
|
726 |
using * by (simp add: relcomp_mono) |
|
727 |
finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" |
|
728 |
by (simp add: O_assoc[symmetric]) |
|
729 |
then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" |
|
730 |
by (simp add: Image_mono) |
|
731 |
moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" |
|
732 |
using A by (auto simp: relcomp_Image) |
|
733 |
ultimately have "?X \<subseteq> R `` ?X" |
|
734 |
by (auto simp: relcomp_Image) |
|
735 |
then have "?X = {}" |
|
736 |
using \<open>wf R\<close> by (simp add: wfE_pf) |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
737 |
moreover have "A \<subseteq> ?X" by auto |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
738 |
ultimately show "A = {}" by simp |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
739 |
qed |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
740 |
qed |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
741 |
|
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
742 |
corollary wf_relcomp_compatible: |
60148 | 743 |
assumes "wf R" and "R O S \<subseteq> S O R" |
744 |
shows "wf (S O R)" |
|
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
745 |
proof - |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
746 |
have "R O S \<subseteq> (R \<union> S)\<^sup>* O R" |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
747 |
using assms by blast |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
748 |
then have "wf (S\<^sup>* O R O S\<^sup>*)" |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
749 |
by (simp add: assms qc_wf_relto_iff) |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
750 |
then show ?thesis |
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
751 |
by (rule Wellfounded.wf_subset) blast |
60148 | 752 |
qed |
753 |
||
754 |
||
60758 | 755 |
subsection \<open>Acyclic relations\<close> |
33217 | 756 |
|
63108 | 757 |
lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r" |
63572 | 758 |
by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl]) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
759 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
760 |
lemmas wfP_acyclicP = wf_acyclic [to_pred] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
761 |
|
63108 | 762 |
|
763 |
subsubsection \<open>Wellfoundedness of finite acyclic relations\<close> |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
764 |
|
68646 | 765 |
lemma finite_acyclic_wf: |
766 |
assumes "finite r" "acyclic r" shows "wf r" |
|
767 |
using assms |
|
768 |
proof (induction r rule: finite_induct) |
|
769 |
case (insert x r) |
|
770 |
then show ?case |
|
771 |
by (cases x) simp |
|
772 |
qed simp |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
773 |
|
63108 | 774 |
lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)" |
63572 | 775 |
apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) |
776 |
apply (erule acyclic_converse [THEN iffD2]) |
|
777 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
778 |
|
63088
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
779 |
text \<open> |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
780 |
Observe that the converse of an irreflexive, transitive, |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
781 |
and finite relation is again well-founded. Thus, we may |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
782 |
employ it for well-founded induction. |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
783 |
\<close> |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
784 |
lemma wf_converse: |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
785 |
assumes "irrefl r" and "trans r" and "finite r" |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
786 |
shows "wf (r\<inverse>)" |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
787 |
proof - |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
788 |
have "acyclic r" |
63572 | 789 |
using \<open>irrefl r\<close> and \<open>trans r\<close> |
790 |
by (simp add: irrefl_def acyclic_irrefl) |
|
791 |
with \<open>finite r\<close> show ?thesis |
|
792 |
by (rule finite_acyclic_wf_converse) |
|
63088
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
793 |
qed |
f2177f5d2aed
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
haftmann
parents:
61952
diff
changeset
|
794 |
|
63108 | 795 |
lemma wf_iff_acyclic_if_finite: "finite r \<Longrightarrow> wf r = acyclic r" |
63572 | 796 |
by (blast intro: finite_acyclic_wf wf_acyclic) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
797 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
798 |
|
69593 | 799 |
subsection \<open>\<^typ>\<open>nat\<close> is well-founded\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
800 |
|
67399 | 801 |
lemma less_nat_rel: "(<) = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
802 |
proof (rule ext, rule ext, rule iffI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
803 |
fix n m :: nat |
63108 | 804 |
show "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n" |
805 |
using that |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
806 |
proof (induct n) |
63108 | 807 |
case 0 |
808 |
then show ?case by auto |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
809 |
next |
63108 | 810 |
case (Suc n) |
811 |
then show ?case |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
812 |
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
|
813 |
qed |
63108 | 814 |
show "m < n" if "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" |
815 |
using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
816 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
817 |
|
63108 | 818 |
definition pred_nat :: "(nat \<times> nat) set" |
819 |
where "pred_nat = {(m, n). n = Suc m}" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
820 |
|
63108 | 821 |
definition less_than :: "(nat \<times> nat) set" |
822 |
where "less_than = pred_nat\<^sup>+" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
823 |
|
63108 | 824 |
lemma less_eq: "(m, n) \<in> pred_nat\<^sup>+ \<longleftrightarrow> m < n" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
825 |
unfolding less_nat_rel pred_nat_def trancl_def by simp |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
826 |
|
63108 | 827 |
lemma pred_nat_trancl_eq_le: "(m, n) \<in> pred_nat\<^sup>* \<longleftrightarrow> m \<le> n" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
828 |
unfolding less_eq rtrancl_eq_or_trancl by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
829 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
830 |
lemma wf_pred_nat: "wf pred_nat" |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
831 |
unfolding wf_def |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
832 |
proof clarify |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
833 |
fix P x |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
834 |
assume "\<forall>x'. (\<forall>y. (y, x') \<in> pred_nat \<longrightarrow> P y) \<longrightarrow> P x'" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
835 |
then show "P x" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
836 |
unfolding pred_nat_def by (induction x) blast+ |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
837 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
838 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
839 |
lemma wf_less_than [iff]: "wf less_than" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
840 |
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
|
841 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
842 |
lemma trans_less_than [iff]: "trans less_than" |
35216 | 843 |
by (simp add: less_than_def) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
844 |
|
63108 | 845 |
lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
846 |
by (simp add: less_than_def less_eq) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
847 |
|
71827 | 848 |
lemma irrefl_less_than: "irrefl less_than" |
849 |
using irrefl_def by blast |
|
850 |
||
71935
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
851 |
lemma asym_less_than: "asym less_than" |
76682
e260dabc88e6
added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations
desharna
parents:
76588
diff
changeset
|
852 |
by (rule asymI) simp |
71935
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
853 |
|
71766
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
71544
diff
changeset
|
854 |
lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than" |
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
paulson <lp15@cam.ac.uk>
parents:
71544
diff
changeset
|
855 |
using total_on_def by force+ |
71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
856 |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
857 |
lemma wf_less: "wf {(x, y::nat). x < y}" |
60493
866f41a869e6
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
paulson <lp15@cam.ac.uk>
parents:
60148
diff
changeset
|
858 |
by (rule Wellfounded.wellorder_class.wf) |
26748
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 |
|
60758 | 861 |
subsection \<open>Accessible Part\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
862 |
|
60758 | 863 |
text \<open> |
63108 | 864 |
Inductive definition of the accessible part \<open>acc r\<close> of a |
77172 | 865 |
relation; see also \<^cite>\<open>"paulin-tlca"\<close>. |
60758 | 866 |
\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
867 |
|
63108 | 868 |
inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set" |
869 |
where accI: "(\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
870 |
|
63108 | 871 |
abbreviation termip :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
872 |
where "termip r \<equiv> accp (r\<inverse>\<inverse>)" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
873 |
|
63108 | 874 |
abbreviation termi :: "('a \<times> 'a) set \<Rightarrow> 'a set" |
875 |
where "termi r \<equiv> acc (r\<inverse>)" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
876 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
877 |
lemmas accpI = accp.accI |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
878 |
|
63108 | 879 |
lemma accp_eq_acc [code]: "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})" |
54295 | 880 |
by (simp add: acc_def) |
881 |
||
882 |
||
60758 | 883 |
text \<open>Induction rules\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
884 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
885 |
theorem accp_induct: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
886 |
assumes major: "accp r a" |
63108 | 887 |
assumes hyp: "\<And>x. accp r x \<Longrightarrow> \<forall>y. r y x \<longrightarrow> P y \<Longrightarrow> P x" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
888 |
shows "P a" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
889 |
apply (rule major [THEN accp.induct]) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
890 |
apply (rule hyp) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
891 |
apply (rule accp.accI) |
68646 | 892 |
apply auto |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
893 |
done |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
894 |
|
61337 | 895 |
lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp] |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
896 |
|
63108 | 897 |
theorem accp_downward: "accp r b \<Longrightarrow> r a b \<Longrightarrow> accp r a" |
63572 | 898 |
by (cases rule: accp.cases) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
899 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
900 |
lemma not_accp_down: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
901 |
assumes na: "\<not> accp R x" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
902 |
obtains z where "R z x" and "\<not> accp R z" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
903 |
proof - |
63572 | 904 |
assume a: "\<And>z. R z x \<Longrightarrow> \<not> accp R z \<Longrightarrow> thesis" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
905 |
show thesis |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
906 |
proof (cases "\<forall>z. R z x \<longrightarrow> accp R z") |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
907 |
case True |
63108 | 908 |
then have "\<And>z. R z x \<Longrightarrow> accp R z" by auto |
909 |
then have "accp R x" by (rule accp.accI) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
910 |
with na show thesis .. |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
911 |
next |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
912 |
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
|
913 |
by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
914 |
with a show thesis . |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
915 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
916 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
917 |
|
63108 | 918 |
lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r a \<longrightarrow> accp r b" |
63612 | 919 |
by (erule rtranclp_induct) (blast dest: accp_downward)+ |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
920 |
|
63108 | 921 |
theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b" |
63572 | 922 |
by (blast dest: accp_downwards_aux) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
923 |
|
63108 | 924 |
theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r" |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
925 |
proof (rule wfPUNIVI) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
926 |
fix P x |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
927 |
assume "\<forall>x. accp r x" "\<forall>x. (\<forall>y. r y x \<longrightarrow> P y) \<longrightarrow> P x" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
928 |
then show "P x" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
929 |
using accp_induct[where P = P] by blast |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
930 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
931 |
|
63108 | 932 |
theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
933 |
apply (erule wfP_induct_rule) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
934 |
apply (rule accp.accI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
935 |
apply blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
936 |
done |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
937 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
938 |
theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)" |
63572 | 939 |
by (blast intro: accp_wfPI dest: accp_wfPD) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
940 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
941 |
|
60758 | 942 |
text \<open>Smaller relations have bigger accessible parts:\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
943 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
944 |
lemma accp_subset: |
63572 | 945 |
assumes "R1 \<le> R2" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
946 |
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
|
947 |
proof (rule predicate1I) |
63572 | 948 |
fix x |
949 |
assume "accp R2 x" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
950 |
then show "accp R1 x" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
951 |
proof (induct x) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
952 |
fix x |
63572 | 953 |
assume "\<And>y. R2 y x \<Longrightarrow> accp R1 y" |
954 |
with assms show "accp R1 x" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
955 |
by (blast intro: accp.accI) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
956 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
957 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
958 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
959 |
|
60758 | 960 |
text \<open>This is a generalized induction theorem that works on |
961 |
subsets of the accessible part.\<close> |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
962 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
963 |
lemma accp_subset_induct: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
964 |
assumes subset: "D \<le> accp R" |
63572 | 965 |
and dcl: "\<And>x z. D x \<Longrightarrow> R z x \<Longrightarrow> D z" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
966 |
and "D x" |
63572 | 967 |
and istep: "\<And>x. D x \<Longrightarrow> (\<And>z. R z x \<Longrightarrow> P z) \<Longrightarrow> P x" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
968 |
shows "P x" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
969 |
proof - |
60758 | 970 |
from subset and \<open>D x\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
971 |
have "accp R x" .. |
60758 | 972 |
then show "P x" using \<open>D x\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
973 |
proof (induct x) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
974 |
fix x |
63572 | 975 |
assume "D x" and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
976 |
with dcl and istep show "P x" by blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
977 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
978 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
979 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
980 |
|
60758 | 981 |
text \<open>Set versions of the above theorems\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
982 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
983 |
lemmas acc_induct = accp_induct [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
984 |
lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
985 |
lemmas acc_downward = accp_downward [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
986 |
lemmas not_acc_down = not_accp_down [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
987 |
lemmas acc_downwards_aux = accp_downwards_aux [to_set] |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
988 |
lemmas acc_downwards = accp_downwards [to_set] |
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
989 |
lemmas acc_wfI = accp_wfPI [to_set] |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
990 |
lemmas acc_wfD = accp_wfPD [to_set] |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
991 |
lemmas wf_acc_iff = wfP_accp_iff [to_set] |
46177
adac34829e10
pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
berghofe
parents:
45970
diff
changeset
|
992 |
lemmas acc_subset = accp_subset [to_set] |
adac34829e10
pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
berghofe
parents:
45970
diff
changeset
|
993 |
lemmas acc_subset_induct = accp_subset_induct [to_set] |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
994 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
995 |
|
60758 | 996 |
subsection \<open>Tools for building wellfounded relations\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
997 |
|
60758 | 998 |
text \<open>Inverse Image\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
999 |
|
71544 | 1000 |
lemma wf_inv_image [simp,intro!]: |
1001 |
fixes f :: "'a \<Rightarrow> 'b" |
|
1002 |
assumes "wf r" |
|
1003 |
shows "wf (inv_image r f)" |
|
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1004 |
proof - |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1005 |
have "\<And>x P. x \<in> P \<Longrightarrow> \<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1006 |
proof - |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1007 |
fix P and x::'a |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1008 |
assume "x \<in> P" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1009 |
then obtain w where w: "w \<in> {w. \<exists>x::'a. x \<in> P \<and> f x = w}" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1010 |
by auto |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1011 |
have *: "\<And>Q u. u \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1012 |
using assms by (auto simp add: wf_eq_minimal) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1013 |
show "\<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P" |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1014 |
using * [OF w] by auto |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1015 |
qed |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1016 |
then show ?thesis |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1017 |
by (clarsimp simp: inv_image_def wf_eq_minimal) |
71544 | 1018 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1019 |
|
79999
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1020 |
lemma wfp_on_inv_imagep: |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1021 |
assumes wf: "wfp_on (f ` A) R" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1022 |
shows "wfp_on A (inv_imagep R f)" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1023 |
unfolding wfp_on_iff_ex_minimal |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1024 |
proof (intro allI impI) |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1025 |
fix B assume "B \<subseteq> A" and "B \<noteq> {}" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1026 |
hence "\<exists>z\<in>f ` B. \<forall>y. R y z \<longrightarrow> y \<notin> f ` B" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1027 |
using wf[unfolded wfp_on_iff_ex_minimal, rule_format, of "f ` B"] by blast |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1028 |
thus "\<exists>z\<in>B. \<forall>y. inv_imagep R f y z \<longrightarrow> y \<notin> B" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1029 |
unfolding inv_imagep_def |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1030 |
by auto |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1031 |
qed |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1032 |
|
76267
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1033 |
|
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1034 |
subsubsection \<open>Conversion to a known well-founded relation\<close> |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1035 |
|
79999
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1036 |
lemma wfp_on_if_convertible_to_wfp_on: |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1037 |
assumes |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1038 |
wf: "wfp_on (f ` A) Q" and |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1039 |
convertible: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q (f x) (f y))" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1040 |
shows "wfp_on A R" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1041 |
unfolding wfp_on_iff_ex_minimal |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1042 |
proof (intro allI impI) |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1043 |
fix B assume "B \<subseteq> A" and "B \<noteq> {}" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1044 |
moreover from wf have "wfp_on A (inv_imagep Q f)" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1045 |
by (rule wfp_on_inv_imagep) |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1046 |
ultimately obtain y where "y \<in> B" and "\<And>z. Q (f z) (f y) \<Longrightarrow> z \<notin> B" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1047 |
unfolding wfp_on_iff_ex_minimal in_inv_imagep |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1048 |
by blast |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1049 |
thus "\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1050 |
using \<open>B \<subseteq> A\<close> convertible by blast |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1051 |
qed |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1052 |
|
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1053 |
lemma wf_on_if_convertible_to_wf_on: "wf_on (f ` A) Q \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (f x, f y) \<in> Q) \<Longrightarrow> wf_on A R" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1054 |
using wfp_on_if_convertible_to_wfp_on[to_set] . |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1055 |
|
76267
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1056 |
lemma wf_if_convertible_to_wf: |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1057 |
fixes r :: "'a rel" and s :: "'b rel" and f :: "'a \<Rightarrow> 'b" |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1058 |
assumes "wf s" and convertible: "\<And>x y. (x, y) \<in> r \<Longrightarrow> (f x, f y) \<in> s" |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1059 |
shows "wf r" |
79999
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1060 |
proof (rule wf_on_if_convertible_to_wf_on) |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1061 |
show "wf_on (range f) s" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1062 |
using wf_on_subset[OF \<open>wf s\<close> subset_UNIV] . |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1063 |
next |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1064 |
show "\<And>x y. (x, y) \<in> r \<Longrightarrow> (f x, f y) \<in> s" |
dca9c237d108
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
desharna
parents:
79997
diff
changeset
|
1065 |
using convertible . |
76267
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1066 |
qed |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1067 |
|
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1068 |
lemma wfP_if_convertible_to_wfP: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R" |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1069 |
using wf_if_convertible_to_wf[to_pred, of S R f] by simp |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1070 |
|
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1071 |
text \<open>Converting to @{typ nat} is a very common special case that might be found more easily by |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1072 |
Sledgehammer.\<close> |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1073 |
|
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1074 |
lemma wfP_if_convertible_to_nat: |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1075 |
fixes f :: "_ \<Rightarrow> nat" |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1076 |
shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfP R" |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1077 |
by (rule wfP_if_convertible_to_wfP[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified]) |
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1078 |
|
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1079 |
|
5ea1f8bfb795
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat
desharna
parents:
75669
diff
changeset
|
1080 |
subsubsection \<open>Measure functions into \<^typ>\<open>nat\<close>\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1081 |
|
63108 | 1082 |
definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set" |
1083 |
where "measure = inv_image less_than" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1084 |
|
63108 | 1085 |
lemma in_measure[simp, code_unfold]: "(x, y) \<in> measure f \<longleftrightarrow> f x < f y" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1086 |
by (simp add:measure_def) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1087 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1088 |
lemma wf_measure [iff]: "wf (measure f)" |
63572 | 1089 |
unfolding measure_def by (rule wf_less_than [THEN wf_inv_image]) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1090 |
|
63108 | 1091 |
lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}" |
1092 |
for f :: "'a \<Rightarrow> nat" |
|
68646 | 1093 |
using wf_measure[of f] unfolding measure_def inv_image_def less_than_def less_eq |
1094 |
by (rule wf_subset) auto |
|
41720 | 1095 |
|
1096 |
||
63108 | 1097 |
subsubsection \<open>Lexicographic combinations\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1098 |
|
63108 | 1099 |
definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" |
1100 |
(infixr "<*lex*>" 80) |
|
72184 | 1101 |
where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1102 |
|
72184 | 1103 |
lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1104 |
by (auto simp:lex_prod_def) |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1105 |
|
71410 | 1106 |
lemma wf_lex_prod [intro!]: |
1107 |
assumes "wf ra" "wf rb" |
|
1108 |
shows "wf (ra <*lex*> rb)" |
|
1109 |
proof (rule wfI) |
|
1110 |
fix z :: "'a \<times> 'b" and P |
|
1111 |
assume * [rule_format]: "\<forall>u. (\<forall>v. (v, u) \<in> ra <*lex*> rb \<longrightarrow> P v) \<longrightarrow> P u" |
|
1112 |
obtain x y where zeq: "z = (x,y)" |
|
1113 |
by fastforce |
|
1114 |
have "P(x,y)" using \<open>wf ra\<close> |
|
1115 |
proof (induction x arbitrary: y rule: wf_induct_rule) |
|
1116 |
case (less x) |
|
1117 |
note lessx = less |
|
1118 |
show ?case using \<open>wf rb\<close> less |
|
1119 |
proof (induction y rule: wf_induct_rule) |
|
1120 |
case (less y) |
|
1121 |
show ?case |
|
1122 |
by (force intro: * less.IH lessx) |
|
1123 |
qed |
|
1124 |
qed |
|
1125 |
then show "P z" |
|
1126 |
by (simp add: zeq) |
|
1127 |
qed auto |
|
1128 |
||
76698 | 1129 |
lemma refl_lex_prod[simp]: "refl r\<^sub>B \<Longrightarrow> refl (r\<^sub>A <*lex*> r\<^sub>B)" |
1130 |
by (auto intro!: reflI dest: refl_onD) |
|
1131 |
||
76694
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1132 |
lemma irrefl_on_lex_prod[simp]: |
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1133 |
"irrefl_on A r\<^sub>A \<Longrightarrow> irrefl_on B r\<^sub>B \<Longrightarrow> irrefl_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)" |
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1134 |
by (auto intro!: irrefl_onI dest: irrefl_onD) |
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1135 |
|
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1136 |
lemma irrefl_lex_prod[simp]: "irrefl r\<^sub>A \<Longrightarrow> irrefl r\<^sub>B \<Longrightarrow> irrefl (r\<^sub>A <*lex*> r\<^sub>B)" |
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1137 |
by (rule irrefl_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV]) |
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1138 |
|
76695
e321569ec7a1
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
desharna
parents:
76694
diff
changeset
|
1139 |
lemma sym_on_lex_prod[simp]: |
e321569ec7a1
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
desharna
parents:
76694
diff
changeset
|
1140 |
"sym_on A r\<^sub>A \<Longrightarrow> sym_on B r\<^sub>B \<Longrightarrow> sym_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)" |
e321569ec7a1
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
desharna
parents:
76694
diff
changeset
|
1141 |
by (auto intro!: sym_onI dest: sym_onD) |
e321569ec7a1
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
desharna
parents:
76694
diff
changeset
|
1142 |
|
e321569ec7a1
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
desharna
parents:
76694
diff
changeset
|
1143 |
lemma sym_lex_prod[simp]: |
e321569ec7a1
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
desharna
parents:
76694
diff
changeset
|
1144 |
"sym r\<^sub>A \<Longrightarrow> sym r\<^sub>B \<Longrightarrow> sym (r\<^sub>A <*lex*> r\<^sub>B)" |
e321569ec7a1
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
desharna
parents:
76694
diff
changeset
|
1145 |
by (rule sym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV]) |
e321569ec7a1
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
desharna
parents:
76694
diff
changeset
|
1146 |
|
76696
b6b7f3caa74a
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
desharna
parents:
76695
diff
changeset
|
1147 |
lemma asym_on_lex_prod[simp]: |
b6b7f3caa74a
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
desharna
parents:
76695
diff
changeset
|
1148 |
"asym_on A r\<^sub>A \<Longrightarrow> asym_on B r\<^sub>B \<Longrightarrow> asym_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)" |
b6b7f3caa74a
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
desharna
parents:
76695
diff
changeset
|
1149 |
by (auto intro!: asym_onI dest: asym_onD) |
b6b7f3caa74a
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
desharna
parents:
76695
diff
changeset
|
1150 |
|
b6b7f3caa74a
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
desharna
parents:
76695
diff
changeset
|
1151 |
lemma asym_lex_prod[simp]: |
b6b7f3caa74a
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
desharna
parents:
76695
diff
changeset
|
1152 |
"asym r\<^sub>A \<Longrightarrow> asym r\<^sub>B \<Longrightarrow> asym (r\<^sub>A <*lex*> r\<^sub>B)" |
b6b7f3caa74a
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
desharna
parents:
76695
diff
changeset
|
1153 |
by (rule asym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV]) |
b6b7f3caa74a
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
desharna
parents:
76695
diff
changeset
|
1154 |
|
76753 | 1155 |
lemma trans_on_lex_prod[simp]: |
1156 |
assumes "trans_on A r\<^sub>A" and "trans_on B r\<^sub>B" |
|
1157 |
shows "trans_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)" |
|
1158 |
proof (rule trans_onI) |
|
1159 |
fix x y z |
|
1160 |
show "x \<in> A \<times> B \<Longrightarrow> y \<in> A \<times> B \<Longrightarrow> z \<in> A \<times> B \<Longrightarrow> |
|
1161 |
(x, y) \<in> r\<^sub>A <*lex*> r\<^sub>B \<Longrightarrow> (y, z) \<in> r\<^sub>A <*lex*> r\<^sub>B \<Longrightarrow> (x, z) \<in> r\<^sub>A <*lex*> r\<^sub>B" |
|
1162 |
using trans_onD[OF \<open>trans_on A r\<^sub>A\<close>, of "fst x" "fst y" "fst z"] |
|
1163 |
using trans_onD[OF \<open>trans_on B r\<^sub>B\<close>, of "snd x" "snd y" "snd z"] |
|
1164 |
by auto |
|
1165 |
qed |
|
1166 |
||
1167 |
lemma trans_lex_prod [simp,intro!]: "trans r\<^sub>A \<Longrightarrow> trans r\<^sub>B \<Longrightarrow> trans (r\<^sub>A <*lex*> r\<^sub>B)" |
|
1168 |
by (rule trans_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV]) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1169 |
|
76694
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1170 |
lemma total_on_lex_prod[simp]: |
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1171 |
"total_on A r\<^sub>A \<Longrightarrow> total_on B r\<^sub>B \<Longrightarrow> total_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)" |
71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
1172 |
by (auto simp: total_on_def) |
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
1173 |
|
76694
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1174 |
lemma total_lex_prod[simp]: "total r\<^sub>A \<Longrightarrow> total r\<^sub>B \<Longrightarrow> total (r\<^sub>A <*lex*> r\<^sub>B)" |
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1175 |
by (rule total_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV]) |
2f8219460ac9
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
desharna
parents:
76682
diff
changeset
|
1176 |
|
60758 | 1177 |
text \<open>lexicographic combinations with measure functions\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1178 |
|
63108 | 1179 |
definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80) |
1180 |
where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1181 |
|
66952 | 1182 |
lemma |
1183 |
wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)" and |
|
1184 |
mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R" and |
|
1185 |
mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R" and |
|
1186 |
mlex_iff: "(x, y) \<in> f <*mlex*> R \<longleftrightarrow> f x < f y \<or> f x = f y \<and> (x, y) \<in> R" |
|
63572 | 1187 |
by (auto simp: mlex_prod_def) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1188 |
|
63572 | 1189 |
text \<open>Proper subset relation on finite sets.\<close> |
63108 | 1190 |
definition finite_psubset :: "('a set \<times> 'a set) set" |
63572 | 1191 |
where "finite_psubset = {(A, B). A \<subset> B \<and> finite B}" |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1192 |
|
63108 | 1193 |
lemma wf_finite_psubset[simp]: "wf finite_psubset" |
1194 |
apply (unfold finite_psubset_def) |
|
1195 |
apply (rule wf_measure [THEN wf_subset]) |
|
1196 |
apply (simp add: measure_def inv_image_def less_than_def less_eq) |
|
1197 |
apply (fast elim!: psubset_card_mono) |
|
1198 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1199 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1200 |
lemma trans_finite_psubset: "trans finite_psubset" |
63612 | 1201 |
by (auto simp: finite_psubset_def less_le trans_def) |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1202 |
|
63572 | 1203 |
lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A \<subset> B \<and> finite B" |
63108 | 1204 |
unfolding finite_psubset_def by auto |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1205 |
|
60758 | 1206 |
text \<open>max- and min-extension of order to finite sets\<close> |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1207 |
|
63108 | 1208 |
inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" |
1209 |
for R :: "('a \<times> 'a) set" |
|
63572 | 1210 |
where max_extI[intro]: |
1211 |
"finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1212 |
|
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1213 |
lemma max_ext_wf: |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1214 |
assumes wf: "wf r" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1215 |
shows "wf (max_ext r)" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1216 |
proof (rule acc_wfI, intro allI) |
63915 | 1217 |
show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") for M |
1218 |
proof (induct M rule: infinite_finite_induct) |
|
1219 |
case empty |
|
1220 |
show ?case |
|
1221 |
by (rule accI) (auto elim: max_ext.cases) |
|
1222 |
next |
|
1223 |
case (insert a M) |
|
1224 |
from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W" |
|
1225 |
proof (induct arbitrary: M) |
|
1226 |
fix M a |
|
1227 |
assume "M \<in> ?W" |
|
1228 |
assume [intro]: "finite M" |
|
1229 |
assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W" |
|
1230 |
have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W" |
|
1231 |
if "finite N" "finite M" for N M :: "'a set" |
|
1232 |
using that by (induct N arbitrary: M) (auto simp: hyp) |
|
1233 |
show "insert a M \<in> ?W" |
|
1234 |
proof (rule accI) |
|
1235 |
fix N |
|
1236 |
assume Nless: "(N, insert a M) \<in> max_ext r" |
|
1237 |
then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)" |
|
1238 |
by (auto elim!: max_ext.cases) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1239 |
|
63915 | 1240 |
let ?N1 = "{n \<in> N. (n, a) \<in> r}" |
1241 |
let ?N2 = "{n \<in> N. (n, a) \<notin> r}" |
|
1242 |
have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto |
|
1243 |
from Nless have "finite N" by (auto elim: max_ext.cases) |
|
1244 |
then have finites: "finite ?N1" "finite ?N2" by auto |
|
63108 | 1245 |
|
63915 | 1246 |
have "?N2 \<in> ?W" |
1247 |
proof (cases "M = {}") |
|
1248 |
case [simp]: True |
|
1249 |
have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases) |
|
1250 |
from * have "?N2 = {}" by auto |
|
1251 |
with Mw show "?N2 \<in> ?W" by (simp only:) |
|
1252 |
next |
|
1253 |
case False |
|
1254 |
from * finites have N2: "(?N2, M) \<in> max_ext r" |
|
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74971
diff
changeset
|
1255 |
using max_extI[OF _ _ \<open>M \<noteq> {}\<close>, where ?X = ?N2] by auto |
63915 | 1256 |
with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward) |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1257 |
qed |
63915 | 1258 |
with finites have "?N1 \<union> ?N2 \<in> ?W" |
1259 |
by (rule add_less) simp |
|
1260 |
then show "N \<in> ?W" by (simp only: N) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1261 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1262 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1263 |
next |
63982 | 1264 |
case infinite |
1265 |
show ?case |
|
1266 |
by (rule accI) (auto elim: max_ext.cases simp: infinite) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1267 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1268 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1269 |
|
63572 | 1270 |
lemma max_ext_additive: "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> (A \<union> C, B \<union> D) \<in> max_ext R" |
63108 | 1271 |
by (force elim!: max_ext.cases) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28845
diff
changeset
|
1272 |
|
63108 | 1273 |
definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" |
1274 |
where "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1275 |
|
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1276 |
lemma min_ext_wf: |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1277 |
assumes "wf r" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1278 |
shows "wf (min_ext r)" |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1279 |
proof (rule wfI_min) |
66952 | 1280 |
show "\<exists>m \<in> Q. (\<forall>n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q" |
63108 | 1281 |
for Q :: "'a set set" and x |
1282 |
proof (cases "Q = {{}}") |
|
1283 |
case True |
|
1284 |
then show ?thesis by (simp add: min_ext_def) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1285 |
next |
63108 | 1286 |
case False |
1287 |
with nonempty obtain e x where "x \<in> Q" "e \<in> x" by force |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1288 |
then have eU: "e \<in> \<Union>Q" by auto |
63108 | 1289 |
with \<open>wf r\<close> |
1290 |
obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1291 |
by (erule wfE_min) |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1292 |
from z obtain m where "m \<in> Q" "z \<in> m" by auto |
63572 | 1293 |
from \<open>m \<in> Q\<close> show ?thesis |
1294 |
proof (intro rev_bexI allI impI) |
|
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1295 |
fix n |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1296 |
assume smaller: "(n, m) \<in> min_ext r" |
63572 | 1297 |
with \<open>z \<in> m\<close> obtain y where "y \<in> n" "(y, z) \<in> r" |
1298 |
by (auto simp: min_ext_def) |
|
1299 |
with z(2) show "n \<notin> Q" by auto |
|
63108 | 1300 |
qed |
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1301 |
qed |
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset
|
1302 |
qed |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1303 |
|
63108 | 1304 |
|
1305 |
subsubsection \<open>Bounded increase must terminate\<close> |
|
43137 | 1306 |
|
1307 |
lemma wf_bounded_measure: |
|
63108 | 1308 |
fixes ub :: "'a \<Rightarrow> nat" |
1309 |
and f :: "'a \<Rightarrow> nat" |
|
1310 |
assumes "\<And>a b. (b, a) \<in> r \<Longrightarrow> ub b \<le> ub a \<and> ub a \<ge> f b \<and> f b > f a" |
|
1311 |
shows "wf r" |
|
63572 | 1312 |
by (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]]) (auto dest: assms) |
43137 | 1313 |
|
1314 |
lemma wf_bounded_set: |
|
63108 | 1315 |
fixes ub :: "'a \<Rightarrow> 'b set" |
1316 |
and f :: "'a \<Rightarrow> 'b set" |
|
1317 |
assumes "\<And>a b. (b,a) \<in> r \<Longrightarrow> finite (ub a) \<and> ub b \<subseteq> ub a \<and> ub a \<supseteq> f b \<and> f b \<supset> f a" |
|
1318 |
shows "wf r" |
|
63572 | 1319 |
apply (rule wf_bounded_measure[of r "\<lambda>a. card (ub a)" "\<lambda>a. card (f a)"]) |
1320 |
apply (drule assms) |
|
63108 | 1321 |
apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) |
1322 |
done |
|
43137 | 1323 |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
1324 |
lemma finite_subset_wf: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63088
diff
changeset
|
1325 |
assumes "finite A" |
66952 | 1326 |
shows "wf {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}" |
1327 |
by (rule wf_subset[OF wf_finite_psubset[unfolded finite_psubset_def]]) |
|
1328 |
(auto intro: finite_subset[OF _ assms]) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1329 |
|
54295 | 1330 |
hide_const (open) acc accp |
1331 |
||
79971
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1332 |
|
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1333 |
subsection \<open>Code Generation Setup\<close> |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1334 |
|
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1335 |
text \<open>Code equations with \<^const>\<open>wf\<close> or \<^const>\<open>wfp\<close> on the left-hand side are not supported by the |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1336 |
code generation module because of the \<^const>\<open>UNIV\<close> hidden behind the abbreviations. To sidestep this |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1337 |
problem, we provide the following wrapper definitions and use @{attribute code_abbrev} to register |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1338 |
the definitions with the pre- and post-processors of the code generator.\<close> |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1339 |
|
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1340 |
definition wf_code :: "('a \<times> 'a) set \<Rightarrow> bool" where |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1341 |
[code_abbrev]: "wf_code r \<longleftrightarrow> wf r" |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1342 |
|
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1343 |
definition wfp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1344 |
[code_abbrev]: "wfp_code R \<longleftrightarrow> wfp R" |
033f90dc441d
redefined wf as an abbreviation for "wf_on UNIV"
desharna
parents:
79965
diff
changeset
|
1345 |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset
|
1346 |
end |