theory Aligned

lemma neg_mask_le_high_bits:
  \<open>NOT (mask n) \<le> w \<longleftrightarrow> (\<forall>i \<in> {n ..< size w}. bit w i)\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
  for w :: \<open>'a::len word\<close> proof assume ?Q then have \<open>w AND NOT (mask n) = NOT (mask n)\<close> by (auto simp add: bit_simps word_size intro: bit_word_eqI) then show ?P by (simp add: and_neg_mask_eq_iff_not_mask_le) next assume ?P then have *: \<open>w AND NOT (mask n) = NOT (mask n)\<close> by (simp add: and_neg_mask_eq_iff_not_mask_le) show \<open>?Q\<close> proof (rule ccontr) assume \<open>\<not> (\<forall>i\<in>{n..<size w}. bit w i)\<close> then obtain m where m: \<open>\<not> bit w m\<close> \<open>n \<le> m\<close> \<open>m < LENGTH('a)\<close> by (auto simp add: word_size) from * have \<open>bit (w AND NOT (mask n)) m \<longleftrightarrow> bit (NOT (mask n :: 'a word)) m\<close> by auto with m show False by (auto simp add: bit_simps) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (NOT (mask n) \<le> w) = (\<forall>i\<in>{n..<size w}. bit w i) proof (state)
goal (2 subgoals):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
 2. \<forall>i\<in>{n..<size w}. bit w i \<Longrightarrow> NOT (mask n) \<le> w proof (state)
this:
\<forall>i\<in>{n..<size w}. bit w i

goal (2 subgoals):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
 2. \<forall>i\<in>{n..<size w}. bit w i \<Longrightarrow> NOT (mask n) \<le> w proof (chain)
picking this:
\<forall>i\<in>{n..<size w}. bit w i proof (prove)
using this:
\<forall>i\<in>{n..<size w}. bit w i

goal (1 subgoal):
 1. w AND NOT (mask n) = NOT (mask n) proof (state)
this:
w AND NOT (mask n) = NOT (mask n)

goal (2 subgoals):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
 2. \<forall>i\<in>{n..<size w}. bit w i \<Longrightarrow> NOT (mask n) \<le> w proof (chain)
picking this:
w AND NOT (mask n) = NOT (mask n) proof (prove)
using this:
w AND NOT (mask n) = NOT (mask n)

goal (1 subgoal):
 1. NOT (mask n) \<le> w proof (state)
this:
NOT (mask n) \<le> w

goal (1 subgoal):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i proof (state)
goal (1 subgoal):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i proof (state)
this:
NOT (mask n) \<le> w

goal (1 subgoal):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i proof (chain)
picking this:
NOT (mask n) \<le> w proof (prove)
using this:
NOT (mask n) \<le> w

goal (1 subgoal):
 1. w AND NOT (mask n) = NOT (mask n) proof (state)
this:
w AND NOT (mask n) = NOT (mask n)

goal (1 subgoal):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{n..<size w}. bit w i proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>i\<in>{n..<size w}. bit w i) \<Longrightarrow> False proof (state)
this:
\<not> (\<forall>i\<in>{n..<size w}. bit w i)

goal (1 subgoal):
 1. \<not> (\<forall>i\<in>{n..<size w}. bit w i) \<Longrightarrow> False proof (chain)
picking this:
\<not> (\<forall>i\<in>{n..<size w}. bit w i) proof (prove)
using this:
\<not> (\<forall>i\<in>{n..<size w}. bit w i)

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<not> bit w m; n \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
\<not> bit w m
n \<le> m
m < LENGTH('a)

goal (1 subgoal):
 1. \<not> (\<forall>i\<in>{n..<size w}. bit w i) \<Longrightarrow> False proof (chain)
picking this:
w AND NOT (mask n) = NOT (mask n) proof (prove)
using this:
w AND NOT (mask n) = NOT (mask n)

goal (1 subgoal):
 1. bit (w AND NOT (mask n)) m = bit (NOT (mask n)) m proof (state)
this:
bit (w AND NOT (mask n)) m = bit (NOT (mask n)) m

goal (1 subgoal):
 1. \<not> (\<forall>i\<in>{n..<size w}. bit w i) \<Longrightarrow> False proof (chain)
picking this:
\<not> bit w m
n \<le> m
m < LENGTH('a)
bit (w AND NOT (mask n)) m = bit (NOT (mask n)) m proof (prove)
using this:
\<not> bit w m
n \<le> m
m < LENGTH('a)
bit (w AND NOT (mask n)) m = bit (NOT (mask n)) m

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

goal:
No subgoals! proof (state)
this:
\<forall>i\<in>{n..<size w}. bit w i

goal:
No subgoals!