equal
deleted
inserted
replaced
104 by (induct_tac "n" 1); |
104 by (induct_tac "n" 1); |
105 by (auto_tac (claset(),simpset() addsimps [abs_mult, |
105 by (auto_tac (claset(),simpset() addsimps [abs_mult, |
106 abs_minus_cancel,abs_one])); |
106 abs_minus_cancel,abs_one])); |
107 qed "abs_realpow_minus_one"; |
107 qed "abs_realpow_minus_one"; |
108 Addsimps [abs_realpow_minus_one]; |
108 Addsimps [abs_realpow_minus_one]; |
|
109 |
|
110 Goal "abs((#-1) ^ n) = (#1::real)"; |
|
111 by (rtac (simplify (simpset()) abs_realpow_minus_one) 1); |
|
112 qed "abs_realpow_minus_one2"; |
|
113 Addsimps [abs_realpow_minus_one2]; |
109 |
114 |
110 Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"; |
115 Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"; |
111 by (induct_tac "n" 1); |
116 by (induct_tac "n" 1); |
112 by (auto_tac (claset(),simpset() addsimps real_mult_ac)); |
117 by (auto_tac (claset(),simpset() addsimps real_mult_ac)); |
113 qed "realpow_mult"; |
118 qed "realpow_mult"; |