src/HOL/Lambda/Commutation.thy
 changeset 13331 47e9950a502d parent 13089 c8c28a1dc787 child 13343 3b2b18c58d80
```     1.1 --- a/src/HOL/Lambda/Commutation.thy	Wed Jul 10 08:09:35 2002 +0200
1.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Jul 10 13:55:32 2002 +0200
1.3 @@ -138,48 +138,46 @@
1.4
1.5  subsection {* Newman's lemma *}
1.6
1.7 -theorem newman:
1.8 +theorem Newman:
1.9    assumes wf: "wf (R\<inverse>)"
1.10    and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
1.11      \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
1.12 -  shows "(a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
1.13 -    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" (is "PROP ?conf b c")
1.14 -proof -
1.15 -  from wf show "\<And>b c. PROP ?conf b c"
1.16 -  proof induct
1.17 -    case (less x b c)
1.18 -    have xc: "(x, c) \<in> R\<^sup>*" .
1.19 -    have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
1.20 +  shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
1.21 +    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
1.22 +  using wf
1.23 +proof induct
1.24 +  case (less x b c)
1.25 +  have xc: "(x, c) \<in> R\<^sup>*" .
1.26 +  have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
1.27 +  proof (rule converse_rtranclE)
1.28 +    assume "x = b"
1.29 +    with xc have "(b, c) \<in> R\<^sup>*" by simp
1.30 +    thus ?thesis by rules
1.31 +  next
1.32 +    fix y
1.33 +    assume xy: "(x, y) \<in> R"
1.34 +    assume yb: "(y, b) \<in> R\<^sup>*"
1.35 +    from xc show ?thesis
1.36      proof (rule converse_rtranclE)
1.37 -      assume "x = b"
1.38 -      with xc have "(b, c) \<in> R\<^sup>*" by simp
1.39 +      assume "x = c"
1.40 +      with xb have "(c, b) \<in> R\<^sup>*" by simp
1.41        thus ?thesis by rules
1.42      next
1.43 -      fix y
1.44 -      assume xy: "(x, y) \<in> R"
1.45 -      assume yb: "(y, b) \<in> R\<^sup>*"
1.46 -      from xc show ?thesis
1.47 -      proof (rule converse_rtranclE)
1.48 -	assume "x = c"
1.49 -	with xb have "(c, b) \<in> R\<^sup>*" by simp
1.50 -	thus ?thesis by rules
1.51 -      next
1.52 -	fix y'
1.53 -	assume y'c: "(y', c) \<in> R\<^sup>*"
1.54 -	assume xy': "(x, y') \<in> R"
1.55 -	with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
1.56 -        then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
1.57 -	from xy have "(y, x) \<in> R\<inverse>" ..
1.58 -	from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
1.59 -	then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
1.60 -	from xy' have "(y', x) \<in> R\<inverse>" ..
1.61 -	moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
1.62 -	moreover note y'c
1.63 -	ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
1.64 -	then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
1.65 -	from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
1.66 -	with cw show ?thesis by rules
1.67 -      qed
1.68 +      fix y'
1.69 +      assume y'c: "(y', c) \<in> R\<^sup>*"
1.70 +      assume xy': "(x, y') \<in> R"
1.71 +      with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
1.72 +      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
1.73 +      from xy have "(y, x) \<in> R\<inverse>" ..
1.74 +      from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
1.75 +      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
1.76 +      from xy' have "(y', x) \<in> R\<inverse>" ..
1.77 +      moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
1.78 +      moreover note y'c
1.79 +      ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
1.80 +      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
1.81 +      from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
1.82 +      with cw show ?thesis by rules
1.83      qed
1.84    qed
1.85  qed
```