# HG changeset patch
# User kleing
# Date 1458686258 -39600
# Node ID 715bf5beedc060bb8b27877185cc88c8e7467e5c
# Parent  e3ca8dc01c4f0ef774a72b71e3e765ad8a7fe2cb
HOL-Word: add stronger bl_to_bin_lt2p_drop

diff -r e3ca8dc01c4f -r 715bf5beedc0 src/HOL/Word/Bool_List_Representation.thy
--- 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)"