equal
deleted
inserted
replaced
6 Examples of performing binary arithmetic by simplification |
6 Examples of performing binary arithmetic by simplification |
7 |
7 |
8 Also a proof that binary arithmetic on normalized operands |
8 Also a proof that binary arithmetic on normalized operands |
9 yields normalized results. |
9 yields normalized results. |
10 *) |
10 *) |
11 |
|
12 set proof_timing; |
|
13 |
11 |
14 (**** The Integers ****) |
12 (**** The Integers ****) |
15 |
13 |
16 (*** Addition ***) |
14 (*** Addition ***) |
17 |
15 |
370 by (ALLGOALS |
368 by (ALLGOALS |
371 (asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT]))); |
369 (asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT]))); |
372 by (safe_tac (claset() addSDs [normal_BIT_D])); |
370 by (safe_tac (claset() addSDs [normal_BIT_D])); |
373 by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1); |
371 by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1); |
374 qed_spec_mp "bin_mult_normal"; |
372 qed_spec_mp "bin_mult_normal"; |
375 |
|