summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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>*"