equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 header {* Positive real numbers *} |
9 header {* Positive real numbers *} |
10 |
10 |
11 theory PReal |
11 theory PReal |
12 imports Rational Dense_Linear_Order |
12 imports Rational |
13 begin |
13 begin |
14 |
14 |
15 text{*Could be generalized and moved to @{text Ring_and_Field}*} |
15 text{*Could be generalized and moved to @{text Ring_and_Field}*} |
16 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
16 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
17 by (rule_tac x="b-a" in exI, simp) |
17 by (rule_tac x="b-a" in exI, simp) |
19 definition |
19 definition |
20 cut :: "rat set => bool" where |
20 cut :: "rat set => bool" where |
21 [code del]: "cut A = ({} \<subset> A & |
21 [code del]: "cut A = ({} \<subset> A & |
22 A < {r. 0 < r} & |
22 A < {r. 0 < r} & |
23 (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))" |
23 (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))" |
|
24 |
|
25 lemma interval_empty_iff: |
|
26 "{y. (x::'a::dense_linear_order) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z" |
|
27 by (auto dest: dense) |
|
28 |
24 |
29 |
25 lemma cut_of_rat: |
30 lemma cut_of_rat: |
26 assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A") |
31 assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A") |
27 proof - |
32 proof - |
28 from q have pos: "?A < {r. 0 < r}" by force |
33 from q have pos: "?A < {r. 0 < r}" by force |