theory Word_Lemmas_Internal

lemma mask_split_aligned_neg:
  fixes x :: "'a::len word"
  fixes p :: "'b::len word"
  assumes len: "a + len_of TYPE('a) \<le> len_of TYPE('b)"
               "m = a + len_of TYPE('a)"
  assumes x: "x \<noteq> ucast (p && mask m >> a)"
  shows "(p && ~~ mask m) + (ucast x << a) = p \<Longrightarrow> False" apply (subst (asm) word_plus_and_or_coroll) apply word_eqI using len apply linarith apply (insert x) apply (erule notE) apply word_eqI subgoal for n using len apply (clarsimp) apply (drule_tac x="n + a" in spec) by (clarsimp simp: add.commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p && ~~ mask m) + (UCAST('a \<rightarrow> 'b) x << a) = p \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. (p && ~~ mask m) && (UCAST('a \<rightarrow> 'b) x << a) = 0
 2. p && ~~ mask m || (UCAST('a \<rightarrow> 'b) x << a) = p \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n - a < LENGTH('b); a \<le> n; m \<le> n; n < LENGTH('b); p !! n; n - a < LENGTH('a); x !! (n - a)\<rbrakk> \<Longrightarrow> False
 2. p && ~~ mask m || (UCAST('a \<rightarrow> 'b) x << a) = p \<Longrightarrow> False proof (prove)
using this:
a + LENGTH('a) \<le> LENGTH('b)
m = a + LENGTH('a)

goal (2 subgoals):
 1. \<And>n. \<lbrakk>n - a < LENGTH('b); a \<le> n; m \<le> n; n < LENGTH('b); p !! n; n - a < LENGTH('a); x !! (n - a)\<rbrakk> \<Longrightarrow> False
 2. p && ~~ mask m || (UCAST('a \<rightarrow> 'b) x << a) = p \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. p && ~~ mask m || (UCAST('a \<rightarrow> 'b) x << a) = p \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p && ~~ mask m || (UCAST('a \<rightarrow> 'b) x << a) = p; x \<noteq> UCAST('b \<rightarrow> 'a) (p && mask m >> a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. p && ~~ mask m || (UCAST('a \<rightarrow> 'b) x << a) = p \<Longrightarrow> x = UCAST('b \<rightarrow> 'a) (p && mask m >> a) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n. (p !! n \<and> n < LENGTH('b) \<and> (LENGTH('b) \<le> n \<or> m \<le> n) \<or> a \<le> n \<and> n < LENGTH('b) \<and> n - a < LENGTH('b) \<and> x !! (n - a)) = p !! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x !! n = (p !! (a + n) \<and> a + n < LENGTH('b) \<and> a + n < m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. (p !! n \<and> n < LENGTH('b) \<and> (LENGTH('b) \<le> n \<or> m \<le> n) \<or> a \<le> n \<and> n < LENGTH('b) \<and> n - a < LENGTH('b) \<and> x !! (n - a)) = p !! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x !! n = (p !! (a + n) \<and> a + n < LENGTH('b) \<and> a + n < m) proof (prove)
using this:
a + LENGTH('a) \<le> LENGTH('b)
m = a + LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>\<forall>n. (p !! n \<and> n < LENGTH('b) \<and> (LENGTH('b) \<le> n \<or> m \<le> n) \<or> a \<le> n \<and> n < LENGTH('b) \<and> n - a < LENGTH('b) \<and> x !! (n - a)) = p !! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x !! n = (p !! (a + n) \<and> a + n < LENGTH('b) \<and> a + n < m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. (p !! n \<and> n < LENGTH('b) \<and> (LENGTH('b) \<le> n \<or> a + LENGTH('a) \<le> n) \<or> a \<le> n \<and> n < LENGTH('b) \<and> n - a < LENGTH('b) \<and> x !! (n - a)) = p !! n; n < LENGTH('a); a + LENGTH('a) \<le> LENGTH('b); m = a + LENGTH('a)\<rbrakk> \<Longrightarrow> x !! n = p !! (a + n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); a + LENGTH('a) \<le> LENGTH('b); m = a + LENGTH('a); (p !! (n + a) \<and> n + a < LENGTH('b) \<and> (LENGTH('b) \<le> n + a \<or> a + LENGTH('a) \<le> n + a) \<or> a \<le> n + a \<and> n + a < LENGTH('b) \<and> n + a - a < LENGTH('b) \<and> x !! (n + a - a)) = p !! (n + a)\<rbrakk> \<Longrightarrow> x !! n = p !! (a + n) proof (prove)
goal:
No subgoals!