theory ArchFinalise_AI

lemma pd_shifting_again5:
  "\<lbrakk>is_aligned (pd :: word32) pd_bits;(sl::word32) = ucast (ae::12 word)\<rbrakk> \<Longrightarrow>
  ucast ((sl << 2) + pd && mask pd_bits >> 2) = ae" apply simp apply (frule_tac pd=pd and ae=ae in pd_shifting_again4) apply simp apply (cut_tac x="ucast ae :: word32" and n=2 in shiftl_shiftr_id) apply ((simp add: word_bits_def less_le_trans[OF ucast_less])+)[2] apply (simp add:ucast_bl) apply (subst word_rep_drop) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; sl = UCAST(12 \<rightarrow> 32) ae\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((sl << 2) + pd && mask pd_bits >> 2) = ae proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; sl = UCAST(12 \<rightarrow> 32) ae\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits >> 2) = ae proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; sl = UCAST(12 \<rightarrow> 32) ae; (UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits = UCAST(12 \<rightarrow> 32) ae << 2\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits >> 2) = ae proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; sl = UCAST(12 \<rightarrow> 32) ae; (UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits = UCAST(12 \<rightarrow> 32) ae << 2\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) ae << 2 >> 2) = ae proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; sl = UCAST(12 \<rightarrow> 32) ae; (UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits = UCAST(12 \<rightarrow> 32) ae << 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<lbrakk>is_aligned pd pd_bits; sl = UCAST(12 \<rightarrow> 32) ae; (UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits = UCAST(12 \<rightarrow> 32) ae << 2\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) ae < 2 ^ (LENGTH(32) - 2)
 3. \<lbrakk>is_aligned pd pd_bits; sl = UCAST(12 \<rightarrow> 32) ae; (UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits = UCAST(12 \<rightarrow> 32) ae << 2; UCAST(12 \<rightarrow> 32) ae << 2 >> 2 = UCAST(12 \<rightarrow> 32) ae\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) ae << 2 >> 2) = ae proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; sl = UCAST(12 \<rightarrow> 32) ae; (UCAST(12 \<rightarrow> 32) ae << 2) + pd && mask pd_bits = UCAST(12 \<rightarrow> 32) ae << 2; UCAST(12 \<rightarrow> 32) ae << 2 >> 2 = UCAST(12 \<rightarrow> 32) ae\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) ae << 2 >> 2) = ae proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; sl = of_bl (to_bl ae); (of_bl (to_bl ae) << 2) + pd && mask pd_bits = of_bl (to_bl ae) << 2; of_bl (to_bl ae) << 2 >> 2 = of_bl (to_bl ae)\<rbrakk> \<Longrightarrow> of_bl (to_bl (of_bl (to_bl ae))) = ae proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; sl = of_bl (to_bl ae); (of_bl (to_bl ae) << 2) + pd && mask pd_bits = of_bl (to_bl ae) << 2; of_bl (to_bl ae) << 2 >> 2 = of_bl (to_bl ae)\<rbrakk> \<Longrightarrow> of_bl (replicate (LENGTH(32) - length (to_bl ae)) False @ drop (length (to_bl ae) - LENGTH(32)) (to_bl ae)) = ae proof (prove)
goal:
No subgoals!