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
```