author | wenzelm |
Sun, 26 Aug 2012 21:46:50 +0200 | |
changeset 48927 | ef462b5558eb |
parent 47596 | c031e65c8ddc |
child 49962 | a8cc904a6820 |
permissions | -rw-r--r-- |
30122 | 1 |
(* Title: HOL/RComplete.thy |
2 |
Author: Jacques D. Fleuriot, University of Edinburgh |
|
3 |
Author: Larry Paulson, University of Cambridge |
|
4 |
Author: Jeremy Avigad, Carnegie Mellon University |
|
5 |
Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen |
|
16893 | 6 |
*) |
5078 | 7 |
|
16893 | 8 |
header {* Completeness of the Reals; Floor and Ceiling Functions *} |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
9 |
|
15131 | 10 |
theory RComplete |
15140 | 11 |
imports Lubs RealDef |
15131 | 12 |
begin |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
13 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
14 |
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" |
16893 | 15 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
16 |
|
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
30242
diff
changeset
|
17 |
lemma abs_diff_less_iff: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32960
diff
changeset
|
18 |
"(\<bar>x - a\<bar> < (r::'a::linordered_idom)) = (a - r < x \<and> x < a + r)" |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
30242
diff
changeset
|
19 |
by auto |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
20 |
|
16893 | 21 |
subsection {* Completeness of Positive Reals *} |
22 |
||
23 |
text {* |
|
24 |
Supremum property for the set of positive reals |
|
25 |
||
26 |
Let @{text "P"} be a non-empty set of positive reals, with an upper |
|
27 |
bound @{text "y"}. Then @{text "P"} has a least upper bound |
|
28 |
(written @{text "S"}). |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
29 |
|
16893 | 30 |
FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}? |
31 |
*} |
|
32 |
||
36795
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
33 |
text {* Only used in HOL/Import/HOL4Compat.thy; delete? *} |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
34 |
|
16893 | 35 |
lemma posreal_complete: |
44690
b6d8b11ed399
remove unused assumption from lemma posreal_complete
huffman
parents:
44679
diff
changeset
|
36 |
fixes P :: "real set" |
b6d8b11ed399
remove unused assumption from lemma posreal_complete
huffman
parents:
44679
diff
changeset
|
37 |
assumes not_empty_P: "\<exists>x. x \<in> P" |
16893 | 38 |
and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y" |
39 |
shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)" |
|
36795
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
40 |
proof - |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
41 |
from upper_bound_Ex have "\<exists>z. \<forall>x\<in>P. x \<le> z" |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
42 |
by (auto intro: less_imp_le) |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
43 |
from complete_real [OF not_empty_P this] obtain S |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
44 |
where S1: "\<And>x. x \<in> P \<Longrightarrow> x \<le> S" and S2: "\<And>z. \<forall>x\<in>P. x \<le> z \<Longrightarrow> S \<le> z" by fast |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
45 |
have "\<forall>y. (\<exists>x \<in> P. y < x) = (y < S)" |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
46 |
proof |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
47 |
fix y show "(\<exists>x\<in>P. y < x) = (y < S)" |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
48 |
apply (cases "\<exists>x\<in>P. y < x", simp_all) |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
49 |
apply (clarify, drule S1, simp) |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
50 |
apply (simp add: not_less S2) |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
51 |
done |
16893 | 52 |
qed |
36795
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
53 |
thus ?thesis .. |
16893 | 54 |
qed |
55 |
||
56 |
text {* |
|
57 |
\medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc. |
|
58 |
*} |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
59 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
60 |
lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)" |
16893 | 61 |
apply (frule isLub_isUb) |
62 |
apply (frule_tac x = y in isLub_isUb) |
|
63 |
apply (blast intro!: order_antisym dest!: isLub_le_isUb) |
|
64 |
done |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
65 |
|
5078 | 66 |
|
16893 | 67 |
text {* |
68 |
\medskip reals Completeness (again!) |
|
69 |
*} |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
70 |
|
16893 | 71 |
lemma reals_complete: |
72 |
assumes notempty_S: "\<exists>X. X \<in> S" |
|
73 |
and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y" |
|
74 |
shows "\<exists>t. isLub (UNIV :: real set) S t" |
|
75 |
proof - |
|
36795
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
76 |
from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y" |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
77 |
unfolding isUb_def setle_def by simp_all |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
78 |
from complete_real [OF this] show ?thesis |
45966 | 79 |
by (simp add: isLub_def leastP_def isUb_def setle_def setge_def) |
16893 | 80 |
qed |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
81 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
82 |
|
16893 | 83 |
subsection {* The Archimedean Property of the Reals *} |
84 |
||
85 |
theorem reals_Archimedean: |
|
86 |
assumes x_pos: "0 < x" |
|
87 |
shows "\<exists>n. inverse (real (Suc n)) < x" |
|
36795
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
88 |
unfolding real_of_nat_def using x_pos |
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
89 |
by (rule ex_inverse_of_nat_Suc_less) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
90 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
91 |
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)" |
36795
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
35578
diff
changeset
|
92 |
unfolding real_of_nat_def by (rule ex_less_of_nat) |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
93 |
|
16893 | 94 |
lemma reals_Archimedean3: |
95 |
assumes x_greater_zero: "0 < x" |
|
96 |
shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
97 |
unfolding real_of_nat_def using `0 < x` |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
98 |
by (auto intro: ex_less_of_nat_mult) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
99 |
|
16819 | 100 |
|
28091
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
101 |
subsection{*Density of the Rational Reals in the Reals*} |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
102 |
|
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
103 |
text{* This density proof is due to Stefan Richter and was ported by TN. The |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
104 |
original source is \emph{Real Analysis} by H.L. Royden. |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
105 |
It employs the Archimedean property of the reals. *} |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
106 |
|
44668 | 107 |
lemma Rats_dense_in_real: |
108 |
fixes x :: real |
|
109 |
assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y" |
|
28091
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
110 |
proof - |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
111 |
from `x<y` have "0 < y-x" by simp |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
112 |
with reals_Archimedean obtain q::nat |
44668 | 113 |
where q: "inverse (real q) < y-x" and "0 < q" by auto |
114 |
def p \<equiv> "ceiling (y * real q) - 1" |
|
115 |
def r \<equiv> "of_int p / real q" |
|
116 |
from q have "x < y - inverse (real q)" by simp |
|
117 |
also have "y - inverse (real q) \<le> r" |
|
118 |
unfolding r_def p_def |
|
119 |
by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`) |
|
120 |
finally have "x < r" . |
|
121 |
moreover have "r < y" |
|
122 |
unfolding r_def p_def |
|
123 |
by (simp add: divide_less_eq diff_less_eq `0 < q` |
|
124 |
less_ceiling_iff [symmetric]) |
|
125 |
moreover from r_def have "r \<in> \<rat>" by simp |
|
28091
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
126 |
ultimately show ?thesis by fast |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
127 |
qed |
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
128 |
|
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset
|
129 |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
130 |
subsection{*Floor and Ceiling Functions from the Reals to the Integers*} |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
131 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
132 |
(* FIXME: theorems for negative numerals *) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
133 |
lemma numeral_less_real_of_int_iff [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
134 |
"((numeral n) < real (m::int)) = (numeral n < m)" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
135 |
apply auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
136 |
apply (rule real_of_int_less_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
137 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
138 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
139 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
140 |
lemma numeral_less_real_of_int_iff2 [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
141 |
"(real (m::int) < (numeral n)) = (m < numeral n)" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
142 |
apply auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
143 |
apply (rule real_of_int_less_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
144 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
145 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
146 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
147 |
lemma numeral_le_real_of_int_iff [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
148 |
"((numeral n) \<le> real (m::int)) = (numeral n \<le> m)" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
149 |
by (simp add: linorder_not_less [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
150 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
151 |
lemma numeral_le_real_of_int_iff2 [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
152 |
"(real (m::int) \<le> (numeral n)) = (m \<le> numeral n)" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
153 |
by (simp add: linorder_not_less [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
154 |
|
24355 | 155 |
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
156 |
unfolding real_of_nat_def by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
157 |
|
24355 | 158 |
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n" |
30102 | 159 |
unfolding real_of_nat_def by (simp add: floor_minus) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
160 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
161 |
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
162 |
unfolding real_of_int_def by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
163 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
164 |
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n" |
30102 | 165 |
unfolding real_of_int_def by (simp add: floor_minus) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
166 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
167 |
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
168 |
unfolding real_of_int_def by (rule floor_exists) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
169 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
170 |
lemma lemma_floor: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
171 |
assumes a1: "real m \<le> r" and a2: "r < real n + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
172 |
shows "m \<le> (n::int)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
173 |
proof - |
23389 | 174 |
have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans) |
175 |
also have "... = real (n + 1)" by simp |
|
176 |
finally have "m < n + 1" by (simp only: real_of_int_less_iff) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
177 |
thus ?thesis by arith |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
178 |
qed |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
179 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
180 |
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
181 |
unfolding real_of_int_def by (rule of_int_floor_le) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
182 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
183 |
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
184 |
by (auto intro: lemma_floor) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
185 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
186 |
lemma real_of_int_floor_cancel [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
187 |
"(real (floor x) = x) = (\<exists>n::int. x = real n)" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
188 |
using floor_real_of_int by metis |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
189 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
190 |
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
191 |
unfolding real_of_int_def using floor_unique [of n x] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
192 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
193 |
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
194 |
unfolding real_of_int_def by (rule floor_unique) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
195 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
196 |
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
197 |
apply (rule inj_int [THEN injD]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
198 |
apply (simp add: real_of_nat_Suc) |
15539 | 199 |
apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"]) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
200 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
201 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
202 |
lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
203 |
apply (drule order_le_imp_less_or_eq) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
204 |
apply (auto intro: floor_eq3) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
205 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
206 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
207 |
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
208 |
unfolding real_of_int_def using floor_correct [of r] by simp |
16819 | 209 |
|
210 |
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
211 |
unfolding real_of_int_def using floor_correct [of r] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
212 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
213 |
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
214 |
unfolding real_of_int_def using floor_correct [of r] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
215 |
|
16819 | 216 |
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
217 |
unfolding real_of_int_def using floor_correct [of r] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
218 |
|
16819 | 219 |
lemma le_floor: "real a <= x ==> a <= floor x" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
220 |
unfolding real_of_int_def by (simp add: le_floor_iff) |
16819 | 221 |
|
222 |
lemma real_le_floor: "a <= floor x ==> real a <= x" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
223 |
unfolding real_of_int_def by (simp add: le_floor_iff) |
16819 | 224 |
|
225 |
lemma le_floor_eq: "(a <= floor x) = (real a <= x)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
226 |
unfolding real_of_int_def by (rule le_floor_iff) |
16819 | 227 |
|
228 |
lemma floor_less_eq: "(floor x < a) = (x < real a)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
229 |
unfolding real_of_int_def by (rule floor_less_iff) |
16819 | 230 |
|
231 |
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
232 |
unfolding real_of_int_def by (rule less_floor_iff) |
16819 | 233 |
|
234 |
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
235 |
unfolding real_of_int_def by (rule floor_le_iff) |
16819 | 236 |
|
237 |
lemma floor_add [simp]: "floor (x + real a) = floor x + a" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
238 |
unfolding real_of_int_def by (rule floor_add_of_int) |
16819 | 239 |
|
240 |
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
241 |
unfolding real_of_int_def by (rule floor_diff_of_int) |
16819 | 242 |
|
35578
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
243 |
lemma le_mult_floor: |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
244 |
assumes "0 \<le> (a :: real)" and "0 \<le> b" |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
245 |
shows "floor a * floor b \<le> floor (a * b)" |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
246 |
proof - |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
247 |
have "real (floor a) \<le> a" |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
248 |
and "real (floor b) \<le> b" by auto |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
249 |
hence "real (floor a * floor b) \<le> a * b" |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
250 |
using assms by (auto intro!: mult_mono) |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
251 |
also have "a * b < real (floor (a * b) + 1)" by auto |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
252 |
finally show ?thesis unfolding real_of_int_less_iff by simp |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
253 |
qed |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
254 |
|
47596 | 255 |
lemma floor_divide_eq_div: |
256 |
"floor (real a / real b) = a div b" |
|
257 |
proof cases |
|
258 |
assume "b \<noteq> 0 \<or> b dvd a" |
|
259 |
with real_of_int_div3[of a b] show ?thesis |
|
260 |
by (auto simp: real_of_int_div[symmetric] intro!: floor_eq2 real_of_int_div4 neq_le_trans) |
|
261 |
(metis add_left_cancel zero_neq_one real_of_int_div_aux real_of_int_inject |
|
262 |
real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial) |
|
263 |
qed (auto simp: real_of_int_div) |
|
264 |
||
24355 | 265 |
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
266 |
unfolding real_of_nat_def by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
267 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
268 |
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
269 |
unfolding real_of_int_def by (rule le_of_int_ceiling) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
270 |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
271 |
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
272 |
unfolding real_of_int_def by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
273 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
274 |
lemma real_of_int_ceiling_cancel [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
275 |
"(real (ceiling x) = x) = (\<exists>n::int. x = real n)" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
276 |
using ceiling_real_of_int by metis |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
277 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
278 |
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
279 |
unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
280 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
281 |
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
282 |
unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
283 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
284 |
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n |] ==> ceiling x = n" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
285 |
unfolding real_of_int_def using ceiling_unique [of n x] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
286 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
287 |
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
288 |
unfolding real_of_int_def using ceiling_correct [of r] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
289 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
290 |
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
291 |
unfolding real_of_int_def using ceiling_correct [of r] by simp |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
292 |
|
16819 | 293 |
lemma ceiling_le: "x <= real a ==> ceiling x <= a" |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
294 |
unfolding real_of_int_def by (simp add: ceiling_le_iff) |
16819 | 295 |
|
296 |
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
297 |
unfolding real_of_int_def by (simp add: ceiling_le_iff) |
16819 | 298 |
|
299 |
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
300 |
unfolding real_of_int_def by (rule ceiling_le_iff) |
16819 | 301 |
|
302 |
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
303 |
unfolding real_of_int_def by (rule less_ceiling_iff) |
16819 | 304 |
|
305 |
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
306 |
unfolding real_of_int_def by (rule ceiling_less_iff) |
16819 | 307 |
|
308 |
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
309 |
unfolding real_of_int_def by (rule le_ceiling_iff) |
16819 | 310 |
|
311 |
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
312 |
unfolding real_of_int_def by (rule ceiling_add_of_int) |
16819 | 313 |
|
314 |
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a" |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset
|
315 |
unfolding real_of_int_def by (rule ceiling_diff_of_int) |
16819 | 316 |
|
317 |
||
318 |
subsection {* Versions for the natural numbers *} |
|
319 |
||
19765 | 320 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
321 |
natfloor :: "real => nat" where |
19765 | 322 |
"natfloor x = nat(floor x)" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
323 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
324 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
325 |
natceiling :: "real => nat" where |
19765 | 326 |
"natceiling x = nat(ceiling x)" |
16819 | 327 |
|
328 |
lemma natfloor_zero [simp]: "natfloor 0 = 0" |
|
329 |
by (unfold natfloor_def, simp) |
|
330 |
||
331 |
lemma natfloor_one [simp]: "natfloor 1 = 1" |
|
332 |
by (unfold natfloor_def, simp) |
|
333 |
||
334 |
lemma zero_le_natfloor [simp]: "0 <= natfloor x" |
|
335 |
by (unfold natfloor_def, simp) |
|
336 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
337 |
lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n" |
16819 | 338 |
by (unfold natfloor_def, simp) |
339 |
||
340 |
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n" |
|
341 |
by (unfold natfloor_def, simp) |
|
342 |
||
343 |
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x" |
|
344 |
by (unfold natfloor_def, simp) |
|
345 |
||
346 |
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0" |
|
44679 | 347 |
unfolding natfloor_def by simp |
348 |
||
16819 | 349 |
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y" |
44679 | 350 |
unfolding natfloor_def by (intro nat_mono floor_mono) |
16819 | 351 |
|
352 |
lemma le_natfloor: "real x <= a ==> x <= natfloor a" |
|
353 |
apply (unfold natfloor_def) |
|
354 |
apply (subst nat_int [THEN sym]) |
|
44679 | 355 |
apply (rule nat_mono) |
16819 | 356 |
apply (rule le_floor) |
357 |
apply simp |
|
358 |
done |
|
359 |
||
44679 | 360 |
lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n" |
361 |
unfolding natfloor_def real_of_nat_def |
|
362 |
by (simp add: nat_less_iff floor_less_iff) |
|
363 |
||
35578
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
364 |
lemma less_natfloor: |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
365 |
assumes "0 \<le> x" and "x < real (n :: nat)" |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
366 |
shows "natfloor x < n" |
44679 | 367 |
using assms by (simp add: natfloor_less_iff) |
35578
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
368 |
|
16819 | 369 |
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)" |
370 |
apply (rule iffI) |
|
371 |
apply (rule order_trans) |
|
372 |
prefer 2 |
|
373 |
apply (erule real_natfloor_le) |
|
374 |
apply (subst real_of_nat_le_iff) |
|
375 |
apply assumption |
|
376 |
apply (erule le_natfloor) |
|
377 |
done |
|
378 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
379 |
lemma le_natfloor_eq_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
380 |
"~ neg((numeral n)::int) ==> 0 <= x ==> |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
381 |
(numeral n <= natfloor x) = (numeral n <= x)" |
16819 | 382 |
apply (subst le_natfloor_eq, assumption) |
383 |
apply simp |
|
384 |
done |
|
385 |
||
16820 | 386 |
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" |
16819 | 387 |
apply (case_tac "0 <= x") |
388 |
apply (subst le_natfloor_eq, assumption, simp) |
|
389 |
apply (rule iffI) |
|
16893 | 390 |
apply (subgoal_tac "natfloor x <= natfloor 0") |
16819 | 391 |
apply simp |
392 |
apply (rule natfloor_mono) |
|
393 |
apply simp |
|
394 |
apply simp |
|
395 |
done |
|
396 |
||
397 |
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n" |
|
44679 | 398 |
unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"]) |
16819 | 399 |
|
400 |
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1" |
|
401 |
apply (case_tac "0 <= x") |
|
402 |
apply (unfold natfloor_def) |
|
403 |
apply simp |
|
404 |
apply simp_all |
|
405 |
done |
|
406 |
||
407 |
lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)" |
|
29667 | 408 |
using real_natfloor_add_one_gt by (simp add: algebra_simps) |
16819 | 409 |
|
410 |
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" |
|
411 |
apply (subgoal_tac "z < real(natfloor z) + 1") |
|
412 |
apply arith |
|
413 |
apply (rule real_natfloor_add_one_gt) |
|
414 |
done |
|
415 |
||
416 |
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a" |
|
44679 | 417 |
unfolding natfloor_def |
418 |
unfolding real_of_int_of_nat_eq [symmetric] floor_add |
|
419 |
by (simp add: nat_add_distrib) |
|
16819 | 420 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
421 |
lemma natfloor_add_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
422 |
"~neg ((numeral n)::int) ==> 0 <= x ==> |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
423 |
natfloor (x + numeral n) = natfloor x + numeral n" |
44679 | 424 |
by (simp add: natfloor_add [symmetric]) |
16819 | 425 |
|
426 |
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1" |
|
44679 | 427 |
by (simp add: natfloor_add [symmetric] del: One_nat_def) |
16819 | 428 |
|
46671 | 429 |
lemma natfloor_subtract [simp]: |
430 |
"natfloor(x - real a) = natfloor x - a" |
|
431 |
unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract |
|
44679 | 432 |
by simp |
16819 | 433 |
|
41550 | 434 |
lemma natfloor_div_nat: |
435 |
assumes "1 <= x" and "y > 0" |
|
436 |
shows "natfloor (x / real y) = natfloor x div y" |
|
44679 | 437 |
proof (rule natfloor_eq) |
438 |
have "(natfloor x) div y * y \<le> natfloor x" |
|
439 |
by (rule add_leD1 [where k="natfloor x mod y"], simp) |
|
440 |
thus "real (natfloor x div y) \<le> x / real y" |
|
441 |
using assms by (simp add: le_divide_eq le_natfloor_eq) |
|
442 |
have "natfloor x < (natfloor x) div y * y + y" |
|
443 |
apply (subst mod_div_equality [symmetric]) |
|
444 |
apply (rule add_strict_left_mono) |
|
445 |
apply (rule mod_less_divisor) |
|
446 |
apply fact |
|
35578
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
447 |
done |
44679 | 448 |
thus "x / real y < real (natfloor x div y) + 1" |
449 |
using assms |
|
450 |
by (simp add: divide_less_eq natfloor_less_iff left_distrib) |
|
35578
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
451 |
qed |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
452 |
|
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
453 |
lemma le_mult_natfloor: |
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
454 |
shows "natfloor a * natfloor b \<le> natfloor (a * b)" |
46671 | 455 |
by (cases "0 <= a & 0 <= b") |
456 |
(auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg) |
|
35578
384ad08a1d1b
Added natfloor and floor rules for multiplication and power.
hoelzl
parents:
35028
diff
changeset
|
457 |
|
16819 | 458 |
lemma natceiling_zero [simp]: "natceiling 0 = 0" |
459 |
by (unfold natceiling_def, simp) |
|
460 |
||
461 |
lemma natceiling_one [simp]: "natceiling 1 = 1" |
|
462 |
by (unfold natceiling_def, simp) |
|
463 |
||
464 |
lemma zero_le_natceiling [simp]: "0 <= natceiling x" |
|
465 |
by (unfold natceiling_def, simp) |
|
466 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
467 |
lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n" |
16819 | 468 |
by (unfold natceiling_def, simp) |
469 |
||
470 |
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n" |
|
471 |
by (unfold natceiling_def, simp) |
|
472 |
||
473 |
lemma real_natceiling_ge: "x <= real(natceiling x)" |
|
44679 | 474 |
unfolding natceiling_def by (cases "x < 0", simp_all) |
16819 | 475 |
|
476 |
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0" |
|
44679 | 477 |
unfolding natceiling_def by simp |
16819 | 478 |
|
479 |
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y" |
|
44679 | 480 |
unfolding natceiling_def by (intro nat_mono ceiling_mono) |
481 |
||
16819 | 482 |
lemma natceiling_le: "x <= real a ==> natceiling x <= a" |
44679 | 483 |
unfolding natceiling_def real_of_nat_def |
484 |
by (simp add: nat_le_iff ceiling_le_iff) |
|
16819 | 485 |
|
44708 | 486 |
lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)" |
487 |
unfolding natceiling_def real_of_nat_def |
|
44679 | 488 |
by (simp add: nat_le_iff ceiling_le_iff) |
16819 | 489 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
490 |
lemma natceiling_le_eq_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
491 |
"~ neg((numeral n)::int) ==> |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
492 |
(natceiling x <= numeral n) = (x <= numeral n)" |
44679 | 493 |
by (simp add: natceiling_le_eq) |
16819 | 494 |
|
16820 | 495 |
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" |
44679 | 496 |
unfolding natceiling_def |
497 |
by (simp add: nat_le_iff ceiling_le_iff) |
|
16819 | 498 |
|
499 |
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1" |
|
44679 | 500 |
unfolding natceiling_def |
501 |
by (simp add: ceiling_eq2 [where n="int n"]) |
|
16819 | 502 |
|
16893 | 503 |
lemma natceiling_add [simp]: "0 <= x ==> |
16819 | 504 |
natceiling (x + real a) = natceiling x + a" |
44679 | 505 |
unfolding natceiling_def |
506 |
unfolding real_of_int_of_nat_eq [symmetric] ceiling_add |
|
507 |
by (simp add: nat_add_distrib) |
|
16819 | 508 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
509 |
lemma natceiling_add_numeral [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
510 |
"~ neg ((numeral n)::int) ==> 0 <= x ==> |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46671
diff
changeset
|
511 |
natceiling (x + numeral n) = natceiling x + numeral n" |
44679 | 512 |
by (simp add: natceiling_add [symmetric]) |
16819 | 513 |
|
514 |
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1" |
|
44679 | 515 |
by (simp add: natceiling_add [symmetric] del: One_nat_def) |
16819 | 516 |
|
46671 | 517 |
lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a" |
518 |
unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract |
|
44679 | 519 |
by simp |
16819 | 520 |
|
36826
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
521 |
subsection {* Exponentiation with floor *} |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
522 |
|
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
523 |
lemma floor_power: |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
524 |
assumes "x = real (floor x)" |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
525 |
shows "floor (x ^ n) = floor x ^ n" |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
526 |
proof - |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
527 |
have *: "x ^ n = real (floor x ^ n)" |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
528 |
using assms by (induct n arbitrary: x) simp_all |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
529 |
show ?thesis unfolding real_of_int_inject[symmetric] |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
530 |
unfolding * floor_real_of_int .. |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
531 |
qed |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
532 |
|
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
533 |
lemma natfloor_power: |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
534 |
assumes "x = real (natfloor x)" |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
535 |
shows "natfloor (x ^ n) = natfloor x ^ n" |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
536 |
proof - |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
537 |
from assms have "0 \<le> floor x" by auto |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
538 |
note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]] |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
539 |
from floor_power[OF this] |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
540 |
show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric] |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
541 |
by simp |
4d4462d644ae
move floor lemmas from RealPow.thy to RComplete.thy
huffman
parents:
36795
diff
changeset
|
542 |
qed |
16819 | 543 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
544 |
end |