183 by (arith_tac 2); |
183 by (arith_tac 2); |
184 by (dres_inst_tac [("n","-n")] pos_zmult_eq_1_iff 1); |
184 by (dres_inst_tac [("n","-n")] pos_zmult_eq_1_iff 1); |
185 by Auto_tac; |
185 by Auto_tac; |
186 qed "zmult_eq_1_iff"; |
186 qed "zmult_eq_1_iff"; |
187 |
187 |
|
188 |
|
189 (*** More about nat ***) |
|
190 |
|
191 Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z+z') = nat z + nat z'"; |
|
192 by (rtac (inj_int RS injD) 1); |
|
193 by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1); |
|
194 qed "nat_add_distrib"; |
|
195 |
|
196 Goal "[| (0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'"; |
|
197 by (rtac (inj_int RS injD) 1); |
|
198 by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1); |
|
199 qed "nat_diff_distrib"; |
|
200 |
|
201 Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'"; |
|
202 by (case_tac "0 <= z'" 1); |
|
203 by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2); |
|
204 by (rtac (inj_int RS injD) 1); |
|
205 by (asm_simp_tac (simpset() addsimps [zmult_int RS sym, |
|
206 int_0_le_mult_iff]) 1); |
|
207 qed "nat_mult_distrib"; |
|
208 |
|
209 Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; |
|
210 by (rtac trans 1); |
|
211 by (rtac nat_mult_distrib 2); |
|
212 by Auto_tac; |
|
213 qed "nat_mult_distrib_neg"; |
|
214 |
|
215 Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)"; |
|
216 by (case_tac "z=0 | w=0" 1); |
|
217 by Auto_tac; |
|
218 by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, |
|
219 nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1); |
|
220 by (arith_tac 1); |
|
221 qed "nat_abs_mult_distrib"; |