# HG changeset patch
# User berghofe
# Date 1026399434 -7200
# Node ID 7d4441c8c46a1cbf9d1e731f7a45cbeedefd35ba
# Parent  374d05460db4e206ed4e0c35f9f704fe6c556359
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).

diff -r 374d05460db4 -r 7d4441c8c46a src/HOL/Lambda/Commutation.thy
--- 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>*"