Added partly automated version of Newman.
authornipkow
Thu Jul 11 09:47:15 2002 +0200 (2002-07-11)
changeset 133466918b6d5192b
parent 13345 bd611943cbc2
child 13347 867f876589e7
Added partly automated version of Newman.
src/HOL/Lambda/Commutation.thy
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Thu Jul 11 09:36:41 2002 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Thu Jul 11 09:47:15 2002 +0200
     1.3 @@ -138,6 +138,8 @@
     1.4  
     1.5  subsection {* Newman's lemma *}
     1.6  
     1.7 +(* Proof by Stefan Berghofer *)
     1.8 +
     1.9  theorem newman:
    1.10    assumes wf: "wf (R\<inverse>)"
    1.11    and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
    1.12 @@ -184,4 +186,48 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 +(* Partly automated by Tobias Nipkow. Takes 2 minutes (2002). *)
    1.17 +
    1.18 +text{* This is the maximal amount of automation possible at the moment. *}
    1.19 +
    1.20 +theorem newman:
    1.21 +  assumes wf: "wf (R\<inverse>)"
    1.22 +  and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
    1.23 +    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
    1.24 +  shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
    1.25 +               \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
    1.26 +using wf
    1.27 +proof induct
    1.28 +  case (less x b c)
    1.29 +  have IH: "\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
    1.30 +                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*" by(rule less)
    1.31 +  have xc: "(x, c) \<in> R\<^sup>*" .
    1.32 +  have xb: "(x, b) \<in> R\<^sup>*" .
    1.33 +  thus ?case
    1.34 +  proof (rule converse_rtranclE)
    1.35 +    assume "x = b"
    1.36 +    with xc have "(b, c) \<in> R\<^sup>*" by simp
    1.37 +    thus ?thesis by rules
    1.38 +  next
    1.39 +    fix y
    1.40 +    assume xy: "(x, y) \<in> R"
    1.41 +    assume yb: "(y, b) \<in> R\<^sup>*"
    1.42 +    from xc show ?thesis
    1.43 +    proof (rule converse_rtranclE)
    1.44 +      assume "x = c"
    1.45 +      with xb have "(c, b) \<in> R\<^sup>*" by simp
    1.46 +      thus ?thesis by rules
    1.47 +    next
    1.48 +      fix y'
    1.49 +      assume y'c: "(y', c) \<in> R\<^sup>*"
    1.50 +      assume xy': "(x, y') \<in> R"
    1.51 +      with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
    1.52 +	by (blast dest:lc)
    1.53 +      from yb u y'c show ?thesis
    1.54 +	by(blast intro:rtrancl_trans
    1.55 +                 dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
    1.56 +    qed
    1.57 +  qed
    1.58 +qed
    1.59 +
    1.60  end