# HG changeset patch
# User berghofe
# Date 1019219584 -7200
# Node ID c8c28a1dc787ee68426850511c993af39aa35bdd
# Parent  56b21879c603cec76379ae3a502a984b21cbc46d
Added proof of Newman's lemma.

diff -r 56b21879c603 -r c8c28a1dc787 src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Tue Apr 16 12:23:49 2002 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Fri Apr 19 14:33:04 2002 +0200
@@ -135,4 +135,53 @@
   apply (blast del: rtrancl_refl intro: rtrancl_trans)
   done
 
+
+subsection {* Newman's lemma *}
+
+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
+    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 = 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
+    qed
+  qed
+qed
+
 end