theory More_Word_Operations

lemma aligned_mask_range_cases:
  "\<lbrakk> is_aligned (p :: 'a :: len word) n; is_aligned (p' :: 'a :: len word) n' \<rbrakk>
   \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {} \<or>
       mask_range p n \<subseteq> mask_range p' n' \<or>
       mask_range p n \<supseteq> mask_range p' n'" apply (simp add: mask_range_to_bl) apply (rule Meson.disj_comm, rule disjCI) apply auto apply (subgoal_tac "(\<exists>n''. LENGTH('a) - n = (LENGTH('a) - n') + n'')
                    \<or> (\<exists>n''. LENGTH('a) - n' = (LENGTH('a) - n) + n'')") apply (fastforce simp: take_add) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> mask_range p n \<inter> mask_range p' n' = {} \<or> mask_range p n \<subseteq> mask_range p' n' \<or> mask_range p' n' \<subseteq> mask_range p n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} \<inter> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} = {} \<or> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} \<subseteq> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<or> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<subseteq> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'; {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} \<inter> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<noteq> {}\<rbrakk> \<Longrightarrow> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} \<subseteq> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<or> {x. take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p')} \<subseteq> {x. take (LENGTH('a) - n) (to_bl x) = take (LENGTH('a) - n) (to_bl p)} proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>is_aligned p n; is_aligned p' n'; take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xa) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n) (to_bl x) \<noteq> take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xa) \<noteq> take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xb) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xb) = take (LENGTH('a) - n') (to_bl p')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>is_aligned p n; is_aligned p' n'; take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xa) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n) (to_bl x) \<noteq> take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xa) \<noteq> take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xb) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xb) = take (LENGTH('a) - n') (to_bl p'); (\<exists>n''. LENGTH('a) - n = LENGTH('a) - n' + n'') \<or> (\<exists>n''. LENGTH('a) - n' = LENGTH('a) - n + n'')\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa xb. \<lbrakk>is_aligned p n; is_aligned p' n'; take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xa) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n) (to_bl x) \<noteq> take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xa) \<noteq> take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xb) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xb) = take (LENGTH('a) - n') (to_bl p')\<rbrakk> \<Longrightarrow> (\<exists>n''. LENGTH('a) - n = LENGTH('a) - n' + n'') \<or> (\<exists>n''. LENGTH('a) - n' = LENGTH('a) - n + n'') proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>is_aligned p n; is_aligned p' n'; take (LENGTH('a) - n') (to_bl x) = take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xa) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n) (to_bl x) \<noteq> take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xa) \<noteq> take (LENGTH('a) - n') (to_bl p'); take (LENGTH('a) - n) (to_bl xb) = take (LENGTH('a) - n) (to_bl p); take (LENGTH('a) - n') (to_bl xb) = take (LENGTH('a) - n') (to_bl p')\<rbrakk> \<Longrightarrow> (\<exists>n''. LENGTH('a) - n = LENGTH('a) - n' + n'') \<or> (\<exists>n''. LENGTH('a) - n' = LENGTH('a) - n + n'') proof (prove)
goal:
No subgoals!