author  wenzelm 
Thu, 14 Jul 2005 17:16:52 +0200  
changeset 16827  c90a1f450327 
parent 16820  5c9d597e4cb9 
child 16893  0cc94e6f6ae5 
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 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

357 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

358 

16819  359 
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

360 
apply (simp add: floor_def Least_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

361 
apply (insert real_lb_ub_int [of x]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

362 
apply (insert real_lb_ub_int [of y], safe) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

363 
apply (rule theI2) 
16819  364 
apply (rule_tac [3] theI2) 
365 
apply simp 

366 
apply (erule conjI) 

367 
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

368 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

369 

16819  370 
lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y" 
371 
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

372 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

373 
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

374 
by (auto intro: lemma_floor) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

375 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

376 
lemma real_of_int_floor_cancel [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

377 
"(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

378 
apply (simp add: floor_def Least_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

379 
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

380 
apply (rule theI2) 
16819  381 
apply (auto intro: lemma_floor) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

382 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

383 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

384 
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

385 
apply (simp add: floor_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

386 
apply (rule Least_equality) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

387 
apply (auto intro: lemma_floor) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

388 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

389 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

390 
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

391 
apply (simp add: floor_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

392 
apply (rule Least_equality) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

393 
apply (auto intro: lemma_floor) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

394 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

395 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

396 
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

397 
apply (rule inj_int [THEN injD]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

398 
apply (simp add: real_of_nat_Suc) 
15539  399 
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

400 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

401 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

402 
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

403 
apply (drule order_le_imp_less_or_eq) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

404 
apply (auto intro: floor_eq3) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

405 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

406 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

407 
lemma floor_number_of_eq [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

408 
"floor(number_of n :: real) = (number_of n :: int)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

409 
apply (subst real_number_of [symmetric]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

410 
apply (rule floor_real_of_int) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

411 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

412 

16819  413 
lemma floor_one [simp]: "floor 1 = 1" 
414 
apply (rule trans) 

415 
prefer 2 

416 
apply (rule floor_real_of_int) 

417 
apply simp 

418 
done 

419 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

420 
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

421 
apply (simp add: floor_def Least_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

422 
apply (insert real_lb_ub_int [of r], safe) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

423 
apply (rule theI2) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

424 
apply (auto intro: lemma_floor) 
16819  425 
done 
426 

427 
lemma real_of_int_floor_gt_diff_one [simp]: "r  1 < real(floor r)" 

428 
apply (simp add: floor_def Least_def) 

429 
apply (insert real_lb_ub_int [of r], safe) 

430 
apply (rule theI2) 

431 
apply (auto intro: lemma_floor) 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

432 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

433 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

434 
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

435 
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

436 
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

437 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

438 

16819  439 
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1" 
440 
apply (insert real_of_int_floor_gt_diff_one [of r]) 

441 
apply (auto simp del: real_of_int_floor_gt_diff_one) 

442 
done 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

443 

16819  444 
lemma le_floor: "real a <= x ==> a <= floor x" 
445 
apply (subgoal_tac "a < floor x + 1") 

446 
apply arith 

447 
apply (subst real_of_int_less_iff [THEN sym]) 

448 
apply simp 

449 
apply (insert real_of_int_floor_add_one_gt [of x]) 

450 
apply arith 

451 
done 

452 

453 
lemma real_le_floor: "a <= floor x ==> real a <= x" 

454 
apply (rule order_trans) 

455 
prefer 2 

456 
apply (rule real_of_int_floor_le) 

457 
apply (subst real_of_int_le_iff) 

458 
apply assumption 

459 
done 

460 

461 
lemma le_floor_eq: "(a <= floor x) = (real a <= x)" 

462 
apply (rule iffI) 

463 
apply (erule real_le_floor) 

464 
apply (erule le_floor) 

465 
done 

466 

467 
lemma le_floor_eq_number_of [simp]: 

468 
"(number_of n <= floor x) = (number_of n <= x)" 

469 
by (simp add: le_floor_eq) 

470 

471 
lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)" 

472 
by (simp add: le_floor_eq) 

473 

474 
lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)" 

475 
by (simp add: le_floor_eq) 

476 

477 
lemma floor_less_eq: "(floor x < a) = (x < real a)" 

478 
apply (subst linorder_not_le [THEN sym])+ 

479 
apply simp 

480 
apply (rule le_floor_eq) 

481 
done 

482 

483 
lemma floor_less_eq_number_of [simp]: 

484 
"(floor x < number_of n) = (x < number_of n)" 

485 
by (simp add: floor_less_eq) 

486 

487 
lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)" 

488 
by (simp add: floor_less_eq) 

489 

490 
lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)" 

491 
by (simp add: floor_less_eq) 

492 

493 
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)" 

494 
apply (insert le_floor_eq [of "a + 1" x]) 

495 
apply auto 

496 
done 

497 

498 
lemma less_floor_eq_number_of [simp]: 

499 
"(number_of n < floor x) = (number_of n + 1 <= x)" 

500 
by (simp add: less_floor_eq) 

501 

502 
lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)" 

503 
by (simp add: less_floor_eq) 

504 

505 
lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)" 

506 
by (simp add: less_floor_eq) 

507 

508 
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)" 

509 
apply (insert floor_less_eq [of x "a + 1"]) 

510 
apply auto 

511 
done 

512 

513 
lemma floor_le_eq_number_of [simp]: 

514 
"(floor x <= number_of n) = (x < number_of n + 1)" 

515 
by (simp add: floor_le_eq) 

516 

517 
lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)" 

518 
by (simp add: floor_le_eq) 

519 

520 
lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)" 

521 
by (simp add: floor_le_eq) 

522 

523 
lemma floor_add [simp]: "floor (x + real a) = floor x + a" 

524 
apply (subst order_eq_iff) 

525 
apply (rule conjI) 

526 
prefer 2 

527 
apply (subgoal_tac "floor x + a < floor (x + real a) + 1") 

528 
apply arith 

529 
apply (subst real_of_int_less_iff [THEN sym]) 

530 
apply simp 

531 
apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1") 

532 
apply (subgoal_tac "real (floor x) <= x") 

533 
apply arith 

534 
apply (rule real_of_int_floor_le) 

535 
apply (rule real_of_int_floor_add_one_gt) 

536 
apply (subgoal_tac "floor (x + real a) < floor x + a + 1") 

537 
apply arith 

538 
apply (subst real_of_int_less_iff [THEN sym]) 

539 
apply simp 

540 
apply (subgoal_tac "real(floor(x + real a)) <= x + real a") 

541 
apply (subgoal_tac "x < real(floor x) + 1") 

542 
apply arith 

543 
apply (rule real_of_int_floor_add_one_gt) 

544 
apply (rule real_of_int_floor_le) 

545 
done 

546 

547 
lemma floor_add_number_of [simp]: 

548 
"floor (x + number_of n) = floor x + number_of n" 

549 
apply (subst floor_add [THEN sym]) 

550 
apply simp 

551 
done 

552 

553 
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1" 

554 
apply (subst floor_add [THEN sym]) 

555 
apply simp 

556 
done 

557 

558 
lemma floor_subtract [simp]: "floor (x  real a) = floor x  a" 

559 
apply (subst diff_minus)+ 

560 
apply (subst real_of_int_minus [THEN sym]) 

561 
apply (rule floor_add) 

562 
done 

563 

564 
lemma floor_subtract_number_of [simp]: "floor (x  number_of n) = 

565 
floor x  number_of n" 

566 
apply (subst floor_subtract [THEN sym]) 

567 
apply simp 

568 
done 

569 

570 
lemma floor_subtract_one [simp]: "floor (x  1) = floor x  1" 

571 
apply (subst floor_subtract [THEN sym]) 

572 
apply simp 

573 
done 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

574 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

575 
lemma ceiling_zero [simp]: "ceiling 0 = 0" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

576 
by (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

577 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

578 
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

579 
by (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

580 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

581 
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

582 
by auto 
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_floor [simp]: "ceiling (real (floor r)) = floor r" 
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 floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r" 
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 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

591 
apply (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

592 
apply (subst le_minus_iff, simp) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

593 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

594 

16819  595 
lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y" 
596 
by (simp add: floor_mono ceiling_def) 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

597 

16819  598 
lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y" 
599 
by (simp add: floor_mono2 ceiling_def) 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

600 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

601 
lemma real_of_int_ceiling_cancel [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

602 
"(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

603 
apply (auto simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

604 
apply (drule arg_cong [where f = uminus], auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

605 
apply (rule_tac x = "n" in exI, auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

606 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

607 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

608 
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

609 
apply (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

610 
apply (rule minus_equation_iff [THEN iffD1]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

611 
apply (simp add: floor_eq [where n = "(n+1)"]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

612 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

613 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

614 
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

615 
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

616 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

617 
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

618 
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

619 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

620 
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

621 
by (simp add: ceiling_def) 
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_number_of_eq [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

624 
"ceiling (number_of n :: real) = (number_of n)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

625 
apply (subst real_number_of [symmetric]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

626 
apply (rule ceiling_real_of_int) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

627 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

628 

16819  629 
lemma ceiling_one [simp]: "ceiling 1 = 1" 
630 
by (unfold ceiling_def, simp) 

631 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

632 
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

633 
apply (rule neg_le_iff_le [THEN iffD1]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

634 
apply (simp add: ceiling_def diff_minus) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

635 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

636 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

637 
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

638 
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

639 
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

640 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

641 

16819  642 
lemma ceiling_le: "x <= real a ==> ceiling x <= a" 
643 
apply (unfold ceiling_def) 

644 
apply (subgoal_tac "a <= floor( x)") 

645 
apply simp 

646 
apply (rule le_floor) 

647 
apply simp 

648 
done 

649 

650 
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a" 

651 
apply (unfold ceiling_def) 

652 
apply (subgoal_tac "real( a) <=  x") 

653 
apply simp 

654 
apply (rule real_le_floor) 

655 
apply simp 

656 
done 

657 

658 
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)" 

659 
apply (rule iffI) 

660 
apply (erule ceiling_le_real) 

661 
apply (erule ceiling_le) 

662 
done 

663 

664 
lemma ceiling_le_eq_number_of [simp]: 

665 
"(ceiling x <= number_of n) = (x <= number_of n)" 

666 
by (simp add: ceiling_le_eq) 

667 

668 
lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)" 

669 
by (simp add: ceiling_le_eq) 

670 

671 
lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)" 

672 
by (simp add: ceiling_le_eq) 

673 

674 
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)" 

675 
apply (subst linorder_not_le [THEN sym])+ 

676 
apply simp 

677 
apply (rule ceiling_le_eq) 

678 
done 

679 

680 
lemma less_ceiling_eq_number_of [simp]: 

681 
"(number_of n < ceiling x) = (number_of n < x)" 

682 
by (simp add: less_ceiling_eq) 

683 

684 
lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)" 

685 
by (simp add: less_ceiling_eq) 

686 

687 
lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)" 

688 
by (simp add: less_ceiling_eq) 

689 

690 
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a  1)" 

691 
apply (insert ceiling_le_eq [of x "a  1"]) 

692 
apply auto 

693 
done 

694 

695 
lemma ceiling_less_eq_number_of [simp]: 

696 
"(ceiling x < number_of n) = (x <= number_of n  1)" 

697 
by (simp add: ceiling_less_eq) 

698 

699 
lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= 1)" 

700 
by (simp add: ceiling_less_eq) 

701 

702 
lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)" 

703 
by (simp add: ceiling_less_eq) 

704 

705 
lemma le_ceiling_eq: "(a <= ceiling x) = (real a  1 < x)" 

706 
apply (insert less_ceiling_eq [of "a  1" x]) 

707 
apply auto 

708 
done 

709 

710 
lemma le_ceiling_eq_number_of [simp]: 

711 
"(number_of n <= ceiling x) = (number_of n  1 < x)" 

712 
by (simp add: le_ceiling_eq) 

713 

714 
lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (1 < x)" 

715 
by (simp add: le_ceiling_eq) 

716 

717 
lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)" 

718 
by (simp add: le_ceiling_eq) 

719 

720 
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a" 

721 
apply (unfold ceiling_def, simp) 

722 
apply (subst real_of_int_minus [THEN sym]) 

723 
apply (subst floor_add) 

724 
apply simp 

725 
done 

726 

727 
lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) = 

728 
ceiling x + number_of n" 

729 
apply (subst ceiling_add [THEN sym]) 

730 
apply simp 

731 
done 

732 

733 
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1" 

734 
apply (subst ceiling_add [THEN sym]) 

735 
apply simp 

736 
done 

737 

738 
lemma ceiling_subtract [simp]: "ceiling (x  real a) = ceiling x  a" 

739 
apply (subst diff_minus)+ 

740 
apply (subst real_of_int_minus [THEN sym]) 

741 
apply (rule ceiling_add) 

742 
done 

743 

744 
lemma ceiling_subtract_number_of [simp]: "ceiling (x  number_of n) = 

745 
ceiling x  number_of n" 

746 
apply (subst ceiling_subtract [THEN sym]) 

747 
apply simp 

748 
done 

749 

750 
lemma ceiling_subtract_one [simp]: "ceiling (x  1) = ceiling x  1" 

751 
apply (subst ceiling_subtract [THEN sym]) 

752 
apply simp 

753 
done 

754 

755 
subsection {* Versions for the natural numbers *} 

756 

757 
constdefs 

758 
natfloor :: "real => nat" 

759 
"natfloor x == nat(floor x)" 

760 
natceiling :: "real => nat" 

761 
"natceiling x == nat(ceiling x)" 

762 

763 
lemma natfloor_zero [simp]: "natfloor 0 = 0" 

764 
by (unfold natfloor_def, simp) 

765 

766 
lemma natfloor_one [simp]: "natfloor 1 = 1" 

767 
by (unfold natfloor_def, simp) 

768 

769 
lemma zero_le_natfloor [simp]: "0 <= natfloor x" 

770 
by (unfold natfloor_def, simp) 

771 

772 
lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n" 

773 
by (unfold natfloor_def, simp) 

774 

775 
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n" 

776 
by (unfold natfloor_def, simp) 

777 

778 
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x" 

779 
by (unfold natfloor_def, simp) 

780 

781 
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0" 

782 
apply (unfold natfloor_def) 

783 
apply (subgoal_tac "floor x <= floor 0") 

784 
apply simp 

785 
apply (erule floor_mono2) 

786 
done 

787 

788 
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y" 

789 
apply (case_tac "0 <= x") 

790 
apply (subst natfloor_def)+ 

791 
apply (subst nat_le_eq_zle) 

792 
apply force 

793 
apply (erule floor_mono2) 

794 
apply (subst natfloor_neg) 

795 
apply simp 

796 
apply simp 

797 
done 

798 

799 
lemma le_natfloor: "real x <= a ==> x <= natfloor a" 

800 
apply (unfold natfloor_def) 

801 
apply (subst nat_int [THEN sym]) 

802 
apply (subst nat_le_eq_zle) 

803 
apply simp 

804 
apply (rule le_floor) 

805 
apply simp 

806 
done 

807 

808 
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)" 

809 
apply (rule iffI) 

810 
apply (rule order_trans) 

811 
prefer 2 

812 
apply (erule real_natfloor_le) 

813 
apply (subst real_of_nat_le_iff) 

814 
apply assumption 

815 
apply (erule le_natfloor) 

816 
done 

817 

818 
lemma le_natfloor_eq_number_of [simp]: 

819 
"~ neg((number_of n)::int) ==> 0 <= x ==> 

820 
(number_of n <= natfloor x) = (number_of n <= x)" 

821 
apply (subst le_natfloor_eq, assumption) 

822 
apply simp 

823 
done 

824 

16820  825 
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" 
16819  826 
apply (case_tac "0 <= x") 
827 
apply (subst le_natfloor_eq, assumption, simp) 

828 
apply (rule iffI) 

829 
apply (subgoal_tac "natfloor x <= natfloor 0") 

830 
apply simp 

831 
apply (rule natfloor_mono) 

832 
apply simp 

833 
apply simp 

834 
done 

835 

836 
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n" 

837 
apply (unfold natfloor_def) 

838 
apply (subst nat_int [THEN sym]);back; 

839 
apply (subst eq_nat_nat_iff) 

840 
apply simp 

841 
apply simp 

842 
apply (rule floor_eq2) 

843 
apply auto 

844 
done 

845 

846 
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1" 

847 
apply (case_tac "0 <= x") 

848 
apply (unfold natfloor_def) 

849 
apply simp 

850 
apply simp_all 

851 
done 

852 

853 
lemma real_natfloor_gt_diff_one: "x  1 < real(natfloor x)" 

854 
apply (simp add: compare_rls) 

855 
apply (rule real_natfloor_add_one_gt) 

856 
done 

857 

858 
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" 

859 
apply (subgoal_tac "z < real(natfloor z) + 1") 

860 
apply arith 

861 
apply (rule real_natfloor_add_one_gt) 

862 
done 

863 

864 
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a" 

865 
apply (unfold natfloor_def) 

866 
apply (subgoal_tac "real a = real (int a)") 

867 
apply (erule ssubst) 

868 
apply (simp add: nat_add_distrib) 

869 
apply simp 

870 
done 

871 

872 
lemma natfloor_add_number_of [simp]: 

873 
"~neg ((number_of n)::int) ==> 0 <= x ==> 

874 
natfloor (x + number_of n) = natfloor x + number_of n" 

875 
apply (subst natfloor_add [THEN sym]) 

876 
apply simp_all 

877 
done 

878 

879 
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1" 

880 
apply (subst natfloor_add [THEN sym]) 

881 
apply assumption 

882 
apply simp 

883 
done 

884 

885 
lemma natfloor_subtract [simp]: "real a <= x ==> 

886 
natfloor(x  real a) = natfloor x  a" 

887 
apply (unfold natfloor_def) 

888 
apply (subgoal_tac "real a = real (int a)") 

889 
apply (erule ssubst) 

890 
apply simp 

891 
apply (subst nat_diff_distrib) 

892 
apply simp 

893 
apply (rule le_floor) 

894 
apply simp_all 

895 
done 

896 

897 
lemma natceiling_zero [simp]: "natceiling 0 = 0" 

898 
by (unfold natceiling_def, simp) 

899 

900 
lemma natceiling_one [simp]: "natceiling 1 = 1" 

901 
by (unfold natceiling_def, simp) 

902 

903 
lemma zero_le_natceiling [simp]: "0 <= natceiling x" 

904 
by (unfold natceiling_def, simp) 

905 

906 
lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n" 

907 
by (unfold natceiling_def, simp) 

908 

909 
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n" 

910 
by (unfold natceiling_def, simp) 

911 

912 
lemma real_natceiling_ge: "x <= real(natceiling x)" 

913 
apply (unfold natceiling_def) 

914 
apply (case_tac "x < 0") 

915 
apply simp 

916 
apply (subst real_nat_eq_real) 

917 
apply (subgoal_tac "ceiling 0 <= ceiling x") 

918 
apply simp 

919 
apply (rule ceiling_mono2) 

920 
apply simp 

921 
apply simp 

922 
done 

923 

924 
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0" 

925 
apply (unfold natceiling_def) 

926 
apply simp 

927 
done 

928 

929 
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y" 

930 
apply (case_tac "0 <= x") 

931 
apply (subst natceiling_def)+ 

932 
apply (subst nat_le_eq_zle) 

933 
apply (rule disjI2) 

934 
apply (subgoal_tac "real (0::int) <= real(ceiling y)") 

935 
apply simp 

936 
apply (rule order_trans) 

937 
apply simp 

938 
apply (erule order_trans) 

939 
apply simp 

940 
apply (erule ceiling_mono2) 

941 
apply (subst natceiling_neg) 

942 
apply simp_all 

943 
done 

944 

945 
lemma natceiling_le: "x <= real a ==> natceiling x <= a" 

946 
apply (unfold natceiling_def) 

947 
apply (case_tac "x < 0") 

948 
apply simp 

949 
apply (subst nat_int [THEN sym]);back; 

950 
apply (subst nat_le_eq_zle) 

951 
apply simp 

952 
apply (rule ceiling_le) 

953 
apply simp 

954 
done 

955 

956 
lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)" 

957 
apply (rule iffI) 

958 
apply (rule order_trans) 

959 
apply (rule real_natceiling_ge) 

960 
apply (subst real_of_nat_le_iff) 

961 
apply assumption 

962 
apply (erule natceiling_le) 

963 
done 

964 

16820  965 
lemma natceiling_le_eq_number_of [simp]: 
966 
"~ neg((number_of n)::int) ==> 0 <= x ==> 

967 
(natceiling x <= number_of n) = (x <= number_of n)" 

16819  968 
apply (subst natceiling_le_eq, assumption) 
969 
apply simp 

970 
done 

971 

16820  972 
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" 
16819  973 
apply (case_tac "0 <= x") 
974 
apply (subst natceiling_le_eq) 

975 
apply assumption 

976 
apply simp 

977 
apply (subst natceiling_neg) 

978 
apply simp 

979 
apply simp 

980 
done 

981 

982 
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1" 

983 
apply (unfold natceiling_def) 

984 
apply (subst nat_int [THEN sym]);back; 

985 
apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)") 

986 
apply (erule ssubst) 

987 
apply (subst eq_nat_nat_iff) 

988 
apply (subgoal_tac "ceiling 0 <= ceiling x") 

989 
apply simp 

990 
apply (rule ceiling_mono2) 

991 
apply force 

992 
apply force 

993 
apply (rule ceiling_eq2) 

994 
apply (simp, simp) 

995 
apply (subst nat_add_distrib) 

996 
apply auto 

997 
done 

998 

999 
lemma natceiling_add [simp]: "0 <= x ==> 

1000 
natceiling (x + real a) = natceiling x + a" 

1001 
apply (unfold natceiling_def) 

1002 
apply (subgoal_tac "real a = real (int a)") 

1003 
apply (erule ssubst) 

1004 
apply simp 

1005 
apply (subst nat_add_distrib) 

1006 
apply (subgoal_tac "0 = ceiling 0") 

1007 
apply (erule ssubst) 

1008 
apply (erule ceiling_mono2) 

1009 
apply simp_all 

1010 
done 

1011 

16820  1012 
lemma natceiling_add_number_of [simp]: 
1013 
"~ neg ((number_of n)::int) ==> 0 <= x ==> 

1014 
natceiling (x + number_of n) = natceiling x + number_of n" 

16819  1015 
apply (subst natceiling_add [THEN sym]) 
1016 
apply simp_all 

1017 
done 

1018 

1019 
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1" 

1020 
apply (subst natceiling_add [THEN sym]) 

1021 
apply assumption 

1022 
apply simp 

1023 
done 

1024 

1025 
lemma natceiling_subtract [simp]: "real a <= x ==> 

1026 
natceiling(x  real a) = natceiling x  a" 

1027 
apply (unfold natceiling_def) 

1028 
apply (subgoal_tac "real a = real (int a)") 

1029 
apply (erule ssubst) 

1030 
apply simp 

1031 
apply (subst nat_diff_distrib) 

1032 
apply simp 

1033 
apply (rule order_trans) 

1034 
prefer 2 

1035 
apply (rule ceiling_mono2) 

1036 
apply assumption 

1037 
apply simp_all 

1038 
done 

1039 

1040 
lemma natfloor_div_nat: "1 <= x ==> 0 < y ==> 

1041 
natfloor (x / real y) = natfloor x div y" 

1042 
proof  

1043 
assume "1 <= (x::real)" and "0 < (y::nat)" 

1044 
have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y" 

1045 
by simp 

1046 
then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + 

1047 
real((natfloor x) mod y)" 

1048 
by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym]) 

1049 
have "x = real(natfloor x) + (x  real(natfloor x))" 

1050 
by simp 

1051 
then have "x = real ((natfloor x) div y) * real y + 

1052 
real((natfloor x) mod y) + (x  real(natfloor x))" 

1053 
by (simp add: a) 

1054 
then have "x / real y = ... / real y" 

1055 
by simp 

1056 
also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / 

1057 
real y + (x  real(natfloor x)) / real y" 

1058 
by (auto simp add: ring_distrib ring_eq_simps add_divide_distrib 

1059 
diff_divide_distrib prems) 

1060 
finally have "natfloor (x / real y) = natfloor(...)" by simp 

1061 
also have "... = natfloor(real((natfloor x) mod y) / 

1062 
real y + (x  real(natfloor x)) / real y + real((natfloor x) div y))" 

1063 
by (simp add: add_ac) 

1064 
also have "... = natfloor(real((natfloor x) mod y) / 

1065 
real y + (x  real(natfloor x)) / real y) + (natfloor x) div y" 

1066 
apply (rule natfloor_add) 

1067 
apply (rule add_nonneg_nonneg) 

1068 
apply (rule divide_nonneg_pos) 

1069 
apply simp 

1070 
apply (simp add: prems) 

1071 
apply (rule divide_nonneg_pos) 

1072 
apply (simp add: compare_rls) 

1073 
apply (rule real_natfloor_le) 

1074 
apply (insert prems, auto) 

1075 
done 

1076 
also have "natfloor(real((natfloor x) mod y) / 

1077 
real y + (x  real(natfloor x)) / real y) = 0" 

1078 
apply (rule natfloor_eq) 

1079 
apply simp 

1080 
apply (rule add_nonneg_nonneg) 

1081 
apply (rule divide_nonneg_pos) 

1082 
apply force 

1083 
apply (force simp add: prems) 

1084 
apply (rule divide_nonneg_pos) 

1085 
apply (simp add: compare_rls) 

1086 
apply (rule real_natfloor_le) 

1087 
apply (auto simp add: prems) 

1088 
apply (insert prems, arith) 

1089 
apply (simp add: add_divide_distrib [THEN sym]) 

1090 
apply (subgoal_tac "real y = real y  1 + 1") 

1091 
apply (erule ssubst) 

1092 
apply (rule add_le_less_mono) 

1093 
apply (simp add: compare_rls) 

1094 
apply (subgoal_tac "real(natfloor x mod y) + 1 = 

1095 
real(natfloor x mod y + 1)") 

1096 
apply (erule ssubst) 

1097 
apply (subst real_of_nat_le_iff) 

1098 
apply (subgoal_tac "natfloor x mod y < y") 

1099 
apply arith 

1100 
apply (rule mod_less_divisor) 

1101 
apply assumption 

1102 
apply auto 

1103 
apply (simp add: compare_rls) 

1104 
apply (subst add_commute) 

1105 
apply (rule real_natfloor_add_one_gt) 

1106 
done 

1107 
finally show ?thesis 

1108 
by simp 

1109 
qed 

1110 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1111 
ML 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1112 
{* 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1113 
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

1114 
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

1115 
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

1116 
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

1117 
val floor_zero = thm "floor_zero"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1118 
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

1119 
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

1120 
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

1121 
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

1122 
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

1123 
val reals_Archimedean6 = thm "reals_Archimedean6"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1124 
val reals_Archimedean6a = thm "reals_Archimedean6a"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1125 
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

1126 
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

1127 
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

1128 
val lemma_floor = thm "lemma_floor"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1129 
val real_of_int_floor_le = thm "real_of_int_floor_le"; 
16819  1130 
(*val floor_le = thm "floor_le"; 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1131 
val floor_le2 = thm "floor_le2"; 
16819  1132 
*) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1133 
val lemma_floor2 = thm "lemma_floor2"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1134 
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

1135 
val floor_eq = thm "floor_eq"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1136 
val floor_eq2 = thm "floor_eq2"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1137 
val floor_eq3 = thm "floor_eq3"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1138 
val floor_eq4 = thm "floor_eq4"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1139 
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

1140 
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

1141 
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

1142 
val ceiling_zero = thm "ceiling_zero"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1143 
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

1144 
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

1145 
val ceiling_floor = thm "ceiling_floor"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1146 
val floor_ceiling = thm "floor_ceiling"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1147 
val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge"; 
16819  1148 
(* 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1149 
val ceiling_le = thm "ceiling_le"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1150 
val ceiling_le2 = thm "ceiling_le2"; 
16819  1151 
*) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1152 
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

1153 
val ceiling_eq = thm "ceiling_eq"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1154 
val ceiling_eq2 = thm "ceiling_eq2"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1155 
val ceiling_eq3 = thm "ceiling_eq3"; 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1156 
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

1157 
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

1158 
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

1159 
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

1160 
*} 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1161 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

1162 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

1163 
end 