theory Aligned

lemma aligned_mask_step:
  "\<lbrakk> n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n' \<rbrakk> \<Longrightarrow>
   (p'::'a::len word) + mask n' \<le> p + mask n" apply (cases "LENGTH('a) \<le> n") apply (frule (1) is_aligned_over_length) apply (drule mask_over_length) apply clarsimp apply (simp add: not_le) apply (simp add: word_le_nat_alt unat_plus_simple) apply (subst unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask)+ apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask) apply (clarsimp simp: dvd_def is_aligned_iff_dvd_nat) apply (rename_tac k k') apply (thin_tac "unat p = x" for p x)+ apply (subst Suc_le_mono[symmetric]) apply (simp only: Suc_2p_unat_mask) apply (drule le_imp_less_Suc, subst (asm) Suc_2p_unat_mask, assumption) apply (erule (1) power_2_mult_step_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
 2. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; LENGTH('a) \<le> n; p = 0\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
 2. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; p = 0; mask n = - 1\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
 2. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; unat p' \<le> unat (p + mask n); is_aligned p n; is_aligned p' n'; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (p' + mask n') \<le> unat (p + mask n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; unat p' \<le> unat (p + mask n); is_aligned p n; is_aligned p' n'; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat p' + unat (mask n') \<le> unat p + unat (mask n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; unat p' \<le> unat p + unat (mask n); is_aligned p n; is_aligned p' n'; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat p' + unat (mask n') \<le> unat p + unat (mask n) proof (prove)
goal (1 subgoal):
 1. \<And>k ka. \<lbrakk>n' \<le> n; 2 ^ n' * ka \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a); unat p = 2 ^ n * k; unat p' = 2 ^ n' * ka\<rbrakk> \<Longrightarrow> 2 ^ n' * ka + unat (mask n') \<le> 2 ^ n * k + unat (mask n) proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; 2 ^ n' * k' \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a); unat p = 2 ^ n * k; unat p' = 2 ^ n' * k'\<rbrakk> \<Longrightarrow> 2 ^ n' * k' + unat (mask n') \<le> 2 ^ n * k + unat (mask n) proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; 2 ^ n' * k' \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n' * k' + unat (mask n') \<le> 2 ^ n * k + unat (mask n) proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; 2 ^ n' * k' \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> Suc (2 ^ n' * k' + unat (mask n')) \<le> Suc (2 ^ n * k + unat (mask n)) proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; 2 ^ n' * k' \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * (k + 1) proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; n < LENGTH('a); 2 ^ n' * k' < 2 ^ n * (k + 1)\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * (k + 1) proof (prove)
goal:
No subgoals!