theory Aligned

lemma is_aligned_no_wrap_le:
  fixes ptr::"'a::len word"
  assumes al: "is_aligned ptr sz"
  and    szv: "sz < LENGTH('a)"
  and    off: "off \<le> 2 ^ sz"
  shows  "unat ptr + off \<le> 2 ^ LENGTH('a)" proof - 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 (auto simp add: le_Suc_eq Suc_le_eq) (simp add: le_less) next case False then have sne: "0 < sz" .. show ?thesis proof - have uq: "unat (of_nat q :: 'a 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 + off \<le> 2 ^ LENGTH('a)" using szv apply (subst uptr) apply (subst mult.commute, rule nat_add_offset_le [OF off qv]) apply simp done qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a) proof (state)
goal (1 subgoal):
 1. unat ptr + off \<le> 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 + off \<le> 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a) proof (state)
goal (2 subgoals):
 1. sz = 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
 2. sz \<noteq> 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a) proof (state)
this:
sz = 0

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

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

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

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

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + off \<le> 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 + off \<le> 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a) proof (state)
goal (1 subgoal):
 1. unat ptr + off \<le> 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 + off \<le> 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 + off \<le> 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a) proof (prove)
using this:
sz < LENGTH('a)

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

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

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

goal:
No subgoals!