theory Aligned

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 < LENGTH('a)" show ?thesis unfolding is_aligned_iff_dvd_nat dvd_def proof - from aligned2 obtain q2 where yv: "y = 2 ^ m * of_nat q2"
      and q2v: "q2 < 2 ^ (LENGTH('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 ^ (LENGTH('a) - (m + k))" by (auto elim: is_alignedE) have l1: "2 ^ (m + k) * q1 < 2 ^ LENGTH('a)" by (rule nat_less_power_trans [OF q1v])
         (subst kv, rule order_less_imp_le [OF nlt]) have l2: "2 ^ m * q2 < 2 ^ LENGTH('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)" proof - have f1: "unat x = 2 ^ (m + k) * q1" using q1v unat_mult_power_lem xv by blast have "unat y = 2 ^ m * q2" using q2v unat_mult_power_lem yv by blast then show ?thesis using f1 by (simp add: power_add semiring_normalization_rules(34)) qed 

    (* (2 ^ k * q1 + q2) *)
     show "\<exists>d. unat (x + y) = 2 ^ m * d" proof (cases "unat x + unat y < 2 ^ LENGTH('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 then have "unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)" by (subst unat_word_ariths(1)) simp also have "\<dots> = (2 ^ m * (2 ^ k * q1 + q2)) mod 2 ^ LENGTH('a)" by (subst upls, rule refl) also have "\<dots> = 2 ^ m * ((2 ^ k * q1 +  q2) mod 2 ^ (LENGTH('a) - m))" proof - have "m \<le> len_of (TYPE('a))" by (meson le_trans less_imp_le_nat lt nlt) then show ?thesis by (metis mult_mod_right ordered_cancel_comm_monoid_diff_class.add_diff_inverse power_add) qed finally show ?thesis .. qed qed next assume "\<not> n < LENGTH('a)" with assms show ?thesis by (simp add: is_aligned_mask not_less take_bit_eq_mod power_overflow word_arith_nat_defs(7) flip: take_bit_eq_mask) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (x + y) m proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (x + y) m
 2. \<not> ?P \<Longrightarrow> is_aligned (x + y) m proof (state)
this:
n < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (x + y) m
 2. \<not> ?P \<Longrightarrow> is_aligned (x + y) m proof (prove)
goal (1 subgoal):
 1. is_aligned (x + y) m proof (prove)
goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (state)
goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (chain)
picking this:
is_aligned y m proof (prove)
using this:
is_aligned y m

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

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (chain)
picking this:
m \<le> n proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. (\<And>k. m + k = n \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
m + k = n

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (chain)
picking this:
is_aligned x n
m + k = n proof (prove)
using this:
is_aligned x n
m + k = n

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

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (prove)
goal (1 subgoal):
 1. 2 ^ (m + k) * q1 < 2 ^ LENGTH('a) proof (state)
this:
2 ^ (m + k) * q1 < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (prove)
goal (1 subgoal):
 1. 2 ^ m * q2 < 2 ^ LENGTH('a) proof (state)
this:
2 ^ m * q2 < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (prove)
goal (1 subgoal):
 1. x = word_of_nat (2 ^ (m + k) * q1) proof (prove)
using this:
x = 2 ^ (m + k) * word_of_nat q1

goal (1 subgoal):
 1. x = word_of_nat (2 ^ (m + k) * q1) proof (state)
this:
x = word_of_nat (2 ^ (m + k) * q1)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (state)
this:
x = word_of_nat (2 ^ (m + k) * q1)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (prove)
goal (1 subgoal):
 1. y = word_of_nat (2 ^ m * q2) proof (prove)
using this:
y = 2 ^ m * word_of_nat q2

goal (1 subgoal):
 1. y = word_of_nat (2 ^ m * q2) proof (state)
this:
y = word_of_nat (2 ^ m * q2)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (chain)
picking this:
x = word_of_nat (2 ^ (m + k) * q1)
y = word_of_nat (2 ^ m * q2) proof (prove)
using this:
x = word_of_nat (2 ^ (m + k) * q1)
y = word_of_nat (2 ^ m * q2)

goal (1 subgoal):
 1. unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2) proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = word_of_nat (2 ^ (m + k) * q1); y = word_of_nat (2 ^ m * q2)\<rbrakk> \<Longrightarrow> unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2) proof (prove)
goal (1 subgoal):
 1. unat x = 2 ^ (m + k) * q1 proof (prove)
using this:
q1 < 2 ^ (LENGTH('a) - (m + k))
?k < 2 ^ (LENGTH(?'a) - ?sz) \<Longrightarrow> unat (2 ^ ?sz * word_of_nat ?k) = 2 ^ ?sz * ?k
x = 2 ^ (m + k) * word_of_nat q1

goal (1 subgoal):
 1. unat x = 2 ^ (m + k) * q1 proof (state)
this:
unat x = 2 ^ (m + k) * q1

goal (1 subgoal):
 1. \<lbrakk>x = word_of_nat (2 ^ (m + k) * q1); y = word_of_nat (2 ^ m * q2)\<rbrakk> \<Longrightarrow> unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2) proof (prove)
goal (1 subgoal):
 1. unat y = 2 ^ m * q2 proof (prove)
using this:
q2 < 2 ^ (LENGTH('a) - m)
?k < 2 ^ (LENGTH(?'a) - ?sz) \<Longrightarrow> unat (2 ^ ?sz * word_of_nat ?k) = 2 ^ ?sz * ?k
y = 2 ^ m * word_of_nat q2

goal (1 subgoal):
 1. unat y = 2 ^ m * q2 proof (state)
this:
unat y = 2 ^ m * q2

goal (1 subgoal):
 1. \<lbrakk>x = word_of_nat (2 ^ (m + k) * q1); y = word_of_nat (2 ^ m * q2)\<rbrakk> \<Longrightarrow> unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2) proof (chain)
picking this:
unat y = 2 ^ m * q2 proof (prove)
using this:
unat y = 2 ^ m * q2

goal (1 subgoal):
 1. unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2) proof (prove)
using this:
unat y = 2 ^ m * q2
unat x = 2 ^ (m + k) * q1

goal (1 subgoal):
 1. unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2) proof (state)
this:
unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)

goal:
No subgoals! proof (state)
this:
unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (state)
this:
unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k proof (prove)
goal (1 subgoal):
 1. \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
this:
unat x + unat y < 2 ^ LENGTH('a)

goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (prove)
goal (1 subgoal):
 1. unat (x + y) = unat x + unat y proof (state)
this:
unat (x + y) = unat x + unat y

goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
this:
unat (x + y) = unat x + unat y

goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (prove)
goal (1 subgoal):
 1. unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2) proof (state)
this:
unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)

goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (chain)
picking this:
unat (x + y) = 2 ^ m * (2 ^ k * q1 + q2) proof (prove)
using this:
unat (x + y) = 2 ^ m * (2 ^ k * q1 + q2)

goal (1 subgoal):
 1. \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
this:
\<exists>d. unat (x + y) = 2 ^ m * d

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
this:
\<not> unat x + unat y < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (chain)
picking this:
\<not> unat x + unat y < 2 ^ LENGTH('a) proof (prove)
using this:
\<not> unat x + unat y < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a) proof (state)
this:
unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
this:
unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (prove)
goal (1 subgoal):
 1. (unat x + unat y) mod 2 ^ LENGTH('a) = 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) proof (state)
this:
(unat x + unat y) mod 2 ^ LENGTH('a) = 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
this:
(unat x + unat y) mod 2 ^ LENGTH('a) = 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (prove)
goal (1 subgoal):
 1. 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m)) proof (state)
goal (1 subgoal):
 1. 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m)) proof (prove)
goal (1 subgoal):
 1. m \<le> LENGTH('a) proof (state)
this:
m \<le> LENGTH('a)

goal (1 subgoal):
 1. 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m)) proof (chain)
picking this:
m \<le> LENGTH('a) proof (prove)
using this:
m \<le> LENGTH('a)

goal (1 subgoal):
 1. 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m)) proof (state)
this:
2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))

goal:
No subgoals! proof (state)
this:
2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d proof (chain)
picking this:
unat (x + y) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m)) proof (prove)
using this:
unat (x + y) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))

goal (1 subgoal):
 1. \<exists>d. unat (x + y) = 2 ^ m * d proof (state)
this:
\<exists>d. unat (x + y) = 2 ^ m * d

goal:
No subgoals! proof (state)
this:
\<exists>d. unat (x + y) = 2 ^ m * d

goal:
No subgoals! proof (state)
this:
is_aligned (x + y) m

goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> is_aligned (x + y) m proof (state)
goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> is_aligned (x + y) m proof (state)
this:
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> is_aligned (x + y) m proof (chain)
picking this:
is_aligned x n
is_aligned y m
m \<le> n
\<not> n < LENGTH('a) proof (prove)
using this:
is_aligned x n
is_aligned y m
m \<le> n
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. is_aligned (x + y) m proof (state)
this:
is_aligned (x + y) m

goal:
No subgoals!