theory More_Word_Operations

lemma alignUp_not_aligned_eq:
  fixes a :: "'a :: len word"
  assumes al: "\<not> is_aligned a n"
  and     sz: "n < LENGTH('a)"
  shows   "alignUp a n = (a div 2 ^ n + 1) * 2 ^ n" proof - from \<open>n < LENGTH('a)\<close> have \<open>(2::int) ^ n < 2 ^ LENGTH('a)\<close> by simp with take_bit_int_less_exp [of n] have *: \<open>take_bit n k < 2 ^ LENGTH('a)\<close> for k :: int by (rule less_trans) have anz: "a mod 2 ^ n \<noteq> 0" by (rule not_aligned_mod_nz) fact+ then have um: "unat (a mod 2 ^ n - 1) div 2 ^ n = 0" apply (transfer fixing: n) using sz apply (simp flip: take_bit_eq_mod add: div_eq_0_iff) apply (subst take_bit_int_eq_self) using * apply (auto simp add: diff_less_eq intro: less_imp_le) apply (simp add: less_le) done have "a + 2 ^ n - 1 = (a div 2 ^ n) * 2 ^ n + (a mod 2 ^ n) + 2 ^ n - 1" by (simp add: word_mod_div_equality) also have "\<dots> = (a mod 2 ^ n - 1) + (a div 2 ^ n + 1) * 2 ^ n" by (simp add: field_simps) finally show "alignUp a n = (a div 2 ^ n + 1) * 2 ^ n" using sz unfolding alignUp_def apply (subst mask_eq_decr_exp [symmetric]) apply (erule ssubst) apply (subst neg_mask_is_div) apply (simp add: word_arith_nat_div) apply (subst unat_word_ariths(1) unat_word_ariths(2))+ apply (subst uno_simps) apply (subst unat_1) apply (subst mod_add_right_eq) apply simp apply (subst power_mod_div) apply (subst div_mult_self1) apply simp apply (subst um) apply simp apply (subst mod_mod_power) apply simp apply (subst word_unat_power, subst Abs_fnat_hom_mult) apply (subst mult_mod_left) apply (subst power_add [symmetric]) apply simp apply (subst Abs_fnat_hom_1) apply (subst Abs_fnat_hom_add) apply (subst word_unat_power, subst Abs_fnat_hom_mult) apply (subst word_unat.Rep_inverse[symmetric], subst Abs_fnat_hom_mult) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (state)
goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (chain)
picking this:
n < LENGTH('a) proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ n < 2 ^ LENGTH('a) proof (state)
this:
2 ^ n < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (chain)
picking this:
take_bit n ?k < 2 ^ n
2 ^ n < 2 ^ LENGTH('a) proof (prove)
using this:
take_bit n ?k < 2 ^ n
2 ^ n < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. take_bit n k < 2 ^ LENGTH('a) proof (state)
this:
take_bit n ?k < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n \<noteq> 0 proof (state)
this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (chain)
picking this:
a mod 2 ^ n \<noteq> 0 proof (prove)
using this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. unat (a mod 2 ^ n - 1) div 2 ^ n = 0 proof (prove)
goal (1 subgoal):
 1. \<And>a. take_bit LENGTH('a) (take_bit LENGTH('a) a mod take_bit LENGTH('a) (2 ^ n)) \<noteq> take_bit LENGTH('a) 0 \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) a mod take_bit LENGTH('a) (2 ^ n) - 1) div 2 ^ n = 0 proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<And>a. take_bit LENGTH('a) (take_bit LENGTH('a) a mod take_bit LENGTH('a) (2 ^ n)) \<noteq> take_bit LENGTH('a) 0 \<Longrightarrow> (nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) a mod take_bit LENGTH('a) (2 ^ n) - 1) div 2 ^ n = 0 proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>take_bit n a \<noteq> 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) (take_bit n a - 1) < 2 ^ n proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>take_bit n a \<noteq> 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 0 \<le> take_bit n a - 1
 2. \<And>a. \<lbrakk>take_bit n a \<noteq> 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit n a - 1 < 2 ^ LENGTH('a)
 3. \<And>a. \<lbrakk>take_bit n a \<noteq> 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit n a - 1 < 2 ^ n proof (prove)
using this:
take_bit n ?k < 2 ^ LENGTH('a)

goal (3 subgoals):
 1. \<And>a. \<lbrakk>take_bit n a \<noteq> 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 0 \<le> take_bit n a - 1
 2. \<And>a. \<lbrakk>take_bit n a \<noteq> 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit n a - 1 < 2 ^ LENGTH('a)
 3. \<And>a. \<lbrakk>take_bit n a \<noteq> 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit n a - 1 < 2 ^ n proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>take_bit n a \<noteq> 0; n < LENGTH('a); \<And>k. take_bit n k < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> 0 < take_bit n a proof (prove)
goal:
No subgoals! proof (state)
this:
unat (a mod 2 ^ n - 1) div 2 ^ n = 0

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. a + 2 ^ n - 1 = a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1 proof (state)
this:
a + 2 ^ n - 1 = a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (state)
this:
a + 2 ^ n - 1 = a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n proof (state)
this:
a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (chain)
picking this:
a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n proof (prove)
using this:
a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
using this:
a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n
n < LENGTH('a)

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
using this:
a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n
n < LENGTH('a)

goal (1 subgoal):
 1. a + 2 ^ n - 1 AND NOT (2 ^ n - 1) = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a + 2 ^ n - 1 AND NOT (mask n) = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n AND NOT (mask n) = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> (a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n) div 2 ^ n * 2 ^ n = (a div 2 ^ n + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (unat (a mod 2 ^ n - 1 + (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + (unat (word_of_nat (unat a div 2 ^ n)) + unat 1) mod 2 ^ LENGTH('a) * unat (2 ^ n) mod 2 ^ LENGTH('a)) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + (unat a div 2 ^ n + unat 1) mod 2 ^ LENGTH('a) * unat (2 ^ n) mod 2 ^ LENGTH('a)) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + (unat a div 2 ^ n + 1) mod 2 ^ LENGTH('a) * unat (2 ^ n) mod 2 ^ LENGTH('a)) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + (unat a div 2 ^ n + 1) mod 2 ^ LENGTH('a) * unat (2 ^ n)) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) * 2 ^ n) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) * 2 ^ n) div 2 ^ n mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (2 subgoals):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n \<noteq> 0
 2. n < LENGTH('a) \<Longrightarrow> word_of_nat ((Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) + unat (a mod 2 ^ n - 1) div 2 ^ n) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) + unat (a mod 2 ^ n - 1) div 2 ^ n) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) + 0) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) mod 2 ^ min LENGTH('a) (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) mod 2 ^ (LENGTH('a) - n) * 2 ^ n) = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) * 2 ^ n mod (2 ^ (LENGTH('a) - n) * 2 ^ n)) = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) * 2 ^ n mod 2 ^ (LENGTH('a) - n + n)) = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + word_of_nat (Suc 0)) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n) * 2 ^ n = word_of_nat (unat a div 2 ^ n + Suc 0) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n * 2 ^ n) = word_of_nat (unat a div 2 ^ n + Suc 0) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n * 2 ^ n) = word_of_nat ((unat a div 2 ^ n + Suc 0) * unat (2 ^ n)) proof (prove)
goal:
No subgoals! proof (state)
this:
alignUp a n = (a div 2 ^ n + 1) * 2 ^ n

goal:
No subgoals!