# HG changeset patch
# User wenzelm
# Date 1026302132 -7200
# Node ID 47e9950a502d650a5cfe4fb33a2695d90deb2cce
# Parent  c9e9b6add7541232249d80d14b465067c3af74bb
tuned;

diff -r c9e9b6add754 -r 47e9950a502d src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Wed Jul 10 08:09:35 2002 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Wed Jul 10 13:55:32 2002 +0200
@@ -138,48 +138,46 @@
 
 subsection {* Newman's lemma *}
 
-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>*"
-  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 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
+      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