author  paulson 
Fri, 19 Mar 2004 10:50:06 +0100  
changeset 14476  758e7acdea2f 
parent 14387  e96d5c42c4b0 
child 14641  79b7bd936264 
permissions  rwrr 
5078  1 
(* Title : RComplete.thy 
7219  2 
ID : $Id$ 
5078  3 
Author : Jacques D. Fleuriot 
4 
Copyright : 1998 University of Cambridge 

5 
Description : Completeness theorems for positive 

6 
reals and reals 

7 
*) 

8 

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

9 
header{*Completeness Theorems for Positive Reals and Reals.*} 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

10 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14365
diff
changeset

11 
theory RComplete = Lubs + RealDef: 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

12 

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

13 
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

14 
by simp 
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 

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

17 
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

18 

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

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

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

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

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

23 
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

24 

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

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

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

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

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

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

30 
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

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

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

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

34 
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

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

36 

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

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

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

42 
Supremum property for the set of positive reals 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

43 
FIXME: long proof  should be improved 
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 

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

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

47 
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

48 
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

49 
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

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

51 
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

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

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

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

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

56 
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

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

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

59 
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

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

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

62 
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

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

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

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

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

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

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

69 

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

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

71 
Completeness properties using isUb, isLub etc. 
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 
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

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

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

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

79 

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

80 
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

81 
by (unfold setle_def setge_def, blast) 
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 
(* 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

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

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

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

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

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

92 
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

93 
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

94 
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

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

96 
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

97 
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

98 
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

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

100 
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

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

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

103 
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

104 
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

105 
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

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

107 

5078  108 

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

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

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

113 
by auto 
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 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

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

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

122 
reals Completeness (again!) 
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 
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

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

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

127 
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

128 
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

129 
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

130 
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

131 
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

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

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

134 
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

135 
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

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

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

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

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

140 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

154 
apply (simp (no_asm_use) add: real_add_assoc) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

155 
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

156 
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

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

158 

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

159 

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

160 
subsection{*Corollary: the Archimedean Property of the Reals*} 
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 
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

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

164 
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

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

166 
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

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

168 
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

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

170 
apply (simp add: real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_commute) 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

171 
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

172 
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

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

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

175 
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

176 
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

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

178 
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

179 
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

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

181 
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

182 
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

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

184 

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

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

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

187 
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

188 
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

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

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

191 
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

192 
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

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

194 
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

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

196 

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

197 
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

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

199 
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

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

201 
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

202 
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

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

204 

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

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

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

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

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

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

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

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

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

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

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

217 

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

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

219 

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

220 

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

221 