# HG changeset patch
# User berghofe
# Date 1222942640 -7200
# Node ID a79701b14a302b228cf9261851159da65035b06c
# Parent  c63168db774c8718accb085def978ec43842b793
Yet another proof of Newman's lemma, this time using the coherent logic prover.

diff -r c63168db774c -r a79701b14a30 src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Wed Oct 01 22:33:29 2008 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Thu Oct 02 12:17:20 2008 +0200
@@ -186,10 +186,10 @@
 qed
 
 text {*
-  \medskip Alternative version.  Partly automated by Tobias
+  Alternative version.  Partly automated by Tobias
   Nipkow. Takes 2 minutes (2002).
 
-  This is the maximal amount of automation possible at the moment.
+  This is the maximal amount of automation possible using @{text blast}.
 *}
 
 theorem newman':
@@ -233,4 +233,34 @@
   qed
 qed
 
+text {*
+  Using the coherent logic prover, the proof of the induction step
+  is completely automatic.
+*}
+
+lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
+  by simp
+
+theorem newman'':
+  assumes wf: "wfP (R\<inverse>\<inverse>)"
+  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
+    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
+  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
+    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
+  using wf
+proof induct
+  case (less x b c)
+  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
+                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
+  show ?case
+    by (coherent
+      `R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b`
+      refl [where 'a='a] sym
+      eq_imp_rtranclp
+      r_into_rtranclp [of R]
+      rtranclp_trans
+      lc IH [OF conversepI]
+      converse_rtranclpE)
+qed
+
 end