equal
deleted
inserted
replaced
1 |
1 |
2 (*** Examples of performing binary arithmetic by simplification ***) |
2 (*** Examples of performing binary arithmetic by simplification ***) |
|
3 |
|
4 (** Addition **) |
3 |
5 |
4 Goal "#13 + #19 = #32"; |
6 Goal "#13 + #19 = #32"; |
5 by (Simp_tac 1); |
7 by (Simp_tac 1); |
6 result(); |
8 result(); |
7 |
9 |
15 |
17 |
16 Goal "#93746 + #~46375 = #47371"; |
18 Goal "#93746 + #~46375 = #47371"; |
17 by (Simp_tac 1); |
19 by (Simp_tac 1); |
18 result(); |
20 result(); |
19 |
21 |
20 Goal "$~ #65745 = #~65745"; |
22 (** Negation **) |
|
23 |
|
24 Goal "- #65745 = #~65745"; |
21 by (Simp_tac 1); |
25 by (Simp_tac 1); |
22 result(); |
26 result(); |
23 |
27 |
24 Goal "$~ #~54321 = #54321"; |
28 Goal "- #~54321 = #54321"; |
25 by (Simp_tac 1); |
29 by (Simp_tac 1); |
26 result(); |
30 result(); |
|
31 |
|
32 |
|
33 (** Multiplication **) |
27 |
34 |
28 Goal "#13 * #19 = #247"; |
35 Goal "#13 * #19 = #247"; |
29 by (Simp_tac 1); |
36 by (Simp_tac 1); |
30 result(); |
37 result(); |
31 |
38 |