theory Aligned

lemma is_aligned_addD1:
  assumes al1: "is_aligned (x + y) n"
  and     al2: "is_aligned (x::'a::len word) n"
  shows "is_aligned y n" using al2 proof (rule is_aligned_get_word_bits) assume "x = 0" then show ?thesis using al1 by simp next assume nv: "n < LENGTH('a)" from al1 obtain q1
    where xy: "x + y = 2 ^ n * of_nat q1" and "q1 < 2 ^ (LENGTH('a) - n)" by (rule is_alignedE) moreover from al2 obtain q2
    where x: "x = 2 ^ n * of_nat q2" and "q2 < 2 ^ (LENGTH('a) - n)" by (rule is_alignedE) ultimately have "y = 2 ^ n * (of_nat q1 - of_nat q2)" by (simp add: field_simps) then show ?thesis using nv by (simp add: is_aligned_mult_triv1) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned y n proof (prove)
using this:
is_aligned x n

goal (1 subgoal):
 1. is_aligned y n proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
 2. \<lbrakk>x = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> is_aligned y n proof (state)
this:
x = 0

goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
 2. \<lbrakk>x = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> is_aligned y n proof (chain)
picking this:
x = 0 proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. is_aligned y n proof (prove)
using this:
x = 0
is_aligned (x + y) n

goal (1 subgoal):
 1. is_aligned y n proof (state)
this:
is_aligned y n

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n proof (state)
this:
n < LENGTH('a)

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

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

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

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n proof (chain)
picking this:
is_aligned x n proof (prove)
using this:
is_aligned x n

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

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n proof (chain)
picking this:
x + y = 2 ^ n * word_of_nat q1
q1 < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat q2
q2 < 2 ^ (LENGTH('a) - n) proof (prove)
using this:
x + y = 2 ^ n * word_of_nat q1
q1 < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat q2
q2 < 2 ^ (LENGTH('a) - n)

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

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n proof (chain)
picking this:
y = 2 ^ n * (word_of_nat q1 - word_of_nat q2) proof (prove)
using this:
y = 2 ^ n * (word_of_nat q1 - word_of_nat q2)

goal (1 subgoal):
 1. is_aligned y n proof (prove)
using this:
y = 2 ^ n * (word_of_nat q1 - word_of_nat q2)
n < LENGTH('a)

goal (1 subgoal):
 1. is_aligned y n proof (state)
this:
is_aligned y n

goal:
No subgoals!