138 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT]))); |
138 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT]))); |
139 by (safe_tac (claset() addSDs [normal_BIT_D])); |
139 by (safe_tac (claset() addSDs [normal_BIT_D])); |
140 by (ALLGOALS Asm_simp_tac); |
140 by (ALLGOALS Asm_simp_tac); |
141 qed_spec_mp "bin_add_normal"; |
141 qed_spec_mp "bin_add_normal"; |
142 |
142 |
143 |
|
144 |
|
145 Goal "w: normal ==> (w = Pls) = (integ_of w = #0)"; |
143 Goal "w: normal ==> (w = Pls) = (integ_of w = #0)"; |
146 by (etac normal.induct 1); |
144 by (etac normal.induct 1); |
147 by Auto_tac; |
145 by Auto_tac; |
148 qed "normal_Pls_eq_0"; |
146 qed "normal_Pls_eq_0"; |
149 |
147 |
152 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT]))); |
150 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT]))); |
153 by (resolve_tac normal.intrs 1); |
151 by (resolve_tac normal.intrs 1); |
154 by (assume_tac 1); |
152 by (assume_tac 1); |
155 by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1); |
153 by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1); |
156 by (asm_full_simp_tac |
154 by (asm_full_simp_tac |
157 (simpset_of Integ.thy addsimps [integ_of_minus, iszero_def, |
155 (simpset_of Int.thy addsimps [integ_of_minus, iszero_def, |
158 zminus_exchange]) 1); |
156 zminus_exchange]) 1); |
159 qed "bin_minus_normal"; |
157 qed "bin_minus_normal"; |
160 |
|
161 |
158 |
162 Goal "w : normal ==> z: normal --> bin_mult w z : normal"; |
159 Goal "w : normal ==> z: normal --> bin_mult w z : normal"; |
163 by (etac normal.induct 1); |
160 by (etac normal.induct 1); |
164 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_normal, |
161 by (ALLGOALS |
165 bin_mult_BIT]))); |
162 (asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT]))); |
166 by (safe_tac (claset() addSDs [normal_BIT_D])); |
163 by (safe_tac (claset() addSDs [normal_BIT_D])); |
167 by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1); |
164 by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1); |
168 qed_spec_mp "bin_mult_normal"; |
165 qed_spec_mp "bin_mult_normal"; |
169 |
166 |