isabelle: src/HOL/Real.thy@894e82be8d05 (annotated)

28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 27964 diff changeset	1	theory Real
29197 6d4cb27ed19c adapted HOL source structure to distribution layout haftmann parents: 29108 diff changeset	2	imports RComplete RealVector
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 27964 diff changeset	3	begin
19640 40ec89317425 added Ferrante and Rackoff Algorithm -- by Amine Chaieb; wenzelm parents: 19023 diff changeset	4
32877 6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	5	lemma field_le_epsilon:
35028 108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS haftmann parents: 32877 diff changeset	6	fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}"
32877 6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	7	assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	8	shows "x \<le> y"
6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	9	proof (rule ccontr)
6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	10	assume xy: "\<not> x \<le> y"
6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	11	hence "(x-y)/2 > 0"
35066 894e82be8d05 simple proofs make life faster and easier haftmann parents: 35028 diff changeset	12	by simp
32877 6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	13	hence "x \<le> y + (x - y) / 2"
6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	14	by (rule e [of "(x-y)/2"])
6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	15	also have "... = (x - y + 2*y)/2"
35066 894e82be8d05 simple proofs make life faster and easier haftmann parents: 35028 diff changeset	16	by (simp add: diff_divide_distrib)
32877 6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	17	also have "... = (x + y) / 2"
35066 894e82be8d05 simple proofs make life faster and easier haftmann parents: 35028 diff changeset	18	by simp
32877 6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	19	also have "... < x" using xy
35066 894e82be8d05 simple proofs make life faster and easier haftmann parents: 35028 diff changeset	20	by simp
32877 6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	21	finally have "x<x" .
6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	22	thus False
35066 894e82be8d05 simple proofs make life faster and easier haftmann parents: 35028 diff changeset	23	by simp
32877 6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	24	qed
6f09346c7c08 New lemmas connected with the reals and infinite series paulson parents: 29197 diff changeset	25
19640 40ec89317425 added Ferrante and Rackoff Algorithm -- by Amine Chaieb; wenzelm parents: 19023 diff changeset	26	end

author	haftmann
	Tue, 09 Feb 2010 16:07:09 +0100
changeset 35066	894e82be8d05
parent 35028	108662d50512
child 35090	88cc65ae046e
permissions	-rw-r--r--