lh-l4v/lib/Aligned.thy

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory Aligned
imports WordLib MoreDivides WordSetup
begin

lemma is_aligned_mask: "(is_aligned w n) = (w && mask n = 0)"
  unfolding is_aligned_def by (rule and_mask_dvd_nat)


lemma list_of_false:
  "True \<notin> set xs \<Longrightarrow> xs = replicate (length xs) False"
  by (induct xs, simp_all)

lemma eq_zero_set_bl: "(w = 0) = (True \<notin> set (to_bl w))"
  apply (subst word_bl.Rep_inject[symmetric])
  apply (subst to_bl_0)
  apply (rule iffI)
   apply clarsimp
  apply (drule list_of_false)
  apply simp
  done

lemmas and_bang = word_and_nth

lemma diff_diff_less: "(i < m - (m - (n :: nat))) = (i < m \<and> i < n)"
  apply (case_tac "n \<le> m")
   apply fastforce+
  done

lemma is_aligned_to_bl:
  "is_aligned (w :: 'a :: len word) n = (True \<notin> set (drop (size w - n) (to_bl w)))"
  apply (simp add: is_aligned_mask eq_zero_set_bl)
  apply (clarsimp simp: in_set_conv_nth word_size)
  apply (simp add: to_bl_nth word_size cong: conj_cong)
  apply (simp add: diff_diff_less)
  apply safe
   apply (case_tac "n \<le> len_of TYPE('a)")
    prefer 2
    apply (rule_tac x=i in exI)
    apply clarsimp
   apply (subgoal_tac "\<exists>j < len_of TYPE('a). j < n \<and> len_of TYPE('a) - n + j = i")
    apply (erule exE)
    apply (rule_tac x=j in exI)
    apply clarsimp
   apply (thin_tac "w !! ?t")
   apply (rule_tac x="i + n - len_of TYPE('a)" in exI)
   apply clarsimp
   apply arith
  apply (rule_tac x="len_of TYPE('a) - n + i" in exI)
  apply clarsimp
  apply arith
  done

lemma unat_power_lower [simp]:
  assumes nv: "n < len_of TYPE('a::len)"
  shows "unat ((2::'a::len word) ^ n) = 2 ^ n" 
  apply (subst word_unat_power)
  apply (subst unat_of_nat)
  apply (subst mod_less)
   apply (simp add: nv)
  apply simp
  done

lemma power_overflow:
  "n \<ge> len_of TYPE('a) \<Longrightarrow> 2 ^ n = (0 :: 'a::len word)"
  apply (subgoal_tac "\<exists>m. n = (len_of TYPE ('a)) + m")
   apply safe
   apply (simp only: power_add word_pow_0)
   apply simp
  apply (rule exI[where x="n - len_of TYPE ('a)"])
  apply simp
  done

lemma is_alignedI [intro?]:
  fixes x::"'a::len word"
  assumes xv: "x = 2 ^ n * k"
  shows   "is_aligned x n"
proof cases
  assume nv: "n < len_of TYPE('a)"
  show ?thesis
    unfolding is_aligned_def
  proof (rule dvdI [where k = "unat k mod 2 ^ (len_of TYPE('a) - n)"])
    from xv
    have "unat x = (unat (2::word32) ^ n * unat k) mod 2 ^ len_of TYPE('a)"
      using nv
      by (subst (asm) word_unat.Rep_inject [symmetric], simp,
          subst unat_word_ariths, simp)

    also have "\<dots> =  2 ^ n * (unat k mod 2 ^ (len_of TYPE('a) - n))" using nv
      by (simp add: mult_mod_right power_add [symmetric] add_diff_inverse)

    finally show "unat x = 2 ^ n * (unat k mod 2 ^ (len_of TYPE('a) - n))" .
  qed
next
  assume "\<not> n < len_of TYPE('a)"
  with xv
  show ?thesis by (simp add: not_less power_overflow is_aligned_def)
qed

lemma is_aligned_weaken:
  "\<lbrakk> is_aligned w x; x \<ge> y \<rbrakk> \<Longrightarrow> is_aligned w y"
  apply (simp add: is_aligned_def)
  apply (rule dvd_trans)
   prefer 2
   apply assumption
  apply (simp add: le_imp_power_dvd)
  done


lemma nat_power_less_diff:
  assumes lt: "(2::nat) ^ n * q < 2 ^ m"
  shows "q < 2 ^ (m - n)"
  using lt
proof (induct n arbitrary: m)
  case 0
  thus ?case by simp
next
  case (Suc n)

  have ih: "\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n)" 
    and prem: "2 ^ Suc n * q < 2 ^ m" by fact+
  
  show ?case
  proof (cases m)
    case 0
    thus ?thesis using Suc by simp
  next
    case (Suc m')
    thus ?thesis using prem
      apply simp
      apply (rule ih)
      apply (simp add: mult_ac)
      done
  qed
qed

lemma is_alignedE_pre:
  fixes w::"'a::len word"
  assumes aligned: "is_aligned w n"
  shows        rl: "\<exists>q. w = 2 ^ n * (of_nat q) \<and> q < 2 ^ (len_of TYPE('a) - n)"
proof -
  from aligned obtain q where wv: "unat w = 2 ^ n * q"
    unfolding is_aligned_def ..

  show ?thesis
  proof (rule exI, intro conjI)
    show "q < 2 ^ (len_of TYPE('a) - n)"
    proof (rule nat_power_less_diff)
      have "unat w < 2 ^ size w" unfolding word_size ..
      hence "unat w < 2 ^ len_of TYPE('a)" by simp
      with wv show "2 ^ n * q < 2 ^ len_of TYPE('a)" by simp
    qed

    have r: "of_nat (2 ^ n) = (2::word32) ^ n"
      by (induct n) simp+
    
    from wv have "of_nat (unat w) = of_nat (2 ^ n * q)" by simp
    hence "w = of_nat (2 ^ n * q)" by (subst word_unat.Rep_inverse [symmetric])
    thus "w = 2 ^ n * (of_nat q)" by (simp add: r)      
  qed
qed

lemma is_alignedE:
  "\<lbrakk>is_aligned (w::'a::len word) n;
    \<And>q. \<lbrakk>w = 2 ^ n * (of_nat q); q < 2 ^ (len_of TYPE('a) - n)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
  by (auto dest: is_alignedE_pre)

lemma is_aligned_replicate:
  fixes w::"'a::len word"
  assumes aligned: "is_aligned w n"
  and          nv: "n \<le> len_of TYPE('a)"
  shows   "to_bl w = (take (len_of TYPE('a) - n) (to_bl w)) @ replicate n False"
proof -
    from nv have rl: "\<And>q. q < 2 ^ (len_of TYPE('a) - n) \<Longrightarrow> 
      to_bl (2 ^ n * (of_nat q :: 'a word)) =
      drop n (to_bl (of_nat q :: 'a word)) @ replicate n False"
      apply (subst shiftl_t2n [symmetric])
      apply (subst bl_shiftl)
      apply (simp add: min_def word_size)
      done

    show ?thesis using aligned
      by (auto simp: rl elim: is_alignedE)
qed

lemma is_aligned_drop:
  fixes w::"'a::len word"
  assumes "is_aligned w n" "n \<le> len_of TYPE('a)"
  shows "drop (len_of TYPE('a) - n) (to_bl w) = replicate n False"
proof -
  have "to_bl w = take (len_of TYPE('a) - n) (to_bl w) @ replicate n False" 
    by (rule is_aligned_replicate) fact+
  hence "drop (len_of TYPE('a) - n) (to_bl w) = drop (len_of TYPE('a) - n) \<dots>" by simp
  also have "\<dots> = replicate n False" by simp
  finally show ?thesis .
qed

lemma less_is_drop_replicate:
  fixes x::"'a::len word"
  assumes lt: "x < 2 ^ n"
  shows   "to_bl x = replicate (len_of TYPE('a) - n) False @ drop (len_of TYPE('a) - n) (to_bl x)"
proof -
  show ?thesis 
    apply (subst less_mask_eq [OF lt, symmetric])
    apply (subst bl_and_mask)
    apply simp
    done
qed

lemma is_aligned_add_conv:
  fixes off::"'a::len word"
  assumes aligned: "is_aligned w n"
  and        offv: "off < 2 ^ n"
  shows    "to_bl (w + off) = 
   (take (len_of TYPE('a) - n) (to_bl w)) @ (drop (len_of TYPE('a) - n) (to_bl off))"
proof cases
  assume nv: "n \<le> len_of TYPE('a)"
  show ?thesis
  proof (subst aligned_bl_add_size, simp_all only: word_size)
    show "drop (len_of TYPE('a) - n) (to_bl w) = replicate n False"
      by (subst is_aligned_replicate [OF aligned nv]) (simp add: word_size)

    from offv show "take (len_of TYPE('a) - n) (to_bl off) =
                    replicate (len_of TYPE('a) - n) False"
      by (subst less_is_drop_replicate, assumption) simp
  qed fact
next
  assume "\<not> n \<le> len_of TYPE('a)"
  with offv show ?thesis by (simp add: power_overflow)
qed

lemma nat_less_power_trans:
  fixes n :: nat
  assumes nv: "n < 2 ^ (m - k)" 
  and     kv: "k \<le> m"
  shows "2 ^ k * n < 2 ^ m"
proof (rule order_less_le_trans)
  show "2 ^ k * n < 2 ^ k * 2 ^ (m - k)"
    by (rule mult_less_mono2 [OF nv zero_less_power]) simp
    
  show "(2::nat) ^ k * 2 ^ (m - k) \<le> 2 ^ m" using nv kv
    by (subst power_add [symmetric]) simp
qed

lemma aligned_add_aligned:
  fixes x::"'a::len word"
  assumes aligned1: "is_aligned x n"
  and     aligned2: "is_aligned y m"
  and           lt: "m \<le> n"
  shows   "is_aligned (x + y) m"
proof cases
  assume nlt: "n < len_of TYPE('a)"
  show ?thesis
    unfolding is_aligned_def dvd_def
  proof -
    from aligned2 obtain q2 where yv: "y = 2 ^ m * of_nat q2"
      and q2v: "q2 < 2 ^ (len_of TYPE('a) - m)"
      by (auto elim: is_alignedE)

    from lt obtain k where kv: "m + k = n" by (auto simp: le_iff_add)
    with aligned1 obtain q1 where xv: "x = 2 ^ (m + k) * of_nat q1"
      and q1v: "q1 < 2 ^ (len_of TYPE('a) - (m + k))"
      by (auto elim: is_alignedE)

    have l1: "2 ^ (m + k) * q1 < 2 ^ len_of TYPE('a)"
      by (rule nat_less_power_trans [OF q1v])
         (subst kv, rule order_less_imp_le [OF nlt])

    have l2: "2 ^ m * q2 < 2 ^ len_of TYPE('a)"
      by (rule nat_less_power_trans [OF q2v],
          rule order_less_imp_le [OF order_le_less_trans])
         fact+

    have "x = of_nat (2 ^ (m + k) *  q1)" using xv
      by simp

    moreover have "y = of_nat (2 ^ m * q2)" using yv
      by simp

    ultimately have upls: "unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)"
      apply -
      apply (erule ssubst)+
      apply (subst unat_of_nat)
      apply (subst mod_less [OF l1])
      apply (subst unat_of_nat)
      apply (subst mod_less [OF l2])
      apply (subst power_add)
      apply (subst add_mult_distrib2)
      apply simp
      done

    (* (2 ^ k * q1 + q2) *)
    show "\<exists>d. unat (x + y) = 2 ^ m * d"
    proof (cases "unat x + unat y < 2 ^ len_of TYPE('a)")
      case True

      have "unat (x + y) = unat x + unat y"
        by (subst unat_plus_if', rule if_P) fact

      also have "\<dots> = 2 ^ m * (2 ^ k * q1 + q2)" by (rule upls)
      finally show ?thesis ..
    next
      case False
      hence "unat (x + y) = (unat x + unat y) mod 2 ^ len_of TYPE('a)"
        by (subst unat_word_ariths(1)) simp

      also have "\<dots> = (2 ^ m * (2 ^ k * q1 + q2)) mod 2 ^ len_of TYPE('a)"
        by (subst upls, rule refl)

      also have "\<dots> = 2 ^ m * ((2 ^ k * q1 +  q2) mod 2 ^ (len_of TYPE('a) - m))"
        apply (subst mult_mod_right)
        apply (subst power_add [symmetric])
        apply (subst le_add_diff_inverse
                     [OF order_trans[OF lt order_less_imp_le[OF nlt]]])
        apply (rule refl)
        done

      finally show ?thesis ..
    qed
  qed
next
  assume "\<not> n < len_of TYPE('a)"
  with assms
  show ?thesis by (simp add: not_less power_overflow is_aligned_mask mask_def)
qed

corollary aligned_sub_aligned:
  "\<lbrakk>is_aligned (x::'a::len word) n; is_aligned y m; m \<le> n\<rbrakk>
   \<Longrightarrow> is_aligned (x - y) m"
  apply (simp add: diff_def)
  apply (erule aligned_add_aligned, simp_all)
  apply (erule is_alignedE)
  apply (rule_tac k="- of_nat q" in is_alignedI)
  apply simp
  done

lemma is_aligned_shift:
  fixes k::"'a::len word"
  shows "is_aligned (k << m) m"
proof cases
  assume mv: "m < len_of TYPE('a)"
  from mv obtain q where mq: "m + q = len_of TYPE('a)" and "0 < q"
    by (auto dest: less_imp_add_positive)

  have "(2\<Colon>nat) ^ m dvd unat (k << m)"
  proof
    have kv: "(unat k div 2 ^ q) * 2 ^ q + unat k mod 2 ^ q = unat k" 
      by (rule mod_div_equality)
    
    have "unat (k << m) = unat (2 ^ m * k)" by (simp add: shiftl_t2n)
    also have "\<dots> = (2 ^ m * unat k) mod (2 ^ len_of TYPE('a))" using mv
      by (subst unat_word_ariths(2))+ simp
    also have "\<dots> = 2 ^ m * (unat k mod 2 ^ q)"
      by (subst mq [symmetric], subst power_add, subst mod_mult2_eq) simp
    finally show "unat (k << m) = 2 ^ m * (unat k mod 2 ^ q)" .
  qed

  thus ?thesis by (unfold is_aligned_def)
next
  assume "\<not> m < len_of TYPE('a)"
  thus ?thesis
    by (simp add: not_less power_overflow is_aligned_mask mask_def
                  shiftl_zero_size word_size)
qed

lemma word_mod_by_0: "k mod (0::'a::len word) = k"
  by (simp add: word_arith_nat_mod)

lemma aligned_mod_eq_0:
  fixes p::"'a::len word"
  assumes al: "is_aligned p sz"
  shows   "p mod 2 ^ sz = 0"
proof cases
  assume szv: "sz < len_of TYPE('a)"
  with al
  show ?thesis
    unfolding is_aligned_def
    apply -
    apply (rule word_unat.Rep_eqD)
    apply (subst unat_mod)
    apply (simp add: dvd_eq_mod_eq_0)
    done
next
  assume "\<not> sz < len_of TYPE('a)"
  with al show ?thesis
    by (simp add: not_less power_overflow is_aligned_mask mask_def
                  word_mod_by_0)
qed

lemma is_aligned_triv: "is_aligned (2 ^ n ::'a::len word) n"
  by (rule is_alignedI [where k = 1], simp)

lemma is_aligned_mult_triv1: "is_aligned (2 ^ n * x  ::'a::len word) n"
  by (rule is_alignedI [OF refl])

lemma is_aligned_mult_triv2: "is_aligned (x * 2 ^ n ::'a::len word) n"
  by (subst mult_commute, simp add: is_aligned_mult_triv1)

lemma word_power_less_0_is_0:
  fixes x :: "'a::len word"
  shows "x < a ^ 0 \<Longrightarrow> x = 0" by simp

lemma nat_add_offset_less:
  fixes x :: nat
  assumes yv: "y < 2 ^ n"
  and     xv: "x < 2 ^ m"
  and     mn: "sz = m + n"
  shows   "x * 2 ^ n + y < 2 ^ sz"
proof (subst mn)
  from yv obtain qy where "y + qy = 2 ^ n" and "0 < qy" 
    by (auto dest: less_imp_add_positive)

  have "x * 2 ^ n + y < x * 2 ^ n + 2 ^ n" by simp fact+
  also have "\<dots> = (x + 1) * 2 ^ n" by simp
  also have "\<dots> \<le> 2 ^ (m + n)" using xv
    by (subst power_add) (rule mult_le_mono1, simp)
  finally show "x * 2 ^ n + y < 2 ^ (m + n)" .
qed

lemma is_aligned_no_wrap:
  fixes off :: "'a::len word"
  fixes ptr :: "'a::len word"
  assumes al: "is_aligned ptr sz"
  and    off: "off < 2 ^ sz"
  shows  "unat ptr + unat off < 2 ^ len_of TYPE('a)"
proof -
  have szv: "sz < len_of TYPE('a)"
    apply (rule ccontr)
    using off
    by (clarsimp simp: not_less p2_eq_0[THEN iffD2])

  from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and
    qv: "q < 2 ^ (len_of TYPE('a) - sz)" by (auto elim: is_alignedE)
  
  show ?thesis
  proof (cases "sz = 0")
    case True
    thus ?thesis using off ptrq qv
      by clarsimp
  next
    case False
    hence sne: "0 < sz" ..
    
    show ?thesis
    proof -
      have uq: "unat (of_nat q ::'a::len word) = q"
        apply (subst unat_of_nat)
        apply (rule mod_less)
        apply (rule order_less_trans [OF qv])
        apply (rule power_strict_increasing [OF diff_less [OF sne]])
         apply (simp_all)
        done
      
      have uptr: "unat ptr = 2 ^ sz * q"
        apply (subst ptrq)
        apply (subst iffD1 [OF unat_mult_lem])
         apply (subst unat_power_lower [OF szv])
         apply (subst uq)
         apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]])
        apply (subst uq)
        apply (subst unat_power_lower [OF szv])
        apply simp    
        done  
      
      show "unat ptr + unat off < 2 ^ len_of TYPE('a)" using szv
        apply (subst uptr)
        apply (subst mult_commute, rule nat_add_offset_less [OF _ qv])
        apply (rule order_less_le_trans [OF unat_mono [OF off] order_eq_refl])
         apply simp_all
        done
    qed
  qed
qed
 
lemma is_aligned_no_wrap':
  fixes ptr :: "'a::len word"
  assumes al: "is_aligned ptr sz"
  and    off: "off < 2 ^ sz"
  shows  "ptr \<le> ptr + off"
  by (subst no_plus_overflow_unat_size, subst word_size, rule is_aligned_no_wrap) fact+

lemma is_aligned_no_overflow':
  fixes p :: "'a::len word"
  assumes al: "is_aligned p n"
  shows "p \<le> p + (2 ^ n - 1)"
proof cases
  assume "n<len_of TYPE('a)"
  with al
  have "2^n - (1::'a::len word) < 2^n"
    by (simp add: word_less_nat_alt unat_sub_if_size)
  with al
  show ?thesis by (rule is_aligned_no_wrap')
next
  assume "\<not> n<len_of TYPE('a)"
  with al
  show ?thesis
  by (simp add: not_less power_overflow is_aligned_mask mask_2pm1)
qed

lemma is_aligned_no_overflow:
  "is_aligned ptr sz \<Longrightarrow> ptr \<le> ptr + 2^sz - 1"
  by (drule is_aligned_no_overflow') (simp add: field_simps)

lemma replicate_not_True:
  "\<And>n. xs = replicate n False \<Longrightarrow> True \<notin> set xs"
  by (induct xs) auto

lemma is_aligned_replicateI:
  "to_bl p = addr @ replicate n False \<Longrightarrow> is_aligned (p::'a::len word) n"
  apply (simp add: is_aligned_to_bl word_size)
  apply (subgoal_tac "length addr = len_of TYPE('a) - n")
   apply (simp add: replicate_not_True)
  apply (drule arg_cong [where f=length])
  apply simp
  done 

lemma to_bl_1: "to_bl (1::'a::len word) = replicate (len_of TYPE('a) - 1) False @ [True]"
proof -
  have "to_bl (1 :: 'a::len word) = to_bl (mask 1 :: 'a::len word)"
    by (simp add: mask_def)
  
  also have "\<dots> = replicate (len_of TYPE('a) - 1) False @ [True]"
    apply (subst to_bl_mask)
    apply (clarsimp simp add: min_def)
    apply (case_tac "len_of TYPE('a)", simp)
    apply simp
    done
  
  finally show ?thesis .
qed

lemma to_bl_2p:
  "n < len_of TYPE('a) \<Longrightarrow>
   to_bl ((2::'a::len word) ^ n) = 
   replicate (len_of TYPE('a) - Suc n) False @ True # replicate n False"
  apply (subst shiftl_1 [symmetric])  
  apply (subst bl_shiftl)
  apply (simp add: to_bl_1 min_def word_size)
  done  

lemma map_zip_replicate_False_xor:
  "n = length xs \<Longrightarrow> map (\<lambda>(x, y). x = (\<not> y)) (zip xs (replicate n False)) = xs"
  by (induct xs arbitrary: n, auto)

lemma drop_minus_lem:
  "\<lbrakk> n \<le> length xs; 0 < n; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1)  # drop (Suc (n' - n)) xs"  
proof (induct xs arbitrary: n n')
  case Nil thus ?case by simp
next
  case (Cons y ys)
  from Cons.prems
  show ?case
    apply simp
    apply (cases "n = Suc (length ys)")
     apply (simp add: nth_append)
    apply (simp add: Suc_diff_le Cons.hyps nth_append)
    apply clarsimp
    apply arith
    done
qed

lemma drop_minus:
  "\<lbrakk> n < length xs; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - Suc n) xs = rev xs ! n  # drop (n' - n) xs"
  apply (subst drop_minus_lem)
     apply simp
    apply simp
   apply simp
  apply simp
  apply (cases "length xs", simp)
  apply (simp add: Suc_diff_le)
  done

lemma xor_2p_to_bl:
  fixes x::"'a::len word"
  shows "to_bl (x xor 2^n) = 
  (if n < len_of TYPE('a) 
   then take (len_of TYPE('a)-Suc n) (to_bl x) @ (\<not>rev (to_bl x)!n) # drop (len_of TYPE('a)-n) (to_bl x)
   else to_bl x)"
proof -
  have x: "to_bl x = take (len_of TYPE('a)-Suc n) (to_bl x) @ drop (len_of TYPE('a)-Suc n) (to_bl x)"
    by simp
  
  show ?thesis
  apply simp
  apply (rule conjI)
   apply (clarsimp simp: word_size)
   apply (simp add: bl_word_xor map2_def to_bl_2p)
   apply (subst x)
   apply (subst zip_append)
    apply simp
   apply (simp add: map_append)
   apply (simp add: map_zip_replicate_False_xor drop_minus)
  apply clarsimp
  apply (rule word_eqI)
  apply (simp add: word_size nth_w2p)
  done
qed

lemma aligned_add_xor: 
  assumes al: "is_aligned (x::'a::len word) n'" and le: "n < n'"
  shows "(x + 2^n) xor 2^n = x"
proof cases
  assume "n' < len_of TYPE('a)"
  with assms show ?thesis
  apply -
  apply (rule word_bl.Rep_eqD)
  apply (subst xor_2p_to_bl)
  apply simp
  apply (subst is_aligned_add_conv, simp,
         simp add: word_less_nat_alt)+
  apply (simp add: to_bl_2p nth_append)
  apply (cases "n' = Suc n")
   apply simp
   apply (subst is_aligned_replicate [where n="Suc n", 
                                      simplified, symmetric])
     apply assumption
    apply simp
   apply (rule refl)
  apply (subgoal_tac "\<not> len_of TYPE('a) - Suc n \<le> len_of TYPE('a) - n'")
   prefer 2
   apply arith
  apply (simp add: min_def)
  apply (subst replicate_Suc [symmetric])
  apply (subst replicate_add [symmetric])
  apply simp
  apply (simp add: is_aligned_replicate [simplified, symmetric])
  done
next
  assume "\<not> n' < len_of TYPE('a)"
  with al show ?thesis
    by (simp add: is_aligned_mask mask_def not_less power_overflow)
qed

lemma is_aligned_0 [simp]:
  "is_aligned p 0"
  by (simp add: is_aligned_def)

lemma is_aligned_replicateD:
  "\<lbrakk> is_aligned (w::'a::len word) n; n \<le> len_of TYPE('a) \<rbrakk>
     \<Longrightarrow> \<exists>xs. to_bl w = xs @ replicate n False
               \<and> length xs = size w - n"
  apply (subst is_aligned_replicate, assumption+)
  apply (rule exI, rule conjI, rule refl)
  apply (simp add: word_size)
  done

lemma is_aligned_add_mult_multI:
  fixes p :: "'a::len word"
  shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n * z) n'"
  apply (erule aligned_add_aligned)
  apply (auto intro: is_alignedI [where k="x*z"])
  done

lemma is_aligned_add_multI:
  fixes p :: "'a::len word"
  shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n) n'"
  apply (erule aligned_add_aligned)
  apply (auto intro: is_alignedI [where k="x"])
  done

lemma unat_of_nat_len:
  "x < 2 ^ len_of TYPE('a) \<Longrightarrow> unat (of_nat x :: 'a::len word) = x"
  by (simp add: word_size unat_of_nat)

lemma is_aligned_no_wrap''':
  fixes ptr :: "'a::len word"
  shows"\<lbrakk> is_aligned ptr sz; sz < len_of TYPE('a); off < 2 ^ sz \<rbrakk>
         \<Longrightarrow> unat ptr + off < 2 ^ len_of TYPE('a)"
  apply (drule is_aligned_no_wrap[where off="of_nat off"])
   apply (simp add: word_less_nat_alt)
   apply (erule order_le_less_trans[rotated])
   apply (subst unat_of_nat)
   apply (rule mod_le_dividend)
  apply (subst(asm) unat_of_nat_len)
   apply (erule order_less_trans)
   apply (erule power_strict_increasing)
   apply simp
  apply assumption
  done

lemma is_aligned_get_word_bits:
  fixes p :: "'a::len word"
  shows "\<lbrakk> is_aligned p n; \<lbrakk> is_aligned p n; n < len_of TYPE('a) \<rbrakk> \<Longrightarrow> P;
           \<lbrakk> p = 0; n \<ge> len_of TYPE('a) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
  apply (cases "n < len_of TYPE('a)")
   apply simp
  apply simp
  apply (erule meta_mp)
  apply (clarsimp simp: is_aligned_mask mask_def power_add
                        power_overflow)
  done

lemma rsubst:
  "\<lbrakk> P s; s = t \<rbrakk> \<Longrightarrow> P t"
  by simp

lemma aligned_small_is_0:
  "\<lbrakk> is_aligned x n; x < 2 ^ n \<rbrakk> \<Longrightarrow> x = 0"
  apply (erule is_aligned_get_word_bits)
   apply (frule is_aligned_add_conv [rotated, where w=0])
    apply (simp add: is_aligned_def)
   apply simp
   apply (drule is_aligned_replicateD)
    apply simp
   apply (clarsimp simp: word_size)
   apply (subst (asm) replicate_add [symmetric])
   apply (drule arg_cong[where f="of_bl :: bool list \<Rightarrow> 'a::len word"])
   apply simp
  apply (simp only: replicate.simps[symmetric, where x=False]
                    drop_replicate)
  done

corollary is_aligned_less_sz:
  "\<lbrakk>is_aligned a sz; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> a < 2 ^ sz"
  by (rule notI, drule(1) aligned_small_is_0, erule(1) notE)

lemma aligned_at_least_t2n_diff:
  "\<lbrakk>is_aligned x n; is_aligned y n; x < y\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n"
  apply (erule is_aligned_get_word_bits[where p=y])
   apply (rule ccontr)
   apply (clarsimp simp: linorder_not_le)
   apply (subgoal_tac "y - x = 0")
    apply clarsimp
   apply (rule aligned_small_is_0)
    apply (erule(1) aligned_sub_aligned)
    apply simp
   apply unat_arith
  apply simp
  done

lemma word_sub_1_le:
  "x \<noteq> 0 \<Longrightarrow> x - 1 \<le> (x :: ('a :: len) word)"
  apply (subst no_ulen_sub)
  apply simp
  apply (cases "uint x = 0")
   apply (simp add: uint_0_iff)
  apply (insert uint_ge_0[where x=x])
  apply arith
  done

lemma is_aligned_no_overflow'':
  "\<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n"
  apply (frule is_aligned_no_overflow')
  apply (erule order_trans)
  apply (simp add: field_simps)
  apply (erule word_sub_1_le)
  done

lemma is_aligned_nth:
  "is_aligned p m = (\<forall>n < m. \<not>p !! n)"
  apply (clarsimp simp: is_aligned_mask bang_eq word_size)
  apply (rule iffI)
   apply clarsimp
   apply (case_tac "n < size p")
    apply (simp add: word_size)      
   apply (drule test_bit_size)
   apply simp
  apply clarsimp
  done

lemma range_inter:
  "({a..b} \<inter> {c..d} = {}) = (\<forall>x. \<not>(a \<le> x \<and> x \<le> b \<and> c \<le> x \<and> x \<le> d))"
  by auto

lemma aligned_inter_non_empty:
  "\<lbrakk> {p..p + (2 ^ n - 1)} \<inter> {p..p + 2 ^ m - 1} = {};
     is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False"
  apply (clarsimp simp only: range_inter)
  apply (erule_tac x=p in allE)
  apply simp
  apply (erule impE)
   apply (erule is_aligned_no_overflow')
  apply (erule notE)
  apply (erule is_aligned_no_overflow)
  done

lemma not_aligned_mod_nz:
  assumes al: "\<not> is_aligned a n"
  shows "a mod 2 ^ n \<noteq> 0"
proof cases
  assume "n < len_of TYPE('a)"
  with al
  show ?thesis
    apply (simp add: is_aligned_def dvd_eq_mod_eq_0 word_arith_nat_mod
                del: word_neq_0_conv)
    apply (erule of_nat_neq_0)
    apply (rule order_less_trans)
     apply (rule mod_less_divisor)
     apply simp
    apply simp
    done
next
  assume "\<not> n < len_of TYPE('a)"
  with al
  show ?thesis
    by (simp add: is_aligned_mask mask_def not_less power_overflow
                  word_less_nat_alt word_mod_by_0)
qed

lemma nat_add_offset_le:
  fixes x :: nat
  assumes yv: "y \<le> 2 ^ n"
  and     xv: "x < 2 ^ m"
  and     mn: "sz = m + n"
  shows   "x * 2 ^ n + y \<le> 2 ^ sz"
proof (subst mn)
  from yv obtain qy where "y + qy = 2 ^ n"
    by (auto simp: le_iff_add)

  have "x * 2 ^ n + y \<le> x * 2 ^ n + 2 ^ n"
    using yv xv by simp
  also have "\<dots> = (x + 1) * 2 ^ n" by simp
  also have "\<dots> \<le> 2 ^ (m + n)" using xv
    by (subst power_add) (rule mult_le_mono1, simp)
  finally show "x * 2 ^ n + y \<le> 2 ^ (m + n)" .
qed

lemma is_aligned_no_wrap_le:
  fixes ptr::"'a::len word"
  assumes al: "is_aligned ptr sz"
  and    szv: "sz < len_of TYPE('a)"
  and    off: "off \<le> 2 ^ sz"
  shows  "unat ptr + off \<le> 2 ^ len_of TYPE('a)"
proof -
  from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and
    qv: "q < 2 ^ (len_of TYPE('a) - sz)" by (auto elim: is_alignedE)

  show ?thesis
  proof (cases "sz = 0")
    case True
    thus ?thesis using off ptrq qv
      apply (clarsimp)
      apply (erule le_SucE)
       apply (simp add: unat_of_nat)
      apply (simp add: less_eq_Suc_le [symmetric] unat_of_nat)
      done
  next
    case False
    hence sne: "0 < sz" ..

    show ?thesis
    proof -
      have uq: "unat (of_nat q :: 'a word) = q"
        apply (subst unat_of_nat)
        apply (rule mod_less)
        apply (rule order_less_trans [OF qv])
        apply (rule power_strict_increasing [OF diff_less [OF sne]])
        apply simp_all
        done

      have uptr: "unat ptr = 2 ^ sz * q"
        apply (subst ptrq)
        apply (subst iffD1 [OF unat_mult_lem])
        apply (subst unat_power_lower [OF szv])
        apply (subst uq)
        apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]])
        apply (subst uq)
        apply (subst unat_power_lower [OF szv])
        apply simp
        done

      show "unat ptr + off \<le> 2 ^ len_of TYPE('a)" using szv
        apply (subst uptr)
        apply (subst mult_commute, rule nat_add_offset_le [OF off qv])
        apply simp
        done
    qed
  qed
qed

lemma is_aligned_neg_mask:
  "m \<le> n \<Longrightarrow> is_aligned (x && ~~ mask n) m"
  apply (simp add: and_not_mask)
  apply (erule is_aligned_weaken[rotated])
  apply (rule is_aligned_shift)
  done

lemma unat_minus:
  "unat (- (x :: ('a :: len) word))
    = (if x = 0 then 0 else (2 ^ size x) - unat x)"
  using unat_sub_if_size[where x="2 ^ size x" and y=x]
  apply (clarsimp simp: word_size word_pow_0)
  apply (simp add: unat_eq_0)
  done

lemma is_aligned_minus:
  "is_aligned p n \<Longrightarrow> is_aligned (- p) n"
  apply (clarsimp simp: is_aligned_def unat_minus word_size word_neq_0_conv)
  apply (rule dvd_diff_nat, simp_all)
  apply (rule le_imp_power_dvd)
  apply (fold is_aligned_def)
  apply (erule_tac Q="0<p" in contrapos_pp)
  apply (clarsimp simp add: is_aligned_mask mask_def power_overflow)
  done

end