author  paulson 
Thu, 29 Jul 2004 16:14:42 +0200  
changeset 15085  5693a977a767 
parent 15003  6145dd7538d7 
child 15131  c69542757a4d 
permissions  rwrr 
9435
c3a13a7d4424
lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
wenzelm
parents:
9013
diff
changeset

1 
(* Title : HOL/Real/RealPow.thy 
7219  2 
ID : $Id$ 
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

3 
Author : Jacques D. Fleuriot 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

4 
Copyright : 1998 University of Cambridge 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

5 
Description : Natural powers theory 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

6 

60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

7 
*) 
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

8 

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

9 
theory RealPow = RealDef: 
9435
c3a13a7d4424
lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
wenzelm
parents:
9013
diff
changeset

10 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

11 
declare abs_mult_self [simp] 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

12 

10309  13 
instance real :: power .. 
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

14 

8856  15 
primrec (realpow) 
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset

16 
realpow_0: "r ^ 0 = 1" 
9435
c3a13a7d4424
lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
wenzelm
parents:
9013
diff
changeset

17 
realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" 
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

18 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

19 

15003  20 
instance real :: recpower 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

21 
proof 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

22 
fix z :: real 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

23 
fix n :: nat 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

24 
show "z^0 = 1" by simp 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

25 
show "z^(Suc n) = z * (z^n)" by simp 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

26 
qed 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

27 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

28 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

29 
lemma realpow_not_zero: "r \<noteq> (0::real) ==> r ^ n \<noteq> 0" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

30 
by (rule field_power_not_zero) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

31 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

32 
lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

33 
by simp 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

34 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

35 
lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

36 
by simp 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

37 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

38 
text{*Legacy: weaker version of the theorem @{text power_strict_mono}, 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

39 
used 6 times in NthRoot and Transcendental*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

40 
lemma realpow_less: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

41 
"[(0::real) < x; x < y; 0 < n] ==> x ^ n < y ^ n" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

42 
apply (rule power_strict_mono, auto) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

43 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

44 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

45 
lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

46 
by (simp add: real_le_square) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

47 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

48 
lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

49 
by (simp add: abs_mult) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

50 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

51 
lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

52 
by (simp add: power_abs [symmetric] abs_eqI1 del: realpow_Suc) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

53 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

54 
lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

55 
by (insert power_increasing [of 0 n "2::real"], simp) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

56 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

57 
lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

58 
apply (induct_tac "n") 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

59 
apply (auto simp add: real_of_nat_Suc) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14352
diff
changeset

60 
apply (subst mult_2) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

61 
apply (rule real_add_less_le_mono) 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

62 
apply (auto simp add: two_realpow_ge_one) 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

63 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

64 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

65 
lemma realpow_Suc_le_self: "[ 0 \<le> r; r \<le> (1::real) ] ==> r ^ Suc n \<le> r" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

66 
by (insert power_decreasing [of 1 "Suc n" r], simp) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

67 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

68 
text{*Used ONCE in Transcendental*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

69 
lemma realpow_Suc_less_one: "[ 0 < r; r < (1::real) ] ==> r ^ Suc n < 1" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

70 
by (insert power_strict_decreasing [of 0 "Suc n" r], simp) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

71 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

72 
text{*Used ONCE in Lim.ML*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

73 
lemma realpow_minus_mult [rule_format]: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

74 
"0 < n > (x::real) ^ (n  1) * x = x ^ n" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

75 
apply (simp split add: nat_diff_split) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

76 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

77 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

78 
lemma realpow_two_mult_inverse [simp]: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

79 
"r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

80 
by (simp add: realpow_two real_mult_assoc [symmetric]) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

81 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

82 
lemma realpow_two_minus [simp]: "(x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

83 
by simp 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

84 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

85 
lemma realpow_two_diff: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

86 
"(x::real)^Suc (Suc 0)  y^Suc (Suc 0) = (x  y) * (x + y)" 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

87 
apply (unfold real_diff_def) 
14334  88 
apply (simp add: right_distrib left_distrib mult_ac) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

89 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

90 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

91 
lemma realpow_two_disj: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

92 
"((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y  x = y)" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

93 
apply (cut_tac x = x and y = y in realpow_two_diff) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

94 
apply (auto simp del: realpow_Suc) 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

95 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

96 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

97 
lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)" 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

98 
apply (induct_tac "n") 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

99 
apply (auto simp add: real_of_nat_one real_of_nat_mult) 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

100 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

101 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

102 
lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)" 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

103 
apply (induct_tac "n") 
14334  104 
apply (auto simp add: real_of_nat_mult zero_less_mult_iff) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

105 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

106 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

107 
lemma realpow_increasing: 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

108 
"[(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n] ==> x \<le> y" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

109 
by (rule power_le_imp_le_base) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

110 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

111 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

112 
lemma zero_less_realpow_abs_iff [simp]: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

113 
"(0 < (abs x)^n) = (x \<noteq> (0::real)  n=0)" 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

114 
apply (induct_tac "n") 
14334  115 
apply (auto simp add: zero_less_mult_iff) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

116 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

117 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

118 
lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n" 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

119 
apply (induct_tac "n") 
14334  120 
apply (auto simp add: zero_le_mult_iff) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

121 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

122 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

123 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

124 
subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*} 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

125 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

126 
lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)" 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

127 
apply (induct_tac "n") 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14352
diff
changeset

128 
apply (simp_all add: nat_mult_distrib) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

129 
done 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

130 
declare real_of_int_power [symmetric, simp] 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

131 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

132 
lemma power_real_number_of: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

133 
"(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)" 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14352
diff
changeset

134 
by (simp only: real_number_of [symmetric] real_of_int_power) 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

135 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

136 
declare power_real_number_of [of _ "number_of w", standard, simp] 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

137 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

138 

14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

139 
subsection{*Various Other Theorems*} 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

140 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

141 
text{*Used several times in Hyperreal/Transcendental.ML*} 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

142 
lemma real_sum_squares_cancel_a: "x * x = (y * y) ==> x = (0::real) & y=0" 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15003
diff
changeset

143 
apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric]) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15003
diff
changeset

144 
apply (auto dest: real_sum_squares_cancel simp add: add_commute) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15003
diff
changeset

145 
done 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

146 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

147 
lemma real_squared_diff_one_factored: "x*x  (1::real) = (x + 1)*(x  1)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

148 
by (auto simp add: left_distrib right_distrib real_diff_def) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

149 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

150 
lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1  x =  1)" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

151 
apply auto 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

152 
apply (drule right_minus_eq [THEN iffD2]) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

153 
apply (auto simp add: real_squared_diff_one_factored) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

154 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

155 

14304  156 
lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

157 
by auto 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

158 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

159 
lemma real_minus_half_eq [simp]: "(x::real)  x/2 = x/2" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

160 
by auto 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

161 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

162 
lemma real_mult_inverse_cancel: 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

163 
"[(0::real) < x; 0 < x1; x1 * y < x * u ] 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

164 
==> inverse x * y < inverse x1 * u" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

165 
apply (rule_tac c=x in mult_less_imp_less_left) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

166 
apply (auto simp add: real_mult_assoc [symmetric]) 
14334  167 
apply (simp (no_asm) add: mult_ac) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

168 
apply (rule_tac c=x1 in mult_less_imp_less_right) 
14334  169 
apply (auto simp add: mult_ac) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

170 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

171 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

172 
text{*Used once: in Hyperreal/Transcendental.ML*} 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

173 
lemma real_mult_inverse_cancel2: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

174 
"[(0::real) < x;0 < x1; x1 * y < x * u ] ==> y * inverse x < u * inverse x1" 
14334  175 
apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

176 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

177 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

178 
lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

179 
by auto 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

180 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

181 
lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

182 
by auto 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

183 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

184 
lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

185 
by (blast dest!: real_sum_squares_cancel) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

186 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

187 
lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

188 
by (blast dest!: real_sum_squares_cancel2) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

189 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

190 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

191 
subsection {*Various Other Theorems*} 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

192 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

193 
lemma realpow_divide: 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

194 
"(x/y) ^ n = ((x::real) ^ n/ y ^ n)" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

195 
apply (unfold real_divide_def) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

196 
apply (auto simp add: power_mult_distrib power_inverse) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

197 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

198 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

199 
lemma realpow_two_sum_zero_iff [simp]: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

200 
"(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

201 
apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 
14352  202 
simp add: power2_eq_square) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

203 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

204 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

205 
lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

206 
apply (rule real_le_add_order) 
14352  207 
apply (auto simp add: power2_eq_square) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

208 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

209 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

210 
lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

211 
apply (rule real_le_add_order)+ 
14352  212 
apply (auto simp add: power2_eq_square) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

213 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

214 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

215 
lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

216 
apply (cut_tac x = x and y = y in real_mult_self_sum_ge_zero) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

217 
apply (drule real_le_imp_less_or_eq) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

218 
apply (drule_tac y = y in real_sum_squares_not_zero, auto) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

219 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

220 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

221 
lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y" 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

222 
apply (rule real_add_commute [THEN subst]) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

223 
apply (erule real_sum_square_gt_zero) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

224 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

225 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

226 
lemma real_minus_mult_self_le [simp]: "(u * u) \<le> (x * (x::real))" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

227 
by (rule_tac j = 0 in real_le_trans, auto) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

228 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

229 
lemma realpow_square_minus_le [simp]: "(u ^ 2) \<le> (x::real) ^ 2" 
14352  230 
by (auto simp add: power2_eq_square) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

231 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

232 
lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n  1))" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

233 
by (case_tac "n", auto) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

234 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

235 
lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

236 
apply (induct_tac "d") 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

237 
apply (auto simp add: realpow_num_eq_if) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

238 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

239 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

240 
lemma lemma_realpow_num_two_mono: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14334
diff
changeset

241 
"x * (4::real) < y ==> x * (2 ^ 8) < y * (2 ^ 6)" 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

242 
apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ") 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

243 
apply (simp (no_asm_simp) add: real_mult_assoc [symmetric]) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

244 
apply (auto simp add: realpow_num_eq_if) 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

245 
done 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

246 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

247 

14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

248 
ML 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

249 
{* 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

250 
val realpow_0 = thm "realpow_0"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

251 
val realpow_Suc = thm "realpow_Suc"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

252 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

253 
val realpow_not_zero = thm "realpow_not_zero"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

254 
val realpow_zero_zero = thm "realpow_zero_zero"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

255 
val realpow_two = thm "realpow_two"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

256 
val realpow_less = thm "realpow_less"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

257 
val realpow_two_le = thm "realpow_two_le"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

258 
val abs_realpow_two = thm "abs_realpow_two"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

259 
val realpow_two_abs = thm "realpow_two_abs"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

260 
val two_realpow_ge_one = thm "two_realpow_ge_one"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

261 
val two_realpow_gt = thm "two_realpow_gt"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

262 
val realpow_Suc_le_self = thm "realpow_Suc_le_self"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

263 
val realpow_Suc_less_one = thm "realpow_Suc_less_one"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

264 
val realpow_minus_mult = thm "realpow_minus_mult"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

265 
val realpow_two_mult_inverse = thm "realpow_two_mult_inverse"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

266 
val realpow_two_minus = thm "realpow_two_minus"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

267 
val realpow_two_disj = thm "realpow_two_disj"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

268 
val realpow_real_of_nat = thm "realpow_real_of_nat"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

269 
val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

270 
val realpow_increasing = thm "realpow_increasing"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

271 
val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

272 
val zero_le_realpow_abs = thm "zero_le_realpow_abs"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

273 
val real_of_int_power = thm "real_of_int_power"; 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

274 
val power_real_number_of = thm "power_real_number_of"; 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

275 
val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

276 
val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

277 
val real_squared_diff_one_factored = thm "real_squared_diff_one_factored"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

278 
val real_mult_is_one = thm "real_mult_is_one"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

279 
val real_le_add_half_cancel = thm "real_le_add_half_cancel"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

280 
val real_minus_half_eq = thm "real_minus_half_eq"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

281 
val real_mult_inverse_cancel = thm "real_mult_inverse_cancel"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

282 
val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

283 
val inverse_real_of_nat_gt_zero = thm "inverse_real_of_nat_gt_zero"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

284 
val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

285 
val real_sum_squares_not_zero = thm "real_sum_squares_not_zero"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

286 
val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

287 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

288 
val realpow_divide = thm "realpow_divide"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

289 
val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

290 
val realpow_two_le_add_order = thm "realpow_two_le_add_order"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

291 
val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

292 
val real_sum_square_gt_zero = thm "real_sum_square_gt_zero"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

293 
val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

294 
val real_minus_mult_self_le = thm "real_minus_mult_self_le"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

295 
val realpow_square_minus_le = thm "realpow_square_minus_le"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

296 
val realpow_num_eq_if = thm "realpow_num_eq_if"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

297 
val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow"; 
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14265
diff
changeset

298 
val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono"; 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

299 
*} 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

300 

95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
12018
diff
changeset

301 

7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset

302 
end 