summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Thu, 11 Jul 2002 16:57:14 +0200 | |

changeset 13349 | 7d4441c8c46a |

parent 13348 | 374d05460db4 |

child 13350 | 626b79677dfa |

Added "using" to the beginning of original newman proof again, because
it was lost during last update; renamed second version of newman to
newman' (this allows for a comparison of the primitive proof objects,
for example).

--- a/src/HOL/Lambda/Commutation.thy Thu Jul 11 13:43:24 2002 +0200 +++ b/src/HOL/Lambda/Commutation.thy Thu Jul 11 16:57:14 2002 +0200 @@ -138,59 +138,60 @@ subsection {* Newman's lemma *} -(* Proof by Stefan Berghofer *) +text {* Proof by Stefan Berghofer *} theorem newman: assumes wf: "wf (R\<inverse>)" and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" - shows "(a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> - \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" (is "PROP ?conf b c") -proof - - from wf show "\<And>b c. PROP ?conf b c" - proof induct - case (less x b c) - have xc: "(x, c) \<in> R\<^sup>*" . - have xb: "(x, b) \<in> R\<^sup>*" . thus ?case + shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> + \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" + using wf +proof induct + case (less x b c) + have xc: "(x, c) \<in> R\<^sup>*" . + have xb: "(x, b) \<in> R\<^sup>*" . thus ?case + proof (rule converse_rtranclE) + assume "x = b" + with xc have "(b, c) \<in> R\<^sup>*" by simp + thus ?thesis by rules + next + fix y + assume xy: "(x, y) \<in> R" + assume yb: "(y, b) \<in> R\<^sup>*" + from xc show ?thesis proof (rule converse_rtranclE) - assume "x = b" - with xc have "(b, c) \<in> R\<^sup>*" by simp + assume "x = c" + with xb have "(c, b) \<in> R\<^sup>*" by simp thus ?thesis by rules next - fix y - assume xy: "(x, y) \<in> R" - assume yb: "(y, b) \<in> R\<^sup>*" - from xc show ?thesis - proof (rule converse_rtranclE) - assume "x = c" - with xb have "(c, b) \<in> R\<^sup>*" by simp - thus ?thesis by rules - next - fix y' - assume y'c: "(y', c) \<in> R\<^sup>*" - assume xy': "(x, y') \<in> R" - with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc) - then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules - from xy[symmetric] yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" - by (rule less) - then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules - note xy'[symmetric] - moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans) - moreover note y'c - ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less) - then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules - from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans) - with cw show ?thesis by rules - qed + fix y' + assume y'c: "(y', c) \<in> R\<^sup>*" + assume xy': "(x, y') \<in> R" + with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc) + then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules + from xy have "(y, x) \<in> R\<inverse>" .. + from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less) + then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules + from xy' have "(y', x) \<in> R\<inverse>" .. + moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans) + moreover note y'c + ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less) + then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules + from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans) + with cw show ?thesis by rules qed qed qed -(* Partly automated by Tobias Nipkow. Takes 2 minutes (2002). *) +text {* + \medskip Alternative version. Partly automated by Tobias + Nipkow. Takes 2 minutes (2002). -text{* This is the maximal amount of automation possible at the moment. *} + This is the maximal amount of automation possible at the moment. +*} -theorem newman: +theorem newman': assumes wf: "wf (R\<inverse>)" and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"