author  nipkow 
Mon, 21 Feb 2005 15:04:10 +0100  
changeset 15539  333a88244569 
parent 15234  ec91a90c604e 
child 16819  00d8f9300d13 
permissions  rwrr 
5078  1 
(* Title : RComplete.thy 
7219  2 
ID : $Id$ 
5078  3 
Author : Jacques D. Fleuriot 
4 
Copyright : 1998 University of Cambridge 

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

5 
Copyright : 2001,2002 University of Edinburgh 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

6 
Converted to Isar and polished by lcp 
5078  7 
*) 
8 

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

9 
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

10 

15131  11 
theory RComplete 
15140  12 
imports Lubs RealDef 
15131  13 
begin 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

14 

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

15 
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

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

17 

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

20 

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

21 
(*a few lemmas*) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

23 
"\<forall>x \<in> P. 0 < x ==> 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

24 
((\<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

25 
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

26 

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

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

28 
"[ \<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

29 
==> (\<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

30 
(\<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

31 
apply (rule conjI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

32 
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

33 
apply (drule bspec, assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

34 
apply (frule bspec, assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

35 
apply (drule order_less_trans, assumption) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset

36 
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

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

38 

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 
Completeness of Positive Reals 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

41 
*) 
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 
Supremum property for the set of positive reals 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

45 
FIXME: long proof  should be improved 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

46 
**) 
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 
(*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

49 
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

50 
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

51 
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

52 
==> (\<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

53 
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

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

55 
apply (case_tac "0 < ya", auto) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

56 
apply (frule real_sup_lemma2, assumption+) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

57 
apply (drule real_gt_zero_preal_Ex [THEN iffD1]) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset

58 
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

59 
apply (rule preal_complete [THEN iffD1]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

60 
apply (auto intro: order_less_imp_le) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset

61 
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

62 
(* second part *) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

63 
apply (rule real_sup_lemma1 [THEN iffD2], assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

64 
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

65 
apply (frule_tac [2] real_sup_lemma2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

66 
apply (frule real_sup_lemma2, assumption+, clarify) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

67 
apply (rule preal_complete [THEN iffD2, THEN bexE]) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

69 
apply (blast intro!: order_less_imp_le)+ 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

71 

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 
Completeness properties using isUb, isLub etc. 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

74 
*) 
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 
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

77 
apply (frule isLub_isUb) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

78 
apply (frule_tac x = y in isLub_isUb) 
14476  79 
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

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

81 

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

82 
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

83 
by (unfold setle_def setge_def, blast) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

84 

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 
Completeness theorem for the positive reals(again) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

87 
*) 
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 
lemma posreals_complete: 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

90 
"[ \<forall>x \<in>S. 0 < x; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

91 
\<exists>x. x \<in>S; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

92 
\<exists>u. isUb (UNIV::real set) S u 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

93 
] ==> \<exists>t. isLub (UNIV::real set) S t" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

94 
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

95 
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

96 
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

97 
apply (frule_tac x = y in bspec, assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

98 
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

99 
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

100 
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

101 
apply (frule real_ge_preal_preal_Ex, safe) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

102 
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

103 
apply (frule_tac x = x in bspec, assumption) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

104 
apply (frule isUbD2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

105 
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

106 
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

107 
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

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

109 

5078  110 

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

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

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

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

114 
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

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

116 

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

117 
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

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

119 

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

120 
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

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

122 

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 
reals Completeness (again!) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

126 
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

127 
==> \<exists>t. isLub (UNIV :: real set) S t" 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

129 
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

130 
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

131 
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

132 
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

133 
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

134 
apply (rule isLubI2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

135 
apply (rule_tac [2] setgeI, safe) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

136 
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

137 
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

138 
prefer 2 apply assumption 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

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

141 
apply (rule setleI [THEN isUbI], safe) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

142 
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

143 
apply (subst lemma_le_swap2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

144 
apply (frule isLubD2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

145 
prefer 2 apply assumption 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

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

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

149 
apply (subst lemma_le_swap2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

150 
apply (frule isLubD2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

151 
prefer 2 apply assumption 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

153 
apply (rule lemma_real_complete2b) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

154 
apply (erule_tac [2] order_less_imp_le) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

155 
apply (blast intro!: isLubD2, blast) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

156 
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

157 
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

158 
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

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

160 

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 
subsection{*Corollary: the Archimedean Property of the Reals*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

163 

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

164 
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

165 
apply (rule ccontr) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

166 
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

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

168 
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

169 
apply (drule_tac x = n in spec) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

170 
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

171 
apply (rule real_of_nat_ge_zero) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

172 
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

173 
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

174 
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

175 
apply (drule reals_complete) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

176 
apply (auto intro: isUbI setleI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

177 
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

178 
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

179 
prefer 2 apply (blast intro: isLubD2) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

180 
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

181 
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

182 
prefer 2 apply (blast intro!: isUbI setleI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

183 
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

184 
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

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

186 

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

187 
(*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

188 
cut representing x*) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

189 
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

190 
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

191 
apply (rule_tac x = 0 in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

192 
apply (rule_tac [2] x = 1 in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

193 
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

194 
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

195 
apply (rule_tac x = "Suc n" in exI) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

196 
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

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

198 

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

199 
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

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

201 
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

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

203 
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

204 
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

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

206 

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

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

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

209 
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

210 
val posreal_complete = thm "posreal_complete"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

211 
val real_isLub_unique = thm "real_isLub_unique"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

212 
val real_order_restrict = thm "real_order_restrict"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

213 
val posreals_complete = thm "posreals_complete"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

214 
val reals_complete = thm "reals_complete"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

215 
val reals_Archimedean = thm "reals_Archimedean"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

216 
val reals_Archimedean2 = thm "reals_Archimedean2"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

217 
val reals_Archimedean3 = thm "reals_Archimedean3"; 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

219 

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

220 

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

221 
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

222 

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

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

224 

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

225 
floor :: "real => int" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

226 
"floor r == (LEAST n::int. r < real (n+1))" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

227 

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

228 
ceiling :: "real => int" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

229 
"ceiling r ==  floor ( r)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

230 

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

231 
syntax (xsymbols) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

232 
floor :: "real => int" ("\<lfloor>_\<rfloor>") 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

233 
ceiling :: "real => int" ("\<lceil>_\<rceil>") 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

234 

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

235 
syntax (HTML output) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

236 
floor :: "real => int" ("\<lfloor>_\<rfloor>") 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

237 
ceiling :: "real => int" ("\<lceil>_\<rceil>") 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

238 

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

239 

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

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

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

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

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

244 
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

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

246 

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

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

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

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

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

251 
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

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

253 

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

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

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

256 
by (simp add: linorder_not_less [symmetric]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

257 

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

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

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

260 
by (simp add: linorder_not_less [symmetric]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

261 

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

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

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

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

265 
done 
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 
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

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

269 

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

270 
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

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

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

273 
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

274 
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

275 
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

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

277 

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

278 
lemma 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

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

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

281 
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

282 
apply (drule_tac [2] real_of_int_minus [THEN subst]) 
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 iffD1]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

284 
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

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

286 

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

287 
lemma 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

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

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

290 
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

291 
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

292 
done 
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_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

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

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

297 
apply (drule_tac [2] real_of_int_minus [THEN subst]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

298 
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

299 
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

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

301 

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

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

303 
"0 \<le> r ==> \<exists>(n::nat). real (n  1) \<le> r & r < real (n)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

305 
apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

306 
in ex_has_least_nat, auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

308 
apply (case_tac x, simp) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

309 
apply (rename_tac x') 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

310 
apply (drule_tac x = x' in spec, simp) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

312 

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

313 
lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

314 
by (drule reals_Archimedean6, auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

315 

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

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

317 
"0 \<le> r ==> \<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

318 
apply (drule reals_Archimedean6a, auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

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

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

322 

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

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

324 
"r < 0 ==> \<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

325 
apply (rule reals_Archimedean_6b_int [of "r", THEN exE], simp, auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

326 
apply (rename_tac n) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

327 
apply (drule real_le_imp_less_or_eq, auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

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

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

331 

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

332 
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

333 
apply (case_tac "r < 0") 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

334 
apply (blast intro: reals_Archimedean_6c_int) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

335 
apply (simp only: linorder_not_less) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

336 
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

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

338 

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

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

340 
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

341 
shows "m \<le> (n::int)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

343 
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

344 
also have "... = real(n+1)" by simp 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

345 
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

346 
thus ?thesis by arith 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

348 

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

349 
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

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

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

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

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

354 

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

355 
lemma floor_le: "x < y ==> floor x \<le> floor y" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

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

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

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

360 
apply (rule_tac [3] theI2, auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

362 

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

363 
lemma floor_le2: "x \<le> y ==> floor x \<le> floor y" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

364 
by (auto dest: real_le_imp_less_or_eq simp add: floor_le) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

365 

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

366 
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

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

368 

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

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

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

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

372 
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

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

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

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

376 

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

377 
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

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

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

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

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

382 

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

383 
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

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

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

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

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

388 

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

389 
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

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

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

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

394 

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

395 
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

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

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

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

399 

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

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

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

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

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

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

405 

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

406 
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

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

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

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

410 
apply (auto intro: lemma_floor) 
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 

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

413 
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

414 
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

415 
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

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

417 

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

418 

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

419 
subsection{*Ceiling Function for Positive Reals*} 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

420 

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

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

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

423 

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

424 
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

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

426 

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

427 
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

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

429 

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

430 
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

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

432 

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

433 
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

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

435 

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

436 
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

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

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

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

440 

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

441 
lemma ceiling_le: "x < y ==> ceiling x \<le> ceiling y" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

443 

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

444 
lemma ceiling_le2: "x \<le> y ==> ceiling x \<le> ceiling y" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

446 

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

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

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

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

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

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

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

453 

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

454 
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

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

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

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

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

459 

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

460 
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

461 
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

462 

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

463 
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

464 
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

465 

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

466 
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

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

468 

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

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

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

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

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

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

474 

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

475 
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

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

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

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

479 

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

480 
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

481 
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

482 
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

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

484 

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

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

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

487 
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

488 
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

489 
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

490 
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

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

492 
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

493 
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

494 
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

495 
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

496 
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

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

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

499 
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

500 
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

501 
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

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

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

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

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

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

507 
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

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

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

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

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

512 
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

513 
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

514 
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

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

516 
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

517 
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

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

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

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

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

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

523 
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

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

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

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

527 
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

528 
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

529 
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

530 
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

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

532 

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

533 

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

534 
end 