author | avigad |
Wed, 13 Jul 2005 20:02:54 +0200 | |
changeset 16820 | 5c9d597e4cb9 |
parent 16819 | 00d8f9300d13 |
child 16827 | c90a1f450327 |
permissions | -rw-r--r-- |
5078 | 1 |
(* Title : RComplete.thy |
7219 | 2 |
ID : $Id$ |
5078 | 3 |
Author : Jacques D. Fleuriot |
16819 | 4 |
Converted to Isar and polished by lcp |
5 |
Most floor and ceiling lemmas by Jeremy Avigad |
|
5078 | 6 |
Copyright : 1998 University of Cambridge |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
7 |
Copyright : 2001,2002 University of Edinburgh |
5078 | 8 |
*) |
9 |
||
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
10 |
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
|
11 |
|
15131 | 12 |
theory RComplete |
15140 | 13 |
imports Lubs RealDef |
15131 | 14 |
begin |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
15 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
16 |
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset
|
17 |
by simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
18 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
19 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
20 |
subsection{*Completeness of Reals by Supremum Property of type @{typ preal}*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
21 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
22 |
(*a few lemmas*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
23 |
lemma real_sup_lemma1: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
24 |
"\<forall>x \<in> P. 0 < x ==> |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
25 |
((\<exists>x \<in> P. y < x) = (\<exists>X. real_of_preal X \<in> P & y < real_of_preal X))" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
26 |
by (blast dest!: bspec real_gt_zero_preal_Ex [THEN iffD1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
27 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
28 |
lemma real_sup_lemma2: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
29 |
"[| \<forall>x \<in> P. 0 < x; a \<in> P; \<forall>x \<in> P. x < y |] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
30 |
==> (\<exists>X. X\<in> {w. real_of_preal w \<in> P}) & |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
31 |
(\<exists>Y. \<forall>X\<in> {w. real_of_preal w \<in> P}. X < Y)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
32 |
apply (rule conjI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
33 |
apply (blast dest: bspec real_gt_zero_preal_Ex [THEN iffD1], auto) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
34 |
apply (drule bspec, assumption) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
35 |
apply (frule bspec, assumption) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
36 |
apply (drule order_less_trans, assumption) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset
|
37 |
apply (drule real_gt_zero_preal_Ex [THEN iffD1], force) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
38 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
39 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
40 |
(*------------------------------------------------------------- |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
41 |
Completeness of Positive Reals |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
42 |
-------------------------------------------------------------*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
43 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
44 |
(** |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
45 |
Supremum property for the set of positive reals |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
46 |
FIXME: long proof - should be improved |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
47 |
**) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
48 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
49 |
(*Let P be a non-empty set of positive reals, with an upper bound y. |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
50 |
Then P has a least upper bound (written S). |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
51 |
FIXME: Can the premise be weakened to \<forall>x \<in> P. x\<le> y ??*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
52 |
lemma posreal_complete: "[| \<forall>x \<in> P. (0::real) < x; \<exists>x. x \<in> P; \<exists>y. \<forall>x \<in> P. x<y |] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
53 |
==> (\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S))" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
54 |
apply (rule_tac x = "real_of_preal (psup ({w. real_of_preal w \<in> P}))" in exI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
55 |
apply clarify |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
56 |
apply (case_tac "0 < ya", auto) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
57 |
apply (frule real_sup_lemma2, assumption+) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
58 |
apply (drule real_gt_zero_preal_Ex [THEN iffD1]) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset
|
59 |
apply (drule_tac [3] real_less_all_real2, auto) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
60 |
apply (rule preal_complete [THEN iffD1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
61 |
apply (auto intro: order_less_imp_le) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset
|
62 |
apply (frule real_gt_preal_preal_Ex, force) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
63 |
(* second part *) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
64 |
apply (rule real_sup_lemma1 [THEN iffD2], assumption) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
65 |
apply (auto dest!: real_less_all_real2 real_gt_zero_preal_Ex [THEN iffD1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
66 |
apply (frule_tac [2] real_sup_lemma2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
67 |
apply (frule real_sup_lemma2, assumption+, clarify) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
68 |
apply (rule preal_complete [THEN iffD2, THEN bexE]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
69 |
prefer 3 apply blast |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
70 |
apply (blast intro!: order_less_imp_le)+ |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
71 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
72 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
73 |
(*-------------------------------------------------------- |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
74 |
Completeness properties using isUb, isLub etc. |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
75 |
-------------------------------------------------------*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
76 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
77 |
lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
78 |
apply (frule isLub_isUb) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
79 |
apply (frule_tac x = y in isLub_isUb) |
14476 | 80 |
apply (blast intro!: order_antisym dest!: isLub_le_isUb) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
81 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
82 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
83 |
lemma real_order_restrict: "[| (x::real) <=* S'; S <= S' |] ==> x <=* S" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
84 |
by (unfold setle_def setge_def, blast) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
85 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
86 |
(*---------------------------------------------------------------- |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
87 |
Completeness theorem for the positive reals(again) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
88 |
----------------------------------------------------------------*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
89 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
90 |
lemma posreals_complete: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
91 |
"[| \<forall>x \<in>S. 0 < x; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
92 |
\<exists>x. x \<in>S; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
93 |
\<exists>u. isUb (UNIV::real set) S u |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
94 |
|] ==> \<exists>t. isLub (UNIV::real set) S t" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
95 |
apply (rule_tac x = "real_of_preal (psup ({w. real_of_preal w \<in> S}))" in exI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
96 |
apply (auto simp add: isLub_def leastP_def isUb_def) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
97 |
apply (auto intro!: setleI setgeI dest!: real_gt_zero_preal_Ex [THEN iffD1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
98 |
apply (frule_tac x = y in bspec, assumption) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
99 |
apply (drule real_gt_zero_preal_Ex [THEN iffD1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
100 |
apply (auto simp add: real_of_preal_le_iff) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
101 |
apply (frule_tac y = "real_of_preal ya" in setleD, assumption) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
102 |
apply (frule real_ge_preal_preal_Ex, safe) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
103 |
apply (blast intro!: preal_psup_le dest!: setleD intro: real_of_preal_le_iff [THEN iffD1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
104 |
apply (frule_tac x = x in bspec, assumption) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
105 |
apply (frule isUbD2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
106 |
apply (drule real_gt_zero_preal_Ex [THEN iffD1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
107 |
apply (auto dest!: isUbD real_ge_preal_preal_Ex simp add: real_of_preal_le_iff) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
108 |
apply (blast dest!: setleD intro!: psup_le_ub intro: real_of_preal_le_iff [THEN iffD1]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
109 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
110 |
|
5078 | 111 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
112 |
(*------------------------------- |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
113 |
Lemmas |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
114 |
-------------------------------*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
115 |
lemma real_sup_lemma3: "\<forall>y \<in> {z. \<exists>x \<in> P. z = x + (-xa) + 1} Int {x. 0 < x}. 0 < y" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
116 |
by auto |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
117 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
118 |
lemma lemma_le_swap2: "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
119 |
by auto |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
120 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
121 |
lemma lemma_real_complete2b: "[| (x::real) + (-X) + 1 <= S; xa <= x |] ==> xa <= S + X + (- 1)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
122 |
by arith |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
123 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
124 |
(*---------------------------------------------------------- |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
125 |
reals Completeness (again!) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
126 |
----------------------------------------------------------*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
127 |
lemma reals_complete: "[| \<exists>X. X \<in>S; \<exists>Y. isUb (UNIV::real set) S Y |] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
128 |
==> \<exists>t. isLub (UNIV :: real set) S t" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
129 |
apply safe |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
130 |
apply (subgoal_tac "\<exists>u. u\<in> {z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}") |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
131 |
apply (subgoal_tac "isUb (UNIV::real set) ({z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}) (Y + (-X) + 1) ") |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
132 |
apply (cut_tac P = S and xa = X in real_sup_lemma3) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset
|
133 |
apply (frule posreals_complete [OF _ _ exI], blast, blast, safe) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
134 |
apply (rule_tac x = "t + X + (- 1) " in exI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
135 |
apply (rule isLubI2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
136 |
apply (rule_tac [2] setgeI, safe) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
137 |
apply (subgoal_tac [2] "isUb (UNIV:: real set) ({z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}) (y + (-X) + 1) ") |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
138 |
apply (drule_tac [2] y = " (y + (- X) + 1) " in isLub_le_isUb) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
139 |
prefer 2 apply assumption |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
140 |
prefer 2 |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
141 |
apply arith |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
142 |
apply (rule setleI [THEN isUbI], safe) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
143 |
apply (rule_tac x = x and y = y in linorder_cases) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
144 |
apply (subst lemma_le_swap2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
145 |
apply (frule isLubD2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
146 |
prefer 2 apply assumption |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
147 |
apply safe |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
148 |
apply blast |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
149 |
apply arith |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
150 |
apply (subst lemma_le_swap2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
151 |
apply (frule isLubD2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
152 |
prefer 2 apply assumption |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
153 |
apply blast |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
154 |
apply (rule lemma_real_complete2b) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
155 |
apply (erule_tac [2] order_less_imp_le) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
156 |
apply (blast intro!: isLubD2, blast) |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
157 |
apply (simp (no_asm_use) add: add_assoc) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
158 |
apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
159 |
apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono, auto) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
160 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
161 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
162 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
163 |
subsection{*Corollary: the Archimedean Property of the Reals*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
164 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
165 |
lemma reals_Archimedean: "0 < x ==> \<exists>n. inverse (real(Suc n)) < x" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
166 |
apply (rule ccontr) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
167 |
apply (subgoal_tac "\<forall>n. x * real (Suc n) <= 1") |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
168 |
prefer 2 |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
169 |
apply (simp add: linorder_not_less inverse_eq_divide, clarify) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
170 |
apply (drule_tac x = n in spec) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
171 |
apply (drule_tac c = "real (Suc n)" in mult_right_mono) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
172 |
apply (rule real_of_nat_ge_zero) |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
173 |
apply (simp add: times_divide_eq_right real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] mult_commute) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
174 |
apply (subgoal_tac "isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} 1") |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
175 |
apply (subgoal_tac "\<exists>X. X \<in> {z. \<exists>n. z = x* (real (Suc n))}") |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
176 |
apply (drule reals_complete) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
177 |
apply (auto intro: isUbI setleI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
178 |
apply (subgoal_tac "\<forall>m. x* (real (Suc m)) <= t") |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
179 |
apply (simp add: real_of_nat_Suc right_distrib) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
180 |
prefer 2 apply (blast intro: isLubD2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
181 |
apply (simp add: le_diff_eq [symmetric] real_diff_def) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
182 |
apply (subgoal_tac "isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} (t + (-x))") |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
183 |
prefer 2 apply (blast intro!: isUbI setleI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
184 |
apply (drule_tac y = "t+ (-x) " in isLub_le_isUb) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
185 |
apply (auto simp add: real_of_nat_Suc right_distrib) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
186 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
187 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
188 |
(*There must be other proofs, e.g. Suc of the largest integer in the |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
189 |
cut representing x*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
190 |
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
191 |
apply (rule_tac x = x and y = 0 in linorder_cases) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
192 |
apply (rule_tac x = 0 in exI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
193 |
apply (rule_tac [2] x = 1 in exI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
194 |
apply (auto elim: order_less_trans simp add: real_of_nat_one) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
195 |
apply (frule positive_imp_inverse_positive [THEN reals_Archimedean], safe) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
196 |
apply (rule_tac x = "Suc n" in exI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
197 |
apply (frule_tac b = "inverse x" in mult_strict_right_mono, auto) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
198 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
199 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
200 |
lemma reals_Archimedean3: "0 < x ==> \<forall>y. \<exists>(n::nat). y < real n * x" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
201 |
apply safe |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
202 |
apply (cut_tac x = "y*inverse (x) " in reals_Archimedean2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
203 |
apply safe |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
204 |
apply (frule_tac a = "y * inverse x" in mult_strict_right_mono) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
205 |
apply (auto simp add: mult_assoc real_of_nat_def) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
206 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
207 |
|
16819 | 208 |
lemma reals_Archimedean6: |
209 |
"0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)" |
|
210 |
apply (insert reals_Archimedean2 [of r], safe) |
|
211 |
apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x" |
|
212 |
in ex_has_least_nat, auto) |
|
213 |
apply (rule_tac x = x in exI) |
|
214 |
apply (case_tac x, simp) |
|
215 |
apply (rename_tac x') |
|
216 |
apply (drule_tac x = x' in spec, simp) |
|
217 |
done |
|
218 |
||
219 |
lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)" |
|
220 |
by (drule reals_Archimedean6, auto) |
|
221 |
||
222 |
lemma reals_Archimedean_6b_int: |
|
223 |
"0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)" |
|
224 |
apply (drule reals_Archimedean6a, auto) |
|
225 |
apply (rule_tac x = "int n" in exI) |
|
226 |
apply (simp add: real_of_int_real_of_nat real_of_nat_Suc) |
|
227 |
done |
|
228 |
||
229 |
lemma reals_Archimedean_6c_int: |
|
230 |
"r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)" |
|
231 |
apply (rule reals_Archimedean_6b_int [of "-r", THEN exE], simp, auto) |
|
232 |
apply (rename_tac n) |
|
233 |
apply (drule real_le_imp_less_or_eq, auto) |
|
234 |
apply (rule_tac x = "- n - 1" in exI) |
|
235 |
apply (rule_tac [2] x = "- n" in exI, auto) |
|
236 |
done |
|
237 |
||
238 |
||
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
239 |
ML |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
240 |
{* |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
241 |
val real_sum_of_halves = thm "real_sum_of_halves"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
242 |
val posreal_complete = thm "posreal_complete"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
243 |
val real_isLub_unique = thm "real_isLub_unique"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
244 |
val real_order_restrict = thm "real_order_restrict"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
245 |
val posreals_complete = thm "posreals_complete"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
246 |
val reals_complete = thm "reals_complete"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
247 |
val reals_Archimedean = thm "reals_Archimedean"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
248 |
val reals_Archimedean2 = thm "reals_Archimedean2"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
249 |
val reals_Archimedean3 = thm "reals_Archimedean3"; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
250 |
*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
251 |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
252 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
253 |
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
|
254 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
255 |
constdefs |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
256 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
257 |
floor :: "real => int" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
258 |
"floor r == (LEAST n::int. r < real (n+1))" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
259 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
260 |
ceiling :: "real => int" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
261 |
"ceiling r == - floor (- r)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
262 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
263 |
syntax (xsymbols) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
264 |
floor :: "real => int" ("\<lfloor>_\<rfloor>") |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
265 |
ceiling :: "real => int" ("\<lceil>_\<rceil>") |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
266 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
267 |
syntax (HTML output) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
268 |
floor :: "real => int" ("\<lfloor>_\<rfloor>") |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
269 |
ceiling :: "real => int" ("\<lceil>_\<rceil>") |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
270 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
271 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
272 |
lemma number_of_less_real_of_int_iff [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
273 |
"((number_of n) < real (m::int)) = (number_of n < m)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
274 |
apply auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
275 |
apply (rule real_of_int_less_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
276 |
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
|
277 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
278 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
279 |
lemma number_of_less_real_of_int_iff2 [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
280 |
"(real (m::int) < (number_of n)) = (m < number_of n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
281 |
apply auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
282 |
apply (rule real_of_int_less_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
283 |
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
|
284 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
285 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
286 |
lemma number_of_le_real_of_int_iff [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
287 |
"((number_of n) \<le> real (m::int)) = (number_of n \<le> m)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
288 |
by (simp add: linorder_not_less [symmetric]) |
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 number_of_le_real_of_int_iff2 [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
291 |
"(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
292 |
by (simp add: linorder_not_less [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
293 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
294 |
lemma floor_zero [simp]: "floor 0 = 0" |
16819 | 295 |
apply (simp add: floor_def del: real_of_int_add) |
296 |
apply (rule Least_equality) |
|
297 |
apply simp_all |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
298 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
299 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
300 |
lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
301 |
by auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
302 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
303 |
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
304 |
apply (simp only: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
305 |
apply (rule Least_equality) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
306 |
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
307 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
308 |
apply (simp_all add: real_of_int_real_of_nat) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
309 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
310 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
311 |
lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
312 |
apply (simp only: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
313 |
apply (rule Least_equality) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
314 |
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) |
16819 | 315 |
apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst]) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
316 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
317 |
apply (simp_all add: real_of_int_real_of_nat) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
318 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
319 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
320 |
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
321 |
apply (simp only: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
322 |
apply (rule Least_equality) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
323 |
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
324 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
325 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
326 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
327 |
lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
328 |
apply (simp only: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
329 |
apply (rule Least_equality) |
16819 | 330 |
apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst]) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
331 |
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
332 |
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
333 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
334 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
335 |
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
336 |
apply (case_tac "r < 0") |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
337 |
apply (blast intro: reals_Archimedean_6c_int) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
338 |
apply (simp only: linorder_not_less) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
339 |
apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
340 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
341 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
342 |
lemma lemma_floor: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
343 |
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
|
344 |
shows "m \<le> (n::int)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
345 |
proof - |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
346 |
have "real m < real n + 1" by (rule order_le_less_trans) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
347 |
also have "... = real(n+1)" by simp |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
348 |
finally have "m < n+1" by (simp only: real_of_int_less_iff) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
349 |
thus ?thesis by arith |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
350 |
qed |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
351 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
352 |
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
353 |
apply (simp add: floor_def Least_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
354 |
apply (insert real_lb_ub_int [of r], safe) |
16819 | 355 |
apply (rule theI2) |
356 |
apply auto |
|
357 |
apply (subst int_le_real_less, simp) |
|
358 |
apply (drule_tac x = n in spec) |
|
359 |
apply auto |
|
360 |
apply (subgoal_tac "n <= x") |
|
361 |
apply simp |
|
362 |
apply (subst int_le_real_less, simp) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
363 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
364 |
|
16819 | 365 |
lemma floor_mono: "x < y ==> floor x \<le> floor y" |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
366 |
apply (simp add: floor_def Least_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
367 |
apply (insert real_lb_ub_int [of x]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
368 |
apply (insert real_lb_ub_int [of y], safe) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
369 |
apply (rule theI2) |
16819 | 370 |
apply (rule_tac [3] theI2) |
371 |
apply simp |
|
372 |
apply (erule conjI) |
|
373 |
apply (auto simp add: order_eq_iff int_le_real_less) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
374 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
375 |
|
16819 | 376 |
lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y" |
377 |
by (auto dest: real_le_imp_less_or_eq simp add: floor_mono) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
378 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
379 |
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
|
380 |
by (auto intro: lemma_floor) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
381 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
382 |
lemma real_of_int_floor_cancel [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
383 |
"(real (floor x) = x) = (\<exists>n::int. x = real n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
384 |
apply (simp add: floor_def Least_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
385 |
apply (insert real_lb_ub_int [of x], erule exE) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
386 |
apply (rule theI2) |
16819 | 387 |
apply (auto intro: lemma_floor) |
388 |
apply (auto simp add: order_eq_iff int_le_real_less) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
389 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
390 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
391 |
lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
392 |
apply (simp add: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
393 |
apply (rule Least_equality) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
394 |
apply (auto intro: lemma_floor) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
395 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
396 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
397 |
lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
398 |
apply (simp add: floor_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
399 |
apply (rule Least_equality) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
400 |
apply (auto intro: lemma_floor) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
401 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
402 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
403 |
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
|
404 |
apply (rule inj_int [THEN injD]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
405 |
apply (simp add: real_of_nat_Suc) |
15539 | 406 |
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
|
407 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
408 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
409 |
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
|
410 |
apply (drule order_le_imp_less_or_eq) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
411 |
apply (auto intro: floor_eq3) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
412 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
413 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
414 |
lemma floor_number_of_eq [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
415 |
"floor(number_of n :: real) = (number_of n :: int)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
416 |
apply (subst real_number_of [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
417 |
apply (rule floor_real_of_int) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
418 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
419 |
|
16819 | 420 |
lemma floor_one [simp]: "floor 1 = 1" |
421 |
apply (rule trans) |
|
422 |
prefer 2 |
|
423 |
apply (rule floor_real_of_int) |
|
424 |
apply simp |
|
425 |
done |
|
426 |
||
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
427 |
lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
428 |
apply (simp add: floor_def Least_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
429 |
apply (insert real_lb_ub_int [of r], safe) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
430 |
apply (rule theI2) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
431 |
apply (auto intro: lemma_floor) |
16819 | 432 |
apply (auto simp add: order_eq_iff int_le_real_less) |
433 |
done |
|
434 |
||
435 |
lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)" |
|
436 |
apply (simp add: floor_def Least_def) |
|
437 |
apply (insert real_lb_ub_int [of r], safe) |
|
438 |
apply (rule theI2) |
|
439 |
apply (auto intro: lemma_floor) |
|
440 |
apply (auto simp add: order_eq_iff int_le_real_less) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
441 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
442 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
443 |
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
444 |
apply (insert real_of_int_floor_ge_diff_one [of r]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
445 |
apply (auto simp del: real_of_int_floor_ge_diff_one) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
446 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
447 |
|
16819 | 448 |
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1" |
449 |
apply (insert real_of_int_floor_gt_diff_one [of r]) |
|
450 |
apply (auto simp del: real_of_int_floor_gt_diff_one) |
|
451 |
done |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
452 |
|
16819 | 453 |
lemma le_floor: "real a <= x ==> a <= floor x" |
454 |
apply (subgoal_tac "a < floor x + 1") |
|
455 |
apply arith |
|
456 |
apply (subst real_of_int_less_iff [THEN sym]) |
|
457 |
apply simp |
|
458 |
apply (insert real_of_int_floor_add_one_gt [of x]) |
|
459 |
apply arith |
|
460 |
done |
|
461 |
||
462 |
lemma real_le_floor: "a <= floor x ==> real a <= x" |
|
463 |
apply (rule order_trans) |
|
464 |
prefer 2 |
|
465 |
apply (rule real_of_int_floor_le) |
|
466 |
apply (subst real_of_int_le_iff) |
|
467 |
apply assumption |
|
468 |
done |
|
469 |
||
470 |
lemma le_floor_eq: "(a <= floor x) = (real a <= x)" |
|
471 |
apply (rule iffI) |
|
472 |
apply (erule real_le_floor) |
|
473 |
apply (erule le_floor) |
|
474 |
done |
|
475 |
||
476 |
lemma le_floor_eq_number_of [simp]: |
|
477 |
"(number_of n <= floor x) = (number_of n <= x)" |
|
478 |
by (simp add: le_floor_eq) |
|
479 |
||
480 |
lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)" |
|
481 |
by (simp add: le_floor_eq) |
|
482 |
||
483 |
lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)" |
|
484 |
by (simp add: le_floor_eq) |
|
485 |
||
486 |
lemma floor_less_eq: "(floor x < a) = (x < real a)" |
|
487 |
apply (subst linorder_not_le [THEN sym])+ |
|
488 |
apply simp |
|
489 |
apply (rule le_floor_eq) |
|
490 |
done |
|
491 |
||
492 |
lemma floor_less_eq_number_of [simp]: |
|
493 |
"(floor x < number_of n) = (x < number_of n)" |
|
494 |
by (simp add: floor_less_eq) |
|
495 |
||
496 |
lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)" |
|
497 |
by (simp add: floor_less_eq) |
|
498 |
||
499 |
lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)" |
|
500 |
by (simp add: floor_less_eq) |
|
501 |
||
502 |
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)" |
|
503 |
apply (insert le_floor_eq [of "a + 1" x]) |
|
504 |
apply auto |
|
505 |
done |
|
506 |
||
507 |
lemma less_floor_eq_number_of [simp]: |
|
508 |
"(number_of n < floor x) = (number_of n + 1 <= x)" |
|
509 |
by (simp add: less_floor_eq) |
|
510 |
||
511 |
lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)" |
|
512 |
by (simp add: less_floor_eq) |
|
513 |
||
514 |
lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)" |
|
515 |
by (simp add: less_floor_eq) |
|
516 |
||
517 |
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)" |
|
518 |
apply (insert floor_less_eq [of x "a + 1"]) |
|
519 |
apply auto |
|
520 |
done |
|
521 |
||
522 |
lemma floor_le_eq_number_of [simp]: |
|
523 |
"(floor x <= number_of n) = (x < number_of n + 1)" |
|
524 |
by (simp add: floor_le_eq) |
|
525 |
||
526 |
lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)" |
|
527 |
by (simp add: floor_le_eq) |
|
528 |
||
529 |
lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)" |
|
530 |
by (simp add: floor_le_eq) |
|
531 |
||
532 |
lemma floor_add [simp]: "floor (x + real a) = floor x + a" |
|
533 |
apply (subst order_eq_iff) |
|
534 |
apply (rule conjI) |
|
535 |
prefer 2 |
|
536 |
apply (subgoal_tac "floor x + a < floor (x + real a) + 1") |
|
537 |
apply arith |
|
538 |
apply (subst real_of_int_less_iff [THEN sym]) |
|
539 |
apply simp |
|
540 |
apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1") |
|
541 |
apply (subgoal_tac "real (floor x) <= x") |
|
542 |
apply arith |
|
543 |
apply (rule real_of_int_floor_le) |
|
544 |
apply (rule real_of_int_floor_add_one_gt) |
|
545 |
apply (subgoal_tac "floor (x + real a) < floor x + a + 1") |
|
546 |
apply arith |
|
547 |
apply (subst real_of_int_less_iff [THEN sym]) |
|
548 |
apply simp |
|
549 |
apply (subgoal_tac "real(floor(x + real a)) <= x + real a") |
|
550 |
apply (subgoal_tac "x < real(floor x) + 1") |
|
551 |
apply arith |
|
552 |
apply (rule real_of_int_floor_add_one_gt) |
|
553 |
apply (rule real_of_int_floor_le) |
|
554 |
done |
|
555 |
||
556 |
lemma floor_add_number_of [simp]: |
|
557 |
"floor (x + number_of n) = floor x + number_of n" |
|
558 |
apply (subst floor_add [THEN sym]) |
|
559 |
apply simp |
|
560 |
done |
|
561 |
||
562 |
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1" |
|
563 |
apply (subst floor_add [THEN sym]) |
|
564 |
apply simp |
|
565 |
done |
|
566 |
||
567 |
lemma floor_subtract [simp]: "floor (x - real a) = floor x - a" |
|
568 |
apply (subst diff_minus)+ |
|
569 |
apply (subst real_of_int_minus [THEN sym]) |
|
570 |
apply (rule floor_add) |
|
571 |
done |
|
572 |
||
573 |
lemma floor_subtract_number_of [simp]: "floor (x - number_of n) = |
|
574 |
floor x - number_of n" |
|
575 |
apply (subst floor_subtract [THEN sym]) |
|
576 |
apply simp |
|
577 |
done |
|
578 |
||
579 |
lemma floor_subtract_one [simp]: "floor (x - 1) = floor x - 1" |
|
580 |
apply (subst floor_subtract [THEN sym]) |
|
581 |
apply simp |
|
582 |
done |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
583 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
584 |
lemma ceiling_zero [simp]: "ceiling 0 = 0" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
585 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
586 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
587 |
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
588 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
589 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
590 |
lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
591 |
by auto |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
592 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
593 |
lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
594 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
595 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
596 |
lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
597 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
598 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
599 |
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
600 |
apply (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
601 |
apply (subst le_minus_iff, simp) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
602 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
603 |
|
16819 | 604 |
lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y" |
605 |
by (simp add: floor_mono ceiling_def) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
606 |
|
16819 | 607 |
lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y" |
608 |
by (simp add: floor_mono2 ceiling_def) |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
609 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
610 |
lemma real_of_int_ceiling_cancel [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
611 |
"(real (ceiling x) = x) = (\<exists>n::int. x = real n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
612 |
apply (auto simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
613 |
apply (drule arg_cong [where f = uminus], auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
614 |
apply (rule_tac x = "-n" in exI, auto) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
615 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
616 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
617 |
lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
618 |
apply (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
619 |
apply (rule minus_equation_iff [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
620 |
apply (simp add: floor_eq [where n = "-(n+1)"]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
621 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
622 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
623 |
lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
624 |
by (simp add: ceiling_def floor_eq2 [where n = "-(n+1)"]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
625 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
626 |
lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n |] ==> ceiling x = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
627 |
by (simp add: ceiling_def floor_eq2 [where n = "-n"]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
628 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
629 |
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
630 |
by (simp add: ceiling_def) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
631 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
632 |
lemma ceiling_number_of_eq [simp]: |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
633 |
"ceiling (number_of n :: real) = (number_of n)" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
634 |
apply (subst real_number_of [symmetric]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
635 |
apply (rule ceiling_real_of_int) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
636 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
637 |
|
16819 | 638 |
lemma ceiling_one [simp]: "ceiling 1 = 1" |
639 |
by (unfold ceiling_def, simp) |
|
640 |
||
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
641 |
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
642 |
apply (rule neg_le_iff_le [THEN iffD1]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
643 |
apply (simp add: ceiling_def diff_minus) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
644 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
645 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
646 |
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1" |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
647 |
apply (insert real_of_int_ceiling_diff_one_le [of r]) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
648 |
apply (simp del: real_of_int_ceiling_diff_one_le) |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
649 |
done |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
650 |
|
16819 | 651 |
lemma ceiling_le: "x <= real a ==> ceiling x <= a" |
652 |
apply (unfold ceiling_def) |
|
653 |
apply (subgoal_tac "-a <= floor(- x)") |
|
654 |
apply simp |
|
655 |
apply (rule le_floor) |
|
656 |
apply simp |
|
657 |
done |
|
658 |
||
659 |
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a" |
|
660 |
apply (unfold ceiling_def) |
|
661 |
apply (subgoal_tac "real(- a) <= - x") |
|
662 |
apply simp |
|
663 |
apply (rule real_le_floor) |
|
664 |
apply simp |
|
665 |
done |
|
666 |
||
667 |
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)" |
|
668 |
apply (rule iffI) |
|
669 |
apply (erule ceiling_le_real) |
|
670 |
apply (erule ceiling_le) |
|
671 |
done |
|
672 |
||
673 |
lemma ceiling_le_eq_number_of [simp]: |
|
674 |
"(ceiling x <= number_of n) = (x <= number_of n)" |
|
675 |
by (simp add: ceiling_le_eq) |
|
676 |
||
677 |
lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)" |
|
678 |
by (simp add: ceiling_le_eq) |
|
679 |
||
680 |
lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)" |
|
681 |
by (simp add: ceiling_le_eq) |
|
682 |
||
683 |
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)" |
|
684 |
apply (subst linorder_not_le [THEN sym])+ |
|
685 |
apply simp |
|
686 |
apply (rule ceiling_le_eq) |
|
687 |
done |
|
688 |
||
689 |
lemma less_ceiling_eq_number_of [simp]: |
|
690 |
"(number_of n < ceiling x) = (number_of n < x)" |
|
691 |
by (simp add: less_ceiling_eq) |
|
692 |
||
693 |
lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)" |
|
694 |
by (simp add: less_ceiling_eq) |
|
695 |
||
696 |
lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)" |
|
697 |
by (simp add: less_ceiling_eq) |
|
698 |
||
699 |
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)" |
|
700 |
apply (insert ceiling_le_eq [of x "a - 1"]) |
|
701 |
apply auto |
|
702 |
done |
|
703 |
||
704 |
lemma ceiling_less_eq_number_of [simp]: |
|
705 |
"(ceiling x < number_of n) = (x <= number_of n - 1)" |
|
706 |
by (simp add: ceiling_less_eq) |
|
707 |
||
708 |
lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= -1)" |
|
709 |
by (simp add: ceiling_less_eq) |
|
710 |
||
711 |
lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)" |
|
712 |
by (simp add: ceiling_less_eq) |
|
713 |
||
714 |
lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)" |
|
715 |
apply (insert less_ceiling_eq [of "a - 1" x]) |
|
716 |
apply auto |
|
717 |
done |
|
718 |
||
719 |
lemma le_ceiling_eq_number_of [simp]: |
|
720 |
"(number_of n <= ceiling x) = (number_of n - 1 < x)" |
|
721 |
by (simp add: le_ceiling_eq) |
|
722 |
||
723 |
lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (-1 < x)" |
|
724 |
by (simp add: le_ceiling_eq) |
|
725 |
||
726 |
lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)" |
|
727 |
by (simp add: le_ceiling_eq) |
|
728 |
||
729 |
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a" |
|
730 |
apply (unfold ceiling_def, simp) |
|
731 |
apply (subst real_of_int_minus [THEN sym]) |
|
732 |
apply (subst floor_add) |
|
733 |
apply simp |
|
734 |
done |
|
735 |
||
736 |
lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) = |
|
737 |
ceiling x + number_of n" |
|
738 |
apply (subst ceiling_add [THEN sym]) |
|
739 |
apply simp |
|
740 |
done |
|
741 |
||
742 |
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1" |
|
743 |
apply (subst ceiling_add [THEN sym]) |
|
744 |
apply simp |
|
745 |
done |
|
746 |
||
747 |
lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a" |
|
748 |
apply (subst diff_minus)+ |
|
749 |
apply (subst real_of_int_minus [THEN sym]) |
|
750 |
apply (rule ceiling_add) |
|
751 |
done |
|
752 |
||
753 |
lemma ceiling_subtract_number_of [simp]: "ceiling (x - number_of n) = |
|
754 |
ceiling x - number_of n" |
|
755 |
apply (subst ceiling_subtract [THEN sym]) |
|
756 |
apply simp |
|
757 |
done |
|
758 |
||
759 |
lemma ceiling_subtract_one [simp]: "ceiling (x - 1) = ceiling x - 1" |
|
760 |
apply (subst ceiling_subtract [THEN sym]) |
|
761 |
apply simp |
|
762 |
done |
|
763 |
||
764 |
subsection {* Versions for the natural numbers *} |
|
765 |
||
766 |
constdefs |
|
767 |
natfloor :: "real => nat" |
|
768 |
"natfloor x == nat(floor x)" |
|
769 |
natceiling :: "real => nat" |
|
770 |
"natceiling x == nat(ceiling x)" |
|
771 |
||
772 |
lemma natfloor_zero [simp]: "natfloor 0 = 0" |
|
773 |
by (unfold natfloor_def, simp) |
|
774 |
||
775 |
lemma natfloor_one [simp]: "natfloor 1 = 1" |
|
776 |
by (unfold natfloor_def, simp) |
|
777 |
||
778 |
lemma zero_le_natfloor [simp]: "0 <= natfloor x" |
|
779 |
by (unfold natfloor_def, simp) |
|
780 |
||
781 |
lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n" |
|
782 |
by (unfold natfloor_def, simp) |
|
783 |
||
784 |
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n" |
|
785 |
by (unfold natfloor_def, simp) |
|
786 |
||
787 |
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x" |
|
788 |
by (unfold natfloor_def, simp) |
|
789 |
||
790 |
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0" |
|
791 |
apply (unfold natfloor_def) |
|
792 |
apply (subgoal_tac "floor x <= floor 0") |
|
793 |
apply simp |
|
794 |
apply (erule floor_mono2) |
|
795 |
done |
|
796 |
||
797 |
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y" |
|
798 |
apply (case_tac "0 <= x") |
|
799 |
apply (subst natfloor_def)+ |
|
800 |
apply (subst nat_le_eq_zle) |
|
801 |
apply force |
|
802 |
apply (erule floor_mono2) |
|
803 |
apply (subst natfloor_neg) |
|
804 |
apply simp |
|
805 |
apply simp |
|
806 |
done |
|
807 |
||
808 |
lemma le_natfloor: "real x <= a ==> x <= natfloor a" |
|
809 |
apply (unfold natfloor_def) |
|
810 |
apply (subst nat_int [THEN sym]) |
|
811 |
apply (subst nat_le_eq_zle) |
|
812 |
apply simp |
|
813 |
apply (rule le_floor) |
|
814 |
apply simp |
|
815 |
done |
|
816 |
||
817 |
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)" |
|
818 |
apply (rule iffI) |
|
819 |
apply (rule order_trans) |
|
820 |
prefer 2 |
|
821 |
apply (erule real_natfloor_le) |
|
822 |
apply (subst real_of_nat_le_iff) |
|
823 |
apply assumption |
|
824 |
apply (erule le_natfloor) |
|
825 |
done |
|
826 |
||
827 |
lemma le_natfloor_eq_number_of [simp]: |
|
828 |
"~ neg((number_of n)::int) ==> 0 <= x ==> |
|
829 |
(number_of n <= natfloor x) = (number_of n <= x)" |
|
830 |
apply (subst le_natfloor_eq, assumption) |
|
831 |
apply simp |
|
832 |
done |
|
833 |
||
16820 | 834 |
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" |
16819 | 835 |
apply (case_tac "0 <= x") |
836 |
apply (subst le_natfloor_eq, assumption, simp) |
|
837 |
apply (rule iffI) |
|
838 |
apply (subgoal_tac "natfloor x <= natfloor 0") |
|
839 |
apply simp |
|
840 |
apply (rule natfloor_mono) |
|
841 |
apply simp |
|
842 |
apply simp |
|
843 |
done |
|
844 |
||
845 |
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n" |
|
846 |
apply (unfold natfloor_def) |
|
847 |
apply (subst nat_int [THEN sym]);back; |
|
848 |
apply (subst eq_nat_nat_iff) |
|
849 |
apply simp |
|
850 |
apply simp |
|
851 |
apply (rule floor_eq2) |
|
852 |
apply auto |
|
853 |
done |
|
854 |
||
855 |
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1" |
|
856 |
apply (case_tac "0 <= x") |
|
857 |
apply (unfold natfloor_def) |
|
858 |
apply simp |
|
859 |
apply simp_all |
|
860 |
done |
|
861 |
||
862 |
lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)" |
|
863 |
apply (simp add: compare_rls) |
|
864 |
apply (rule real_natfloor_add_one_gt) |
|
865 |
done |
|
866 |
||
867 |
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" |
|
868 |
apply (subgoal_tac "z < real(natfloor z) + 1") |
|
869 |
apply arith |
|
870 |
apply (rule real_natfloor_add_one_gt) |
|
871 |
done |
|
872 |
||
873 |
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a" |
|
874 |
apply (unfold natfloor_def) |
|
875 |
apply (subgoal_tac "real a = real (int a)") |
|
876 |
apply (erule ssubst) |
|
877 |
apply (simp add: nat_add_distrib) |
|
878 |
apply simp |
|
879 |
done |
|
880 |
||
881 |
lemma natfloor_add_number_of [simp]: |
|
882 |
"~neg ((number_of n)::int) ==> 0 <= x ==> |
|
883 |
natfloor (x + number_of n) = natfloor x + number_of n" |
|
884 |
apply (subst natfloor_add [THEN sym]) |
|
885 |
apply simp_all |
|
886 |
done |
|
887 |
||
888 |
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1" |
|
889 |
apply (subst natfloor_add [THEN sym]) |
|
890 |
apply assumption |
|
891 |
apply simp |
|
892 |
done |
|
893 |
||
894 |
lemma natfloor_subtract [simp]: "real a <= x ==> |
|
895 |
natfloor(x - real a) = natfloor x - a" |
|
896 |
apply (unfold natfloor_def) |
|
897 |
apply (subgoal_tac "real a = real (int a)") |
|
898 |
apply (erule ssubst) |
|
899 |
apply simp |
|
900 |
apply (subst nat_diff_distrib) |
|
901 |
apply simp |
|
902 |
apply (rule le_floor) |
|
903 |
apply simp_all |
|
904 |
done |
|
905 |
||
906 |
lemma natceiling_zero [simp]: "natceiling 0 = 0" |
|
907 |
by (unfold natceiling_def, simp) |
|
908 |
||
909 |
lemma natceiling_one [simp]: "natceiling 1 = 1" |
|
910 |
by (unfold natceiling_def, simp) |
|
911 |
||
912 |
lemma zero_le_natceiling [simp]: "0 <= natceiling x" |
|
913 |
by (unfold natceiling_def, simp) |
|
914 |
||
915 |
lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n" |
|
916 |
by (unfold natceiling_def, simp) |
|
917 |
||
918 |
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n" |
|
919 |
by (unfold natceiling_def, simp) |
|
920 |
||
921 |
lemma real_natceiling_ge: "x <= real(natceiling x)" |
|
922 |
apply (unfold natceiling_def) |
|
923 |
apply (case_tac "x < 0") |
|
924 |
apply simp |
|
925 |
apply (subst real_nat_eq_real) |
|
926 |
apply (subgoal_tac "ceiling 0 <= ceiling x") |
|
927 |
apply simp |
|
928 |
apply (rule ceiling_mono2) |
|
929 |
apply simp |
|
930 |
apply simp |
|
931 |
done |
|
932 |
||
933 |
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0" |
|
934 |
apply (unfold natceiling_def) |
|
935 |
apply simp |
|
936 |
done |
|
937 |
||
938 |
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y" |
|
939 |
apply (case_tac "0 <= x") |
|
940 |
apply (subst natceiling_def)+ |
|
941 |
apply (subst nat_le_eq_zle) |
|
942 |
apply (rule disjI2) |
|
943 |
apply (subgoal_tac "real (0::int) <= real(ceiling y)") |
|
944 |
apply simp |
|
945 |
apply (rule order_trans) |
|
946 |
apply simp |
|
947 |
apply (erule order_trans) |
|
948 |
apply simp |
|
949 |
apply (erule ceiling_mono2) |
|
950 |
apply (subst natceiling_neg) |
|
951 |
apply simp_all |
|
952 |
done |
|
953 |
||
954 |
lemma natceiling_le: "x <= real a ==> natceiling x <= a" |
|
955 |
apply (unfold natceiling_def) |
|
956 |
apply (case_tac "x < 0") |
|
957 |
apply simp |
|
958 |
apply (subst nat_int [THEN sym]);back; |
|
959 |
apply (subst nat_le_eq_zle) |
|
960 |
apply simp |
|
961 |
apply (rule ceiling_le) |
|
962 |
apply simp |
|
963 |
done |
|
964 |
||
965 |
lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)" |
|
966 |
apply (rule iffI) |
|
967 |
apply (rule order_trans) |
|
968 |
apply (rule real_natceiling_ge) |
|
969 |
apply (subst real_of_nat_le_iff) |
|
970 |
apply assumption |
|
971 |
apply (erule natceiling_le) |
|
972 |
done |
|
973 |
||
16820 | 974 |
lemma natceiling_le_eq_number_of [simp]: |
975 |
"~ neg((number_of n)::int) ==> 0 <= x ==> |
|
976 |
(natceiling x <= number_of n) = (x <= number_of n)" |
|
16819 | 977 |
apply (subst natceiling_le_eq, assumption) |
978 |
apply simp |
|
979 |
done |
|
980 |
||
16820 | 981 |
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" |
16819 | 982 |
apply (case_tac "0 <= x") |
983 |
apply (subst natceiling_le_eq) |
|
984 |
apply assumption |
|
985 |
apply simp |
|
986 |
apply (subst natceiling_neg) |
|
987 |
apply simp |
|
988 |
apply simp |
|
989 |
done |
|
990 |
||
991 |
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1" |
|
992 |
apply (unfold natceiling_def) |
|
993 |
apply (subst nat_int [THEN sym]);back; |
|
994 |
apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)") |
|
995 |
apply (erule ssubst) |
|
996 |
apply (subst eq_nat_nat_iff) |
|
997 |
apply (subgoal_tac "ceiling 0 <= ceiling x") |
|
998 |
apply simp |
|
999 |
apply (rule ceiling_mono2) |
|
1000 |
apply force |
|
1001 |
apply force |
|
1002 |
apply (rule ceiling_eq2) |
|
1003 |
apply (simp, simp) |
|
1004 |
apply (subst nat_add_distrib) |
|
1005 |
apply auto |
|
1006 |
done |
|
1007 |
||
1008 |
lemma natceiling_add [simp]: "0 <= x ==> |
|
1009 |
natceiling (x + real a) = natceiling x + a" |
|
1010 |
apply (unfold natceiling_def) |
|
1011 |
apply (subgoal_tac "real a = real (int a)") |
|
1012 |
apply (erule ssubst) |
|
1013 |
apply simp |
|
1014 |
apply (subst nat_add_distrib) |
|
1015 |
apply (subgoal_tac "0 = ceiling 0") |
|
1016 |
apply (erule ssubst) |
|
1017 |
apply (erule ceiling_mono2) |
|
1018 |
apply simp_all |
|
1019 |
done |
|
1020 |
||
16820 | 1021 |
lemma natceiling_add_number_of [simp]: |
1022 |
"~ neg ((number_of n)::int) ==> 0 <= x ==> |
|
1023 |
natceiling (x + number_of n) = natceiling x + number_of n" |
|
16819 | 1024 |
apply (subst natceiling_add [THEN sym]) |
1025 |
apply simp_all |
|
1026 |
done |
|
1027 |
||
1028 |
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1" |
|
1029 |
apply (subst natceiling_add [THEN sym]) |
|
1030 |
apply assumption |
|
1031 |
apply simp |
|
1032 |
done |
|
1033 |
||
1034 |
lemma natceiling_subtract [simp]: "real a <= x ==> |
|
1035 |
natceiling(x - real a) = natceiling x - a" |
|
1036 |
apply (unfold natceiling_def) |
|
1037 |
apply (subgoal_tac "real a = real (int a)") |
|
1038 |
apply (erule ssubst) |
|
1039 |
apply simp |
|
1040 |
apply (subst nat_diff_distrib) |
|
1041 |
apply simp |
|
1042 |
apply (rule order_trans) |
|
1043 |
prefer 2 |
|
1044 |
apply (rule ceiling_mono2) |
|
1045 |
apply assumption |
|
1046 |
apply simp_all |
|
1047 |
done |
|
1048 |
||
1049 |
lemma natfloor_div_nat: "1 <= x ==> 0 < y ==> |
|
1050 |
natfloor (x / real y) = natfloor x div y" |
|
1051 |
proof - |
|
1052 |
assume "1 <= (x::real)" and "0 < (y::nat)" |
|
1053 |
have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y" |
|
1054 |
by simp |
|
1055 |
then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + |
|
1056 |
real((natfloor x) mod y)" |
|
1057 |
by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym]) |
|
1058 |
have "x = real(natfloor x) + (x - real(natfloor x))" |
|
1059 |
by simp |
|
1060 |
then have "x = real ((natfloor x) div y) * real y + |
|
1061 |
real((natfloor x) mod y) + (x - real(natfloor x))" |
|
1062 |
by (simp add: a) |
|
1063 |
then have "x / real y = ... / real y" |
|
1064 |
by simp |
|
1065 |
also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / |
|
1066 |
real y + (x - real(natfloor x)) / real y" |
|
1067 |
by (auto simp add: ring_distrib ring_eq_simps add_divide_distrib |
|
1068 |
diff_divide_distrib prems) |
|
1069 |
finally have "natfloor (x / real y) = natfloor(...)" by simp |
|
1070 |
also have "... = natfloor(real((natfloor x) mod y) / |
|
1071 |
real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))" |
|
1072 |
by (simp add: add_ac) |
|
1073 |
also have "... = natfloor(real((natfloor x) mod y) / |
|
1074 |
real y + (x - real(natfloor x)) / real y) + (natfloor x) div y" |
|
1075 |
apply (rule natfloor_add) |
|
1076 |
apply (rule add_nonneg_nonneg) |
|
1077 |
apply (rule divide_nonneg_pos) |
|
1078 |
apply simp |
|
1079 |
apply (simp add: prems) |
|
1080 |
apply (rule divide_nonneg_pos) |
|
1081 |
apply (simp add: compare_rls) |
|
1082 |
apply (rule real_natfloor_le) |
|
1083 |
apply (insert prems, auto) |
|
1084 |
done |
|
1085 |
also have "natfloor(real((natfloor x) mod y) / |
|
1086 |
real y + (x - real(natfloor x)) / real y) = 0" |
|
1087 |
apply (rule natfloor_eq) |
|
1088 |
apply simp |
|
1089 |
apply (rule add_nonneg_nonneg) |
|
1090 |
apply (rule divide_nonneg_pos) |
|
1091 |
apply force |
|
1092 |
apply (force simp add: prems) |
|
1093 |
apply (rule divide_nonneg_pos) |
|
1094 |
apply (simp add: compare_rls) |
|
1095 |
apply (rule real_natfloor_le) |
|
1096 |
apply (auto simp add: prems) |
|
1097 |
apply (insert prems, arith) |
|
1098 |
apply (simp add: add_divide_distrib [THEN sym]) |
|
1099 |
apply (subgoal_tac "real y = real y - 1 + 1") |
|
1100 |
apply (erule ssubst) |
|
1101 |
apply (rule add_le_less_mono) |
|
1102 |
apply (simp add: compare_rls) |
|
1103 |
apply (subgoal_tac "real(natfloor x mod y) + 1 = |
|
1104 |
real(natfloor x mod y + 1)") |
|
1105 |
apply (erule ssubst) |
|
1106 |
apply (subst real_of_nat_le_iff) |
|
1107 |
apply (subgoal_tac "natfloor x mod y < y") |
|
1108 |
apply arith |
|
1109 |
apply (rule mod_less_divisor) |
|
1110 |
apply assumption |
|
1111 |
apply auto |
|
1112 |
apply (simp add: compare_rls) |
|
1113 |
apply (subst add_commute) |
|
1114 |
apply (rule real_natfloor_add_one_gt) |
|
1115 |
done |
|
1116 |
finally show ?thesis |
|
1117 |
by simp |
|
1118 |
qed |
|
1119 |
||
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1120 |
ML |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1121 |
{* |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1122 |
val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1123 |
val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1124 |
val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1125 |
val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1126 |
val floor_zero = thm "floor_zero"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1127 |
val floor_real_of_nat_zero = thm "floor_real_of_nat_zero"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1128 |
val floor_real_of_nat = thm "floor_real_of_nat"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1129 |
val floor_minus_real_of_nat = thm "floor_minus_real_of_nat"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1130 |
val floor_real_of_int = thm "floor_real_of_int"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1131 |
val floor_minus_real_of_int = thm "floor_minus_real_of_int"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1132 |
val reals_Archimedean6 = thm "reals_Archimedean6"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1133 |
val reals_Archimedean6a = thm "reals_Archimedean6a"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1134 |
val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1135 |
val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1136 |
val real_lb_ub_int = thm "real_lb_ub_int"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1137 |
val lemma_floor = thm "lemma_floor"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1138 |
val real_of_int_floor_le = thm "real_of_int_floor_le"; |
16819 | 1139 |
(*val floor_le = thm "floor_le"; |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1140 |
val floor_le2 = thm "floor_le2"; |
16819 | 1141 |
*) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1142 |
val lemma_floor2 = thm "lemma_floor2"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1143 |
val real_of_int_floor_cancel = thm "real_of_int_floor_cancel"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1144 |
val floor_eq = thm "floor_eq"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1145 |
val floor_eq2 = thm "floor_eq2"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1146 |
val floor_eq3 = thm "floor_eq3"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1147 |
val floor_eq4 = thm "floor_eq4"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1148 |
val floor_number_of_eq = thm "floor_number_of_eq"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1149 |
val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1150 |
val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1151 |
val ceiling_zero = thm "ceiling_zero"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1152 |
val ceiling_real_of_nat = thm "ceiling_real_of_nat"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1153 |
val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1154 |
val ceiling_floor = thm "ceiling_floor"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1155 |
val floor_ceiling = thm "floor_ceiling"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1156 |
val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge"; |
16819 | 1157 |
(* |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1158 |
val ceiling_le = thm "ceiling_le"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1159 |
val ceiling_le2 = thm "ceiling_le2"; |
16819 | 1160 |
*) |
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1161 |
val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1162 |
val ceiling_eq = thm "ceiling_eq"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1163 |
val ceiling_eq2 = thm "ceiling_eq2"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1164 |
val ceiling_eq3 = thm "ceiling_eq3"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1165 |
val ceiling_real_of_int = thm "ceiling_real_of_int"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1166 |
val ceiling_number_of_eq = thm "ceiling_number_of_eq"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1167 |
val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1168 |
val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one"; |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1169 |
*} |
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1170 |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset
|
1171 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset
|
1172 |
end |