equal
deleted
inserted
replaced
316 "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)" |
316 "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)" |
317 apply (induct bs arbitrary: w) |
317 apply (induct bs arbitrary: w) |
318 apply clarsimp |
318 apply clarsimp |
319 apply clarsimp |
319 apply clarsimp |
320 apply safe |
320 apply safe |
321 apply (drule meta_spec, erule xtr8 [rotated], |
321 apply (drule meta_spec, erule xtr8 [rotated], simp add: Bit_def)+ |
322 simp add: numeral_simps algebra_simps BIT_simps |
|
323 cong add: number_of_False_cong)+ |
|
324 done |
322 done |
325 |
323 |
326 lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)" |
324 lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)" |
327 apply (unfold bl_to_bin_def) |
325 apply (unfold bl_to_bin_def) |
328 apply (rule xtr1) |
326 apply (rule xtr1) |