74 by (induct_tac "n" 1); |
74 by (induct_tac "n" 1); |
75 by Auto_tac; |
75 by Auto_tac; |
76 qed "realpow_eq_one"; |
76 qed "realpow_eq_one"; |
77 Addsimps [realpow_eq_one]; |
77 Addsimps [realpow_eq_one]; |
78 |
78 |
79 Goal "abs((# -1) ^ n) = (Numeral1::real)"; |
79 Goal "abs((-1) ^ n) = (Numeral1::real)"; |
80 by (induct_tac "n" 1); |
80 by (induct_tac "n" 1); |
81 by (auto_tac (claset(), simpset() addsimps [abs_mult])); |
81 by (auto_tac (claset(), simpset() addsimps [abs_mult])); |
82 qed "abs_realpow_minus_one"; |
82 qed "abs_realpow_minus_one"; |
83 Addsimps [abs_realpow_minus_one]; |
83 Addsimps [abs_realpow_minus_one]; |
84 |
84 |
125 Goal "(Numeral1::real) <= r ==> Numeral1 <= r ^ n"; |
125 Goal "(Numeral1::real) <= r ==> Numeral1 <= r ^ n"; |
126 by (dtac order_le_imp_less_or_eq 1); |
126 by (dtac order_le_imp_less_or_eq 1); |
127 by (auto_tac (claset() addDs [realpow_ge_one], simpset())); |
127 by (auto_tac (claset() addDs [realpow_ge_one], simpset())); |
128 qed "realpow_ge_one2"; |
128 qed "realpow_ge_one2"; |
129 |
129 |
130 Goal "(Numeral1::real) <= # 2 ^ n"; |
130 Goal "(Numeral1::real) <= 2 ^ n"; |
131 by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1); |
131 by (res_inst_tac [("y","Numeral1 ^ n")] order_trans 1); |
132 by (rtac realpow_le 2); |
132 by (rtac realpow_le 2); |
133 by (auto_tac (claset() addIs [order_less_imp_le], simpset())); |
133 by (auto_tac (claset() addIs [order_less_imp_le], simpset())); |
134 qed "two_realpow_ge_one"; |
134 qed "two_realpow_ge_one"; |
135 |
135 |
136 Goal "real (n::nat) < # 2 ^ n"; |
136 Goal "real (n::nat) < 2 ^ n"; |
137 by (induct_tac "n" 1); |
137 by (induct_tac "n" 1); |
138 by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); |
138 by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); |
139 by (stac real_mult_2 1); |
139 by (stac real_mult_2 1); |
140 by (rtac real_add_less_le_mono 1); |
140 by (rtac real_add_less_le_mono 1); |
141 by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one])); |
141 by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one])); |
142 qed "two_realpow_gt"; |
142 qed "two_realpow_gt"; |
143 Addsimps [two_realpow_gt,two_realpow_ge_one]; |
143 Addsimps [two_realpow_gt,two_realpow_ge_one]; |
144 |
144 |
145 Goal "(# -1) ^ (# 2*n) = (Numeral1::real)"; |
145 Goal "(-1) ^ (2*n) = (Numeral1::real)"; |
146 by (induct_tac "n" 1); |
146 by (induct_tac "n" 1); |
147 by Auto_tac; |
147 by Auto_tac; |
148 qed "realpow_minus_one"; |
148 qed "realpow_minus_one"; |
149 Addsimps [realpow_minus_one]; |
149 Addsimps [realpow_minus_one]; |
150 |
150 |
151 Goal "(# -1) ^ Suc (# 2*n) = -(Numeral1::real)"; |
151 Goal "(-1) ^ Suc (2*n) = -(Numeral1::real)"; |
152 by Auto_tac; |
152 by Auto_tac; |
153 qed "realpow_minus_one_odd"; |
153 qed "realpow_minus_one_odd"; |
154 Addsimps [realpow_minus_one_odd]; |
154 Addsimps [realpow_minus_one_odd]; |
155 |
155 |
156 Goal "(# -1) ^ Suc (Suc (# 2*n)) = (Numeral1::real)"; |
156 Goal "(-1) ^ Suc (Suc (2*n)) = (Numeral1::real)"; |
157 by Auto_tac; |
157 by Auto_tac; |
158 qed "realpow_minus_one_even"; |
158 qed "realpow_minus_one_even"; |
159 Addsimps [realpow_minus_one_even]; |
159 Addsimps [realpow_minus_one_even]; |
160 |
160 |
161 Goal "(Numeral0::real) < r & r < (Numeral1::real) --> r ^ Suc n < r ^ n"; |
161 Goal "(Numeral0::real) < r & r < (Numeral1::real) --> r ^ Suc n < r ^ n"; |