src/HOL/Word/Bool_List_Representation.thy

 subsection {* Operations on lists of booleans *}
 
 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
   Nil: "bl_to_bin_aux [] w = w"
   | Cons: "bl_to_bin_aux (b # bs) w = 
-      bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
+      bl_to_bin_aux bs (w BIT b)"
 
 definition bl_to_bin :: "bool list \<Rightarrow> int" where
   bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
 
 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
   Z: "bin_to_bl_aux 0 w bl = bl"
   | Suc: "bin_to_bl_aux (Suc n) w bl =
-      bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
+      bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
 
 definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
   bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
 
 primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where

     bin_to_bl_aux (n - 1) 0 (True # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit_minus_simp [simp]:
   "0 < n ==> bin_to_bl_aux n (w BIT b) bl = 
-    bin_to_bl_aux (n - 1) w ((b = 1) # bl)"
+    bin_to_bl_aux (n - 1) w (b # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
   "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = 
     bin_to_bl_aux (n - 1) (numeral w) (False # bl)"

   "hd (bin_to_bl_aux (Suc n) w bs) = 
     (bin_sign (sbintrunc n w) = -1)"
   apply (induct n arbitrary: w bs)
    apply clarsimp
    apply (cases w rule: bin_exhaust)
-   apply (simp split add : bit.split)
-  apply clarsimp
+   apply simp
   done
     
 lemma bl_sbin_sign: 
   "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)

 lemma bl_to_bin_lt2p_aux:
   "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
   apply (induct bs arbitrary: w)
    apply clarsimp
   apply clarsimp
-  apply safe
   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)

 lemma bl_to_bin_ge2p_aux:
   "bl_to_bin_aux bs w >= w * (2 ^ length bs)"
   apply (induct bs arbitrary: w)
    apply clarsimp
   apply clarsimp
-  apply safe
    apply (drule meta_spec, erule order_trans [rotated],
           simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+
+   apply (simp add: Bit_def)
   done
 
 lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
   apply (unfold bl_to_bin_def)
   apply (rule xtrans(4))

 
 lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
   by (cases xs) auto
 
 lemma last_bin_last': 
-  "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = 1)" 
+  "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)" 
   by (induct xs arbitrary: w) auto
 
 lemma last_bin_last: 
-  "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = 1)" 
+  "size xs > 0 ==> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)" 
   unfolding bl_to_bin_def by (erule last_bin_last')
   
 lemma bin_last_last: 
-  "bin_last w = (if last (bin_to_bl (Suc n) w) then 1 else 0)" 
+  "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)" 
   apply (unfold bin_to_bl_def)
   apply simp
   apply (auto simp add: bin_to_bl_aux_alt)
   done
 

    apply simp
   apply (case_tac v rule: bin_exhaust)
   apply (case_tac w rule: bin_exhaust)
   apply clarsimp
   apply (case_tac b)
-  apply (case_tac ba, safe, simp_all)+
+  apply auto
   done
 
 lemma bl_or_aux_bin:
   "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
     bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)"
   apply (induct n arbitrary: v w bs cs)
    apply simp
   apply (case_tac v rule: bin_exhaust)
   apply (case_tac w rule: bin_exhaust)
   apply clarsimp
-  apply (case_tac b)
-  apply (case_tac ba, safe, simp_all)+
   done
     
 lemma bl_and_aux_bin:
   "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
     bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" 

   by (auto intro: trans [OF rbl_mult_gt1])
   
 lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
 
 lemma rbbl_Cons: 
-  "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b 1 0))"
+  "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))"
   apply (unfold bin_to_bl_def)
   apply simp
   apply (simp add: bin_to_bl_aux_alt)
   done