136 done |
136 done |
137 |
137 |
138 |
138 |
139 subsection {* Newman's lemma *} |
139 subsection {* Newman's lemma *} |
140 |
140 |
141 (* Proof by Stefan Berghofer *) |
141 text {* Proof by Stefan Berghofer *} |
142 |
142 |
143 theorem newman: |
143 theorem newman: |
144 assumes wf: "wf (R\<inverse>)" |
144 assumes wf: "wf (R\<inverse>)" |
145 and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> |
145 and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> |
146 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
146 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
147 shows "(a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> |
147 shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> |
148 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" (is "PROP ?conf b c") |
148 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
149 proof - |
149 using wf |
150 from wf show "\<And>b c. PROP ?conf b c" |
150 proof induct |
151 proof induct |
151 case (less x b c) |
152 case (less x b c) |
152 have xc: "(x, c) \<in> R\<^sup>*" . |
153 have xc: "(x, c) \<in> R\<^sup>*" . |
153 have xb: "(x, b) \<in> R\<^sup>*" . thus ?case |
154 have xb: "(x, b) \<in> R\<^sup>*" . thus ?case |
154 proof (rule converse_rtranclE) |
|
155 assume "x = b" |
|
156 with xc have "(b, c) \<in> R\<^sup>*" by simp |
|
157 thus ?thesis by rules |
|
158 next |
|
159 fix y |
|
160 assume xy: "(x, y) \<in> R" |
|
161 assume yb: "(y, b) \<in> R\<^sup>*" |
|
162 from xc show ?thesis |
155 proof (rule converse_rtranclE) |
163 proof (rule converse_rtranclE) |
156 assume "x = b" |
164 assume "x = c" |
157 with xc have "(b, c) \<in> R\<^sup>*" by simp |
165 with xb have "(c, b) \<in> R\<^sup>*" by simp |
158 thus ?thesis by rules |
166 thus ?thesis by rules |
159 next |
167 next |
160 fix y |
168 fix y' |
161 assume xy: "(x, y) \<in> R" |
169 assume y'c: "(y', c) \<in> R\<^sup>*" |
162 assume yb: "(y, b) \<in> R\<^sup>*" |
170 assume xy': "(x, y') \<in> R" |
163 from xc show ?thesis |
171 with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc) |
164 proof (rule converse_rtranclE) |
172 then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules |
165 assume "x = c" |
173 from xy have "(y, x) \<in> R\<inverse>" .. |
166 with xb have "(c, b) \<in> R\<^sup>*" by simp |
174 from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less) |
167 thus ?thesis by rules |
175 then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules |
168 next |
176 from xy' have "(y', x) \<in> R\<inverse>" .. |
169 fix y' |
177 moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans) |
170 assume y'c: "(y', c) \<in> R\<^sup>*" |
178 moreover note y'c |
171 assume xy': "(x, y') \<in> R" |
179 ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less) |
172 with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc) |
180 then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules |
173 then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules |
181 from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans) |
174 from xy[symmetric] yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" |
182 with cw show ?thesis by rules |
175 by (rule less) |
|
176 then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules |
|
177 note xy'[symmetric] |
|
178 moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans) |
|
179 moreover note y'c |
|
180 ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less) |
|
181 then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules |
|
182 from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans) |
|
183 with cw show ?thesis by rules |
|
184 qed |
|
185 qed |
183 qed |
186 qed |
184 qed |
187 qed |
185 qed |
188 |
186 |
189 (* Partly automated by Tobias Nipkow. Takes 2 minutes (2002). *) |
187 text {* |
190 |
188 \medskip Alternative version. Partly automated by Tobias |
191 text{* This is the maximal amount of automation possible at the moment. *} |
189 Nipkow. Takes 2 minutes (2002). |
192 |
190 |
193 theorem newman: |
191 This is the maximal amount of automation possible at the moment. |
|
192 *} |
|
193 |
|
194 theorem newman': |
194 assumes wf: "wf (R\<inverse>)" |
195 assumes wf: "wf (R\<inverse>)" |
195 and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> |
196 and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> |
196 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
197 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
197 shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> |
198 shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> |
198 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |
199 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" |