1 (* Title: HOL/Cardinals/Wellfounded_More_FP.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 More on well-founded relations (FP). |
|
6 *) |
|
7 |
|
8 header {* More on Well-Founded Relations (FP) *} |
|
9 |
|
10 theory Wellfounded_More_FP |
|
11 imports Wfrec Order_Relation |
|
12 begin |
|
13 |
|
14 |
|
15 text {* This section contains some variations of results in the theory |
|
16 @{text "Wellfounded.thy"}: |
|
17 \begin{itemize} |
|
18 \item means for slightly more direct definitions by well-founded recursion; |
|
19 \item variations of well-founded induction; |
|
20 \item means for proving a linear order to be a well-order. |
|
21 \end{itemize} *} |
|
22 |
|
23 |
|
24 subsection {* Well-founded recursion via genuine fixpoints *} |
|
25 |
|
26 |
|
27 (*2*)lemma wfrec_fixpoint: |
|
28 fixes r :: "('a * 'a) set" and |
|
29 H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
30 assumes WF: "wf r" and ADM: "adm_wf r H" |
|
31 shows "wfrec r H = H (wfrec r H)" |
|
32 proof(rule ext) |
|
33 fix x |
|
34 have "wfrec r H x = H (cut (wfrec r H) r x) x" |
|
35 using wfrec[of r H] WF by simp |
|
36 also |
|
37 {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y" |
|
38 by (auto simp add: cut_apply) |
|
39 hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x" |
|
40 using ADM adm_wf_def[of r H] by auto |
|
41 } |
|
42 finally show "wfrec r H x = H (wfrec r H) x" . |
|
43 qed |
|
44 |
|
45 |
|
46 |
|
47 subsection {* Characterizations of well-founded-ness *} |
|
48 |
|
49 |
|
50 text {* A transitive relation is well-founded iff it is ``locally" well-founded, |
|
51 i.e., iff its restriction to the lower bounds of of any element is well-founded. *} |
|
52 |
|
53 (*3*)lemma trans_wf_iff: |
|
54 assumes "trans r" |
|
55 shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))" |
|
56 proof- |
|
57 obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast |
|
58 {assume *: "wf r" |
|
59 {fix a |
|
60 have "wf(R a)" |
|
61 using * R_def wf_subset[of r "R a"] by auto |
|
62 } |
|
63 } |
|
64 (* *) |
|
65 moreover |
|
66 {assume *: "\<forall>a. wf(R a)" |
|
67 have "wf r" |
|
68 proof(unfold wf_def, clarify) |
|
69 fix phi a |
|
70 assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a" |
|
71 obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast |
|
72 with * have "wf (R a)" by auto |
|
73 hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)" |
|
74 unfolding wf_def by blast |
|
75 moreover |
|
76 have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b" |
|
77 proof(auto simp add: chi_def R_def) |
|
78 fix b |
|
79 assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c" |
|
80 hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c" |
|
81 using assms trans_def[of r] by blast |
|
82 thus "phi b" using ** by blast |
|
83 qed |
|
84 ultimately have "\<forall>b. chi b" by (rule mp) |
|
85 with ** chi_def show "phi a" by blast |
|
86 qed |
|
87 } |
|
88 ultimately show ?thesis using R_def by blast |
|
89 qed |
|
90 |
|
91 |
|
92 text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded, |
|
93 allowing one to assume the set included in the field. *} |
|
94 |
|
95 (*2*)lemma wf_eq_minimal2: |
|
96 "wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))" |
|
97 proof- |
|
98 let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)" |
|
99 have "wf r = (\<forall>A. ?phi A)" |
|
100 by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast) |
|
101 (rule wfI_min, fast) |
|
102 (* *) |
|
103 also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)" |
|
104 proof |
|
105 assume "\<forall>A. ?phi A" |
|
106 thus "\<forall>B \<le> Field r. ?phi B" by simp |
|
107 next |
|
108 assume *: "\<forall>B \<le> Field r. ?phi B" |
|
109 show "\<forall>A. ?phi A" |
|
110 proof(clarify) |
|
111 fix A::"'a set" assume **: "A \<noteq> {}" |
|
112 obtain B where B_def: "B = A Int (Field r)" by blast |
|
113 show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r" |
|
114 proof(cases "B = {}") |
|
115 assume Case1: "B = {}" |
|
116 obtain a where 1: "a \<in> A \<and> a \<notin> Field r" |
|
117 using ** Case1 unfolding B_def by blast |
|
118 hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast |
|
119 thus ?thesis using 1 by blast |
|
120 next |
|
121 assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast |
|
122 obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)" |
|
123 using Case2 1 * by blast |
|
124 have "\<forall>a' \<in> A. (a',a) \<notin> r" |
|
125 proof(clarify) |
|
126 fix a' assume "a' \<in> A" and **: "(a',a) \<in> r" |
|
127 hence "a' \<in> B" unfolding B_def Field_def by blast |
|
128 thus False using 2 ** by blast |
|
129 qed |
|
130 thus ?thesis using 2 unfolding B_def by blast |
|
131 qed |
|
132 qed |
|
133 qed |
|
134 finally show ?thesis by blast |
|
135 qed |
|
136 |
|
137 subsection {* Characterizations of well-founded-ness *} |
|
138 |
|
139 text {* The next lemma and its corollary enable one to prove that |
|
140 a linear order is a well-order in a way which is more standard than |
|
141 via well-founded-ness of the strict version of the relation. *} |
|
142 |
|
143 (*3*) |
|
144 lemma Linear_order_wf_diff_Id: |
|
145 assumes LI: "Linear_order r" |
|
146 shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))" |
|
147 proof(cases "r \<le> Id") |
|
148 assume Case1: "r \<le> Id" |
|
149 hence temp: "r - Id = {}" by blast |
|
150 hence "wf(r - Id)" by (simp add: temp) |
|
151 moreover |
|
152 {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}" |
|
153 obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI |
|
154 unfolding order_on_defs using Case1 Total_subset_Id by auto |
|
155 hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast |
|
156 hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast |
|
157 } |
|
158 ultimately show ?thesis by blast |
|
159 next |
|
160 assume Case2: "\<not> r \<le> Id" |
|
161 hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI |
|
162 unfolding order_on_defs by blast |
|
163 show ?thesis |
|
164 proof |
|
165 assume *: "wf(r - Id)" |
|
166 show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" |
|
167 proof(clarify) |
|
168 fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}" |
|
169 hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" |
|
170 using 1 * unfolding wf_eq_minimal2 by simp |
|
171 moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)" |
|
172 using Linear_order_in_diff_Id[of r] ** LI by blast |
|
173 ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast |
|
174 qed |
|
175 next |
|
176 assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" |
|
177 show "wf(r - Id)" |
|
178 proof(unfold wf_eq_minimal2, clarify) |
|
179 fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}" |
|
180 hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" |
|
181 using 1 * by simp |
|
182 moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)" |
|
183 using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast |
|
184 ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast |
|
185 qed |
|
186 qed |
|
187 qed |
|
188 |
|
189 (*3*)corollary Linear_order_Well_order_iff: |
|
190 assumes "Linear_order r" |
|
191 shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))" |
|
192 using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast |
|
193 |
|
194 end |
|