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