author | nipkow |

Thu Jul 11 09:17:01 2002 +0200 (2002-07-11) | |

changeset 13343 | 3b2b18c58d80 |

parent 13342 | 915d4d004643 |

child 13344 | c8eb3fbf4c0c |

*** empty log message ***

src/HOL/Lambda/Commutation.thy | file | annotate | diff | revisions | |

src/HOL/Relation.thy | file | annotate | diff | revisions |

1.1 --- a/src/HOL/Lambda/Commutation.thy Wed Jul 10 18:39:15 2002 +0200 1.2 +++ b/src/HOL/Lambda/Commutation.thy Thu Jul 11 09:17:01 2002 +0200 1.3 @@ -138,46 +138,48 @@ 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 "\<And>b c. (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>*" 1.14 - using wf 1.15 -proof induct 1.16 - case (less x b c) 1.17 - have xc: "(x, c) \<in> R\<^sup>*" . 1.18 - have xb: "(x, b) \<in> R\<^sup>*" . thus ?case 1.19 - proof (rule converse_rtranclE) 1.20 - assume "x = b" 1.21 - with xc have "(b, c) \<in> R\<^sup>*" by simp 1.22 - thus ?thesis by rules 1.23 - next 1.24 - fix y 1.25 - assume xy: "(x, y) \<in> R" 1.26 - assume yb: "(y, b) \<in> R\<^sup>*" 1.27 - from xc show ?thesis 1.28 + shows "(a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow> 1.29 + \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" (is "PROP ?conf b c") 1.30 +proof - 1.31 + from wf show "\<And>b c. PROP ?conf b c" 1.32 + proof induct 1.33 + case (less x b c) 1.34 + have xc: "(x, c) \<in> R\<^sup>*" . 1.35 + have xb: "(x, b) \<in> R\<^sup>*" . thus ?case 1.36 proof (rule converse_rtranclE) 1.37 - assume "x = c" 1.38 - with xb have "(c, b) \<in> R\<^sup>*" by simp 1.39 + assume "x = b" 1.40 + with xc have "(b, c) \<in> R\<^sup>*" by simp 1.41 thus ?thesis by rules 1.42 next 1.43 - fix y' 1.44 - assume y'c: "(y', c) \<in> R\<^sup>*" 1.45 - assume xy': "(x, y') \<in> R" 1.46 - with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc) 1.47 - then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules 1.48 - from xy have "(y, x) \<in> R\<inverse>" .. 1.49 - from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less) 1.50 - then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules 1.51 - from xy' have "(y', x) \<in> R\<inverse>" .. 1.52 - moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans) 1.53 - moreover note y'c 1.54 - ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less) 1.55 - then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules 1.56 - from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans) 1.57 - with cw show ?thesis by rules 1.58 + fix y 1.59 + assume xy: "(x, y) \<in> R" 1.60 + assume yb: "(y, b) \<in> R\<^sup>*" 1.61 + from xc show ?thesis 1.62 + proof (rule converse_rtranclE) 1.63 + assume "x = c" 1.64 + with xb have "(c, b) \<in> R\<^sup>*" by simp 1.65 + thus ?thesis by rules 1.66 + next 1.67 + fix y' 1.68 + assume y'c: "(y', c) \<in> R\<^sup>*" 1.69 + assume xy': "(x, y') \<in> R" 1.70 + with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc) 1.71 + then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules 1.72 + from xy[symmetric] yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" 1.73 + by (rule less) 1.74 + then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules 1.75 + note xy'[symmetric] 1.76 + moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans) 1.77 + moreover note y'c 1.78 + ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less) 1.79 + then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules 1.80 + from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans) 1.81 + with cw show ?thesis by rules 1.82 + qed 1.83 qed 1.84 qed 1.85 qed

2.1 --- a/src/HOL/Relation.thy Wed Jul 10 18:39:15 2002 +0200 2.2 +++ b/src/HOL/Relation.thy Thu Jul 11 09:17:01 2002 +0200 2.3 @@ -189,10 +189,10 @@ 2.4 lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)" 2.5 by (simp add: converse_def) 2.6 2.7 -lemma converseI: "(a, b) : r ==> (b, a) : r^-1" 2.8 +lemma converseI[sym]: "(a, b) : r ==> (b, a) : r^-1" 2.9 by (simp add: converse_def) 2.10 2.11 -lemma converseD: "(a,b) : r^-1 ==> (b, a) : r" 2.12 +lemma converseD[sym]: "(a,b) : r^-1 ==> (b, a) : r" 2.13 by (simp add: converse_def) 2.14 2.15 lemma converseE [elim!]: