theory Aligned

lemma neg_mask_mono_le:
  "x \<le> y \<Longrightarrow> x AND NOT(mask n) \<le> y AND NOT(mask n)" for x :: "'a :: len word" proof (rule ccontr, simp add: linorder_not_le, cases "n < LENGTH('a)") case False then show "y AND NOT(mask n) < x AND NOT(mask n) \<Longrightarrow> False" by (simp add: mask_eq_decr_exp linorder_not_less power_overflow) next case True assume a: "x \<le> y" and b: "y AND NOT(mask n) < x AND NOT(mask n)" have word_bits: "n < LENGTH('a)" by fact have "y \<le> (y AND NOT(mask n)) + (y AND mask n)" by (simp add: word_plus_and_or_coroll2 add.commute) also have "\<dots> \<le> (y AND NOT(mask n)) + 2 ^ n" apply (rule word_plus_mono_right) apply (rule order_less_imp_le, rule and_mask_less_size) apply (simp add: word_size word_bits) apply (rule is_aligned_no_overflow'', simp add: is_aligned_neg_mask word_bits) apply (rule not_greatest_aligned, rule b; simp add: is_aligned_neg_mask) done also have "\<dots> \<le> x AND NOT(mask n)" using b apply (subst add.commute) apply (rule le_plus) apply (rule aligned_at_least_t2n_diff; simp add: is_aligned_neg_mask) apply (rule ccontr, simp add: linorder_not_le) apply (drule aligned_small_is_0[rotated]; simp add: is_aligned_neg_mask) done also have "\<dots> \<le> x" by (rule word_and_le2) also have "x \<le> y" by fact finally show "False" using b by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x AND NOT (mask n) \<le> y AND NOT (mask n) proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (state)
this:
\<not> n < LENGTH('a)

goal (2 subgoals):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
\<not> n < LENGTH('a) proof (prove)
using this:
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> False proof (state)
this:
y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (state)
this:
x \<le> y
y AND NOT (mask n) < x AND NOT (mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. y \<le> (y AND NOT (mask n)) + (y AND mask n) proof (state)
this:
y \<le> (y AND NOT (mask n)) + (y AND mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (state)
this:
y \<le> (y AND NOT (mask n)) + (y AND mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. (y AND NOT (mask n)) + (y AND mask n) \<le> (y AND NOT (mask n)) + 2 ^ n proof (prove)
goal (2 subgoals):
 1. y AND mask n \<le> 2 ^ n
 2. y AND NOT (mask n) \<le> (y AND NOT (mask n)) + 2 ^ n proof (prove)
goal (2 subgoals):
 1. n < size y
 2. y AND NOT (mask n) \<le> (y AND NOT (mask n)) + 2 ^ n proof (prove)
goal (1 subgoal):
 1. y AND NOT (mask n) \<le> (y AND NOT (mask n)) + 2 ^ n proof (prove)
goal (1 subgoal):
 1. (y AND NOT (mask n)) + 2 ^ n \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
(y AND NOT (mask n)) + (y AND mask n) \<le> (y AND NOT (mask n)) + 2 ^ n

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (state)
this:
(y AND NOT (mask n)) + (y AND mask n) \<le> (y AND NOT (mask n)) + 2 ^ n

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. (y AND NOT (mask n)) + 2 ^ n \<le> x AND NOT (mask n) proof (prove)
using this:
y AND NOT (mask n) < x AND NOT (mask n)

goal (1 subgoal):
 1. (y AND NOT (mask n)) + 2 ^ n \<le> x AND NOT (mask n) proof (prove)
goal (1 subgoal):
 1. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> 2 ^ n + (y AND NOT (mask n)) \<le> x AND NOT (mask n) proof (prove)
goal (2 subgoals):
 1. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> y AND NOT (mask n) \<le> (x AND NOT (mask n)) - 2 ^ n
 2. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> 2 ^ n \<le> x AND NOT (mask n) proof (prove)
goal (1 subgoal):
 1. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> 2 ^ n \<le> x AND NOT (mask n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y AND NOT (mask n) < x AND NOT (mask n); x AND NOT (mask n) < 2 ^ n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
(y AND NOT (mask n)) + 2 ^ n \<le> x AND NOT (mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (state)
this:
(y AND NOT (mask n)) + 2 ^ n \<le> x AND NOT (mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. x AND NOT (mask n) \<le> x proof (state)
this:
x AND NOT (mask n) \<le> x

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (state)
this:
x AND NOT (mask n) \<le> x

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. x \<le> y proof (state)
this:
x \<le> y

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
y = x proof (prove)
using this:
y = x

goal (1 subgoal):
 1. False proof (prove)
using this:
y = x
y AND NOT (mask n) < x AND NOT (mask n)

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

goal:
No subgoals!