equal
deleted
inserted
replaced
1 (* Title : PReal.thy |
1 (* Title : PReal.thy |
2 ID : $Id$ |
|
3 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
4 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
5 Description : The positive reals as Dedekind sections of positive |
4 Description : The positive reals as Dedekind sections of positive |
6 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
5 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
7 provides some of the definitions. |
6 provides some of the definitions. |
8 *) |
7 *) |
9 |
8 |
10 header {* Positive real numbers *} |
9 header {* Positive real numbers *} |
11 |
10 |
12 theory PReal |
11 theory PReal |
13 imports Rational Dense_Linear_Order |
12 imports Rational "~~/src/HOL/Library/Dense_Linear_Order" |
14 begin |
13 begin |
15 |
14 |
16 text{*Could be generalized and moved to @{text Ring_and_Field}*} |
15 text{*Could be generalized and moved to @{text Ring_and_Field}*} |
17 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
16 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
18 by (rule_tac x="b-a" in exI, simp) |
17 by (rule_tac x="b-a" in exI, simp) |