--- a/src/HOL/Word/Bool_List_Representation.thy Wed Mar 23 16:37:19 2016 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Wed Mar 23 09:37:38 2016 +1100
@@ -329,13 +329,15 @@
apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+
done
-lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
- apply (unfold bl_to_bin_def)
- apply (rule xtrans(1))
- prefer 2
- apply (rule bl_to_bin_lt2p_aux)
- apply simp
- done
+lemma bl_to_bin_lt2p_drop:
+ "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
+proof (induct bs)
+ case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1]
+ show ?case unfolding bl_to_bin_def by simp
+qed simp
+
+lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
+ by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
lemma bl_to_bin_ge2p_aux:
"bl_to_bin_aux bs w >= w * (2 ^ length bs)"