324 Goalw [int_def] "int 0 * z = int 0"; |
324 Goalw [int_def] "int 0 * z = int 0"; |
325 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
325 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
326 by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
326 by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
327 qed "zmult_int0"; |
327 qed "zmult_int0"; |
328 |
328 |
329 Goalw [int_def] "int 1 * z = z"; |
329 Goalw [int_def] "int 1' * z = z"; |
330 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
330 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
331 by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
331 by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
332 qed "zmult_int1"; |
332 qed "zmult_int1"; |
333 |
333 |
334 Goal "z * int 0 = int 0"; |
334 Goal "z * int 0 = int 0"; |
335 by (rtac ([zmult_commute, zmult_int0] MRS trans) 1); |
335 by (rtac ([zmult_commute, zmult_int0] MRS trans) 1); |
336 qed "zmult_int0_right"; |
336 qed "zmult_int0_right"; |
337 |
337 |
338 Goal "z * int 1 = z"; |
338 Goal "z * int 1' = z"; |
339 by (rtac ([zmult_commute, zmult_int1] MRS trans) 1); |
339 by (rtac ([zmult_commute, zmult_int1] MRS trans) 1); |
340 qed "zmult_int1_right"; |
340 qed "zmult_int1_right"; |
341 |
341 |
342 Addsimps [zmult_int0, zmult_int0_right, zmult_int1, zmult_int1_right]; |
342 Addsimps [zmult_int0, zmult_int0_right, zmult_int1, zmult_int1_right]; |
343 |
343 |