src/HOL/Lambda/Commutation.thy
 changeset 13346 6918b6d5192b parent 13343 3b2b18c58d80 child 13349 7d4441c8c46a
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.5  subsection {* Newman's lemma *}
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.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