equal
deleted
inserted
replaced
5 Description : The positive reals as Dedekind sections of positive |
5 Description : The positive reals as Dedekind sections of positive |
6 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
6 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
7 provides some of the definitions. |
7 provides some of the definitions. |
8 *) |
8 *) |
9 |
9 |
10 theory PReal = Rational: |
10 theory PReal |
|
11 import Rational |
|
12 begin |
11 |
13 |
12 text{*Could be generalized and moved to @{text Ring_and_Field}*} |
14 text{*Could be generalized and moved to @{text Ring_and_Field}*} |
13 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
15 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
14 by (rule_tac x="b-a" in exI, simp) |
16 by (rule_tac x="b-a" in exI, simp) |
15 |
17 |