theory Aligned

lemma is_aligned_shift:
  fixes k::"'a::len word"
  shows "is_aligned (k << m) m" proof cases assume mv: "m < LENGTH('a)" from mv obtain q where mq: "m + q = LENGTH('a)" and "0 < q" by (auto dest: less_imp_add_positive) have "(2::nat) ^ m dvd unat (push_bit m k)" proof have kv: "(unat k div 2 ^ q) * 2 ^ q + unat k mod 2 ^ q = unat k" by (rule div_mult_mod_eq) have "unat (push_bit m k) = unat (2 ^ m * k)" by (simp add: push_bit_eq_mult ac_simps) also have "\<dots> = (2 ^ m * unat k) mod (2 ^ LENGTH('a))" using mv by (simp add: unat_word_ariths(2)) also have "\<dots> = 2 ^ m * (unat k mod 2 ^ q)" by (subst mq [symmetric], subst power_add, subst mod_mult2_eq) simp finally show "unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)" . qed then show ?thesis by (unfold is_aligned_iff_dvd_nat shiftl_def) next assume "\<not> m < LENGTH('a)" then show ?thesis by (simp add: not_less power_overflow is_aligned_mask word_size shiftl_def) qed

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (k << m) m
 2. \<not> ?P \<Longrightarrow> is_aligned (k << m) m proof (chain)
picking this:
m < LENGTH('a) proof (prove)
using this:
m < LENGTH('a)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>m + q = LENGTH('a); 0 < q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
m + q = LENGTH('a)
0 < q

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (k << m) m
 2. \<not> ?P \<Longrightarrow> is_aligned (k << m) m proof (prove)
goal (1 subgoal):
 1. 2 ^ m dvd unat (push_bit m k) proof (state)
goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k proof (prove)
goal (1 subgoal):
 1. unat k div 2 ^ q * 2 ^ q + unat k mod 2 ^ q = unat k proof (state)
this:
unat k div 2 ^ q * 2 ^ q + unat k mod 2 ^ q = unat k

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k proof (prove)
goal (1 subgoal):
 1. unat (push_bit m k) = unat (2 ^ m * k) proof (state)
this:
unat (push_bit m k) = unat (2 ^ m * k)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k proof (state)
this:
unat (push_bit m k) = unat (2 ^ m * k)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k proof (prove)
goal (1 subgoal):
 1. unat (2 ^ m * k) = 2 ^ m * unat k mod 2 ^ LENGTH('a) proof (prove)
using this:
m < LENGTH('a)

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

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k proof (state)
this:
unat (2 ^ m * k) = 2 ^ m * unat k mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k proof (prove)
goal (1 subgoal):
 1. 2 ^ m * unat k mod 2 ^ LENGTH('a) = 2 ^ m * (unat k mod 2 ^ q) proof (state)
this:
2 ^ m * unat k mod 2 ^ LENGTH('a) = 2 ^ m * (unat k mod 2 ^ q)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k proof (chain)
picking this:
unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q) proof (prove)
using this:
unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q) proof (state)
this:
unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)

goal:
No subgoals! proof (state)
this:
2 ^ m dvd unat (push_bit m k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (k << m) m
 2. \<not> ?P \<Longrightarrow> is_aligned (k << m) m proof (chain)
picking this:
2 ^ m dvd unat (push_bit m k) proof (prove)
using this:
2 ^ m dvd unat (push_bit m k)

goal (1 subgoal):
 1. is_aligned (k << m) m proof (state)
this:
is_aligned (k << m) m

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

goal (1 subgoal):
 1. \<not> m < LENGTH('a) \<Longrightarrow> is_aligned (k << m) m proof (chain)
picking this:
\<not> m < LENGTH('a) proof (prove)
using this:
\<not> m < LENGTH('a)

goal (1 subgoal):
 1. is_aligned (k << m) m proof (state)
this:
is_aligned (k << m) m

goal:
No subgoals!