src/HOL/Lambda/Commutation.thy
 changeset 28455 a79701b14a30 parent 25972 94b15338da8d child 36862 952b2b102a0a
```     1.1 --- a/src/HOL/Lambda/Commutation.thy	Wed Oct 01 22:33:29 2008 +0200
1.2 +++ b/src/HOL/Lambda/Commutation.thy	Thu Oct 02 12:17:20 2008 +0200
1.3 @@ -186,10 +186,10 @@
1.4  qed
1.5
1.6  text {*
1.7 -  \medskip Alternative version.  Partly automated by Tobias
1.8 +  Alternative version.  Partly automated by Tobias
1.9    Nipkow. Takes 2 minutes (2002).
1.10
1.11 -  This is the maximal amount of automation possible at the moment.
1.12 +  This is the maximal amount of automation possible using @{text blast}.
1.13  *}
1.14
1.15  theorem newman':
1.16 @@ -233,4 +233,34 @@
1.17    qed
1.18  qed
1.19
1.20 +text {*
1.21 +  Using the coherent logic prover, the proof of the induction step
1.22 +  is completely automatic.
1.23 +*}
1.24 +
1.25 +lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
1.26 +  by simp
1.27 +
1.28 +theorem newman'':
1.29 +  assumes wf: "wfP (R\<inverse>\<inverse>)"
1.30 +  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
1.31 +    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
1.32 +  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
1.33 +    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
1.34 +  using wf
1.35 +proof induct
1.36 +  case (less x b c)
1.37 +  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
1.38 +                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
1.39 +  show ?case
1.40 +    by (coherent
1.41 +      `R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b`
1.42 +      refl [where 'a='a] sym
1.43 +      eq_imp_rtranclp
1.44 +      r_into_rtranclp [of R]
1.45 +      rtranclp_trans
1.46 +      lc IH [OF conversepI]
1.47 +      converse_rtranclpE)
1.48 +qed
1.49 +
1.50  end
```