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