1.1 --- a/src/HOL/Word/Word.thy	Wed Jul 02 17:34:45 2014 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Wed Jun 11 14:24:23 2014 +1000
     1.3 @@ -3176,6 +3176,12 @@
     1.4                       of_bl_rep_False [where n=1 and bs="[]", simplified])
     1.5    done
     1.6  
     1.7 +lemma zip_replicate:
     1.8 +  "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys" 
     1.9 +  apply (induct ys arbitrary: n, simp_all)
    1.10 +  apply (case_tac n, simp_all)
    1.11 +  done
    1.12 +
    1.13  lemma align_lem_or [rule_format] :
    1.14    "ALL x m. length x = n + m --> length y = n + m --> 
    1.15      drop m x = replicate n False --> take m y = replicate m False --> 
    1.16 @@ -3185,9 +3191,8 @@
    1.17    apply clarsimp
    1.18    apply (case_tac x, force)
    1.19    apply (case_tac m, auto)
    1.20 -  apply (drule sym)
    1.21 -  apply auto
    1.22 -  apply (induct_tac list, auto)
    1.23 +  apply (drule_tac t="length ?xs" in sym)
    1.24 +  apply (clarsimp simp: map2_def zip_replicate o_def)
    1.25    done
    1.26  
    1.27  lemma align_lem_and [rule_format] :
    1.28 @@ -3199,9 +3204,8 @@
    1.29    apply clarsimp
    1.30    apply (case_tac x, force)
    1.31    apply (case_tac m, auto)
    1.32 -  apply (drule sym)
    1.33 -  apply auto
    1.34 -  apply (induct_tac list, auto)
    1.35 +  apply (drule_tac t="length ?xs" in sym)
    1.36 +  apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const)
    1.37    done
    1.38  
    1.39  lemma aligned_bl_add_size [OF refl]:
    1.40 @@ -3676,6 +3680,7 @@
    1.41    apply safe
    1.42     defer
    1.43     apply (clarsimp split: prod.splits)
    1.44 +   apply hypsubst_thin
    1.45     apply (drule word_ubin.norm_Rep [THEN ssubst])
    1.46     apply (drule split_bintrunc)
    1.47     apply (simp add : of_bl_def bl2bin_drop word_size