author | wenzelm |
Mon, 16 Nov 1998 10:41:08 +0100 | |
changeset 5869 | b279a84ac11c |
parent 5747 | 387b5bf9326a |
child 6909 | 21601bc4f3c2 |
permissions | -rw-r--r-- |
5545 | 1 |
(* Title: HOL/ex/BinEx.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5199 | 5 |
|
5545 | 6 |
Examples of performing binary arithmetic by simplification |
7 |
||
8 |
Also a proof that binary arithmetic on normalized operands |
|
9 |
yields normalized results. |
|
10 |
*) |
|
11 |
||
12 |
set proof_timing; |
|
5199 | 13 |
|
5491 | 14 |
(** Addition **) |
15 |
||
5199 | 16 |
Goal "#13 + #19 = #32"; |
17 |
by (Simp_tac 1); |
|
18 |
result(); |
|
19 |
||
20 |
Goal "#1234 + #5678 = #6912"; |
|
21 |
by (Simp_tac 1); |
|
22 |
result(); |
|
23 |
||
5513 | 24 |
Goal "#1359 + #-2468 = #-1109"; |
5199 | 25 |
by (Simp_tac 1); |
26 |
result(); |
|
27 |
||
5513 | 28 |
Goal "#93746 + #-46375 = #47371"; |
5199 | 29 |
by (Simp_tac 1); |
30 |
result(); |
|
31 |
||
5491 | 32 |
(** Negation **) |
33 |
||
5513 | 34 |
Goal "- #65745 = #-65745"; |
5199 | 35 |
by (Simp_tac 1); |
36 |
result(); |
|
37 |
||
5513 | 38 |
Goal "- #-54321 = #54321"; |
5199 | 39 |
by (Simp_tac 1); |
40 |
result(); |
|
41 |
||
5491 | 42 |
|
43 |
(** Multiplication **) |
|
44 |
||
5199 | 45 |
Goal "#13 * #19 = #247"; |
46 |
by (Simp_tac 1); |
|
47 |
result(); |
|
48 |
||
5513 | 49 |
Goal "#-84 * #51 = #-4284"; |
5199 | 50 |
by (Simp_tac 1); |
51 |
result(); |
|
52 |
||
53 |
Goal "#255 * #255 = #65025"; |
|
54 |
by (Simp_tac 1); |
|
55 |
result(); |
|
56 |
||
5513 | 57 |
Goal "#1359 * #-2468 = #-3354012"; |
5199 | 58 |
by (Simp_tac 1); |
59 |
result(); |
|
60 |
||
61 |
Goal "#89 * #10 ~= #889"; |
|
62 |
by (Simp_tac 1); |
|
63 |
result(); |
|
64 |
||
65 |
Goal "#13 < #18 - #4"; |
|
66 |
by (Simp_tac 1); |
|
67 |
result(); |
|
68 |
||
5513 | 69 |
Goal "#-345 < #-242 + #-100"; |
5199 | 70 |
by (Simp_tac 1); |
71 |
result(); |
|
72 |
||
73 |
Goal "#13557456 < #18678654"; |
|
74 |
by (Simp_tac 1); |
|
75 |
result(); |
|
76 |
||
77 |
Goal "#999999 <= (#1000001 + #1)-#2"; |
|
78 |
by (Simp_tac 1); |
|
79 |
result(); |
|
80 |
||
81 |
Goal "#1234567 <= #1234567"; |
|
82 |
by (Simp_tac 1); |
|
83 |
result(); |
|
5545 | 84 |
|
85 |
||
5601 | 86 |
(** Testing the cancellation of complementary terms **) |
87 |
||
5747 | 88 |
Goal "y + (x + -x) = #0 + y"; |
5601 | 89 |
by (Simp_tac 1); |
90 |
result(); |
|
91 |
||
5747 | 92 |
Goal "y + (-x + (- y + x)) = #0"; |
5601 | 93 |
by (Simp_tac 1); |
94 |
result(); |
|
95 |
||
5747 | 96 |
Goal "-x + (y + (- y + x)) = #0"; |
5601 | 97 |
by (Simp_tac 1); |
98 |
result(); |
|
99 |
||
5747 | 100 |
Goal "x + (x + (- x + (- x + (- y + - z)))) = #0 - y - z"; |
5601 | 101 |
by (Simp_tac 1); |
102 |
result(); |
|
103 |
||
5747 | 104 |
Goal "x + x - x - x - y - z = #0 - y - z"; |
5601 | 105 |
by (Simp_tac 1); |
106 |
result(); |
|
107 |
||
5747 | 108 |
Goal "x + y + z - (x + z) = y - #0"; |
5601 | 109 |
by (Simp_tac 1); |
110 |
result(); |
|
111 |
||
5747 | 112 |
Goal "x+(y+(y+(y+ (-x + -x)))) = #0 + y - x + y + y"; |
5601 | 113 |
by (Simp_tac 1); |
114 |
result(); |
|
115 |
||
5747 | 116 |
Goal "x+(y+(y+(y+ (-y + -x)))) = y + #0 + y"; |
5601 | 117 |
by (Simp_tac 1); |
118 |
result(); |
|
119 |
||
5747 | 120 |
Goal "x + y - x + z - x - y - z + x < #1"; |
5601 | 121 |
by (Simp_tac 1); |
122 |
result(); |
|
123 |
||
124 |
||
5545 | 125 |
Addsimps normal.intrs; |
126 |
||
127 |
Goal "(w BIT b): normal ==> (w BIT b BIT c): normal"; |
|
128 |
by (case_tac "c" 1); |
|
129 |
by Auto_tac; |
|
130 |
qed "normal_BIT_I"; |
|
131 |
||
132 |
Addsimps [normal_BIT_I]; |
|
133 |
||
134 |
Goal "w BIT b: normal ==> w: normal"; |
|
135 |
by (etac normal.elim 1); |
|
136 |
by Auto_tac; |
|
137 |
qed "normal_BIT_D"; |
|
138 |
||
139 |
Goal "w : normal --> NCons w b : normal"; |
|
140 |
by (induct_tac "w" 1); |
|
141 |
by (auto_tac (claset(), simpset() addsimps [NCons_Pls, NCons_Min])); |
|
142 |
qed_spec_mp "NCons_normal"; |
|
143 |
||
144 |
Addsimps [NCons_normal]; |
|
145 |
||
146 |
Goal "NCons w True ~= Pls"; |
|
147 |
by (induct_tac "w" 1); |
|
148 |
by Auto_tac; |
|
149 |
qed "NCons_True"; |
|
150 |
||
151 |
Goal "NCons w False ~= Min"; |
|
152 |
by (induct_tac "w" 1); |
|
153 |
by Auto_tac; |
|
154 |
qed "NCons_False"; |
|
155 |
||
156 |
Goal "w: normal ==> bin_succ w : normal"; |
|
157 |
by (etac normal.induct 1); |
|
158 |
by (exhaust_tac "w" 4); |
|
159 |
by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT])); |
|
160 |
qed "bin_succ_normal"; |
|
161 |
||
162 |
Goal "w: normal ==> bin_pred w : normal"; |
|
163 |
by (etac normal.induct 1); |
|
164 |
by (exhaust_tac "w" 3); |
|
165 |
by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT])); |
|
166 |
qed "bin_pred_normal"; |
|
167 |
||
168 |
Addsimps [bin_succ_normal, bin_pred_normal]; |
|
169 |
||
170 |
Goal "w : normal --> (ALL z. z: normal --> bin_add w z : normal)"; |
|
171 |
by (induct_tac "w" 1); |
|
172 |
by (Simp_tac 1); |
|
173 |
by (Simp_tac 1); |
|
174 |
by (rtac impI 1); |
|
175 |
by (rtac allI 1); |
|
176 |
by (induct_tac "z" 1); |
|
177 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT]))); |
|
178 |
by (safe_tac (claset() addSDs [normal_BIT_D])); |
|
179 |
by (ALLGOALS Asm_simp_tac); |
|
180 |
qed_spec_mp "bin_add_normal"; |
|
181 |
||
182 |
Goal "w: normal ==> (w = Pls) = (integ_of w = #0)"; |
|
183 |
by (etac normal.induct 1); |
|
184 |
by Auto_tac; |
|
185 |
qed "normal_Pls_eq_0"; |
|
186 |
||
187 |
Goal "w : normal ==> bin_minus w : normal"; |
|
188 |
by (etac normal.induct 1); |
|
189 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT]))); |
|
190 |
by (resolve_tac normal.intrs 1); |
|
191 |
by (assume_tac 1); |
|
192 |
by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1); |
|
193 |
by (asm_full_simp_tac |
|
5569
8c7e1190e789
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5545
diff
changeset
|
194 |
(simpset_of Int.thy addsimps [integ_of_minus, iszero_def, |
8c7e1190e789
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5545
diff
changeset
|
195 |
zminus_exchange]) 1); |
5545 | 196 |
qed "bin_minus_normal"; |
197 |
||
198 |
Goal "w : normal ==> z: normal --> bin_mult w z : normal"; |
|
199 |
by (etac normal.induct 1); |
|
5569
8c7e1190e789
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5545
diff
changeset
|
200 |
by (ALLGOALS |
8c7e1190e789
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5545
diff
changeset
|
201 |
(asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT]))); |
5545 | 202 |
by (safe_tac (claset() addSDs [normal_BIT_D])); |
203 |
by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1); |
|
204 |
qed_spec_mp "bin_mult_normal"; |
|
205 |