src/HOL/Lambda/Commutation.thy
changeset 13089 c8c28a1dc787
parent 10212 33fe2d701ddd
child 13331 47e9950a502d
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Tue Apr 16 12:23:49 2002 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Fri Apr 19 14:33:04 2002 +0200
     1.3 @@ -135,4 +135,53 @@
     1.4    apply (blast del: rtrancl_refl intro: rtrancl_trans)
     1.5    done
     1.6  
     1.7 +
     1.8 +subsection {* Newman's lemma *}
     1.9 +
    1.10 +theorem newman:
    1.11 +  assumes wf: "wf (R\<inverse>)"
    1.12 +  and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
    1.13 +    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
    1.14 +  shows "(a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
    1.15 +    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" (is "PROP ?conf b c")
    1.16 +proof -
    1.17 +  from wf show "\<And>b c. PROP ?conf b c"
    1.18 +  proof induct
    1.19 +    case (less x b c)
    1.20 +    have xc: "(x, c) \<in> R\<^sup>*" .
    1.21 +    have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
    1.22 +    proof (rule converse_rtranclE)
    1.23 +      assume "x = b"
    1.24 +      with xc have "(b, c) \<in> R\<^sup>*" by simp
    1.25 +      thus ?thesis by rules
    1.26 +    next
    1.27 +      fix y
    1.28 +      assume xy: "(x, y) \<in> R"
    1.29 +      assume yb: "(y, b) \<in> R\<^sup>*"
    1.30 +      from xc show ?thesis
    1.31 +      proof (rule converse_rtranclE)
    1.32 +	assume "x = c"
    1.33 +	with xb have "(c, b) \<in> R\<^sup>*" by simp
    1.34 +	thus ?thesis by rules
    1.35 +      next
    1.36 +	fix y'
    1.37 +	assume y'c: "(y', c) \<in> R\<^sup>*"
    1.38 +	assume xy': "(x, y') \<in> R"
    1.39 +	with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
    1.40 +        then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
    1.41 +	from xy have "(y, x) \<in> R\<inverse>" ..
    1.42 +	from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
    1.43 +	then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
    1.44 +	from xy' have "(y', x) \<in> R\<inverse>" ..
    1.45 +	moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
    1.46 +	moreover note y'c
    1.47 +	ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
    1.48 +	then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
    1.49 +	from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
    1.50 +	with cw show ?thesis by rules
    1.51 +      qed
    1.52 +    qed
    1.53 +  qed
    1.54 +qed
    1.55 +
    1.56  end