theory More_Word_Operations

lemma alignUp_ar_helper:
  fixes a :: "'a :: len word"
  assumes al: "is_aligned x n"
  and     sz: "n < LENGTH('a)"
  and    sub: "{x..x + 2 ^ n - 1} \<subseteq> {a..b}"
  and    anz: "a \<noteq> 0"
  shows "a \<le> alignUp a n \<and> alignUp a n + 2 ^ n - 1 \<le> b" proof from al have xl: "x \<le> x + 2 ^ n - 1" by (simp add: is_aligned_no_overflow) from xl sub have ax: "a \<le> x" by auto show "a \<le> alignUp a n" proof (rule alignUp_ge) show "alignUp a n \<noteq> 0" using al sz ax anz by (rule alignUp_is_aligned_nz) qed fact+ show "alignUp a n + 2 ^ n - 1 \<le> b" proof (rule order_trans) from xl show tp: "x + 2 ^ n - 1 \<le> b" using sub by auto from ax have "alignUp a n \<le> x" by (rule alignUp_le_greater_al) fact+ then have "alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)" using xl al is_aligned_no_overflow' olen_add_eqv word_plus_mcs_3 by blast then show "alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1" by (simp add: field_simps) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> alignUp a n \<and> alignUp a n + 2 ^ n - 1 \<le> b proof (state)
goal (2 subgoals):
 1. a \<le> alignUp a n
 2. alignUp a n + 2 ^ n - 1 \<le> b proof (chain)
picking this:
is_aligned x n proof (prove)
using this:
is_aligned x n

goal (1 subgoal):
 1. x \<le> x + 2 ^ n - 1 proof (state)
this:
x \<le> x + 2 ^ n - 1

goal (2 subgoals):
 1. a \<le> alignUp a n
 2. alignUp a n + 2 ^ n - 1 \<le> b proof (chain)
picking this:
x \<le> x + 2 ^ n - 1
{x..x + 2 ^ n - 1} \<subseteq> {a..b} proof (prove)
using this:
x \<le> x + 2 ^ n - 1
{x..x + 2 ^ n - 1} \<subseteq> {a..b}

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

goal (2 subgoals):
 1. a \<le> alignUp a n
 2. alignUp a n + 2 ^ n - 1 \<le> b proof (prove)
goal (1 subgoal):
 1. a \<le> alignUp a n proof (state)
goal (2 subgoals):
 1. n < LENGTH('a)
 2. alignUp a n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. alignUp a n \<noteq> 0 proof (prove)
using this:
is_aligned x n
n < LENGTH('a)
a \<le> x
a \<noteq> 0

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

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

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> b proof (prove)
goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> b proof (state)
goal (2 subgoals):
 1. alignUp a n + 2 ^ n - 1 \<le> ?y
 2. ?y \<le> b proof (chain)
picking this:
x \<le> x + 2 ^ n - 1 proof (prove)
using this:
x \<le> x + 2 ^ n - 1

goal (1 subgoal):
 1. x + 2 ^ n - 1 \<le> b proof (prove)
using this:
x \<le> x + 2 ^ n - 1
{x..x + 2 ^ n - 1} \<subseteq> {a..b}

goal (1 subgoal):
 1. x + 2 ^ n - 1 \<le> b proof (state)
this:
x + 2 ^ n - 1 \<le> b

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1 proof (chain)
picking this:
a \<le> x proof (prove)
using this:
a \<le> x

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

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1 proof (chain)
picking this:
alignUp a n \<le> x proof (prove)
using this:
alignUp a n \<le> x

goal (1 subgoal):
 1. alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1) proof (prove)
using this:
alignUp a n \<le> x
x \<le> x + 2 ^ n - 1
is_aligned x n
is_aligned ?p ?n \<Longrightarrow> ?p \<le> ?p + (2 ^ ?n - 1)
(?y \<le> ?y + ?x) = (?x \<le> ?y + ?x)
\<lbrakk>?v \<le> ?w; ?x \<le> ?w + ?x\<rbrakk> \<Longrightarrow> ?v + ?x \<le> ?w + ?x

goal (1 subgoal):
 1. alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1) proof (state)
this:
alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1 proof (chain)
picking this:
alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1) proof (prove)
using this:
alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1 proof (state)
this:
alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1

goal:
No subgoals! proof (state)
this:
alignUp a n + 2 ^ n - 1 \<le> b

goal:
No subgoals!