equal
deleted
inserted
replaced
170 Z: "bin_nth w 0 \<longleftrightarrow> bin_last w" |
170 Z: "bin_nth w 0 \<longleftrightarrow> bin_last w" |
171 | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n" |
171 | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n" |
172 |
172 |
173 lemma bin_abs_lem: |
173 lemma bin_abs_lem: |
174 "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 --> |
174 "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 --> |
175 nat (abs w) < nat (abs bin)" |
175 nat \<bar>w\<bar> < nat \<bar>bin\<bar>" |
176 apply clarsimp |
176 apply clarsimp |
177 apply (unfold Bit_def) |
177 apply (unfold Bit_def) |
178 apply (cases b) |
178 apply (cases b) |
179 apply (clarsimp, arith) |
179 apply (clarsimp, arith) |
180 apply (clarsimp, arith) |
180 apply (clarsimp, arith) |