theory Aligned

lemma aligned_neq_into_no_overlap:
  fixes x :: "'a::len word"
  assumes neq: "x \<noteq> y"
  and     alx: "is_aligned x sz"
  and     aly: "is_aligned y sz"
  shows  "{x .. x + (2 ^ sz - 1)} \<inter> {y .. y + (2 ^ sz - 1)} = {}" proof cases assume szv: "sz < LENGTH('a)" show ?thesis proof (rule equals0I, clarsimp) fix z assume xb: "x \<le> z" and xt: "z \<le> x + (2 ^ sz - 1)"
      and yb: "y \<le> z" and yt: "z \<le> y + (2 ^ sz - 1)" have rl: "\<And>(p::'a word) k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; w \<le> p + (2 ^ sz - 1) \<rbrakk>
      \<Longrightarrow> k < 2 ^ sz" apply - apply simp apply (subst (asm) add.commute, subst (asm) add.commute, drule word_plus_mcs_4) apply (subst add.commute, subst no_plus_overflow_uint_size) apply transfer apply simp apply (auto simp add: le_less power_2_ge_iff szv) apply (metis le_less_trans mask_eq_decr_exp mask_lt_2pn order_less_imp_le szv) done from xb obtain kx where
      kx: "z = x + kx" and
      kxl: "uint x + uint kx < 2 ^ LENGTH('a)" by (clarsimp dest!: word_le_exists') from yb obtain ky where
      ky: "z = y + ky" and
      kyl: "uint y + uint ky < 2 ^ LENGTH('a)" by (clarsimp dest!: word_le_exists') have "x = y" proof - have "kx = z mod 2 ^ sz" proof (subst kx, rule sym, rule aligned_add_offset_mod) show "kx < 2 ^ sz" by (rule rl) fact+ qed fact+ also have "\<dots> = ky" proof (subst ky, rule aligned_add_offset_mod) show "ky < 2 ^ sz" using kyl ky yt by (rule rl) qed fact+ finally have kxky: "kx = ky" . moreover have "x + kx = y + ky" by (simp add: kx [symmetric] ky [symmetric]) ultimately show ?thesis by simp qed then show False using neq by simp qed next assume "\<not> sz < LENGTH('a)" with neq alx aly have False by (simp add: is_aligned_mask mask_eq_decr_exp power_overflow) then show ?thesis .. qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
 2. \<not> ?P \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
 2. \<not> ?P \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (state)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False proof (state)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False proof (state)
this:
x \<le> z
z \<le> x + (2 ^ sz - 1)
y \<le> z
z \<le> y + (2 ^ sz - 1)

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; w \<le> p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> k < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; w \<le> p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> k < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; p + k \<le> p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> k < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k\<rbrakk> \<Longrightarrow> p \<le> k + p
 2. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; k \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k\<rbrakk> \<Longrightarrow> uint p + uint k < 2 ^ size p
 2. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; k \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p k w. \<lbrakk>take_bit LENGTH('a) p + take_bit LENGTH('a) k < 2 ^ LENGTH('a); take_bit LENGTH('a) w = take_bit LENGTH('a) (p + k)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) p + take_bit LENGTH('a) k < 2 ^ LENGTH('a)
 2. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; k \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; k \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<And>p k. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); k < 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>uint ?p + uint ?k < 2 ^ LENGTH('a); ?w = ?p + ?k; ?w \<le> ?p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> ?k < 2 ^ sz

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
x \<le> z proof (prove)
using this:
x \<le> z

goal (1 subgoal):
 1. (\<And>kx. \<lbrakk>z = x + kx; uint x + uint kx < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
z = x + kx
uint x + uint kx < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
y \<le> z proof (prove)
using this:
y \<le> z

goal (1 subgoal):
 1. (\<And>ky. \<lbrakk>z = y + ky; uint y + uint ky < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
z = y + ky
uint y + uint ky < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. x = y proof (state)
goal (1 subgoal):
 1. x = y proof (prove)
goal (1 subgoal):
 1. kx = z mod 2 ^ sz proof (state)
goal (2 subgoals):
 1. is_aligned x sz
 2. kx < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. kx < 2 ^ sz proof (state)
this:
kx < 2 ^ sz

goal (1 subgoal):
 1. is_aligned x sz proof (state)
this:
kx = z mod 2 ^ sz

goal (1 subgoal):
 1. x = y proof (state)
this:
kx = z mod 2 ^ sz

goal (1 subgoal):
 1. x = y proof (prove)
goal (1 subgoal):
 1. z mod 2 ^ sz = ky proof (state)
goal (2 subgoals):
 1. is_aligned y sz
 2. ky < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. ky < 2 ^ sz proof (prove)
using this:
uint y + uint ky < 2 ^ LENGTH('a)
z = y + ky
z \<le> y + (2 ^ sz - 1)

goal (1 subgoal):
 1. ky < 2 ^ sz proof (state)
this:
ky < 2 ^ sz

goal (1 subgoal):
 1. is_aligned y sz proof (state)
this:
z mod 2 ^ sz = ky

goal (1 subgoal):
 1. x = y proof (chain)
picking this:
kx = ky proof (prove)
using this:
kx = ky

goal (1 subgoal):
 1. kx = ky proof (state)
this:
kx = ky

goal (1 subgoal):
 1. x = y proof (state)
this:
kx = ky

goal (1 subgoal):
 1. x = y proof (prove)
goal (1 subgoal):
 1. x + kx = y + ky proof (state)
this:
x + kx = y + ky

goal (1 subgoal):
 1. x = y proof (chain)
picking this:
kx = ky
x + kx = y + ky proof (prove)
using this:
kx = ky
x + kx = y + ky

goal (1 subgoal):
 1. x = y proof (state)
this:
x = y

goal:
No subgoals! proof (state)
this:
x = y

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
x = y proof (prove)
using this:
x = y

goal (1 subgoal):
 1. False proof (prove)
using this:
x = y
x \<noteq> y

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals! proof (state)
this:
{x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (chain)
picking this:
x \<noteq> y
is_aligned x sz
is_aligned y sz
\<not> sz < LENGTH('a) proof (prove)
using this:
x \<noteq> y
is_aligned x sz
is_aligned y sz
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. False proof (state)
this:
False

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (chain)
picking this:
False proof (prove)
using this:
False

goal (1 subgoal):
 1. {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {} proof (state)
this:
{x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}

goal:
No subgoals!