theory Word_Lemmas

lemma cast_chunk_assemble_id:
  "\<lbrakk>n = LENGTH('a::len); m = LENGTH('b::len); n * 2 = m\<rbrakk> \<Longrightarrow>
  (((ucast ((ucast (x::'b word))::'a word))::'b word) OR (((ucast ((ucast (x >> n))::'a word))::'b word) << n)) = x" apply (subgoal_tac "((ucast ((ucast (x >> n))::'a word))::'b word) = x >> n") apply clarsimp apply (subst and_not_mask[symmetric]) apply (subst ucast_ucast_mask) apply (subst word_ao_dist2[symmetric]) apply clarsimp apply (rule ucast_ucast_len) apply (rule shiftr_less_t2n') apply (subst and_mask_eq_iff_le_mask) apply (simp_all add: mask_eq_decr_exp flip: mult_2_right) apply (metis add_diff_cancel_left' len_gt_0 mult_2_right zero_less_diff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) x) OR (UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) << n) = x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m; UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) = x >> n\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) x) OR (UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) << n) = x
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) = x >> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); LENGTH('a) * 2 = LENGTH('b); UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> LENGTH('a))) = x >> LENGTH('a)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) x) OR (x >> LENGTH('a) << LENGTH('a)) = x
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) = x >> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); LENGTH('a) * 2 = LENGTH('b); UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> LENGTH('a))) = x >> LENGTH('a)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) x) OR x AND NOT (mask LENGTH('a)) = x
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) = x >> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); LENGTH('a) * 2 = LENGTH('b); UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> LENGTH('a))) = x >> LENGTH('a)\<rbrakk> \<Longrightarrow> x AND mask LENGTH('a) OR x AND NOT (mask LENGTH('a)) = x
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) = x >> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); LENGTH('a) * 2 = LENGTH('b); UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> LENGTH('a))) = x >> LENGTH('a)\<rbrakk> \<Longrightarrow> x AND (mask LENGTH('a) OR NOT (mask LENGTH('a))) = x
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) = x >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) (x >> n)) = x >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> x >> n < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> x AND mask (n + LENGTH('a)) = x
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> LENGTH('a) < LENGTH('b) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> x \<le> mask (n + LENGTH('a))
 2. \<lbrakk>n = LENGTH('a); m = LENGTH('b); n * 2 = m\<rbrakk> \<Longrightarrow> LENGTH('a) < LENGTH('b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = LENGTH('a); m = LENGTH('b); LENGTH('a) * 2 = LENGTH('b)\<rbrakk> \<Longrightarrow> LENGTH('a) < LENGTH('b) proof (prove)
goal:
No subgoals!