summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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