src/HOL/Lambda/Commutation.thy
changeset 17589 58eeffd73be1
parent 16417 9bc16273c2d4
child 18241 afdba6b3e383
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4    proof (rule converse_rtranclE)
     1.5      assume "x = b"
     1.6      with xc have "(b, c) \<in> R\<^sup>*" by simp
     1.7 -    thus ?thesis by rules
     1.8 +    thus ?thesis by iprover
     1.9    next
    1.10      fix y
    1.11      assume xy: "(x, y) \<in> R"
    1.12 @@ -163,23 +163,23 @@
    1.13      proof (rule converse_rtranclE)
    1.14        assume "x = c"
    1.15        with xb have "(c, b) \<in> R\<^sup>*" by simp
    1.16 -      thus ?thesis by rules
    1.17 +      thus ?thesis by iprover
    1.18      next
    1.19        fix y'
    1.20        assume y'c: "(y', c) \<in> R\<^sup>*"
    1.21        assume xy': "(x, y') \<in> R"
    1.22        with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
    1.23 -      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
    1.24 +      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
    1.25        from xy have "(y, x) \<in> R\<inverse>" ..
    1.26        from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
    1.27 -      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
    1.28 +      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
    1.29        from xy' have "(y', x) \<in> R\<inverse>" ..
    1.30        moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
    1.31        moreover note y'c
    1.32        ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
    1.33 -      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
    1.34 +      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
    1.35        from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
    1.36 -      with cw show ?thesis by rules
    1.37 +      with cw show ?thesis by iprover
    1.38      qed
    1.39    qed
    1.40  qed
    1.41 @@ -208,7 +208,7 @@
    1.42    proof (rule converse_rtranclE)
    1.43      assume "x = b"
    1.44      with xc have "(b, c) \<in> R\<^sup>*" by simp
    1.45 -    thus ?thesis by rules
    1.46 +    thus ?thesis by iprover
    1.47    next
    1.48      fix y
    1.49      assume xy: "(x, y) \<in> R"
    1.50 @@ -217,7 +217,7 @@
    1.51      proof (rule converse_rtranclE)
    1.52        assume "x = c"
    1.53        with xb have "(c, b) \<in> R\<^sup>*" by simp
    1.54 -      thus ?thesis by rules
    1.55 +      thus ?thesis by iprover
    1.56      next
    1.57        fix y'
    1.58        assume y'c: "(y', c) \<in> R\<^sup>*"