*** empty log message ***
authornipkow
Thu Jul 11 09:17:01 2002 +0200 (2002-07-11)
changeset 133433b2b18c58d80
parent 13342 915d4d004643
child 13344 c8eb3fbf4c0c
*** empty log message ***
src/HOL/Lambda/Commutation.thy
src/HOL/Relation.thy
     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!]: