summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Fri, 19 Apr 2002 14:33:04 +0200 | |

changeset 13089 | c8c28a1dc787 |

parent 13088 | 56b21879c603 |

child 13090 | 4fb7a2f2c1df |

Added proof of Newman's lemma.

--- a/src/HOL/Lambda/Commutation.thy Tue Apr 16 12:23:49 2002 +0200 +++ b/src/HOL/Lambda/Commutation.thy Fri Apr 19 14:33:04 2002 +0200 @@ -135,4 +135,53 @@ apply (blast del: rtrancl_refl intro: rtrancl_trans) done + +subsection {* Newman's lemma *} + +theorem newman: + assumes wf: "wf (R\<inverse>)" + and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow> + \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" + shows "(a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> + \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" (is "PROP ?conf b c") +proof - + from wf show "\<And>b c. PROP ?conf b c" + proof induct + case (less x b c) + have xc: "(x, c) \<in> R\<^sup>*" . + have xb: "(x, b) \<in> R\<^sup>*" . thus ?case + proof (rule converse_rtranclE) + assume "x = b" + with xc have "(b, c) \<in> R\<^sup>*" by simp + thus ?thesis by rules + next + fix y + assume xy: "(x, y) \<in> R" + assume yb: "(y, b) \<in> R\<^sup>*" + from xc show ?thesis + proof (rule converse_rtranclE) + assume "x = c" + with xb have "(c, b) \<in> R\<^sup>*" by simp + thus ?thesis by rules + next + fix y' + assume y'c: "(y', c) \<in> R\<^sup>*" + assume xy': "(x, y') \<in> R" + with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc) + then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules + from xy have "(y, x) \<in> R\<inverse>" .. + from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less) + then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules + from xy' have "(y', x) \<in> R\<inverse>" .. + moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans) + moreover note y'c + ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less) + then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules + from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans) + with cw show ?thesis by rules + qed + qed + qed +qed + end