theory Word_Lemmas

lemma zero_base_lsb_imp_set_eq_as_bit_operation:
  fixes base ::"'a::len word"
  assumes valid_prefix: "mask (LENGTH('a) - len) AND base = 0"
  shows "(base = NOT (mask (LENGTH('a) - len)) AND a) \<longleftrightarrow>
         (a \<in> {base .. base OR mask (LENGTH('a) - len)})" proof have helper3: "x OR y = x OR y AND NOT x" for x y ::"'a::len word" by (simp add: word_oa_dist2) from assms show "base = NOT (mask (LENGTH('a) - len)) AND a \<Longrightarrow>
                    a \<in> {base..base OR mask (LENGTH('a) - len)}" apply(simp add: word_and_le1) apply(metis helper3 le_word_or2 word_bw_comms(1) word_bw_comms(2)) done next assume "a \<in> {base..base OR mask (LENGTH('a) - len)}" hence a: "base \<le> a \<and> a \<le> base OR mask (LENGTH('a) - len)" by simp show "base = NOT (mask (LENGTH('a) - len)) AND a" proof - have f2: "\<forall>x\<^sub>0. base AND NOT (mask x\<^sub>0) \<le> a AND NOT (mask x\<^sub>0)" using a neg_mask_mono_le by blast have f3: "\<forall>x\<^sub>0. a AND NOT (mask x\<^sub>0) \<le> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>0)" using a neg_mask_mono_le by blast have f4: "base = base AND NOT (mask (LENGTH('a) - len))" using valid_prefix by (metis mask_eq_0_eq_x word_bw_comms(1)) hence f5: "\<forall>x\<^sub>6. (base OR x\<^sub>6) AND NOT (mask (LENGTH('a) - len)) =
                      base OR x\<^sub>6 AND NOT (mask (LENGTH('a) - len))" using word_ao_dist by (metis) have f6: "\<forall>x\<^sub>2 x\<^sub>3. a AND NOT (mask x\<^sub>2) \<le> x\<^sub>3 \<or>
                      \<not> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>2) \<le> x\<^sub>3" using f3 dual_order.trans by auto have "base = (base OR mask (LENGTH('a) - len)) AND NOT (mask (LENGTH('a) - len))" using f5 by auto hence "base = a AND NOT (mask (LENGTH('a) - len))" using f2 f4 f6 by (metis eq_iff) thus "base = NOT (mask (LENGTH('a) - len)) AND a" by (metis word_bw_comms(1)) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (base = NOT (mask (LENGTH('a) - len)) AND a) = (a \<in> {base..base OR mask (LENGTH('a) - len)}) proof (state)
goal (2 subgoals):
 1. base = NOT (mask (LENGTH('a) - len)) AND a \<Longrightarrow> a \<in> {base..base OR mask (LENGTH('a) - len)}
 2. a \<in> {base..base OR mask (LENGTH('a) - len)} \<Longrightarrow> base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
goal (1 subgoal):
 1. x OR y = x OR y AND NOT x proof (state)
this:
?x OR ?y = ?x OR ?y AND NOT ?x

goal (2 subgoals):
 1. base = NOT (mask (LENGTH('a) - len)) AND a \<Longrightarrow> a \<in> {base..base OR mask (LENGTH('a) - len)}
 2. a \<in> {base..base OR mask (LENGTH('a) - len)} \<Longrightarrow> base = NOT (mask (LENGTH('a) - len)) AND a proof (chain)
picking this:
mask (LENGTH('a) - len) AND base = 0 proof (prove)
using this:
mask (LENGTH('a) - len) AND base = 0

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a \<Longrightarrow> a \<in> {base..base OR mask (LENGTH('a) - len)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>base = NOT (mask (LENGTH('a) - len)) AND a; mask (LENGTH('a) - len) AND NOT (mask (LENGTH('a) - len)) AND a = 0\<rbrakk> \<Longrightarrow> a \<le> NOT (mask (LENGTH('a) - len)) AND a OR mask (LENGTH('a) - len) proof (prove)
goal:
No subgoals! proof (state)
this:
base = NOT (mask (LENGTH('a) - len)) AND a \<Longrightarrow> a \<in> {base..base OR mask (LENGTH('a) - len)}

goal (1 subgoal):
 1. a \<in> {base..base OR mask (LENGTH('a) - len)} \<Longrightarrow> base = NOT (mask (LENGTH('a) - len)) AND a proof (state)
goal (1 subgoal):
 1. a \<in> {base..base OR mask (LENGTH('a) - len)} \<Longrightarrow> base = NOT (mask (LENGTH('a) - len)) AND a proof (state)
this:
a \<in> {base..base OR mask (LENGTH('a) - len)}

goal (1 subgoal):
 1. a \<in> {base..base OR mask (LENGTH('a) - len)} \<Longrightarrow> base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
using this:
a \<in> {base..base OR mask (LENGTH('a) - len)}

goal (1 subgoal):
 1. base \<le> a \<and> a \<le> base OR mask (LENGTH('a) - len) proof (state)
this:
base \<le> a \<and> a \<le> base OR mask (LENGTH('a) - len)

goal (1 subgoal):
 1. a \<in> {base..base OR mask (LENGTH('a) - len)} \<Longrightarrow> base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (state)
goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
goal (1 subgoal):
 1. \<forall>x\<^sub>0. base AND NOT (mask x\<^sub>0) \<le> a AND NOT (mask x\<^sub>0) proof (prove)
using this:
base \<le> a \<and> a \<le> base OR mask (LENGTH('a) - len)
?x \<le> ?y \<Longrightarrow> ?x AND NOT (mask ?n) \<le> ?y AND NOT (mask ?n)

goal (1 subgoal):
 1. \<forall>x\<^sub>0. base AND NOT (mask x\<^sub>0) \<le> a AND NOT (mask x\<^sub>0) proof (state)
this:
\<forall>x\<^sub>0. base AND NOT (mask x\<^sub>0) \<le> a AND NOT (mask x\<^sub>0)

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
goal (1 subgoal):
 1. \<forall>x\<^sub>0. a AND NOT (mask x\<^sub>0) \<le> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>0) proof (prove)
using this:
base \<le> a \<and> a \<le> base OR mask (LENGTH('a) - len)
?x \<le> ?y \<Longrightarrow> ?x AND NOT (mask ?n) \<le> ?y AND NOT (mask ?n)

goal (1 subgoal):
 1. \<forall>x\<^sub>0. a AND NOT (mask x\<^sub>0) \<le> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>0) proof (state)
this:
\<forall>x\<^sub>0. a AND NOT (mask x\<^sub>0) \<le> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>0)

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
goal (1 subgoal):
 1. base = base AND NOT (mask (LENGTH('a) - len)) proof (prove)
using this:
mask (LENGTH('a) - len) AND base = 0

goal (1 subgoal):
 1. base = base AND NOT (mask (LENGTH('a) - len)) proof (state)
this:
base = base AND NOT (mask (LENGTH('a) - len))

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
using this:
base = base AND NOT (mask (LENGTH('a) - len))

goal (1 subgoal):
 1. \<forall>x\<^sub>6. (base OR x\<^sub>6) AND NOT (mask (LENGTH('a) - len)) = base OR x\<^sub>6 AND NOT (mask (LENGTH('a) - len)) proof (prove)
using this:
base = base AND NOT (mask (LENGTH('a) - len))
(?x OR ?y) AND ?z = ?x AND ?z OR ?y AND ?z

goal (1 subgoal):
 1. \<forall>x\<^sub>6. (base OR x\<^sub>6) AND NOT (mask (LENGTH('a) - len)) = base OR x\<^sub>6 AND NOT (mask (LENGTH('a) - len)) proof (state)
this:
\<forall>x\<^sub>6. (base OR x\<^sub>6) AND NOT (mask (LENGTH('a) - len)) = base OR x\<^sub>6 AND NOT (mask (LENGTH('a) - len))

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
goal (1 subgoal):
 1. \<forall>x\<^sub>2 x\<^sub>3. a AND NOT (mask x\<^sub>2) \<le> x\<^sub>3 \<or> \<not> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>2) \<le> x\<^sub>3 proof (prove)
using this:
\<forall>x\<^sub>0. a AND NOT (mask x\<^sub>0) \<le> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>0)
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. \<forall>x\<^sub>2 x\<^sub>3. a AND NOT (mask x\<^sub>2) \<le> x\<^sub>3 \<or> \<not> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>2) \<le> x\<^sub>3 proof (state)
this:
\<forall>x\<^sub>2 x\<^sub>3. a AND NOT (mask x\<^sub>2) \<le> x\<^sub>3 \<or> \<not> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>2) \<le> x\<^sub>3

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
goal (1 subgoal):
 1. base = (base OR mask (LENGTH('a) - len)) AND NOT (mask (LENGTH('a) - len)) proof (prove)
using this:
\<forall>x\<^sub>6. (base OR x\<^sub>6) AND NOT (mask (LENGTH('a) - len)) = base OR x\<^sub>6 AND NOT (mask (LENGTH('a) - len))

goal (1 subgoal):
 1. base = (base OR mask (LENGTH('a) - len)) AND NOT (mask (LENGTH('a) - len)) proof (state)
this:
base = (base OR mask (LENGTH('a) - len)) AND NOT (mask (LENGTH('a) - len))

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
using this:
base = (base OR mask (LENGTH('a) - len)) AND NOT (mask (LENGTH('a) - len))

goal (1 subgoal):
 1. base = a AND NOT (mask (LENGTH('a) - len)) proof (prove)
using this:
base = (base OR mask (LENGTH('a) - len)) AND NOT (mask (LENGTH('a) - len))
\<forall>x\<^sub>0. base AND NOT (mask x\<^sub>0) \<le> a AND NOT (mask x\<^sub>0)
base = base AND NOT (mask (LENGTH('a) - len))
\<forall>x\<^sub>2 x\<^sub>3. a AND NOT (mask x\<^sub>2) \<le> x\<^sub>3 \<or> \<not> (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>2) \<le> x\<^sub>3

goal (1 subgoal):
 1. base = a AND NOT (mask (LENGTH('a) - len)) proof (state)
this:
base = a AND NOT (mask (LENGTH('a) - len))

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (prove)
using this:
base = a AND NOT (mask (LENGTH('a) - len))

goal (1 subgoal):
 1. base = NOT (mask (LENGTH('a) - len)) AND a proof (state)
this:
base = NOT (mask (LENGTH('a) - len)) AND a

goal:
No subgoals! proof (state)
this:
base = NOT (mask (LENGTH('a) - len)) AND a

goal:
No subgoals!