summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Real.thy

author | haftmann |

Tue, 09 Feb 2010 16:07:09 +0100 | |

changeset 35066 | 894e82be8d05 |

parent 35028 | 108662d50512 |

child 35090 | 88cc65ae046e |

permissions | -rw-r--r-- |

simple proofs make life faster and easier

theory Real imports RComplete RealVector begin lemma field_le_epsilon: fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}" assumes e: "(!!e. 0 < e ==> x \<le> y + e)" shows "x \<le> y" proof (rule ccontr) assume xy: "\<not> x \<le> y" hence "(x-y)/2 > 0" by simp hence "x \<le> y + (x - y) / 2" by (rule e [of "(x-y)/2"]) also have "... = (x - y + 2*y)/2" by (simp add: diff_divide_distrib) also have "... = (x + y) / 2" by simp also have "... < x" using xy by simp finally have "x<x" . thus False by simp qed end