equal
deleted
inserted
replaced
174 qed "power_Suc"; |
174 qed "power_Suc"; |
175 |
175 |
176 Addsimps [power_0, power_Suc]; |
176 Addsimps [power_0, power_Suc]; |
177 |
177 |
178 Goal "<1> ^ n = (<1>::'a::ring)"; |
178 Goal "<1> ^ n = (<1>::'a::ring)"; |
179 by (nat_ind_tac "n" 1); |
179 by (induct_tac "n" 1); |
180 by (Simp_tac 1); |
180 by Auto_tac; |
181 by (Asm_simp_tac 1); |
|
182 qed "power_one"; |
181 qed "power_one"; |
183 |
182 |
184 Goal "!!n. n ~= 0 ==> <0> ^ n = (<0>::'a::ring)"; |
183 Goal "!!n. n ~= 0 ==> <0> ^ n = (<0>::'a::ring)"; |
185 by (etac rev_mp 1); |
184 by (etac rev_mp 1); |
186 by (nat_ind_tac "n" 1); |
185 by (induct_tac "n" 1); |
187 by (Simp_tac 1); |
186 by Auto_tac; |
188 by (Simp_tac 1); |
|
189 qed "power_zero"; |
187 qed "power_zero"; |
190 |
188 |
191 Addsimps [power_zero, power_one]; |
189 Addsimps [power_zero, power_one]; |
192 |
190 |
193 Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)"; |
191 Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)"; |
194 by (nat_ind_tac "m" 1); |
192 by (induct_tac "m" 1); |
195 by (Simp_tac 1); |
193 by (Simp_tac 1); |
196 by (asm_simp_tac (simpset() addsimps m_ac) 1); |
194 by (asm_simp_tac (simpset() addsimps m_ac) 1); |
197 qed "power_mult"; |
195 qed "power_mult"; |
198 |
196 |
199 (* Divisibility *) |
197 (* Divisibility *) |