theory Word_Lemmas_Internal

lemma mask_split_aligned:
  assumes len: "m \<le> a + len_of TYPE('a)"
  assumes align: "is_aligned p a"
  shows "(p && ~~ mask m) + (ucast ((ucast (p && mask m >> a))::'a::len word) << a) = p" apply (insert align[simplified is_aligned_nth]) apply (subst word_plus_and_or_coroll; word_eqI) apply (rule iffI) apply (erule disjE; clarsimp) apply (case_tac "n < m"; case_tac "n < a") using len by auto

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

goal (4 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n<a. \<not> p !! n; n < LENGTH('b); p !! n; n < m; n < a\<rbrakk> \<Longrightarrow> p !! n \<and> m \<le> n \<or> a \<le> n \<and> n - a < LENGTH('b) \<and> n - a < LENGTH('a) \<and> p !! (a + (n - a)) \<and> a + (n - a) < LENGTH('b) \<and> a + (n - a) < m
 2. \<And>n. \<lbrakk>\<forall>n<a. \<not> p !! n; n < LENGTH('b); p !! n; n < m; \<not> n < a\<rbrakk> \<Longrightarrow> p !! n \<and> m \<le> n \<or> a \<le> n \<and> n - a < LENGTH('b) \<and> n - a < LENGTH('a) \<and> p !! (a + (n - a)) \<and> a + (n - a) < LENGTH('b) \<and> a + (n - a) < m
 3. \<And>n. \<lbrakk>\<forall>n<a. \<not> p !! n; n < LENGTH('b); p !! n; \<not> n < m; n < a\<rbrakk> \<Longrightarrow> p !! n \<and> m \<le> n \<or> a \<le> n \<and> n - a < LENGTH('b) \<and> n - a < LENGTH('a) \<and> p !! (a + (n - a)) \<and> a + (n - a) < LENGTH('b) \<and> a + (n - a) < m
 4. \<And>n. \<lbrakk>\<forall>n<a. \<not> p !! n; n < LENGTH('b); p !! n; \<not> n < m; \<not> n < a\<rbrakk> \<Longrightarrow> p !! n \<and> m \<le> n \<or> a \<le> n \<and> n - a < LENGTH('b) \<and> n - a < LENGTH('a) \<and> p !! (a + (n - a)) \<and> a + (n - a) < LENGTH('b) \<and> a + (n - a) < m