--- a/src/HOL/Lambda/Commutation.thy Wed Jul 10 18:39:15 2002 +0200
+++ b/src/HOL/Lambda/Commutation.thy Thu Jul 11 09:17:01 2002 +0200
@@ -138,46 +138,48 @@
subsection {* Newman's lemma *}
-theorem Newman:
+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 "\<And>b c. (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>*"
- using wf
-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
+ 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 = c"
- with xb have "(c, b) \<in> R\<^sup>*" by simp
+ assume "x = b"
+ with xc have "(b, c) \<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
+ 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[symmetric] 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
+ note xy'[symmetric]
+ 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
--- a/src/HOL/Relation.thy Wed Jul 10 18:39:15 2002 +0200
+++ b/src/HOL/Relation.thy Thu Jul 11 09:17:01 2002 +0200
@@ -189,10 +189,10 @@
lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
by (simp add: converse_def)
-lemma converseI: "(a, b) : r ==> (b, a) : r^-1"
+lemma converseI[sym]: "(a, b) : r ==> (b, a) : r^-1"
by (simp add: converse_def)
-lemma converseD: "(a,b) : r^-1 ==> (b, a) : r"
+lemma converseD[sym]: "(a,b) : r^-1 ==> (b, a) : r"
by (simp add: converse_def)
lemma converseE [elim!]: