src/HOL/Word/Bool_List_Representation.thy

 lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
   "0 < n \<Longrightarrow>
     bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
   by (cases n) auto
 
-text \<open>Link between bin and bool list.\<close>
+text \<open>Link between \<open>bin\<close> and \<open>bool list\<close>.\<close>
 
 lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
   by (induct bs arbitrary: w) auto
 
 lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"

 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 bin_nth_of_bl_aux:
   "bin_nth (bl_to_bin_aux bl w) n =
-    (n < size bl \<and> rev bl ! n | n \<ge> length bl \<and> bin_nth w (n - size bl))"
+    (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
   apply (induct bl arbitrary: w)
    apply clarsimp
   apply clarsimp
   apply (cut_tac x=n and y="size bl" in linorder_less_linear)
   apply (erule disjE, simp add: nth_append)+

 lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
 proof (induct bs)
   case Nil
   then show ?case by simp
 next
-  case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1]
-  show ?case unfolding bl_to_bin_def by simp
+  case (Cons b bs)
+  with bl_to_bin_lt2p_aux[where w=1] show ?case
+    by (simp add: bl_to_bin_def)
 qed
 
 lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
   by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
 

   by (induct m arbitrary: l n) (auto split: list.split)
 
 lemma length_takefill [simp]: "length (takefill fill n l) = n"
   by (simp add: takefill_alt)
 
-lemma take_takefill': "\<And>w n.  n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
-  by (induct k) (auto split: list.split)
-
-lemma drop_takefill: "\<And>w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
-  by (induct k) (auto split: list.split)
+lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
+  by (induct k arbitrary: w n) (auto split: list.split)
+
+lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
+  by (induct k arbitrary: w) (auto split: list.split)
 
 lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
   by (auto simp: le_iff_add takefill_le')
 
 lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"

   apply (case_tac blb, clarsimp)
   apply (clarsimp simp: Let_def)
   done
 
 lemma rbl_add_take2:
-  "length blb >= length bla ==> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
+  "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
   apply (induct bla arbitrary: blb)
    apply simp
   apply clarsimp
   apply (case_tac blb, clarsimp)
   apply (clarsimp simp: Let_def)

   proof (cases "m = 0")
     case True
     with \<open>length bs = length cs\<close> show ?thesis by simp
   next
     case False
-    from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
+    from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close>
+    have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
       length (bin_rsplit_aux n (m - n) v bs) =
       length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
       by auto
     from \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> show ?thesis
       by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split)