theory More_Word_Operations

lemma alignUp_is_aligned_nz:
  fixes a :: "'a :: len word"
  assumes al: "is_aligned x n"
  and     sz: "n < LENGTH('a)"
  and     ax: "a \<le> x"
  and     az: "a \<noteq> 0"
  shows   "alignUp (a::'a :: len word) n \<noteq> 0" proof (cases "is_aligned a n") case True then have "alignUp a n = a" using sz by (simp add: alignUp_idem) then show ?thesis using az by simp next case False then have anz: "a mod 2 ^ n \<noteq> 0" by (rule not_aligned_mod_nz) { assume asm: "alignUp a n = 0" have lt0: "unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)" using sz by (metis le_add_diff_inverse2 less_mult_imp_div_less order_less_imp_le power_add unsigned_less) have leq: "2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)" using sz by (metis One_nat_def Suc_leI add.right_neutral add_Suc_right lt0 nat_le_power_trans
                order_less_imp_le) from al obtain k where  kv: "k < 2 ^ (LENGTH('a) - n)" and xk: "x = 2 ^ n * of_nat k" by (auto elim!: is_alignedE) then have "a div 2 ^ n < of_nat k" using ax sz anz by (rule alignUp_div_helper) then have r: "unat a div 2 ^ n < k" using sz by (simp flip: drop_bit_eq_div unat_drop_bit_eq) (metis leI le_unat_uoi unat_mono) have "alignUp a n = (a div 2 ^ n + 1) * 2 ^ n" by (rule alignUp_not_aligned_eq) fact+ then have "\<dots> = 0" using asm by simp then have "2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)" using sz by (simp add: unat_arith_simps ac_simps)
                  (simp add: unat_word_ariths mod_simps mod_eq_0_iff_dvd) with leq have "2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)" by (force elim!: le_SucE) then have "unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1" by (metis (no_types, opaque_lifting) Groups.add_ac(2) add.right_neutral
                add_diff_cancel_left' div_le_dividend div_mult_self4 gr_implies_not0
                le_neq_implies_less power_eq_0_iff zero_neq_numeral) then have "unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1" using sz by (simp add: power_sub) then have "2 ^ (LENGTH('a) - n) - 1 < k" using r by simp then have False using kv by simp } then show ?thesis by clarsimp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. alignUp a n \<noteq> 0 proof (state)
goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
 2. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (state)
this:
is_aligned a n

goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
 2. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
is_aligned a n proof (prove)
using this:
is_aligned a n

goal (1 subgoal):
 1. alignUp a n = a proof (prove)
using this:
is_aligned a n
n < LENGTH('a)

goal (1 subgoal):
 1. alignUp a n = a proof (state)
this:
alignUp a n = a

goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
 2. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
alignUp a n = a proof (prove)
using this:
alignUp a n = a

goal (1 subgoal):
 1. alignUp a n \<noteq> 0 proof (prove)
using this:
alignUp a n = a
a \<noteq> 0

goal (1 subgoal):
 1. alignUp a n \<noteq> 0 proof (state)
this:
alignUp a n \<noteq> 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (state)
goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (state)
this:
\<not> is_aligned a n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
\<not> is_aligned a n proof (prove)
using this:
\<not> is_aligned a n

goal (1 subgoal):
 1. a mod 2 ^ n \<noteq> 0 proof (state)
this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (state)
this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (state)
this:
alignUp a n = 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. unat a div 2 ^ n < 2 ^ (LENGTH('a) - n) proof (prove)
using this:
n < LENGTH('a)

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

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a) proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a) proof (state)
this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
is_aligned x n proof (prove)
using this:
is_aligned x n

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < 2 ^ (LENGTH('a) - n); x = 2 ^ n * word_of_nat k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
k < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat k

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
k < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat k proof (prove)
using this:
k < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat k

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (prove)
using this:
k < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat k
a \<le> x
n < LENGTH('a)
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k proof (state)
this:
a div 2 ^ n < word_of_nat k

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
a div 2 ^ n < word_of_nat k proof (prove)
using this:
a div 2 ^ n < word_of_nat k

goal (1 subgoal):
 1. unat a div 2 ^ n < k proof (prove)
using this:
a div 2 ^ n < word_of_nat k
n < LENGTH('a)

goal (1 subgoal):
 1. unat a div 2 ^ n < k proof (state)
this:
unat a div 2 ^ n < k

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

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

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

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

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

goal (1 subgoal):
 1. 2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1) proof (prove)
using this:
(a div 2 ^ n + 1) * 2 ^ n = 0
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1) proof (state)
this:
2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1) proof (prove)
using this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)

goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a) proof (state)
this:
2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a) proof (prove)
using this:
2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1 proof (state)
this:
unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1 proof (prove)
using this:
unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1

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

goal (1 subgoal):
 1. unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1 proof (state)
this:
unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1 proof (prove)
using this:
unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1

goal (1 subgoal):
 1. 2 ^ (LENGTH('a) - n) - 1 < k proof (prove)
using this:
unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1
unat a div 2 ^ n < k

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

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
2 ^ (LENGTH('a) - n) - 1 < k proof (prove)
using this:
2 ^ (LENGTH('a) - n) - 1 < k

goal (1 subgoal):
 1. False proof (prove)
using this:
2 ^ (LENGTH('a) - n) - 1 < k
k < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. False proof (state)
this:
False

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (state)
this:
alignUp a n = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0 proof (chain)
picking this:
alignUp a n = 0 \<Longrightarrow> False proof (prove)
using this:
alignUp a n = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. alignUp a n \<noteq> 0 proof (state)
this:
alignUp a n \<noteq> 0

goal:
No subgoals!