author  avigad 
Wed, 13 Jul 2005 20:02:54 +0200  
changeset 16820  5c9d597e4cb9 
parent 16819  00d8f9300d13 
child 16827  c90a1f450327 
permissions  rwrr 
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 nonempty 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 