theory Aligned

lemma is_aligned_no_wrap:
  fixes off :: "'a::len word"
  fixes ptr :: "'a::len word"
  assumes al: "is_aligned ptr sz"
  and    off: "off < 2 ^ sz"
  shows  "unat ptr + unat off < 2 ^ LENGTH('a)" proof - have szv: "sz < LENGTH('a)" using off p2_gt_0 word_neq_0_conv by fastforce from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and
    qv: "q < 2 ^ (LENGTH('a) - sz)" by (auto elim: is_alignedE) show ?thesis proof (cases "sz = 0") case True then show ?thesis using off ptrq qv by simp next case False then have sne: "0 < sz" .. show ?thesis proof - have uq: "unat (of_nat q ::'a::len word) = q" apply (subst unat_of_nat) apply (rule mod_less) apply (rule order_less_trans [OF qv]) apply (rule power_strict_increasing [OF diff_less [OF sne]]) apply (simp_all) done have uptr: "unat ptr = 2 ^ sz * q" apply (subst ptrq) apply (subst iffD1 [OF unat_mult_lem]) apply (subst unat_power_lower [OF szv]) apply (subst uq) apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]]) apply (subst uq) apply (subst unat_power_lower [OF szv]) apply simp done show "unat ptr + unat off < 2 ^ LENGTH('a)" using szv apply (subst uptr) apply (subst mult.commute, rule nat_add_offset_less [OF _ qv]) apply (rule order_less_le_trans [OF unat_mono [OF off] order_eq_refl]) apply simp_all done qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (state)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) proof (prove)
using this:
off < 2 ^ sz
(0 < 2 ^ ?n) = (?n < LENGTH(?'a))
(?w \<noteq> 0) = (0 < ?w)

goal (1 subgoal):
 1. sz < LENGTH('a) proof (state)
this:
sz < LENGTH('a)

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (chain)
picking this:
is_aligned ptr sz proof (prove)
using this:
is_aligned ptr sz

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

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (state)
goal (2 subgoals):
 1. sz = 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
 2. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a) proof (state)
this:
sz = 0

goal (2 subgoals):
 1. sz = 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
 2. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a) proof (chain)
picking this:
sz = 0 proof (prove)
using this:
sz = 0

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
using this:
sz = 0
off < 2 ^ sz
ptr = 2 ^ sz * word_of_nat q
q < 2 ^ (LENGTH('a) - sz)

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (state)
this:
unat ptr + unat off < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a) proof (state)
goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a) proof (state)
this:
sz \<noteq> 0

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a) proof (chain)
picking this:
sz \<noteq> 0 proof (prove)
using this:
sz \<noteq> 0

goal (1 subgoal):
 1. 0 < sz proof (state)
this:
0 < sz

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (state)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat q) = q proof (prove)
goal (1 subgoal):
 1. q mod 2 ^ LENGTH('a) = q proof (prove)
goal (1 subgoal):
 1. q < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. 2 ^ (LENGTH('a) - sz) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. 0 < LENGTH('a)
 2. 1 < 2 proof (prove)
goal:
No subgoals! proof (state)
this:
unat (word_of_nat q) = q

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat ptr = 2 ^ sz * q proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz * word_of_nat q) = 2 ^ sz * q proof (prove)
goal (2 subgoals):
 1. unat (2 ^ sz) * unat (word_of_nat q) < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q proof (prove)
goal (2 subgoals):
 1. 2 ^ sz * unat (word_of_nat q) < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q proof (prove)
goal (2 subgoals):
 1. 2 ^ sz * q < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz) * q = 2 ^ sz * q proof (prove)
goal (1 subgoal):
 1. 2 ^ sz * q = 2 ^ sz * q proof (prove)
goal:
No subgoals! proof (state)
this:
unat ptr = 2 ^ sz * q

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz * q + unat off < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat off < 2 ^ sz
 2. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = LENGTH('a) - sz + sz proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz) = 2 ^ sz
 2. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = LENGTH('a) - sz + sz proof (prove)
goal:
No subgoals! proof (state)
this:
unat ptr + unat off < 2 ^ LENGTH('a)

goal:
No subgoals! proof (state)
this:
unat ptr + unat off < 2 ^ LENGTH('a)

goal:
No subgoals! proof (state)
this:
unat ptr + unat off < 2 ^ LENGTH('a)

goal:
No subgoals!