theory More_Word_Operations

lemma alignUp_ge:
  fixes a :: "'a :: len word"
  assumes sz: "n < LENGTH('a)"
  and nowrap: "alignUp a n \<noteq> 0"
  shows "a \<le> alignUp a n" proof (cases "is_aligned a n") case True then show ?thesis using sz by (subst alignUp_idem, simp_all) next case False 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"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 nat_less_le) moreover have "2 ^ n * (unat a div 2 ^ n + 1) \<noteq> 2 ^ LENGTH('a)" using nowrap sz apply - apply (erule contrapos_nn) apply (subst alignUp_not_aligned_eq [OF False sz]) apply (subst unat_arith_simps) apply (subst unat_word_ariths) apply (subst unat_word_ariths) apply simp apply (subst mult_mod_left) apply (simp add: unat_div field_simps power_add[symmetric] mod_mod_power) done ultimately have lt: "2 ^ n * (unat a div 2 ^ n + 1) < 2 ^ LENGTH('a)" by simp have "a = a div 2 ^ n * 2 ^ n + a mod 2 ^ n" by (rule word_mod_div_equality [symmetric]) also have "\<dots> < (a div 2 ^ n + 1) * 2 ^ n" using sz lt apply (simp add: field_simps) apply (rule word_add_less_mono1) apply (rule word_mod_less_divisor) apply (simp add: word_less_nat_alt) apply (subst unat_word_ariths) apply (simp add: unat_div) done also have "\<dots> =  alignUp a n" by (rule alignUp_not_aligned_eq [symmetric]) fact+ finally show ?thesis by (rule order_less_imp_le) qed

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

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

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

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

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

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

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

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

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> a \<le> alignUp a n proof (prove)
goal (1 subgoal):
 1. a = a div 2 ^ n * 2 ^ n + a mod 2 ^ n proof (state)
this:
a = a div 2 ^ n * 2 ^ n + a mod 2 ^ n

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

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

goal (1 subgoal):
 1. a div 2 ^ n * 2 ^ n + a mod 2 ^ n < (a div 2 ^ n + 1) * 2 ^ n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> a mod 2 ^ n + 2 ^ n * (a div 2 ^ n) < 2 ^ n + 2 ^ n * (a div 2 ^ n) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> a mod 2 ^ n < 2 ^ n
 2. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) + unat (2 ^ n * (a div 2 ^ n)) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> 0 < 2 ^ n
 2. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) + unat (2 ^ n * (a div 2 ^ n)) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) + unat (2 ^ n * (a div 2 ^ n)) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) + unat (2 ^ n) * unat (a div 2 ^ n) mod 2 ^ LENGTH('a) < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals! proof (state)
this:
a div 2 ^ n * 2 ^ n + a mod 2 ^ n < (a div 2 ^ n + 1) * 2 ^ n

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

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

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

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

goal:
No subgoals!