author berghofe Thu, 02 Oct 2008 12:17:20 +0200 changeset 28455 a79701b14a30 parent 28454 c63168db774c child 28456 7a558c872104
Yet another proof of Newman's lemma, this time using the coherent logic prover.
```--- 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```