theory KHeap_DR

lemma branch_map_simp1:
  "\<lbrakk>length ref \<le> 32;length ref = radix_bits + length guard\<rbrakk> \<Longrightarrow>
  ( (((of_bl ref)::word32) >> radix_bits) && mask (length guard) = (of_bl guard)) = (guard \<le> ref)" apply (rule iffI) apply (subst(asm) shiftr_bl_of) apply simp apply (rule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD1[OF guard_mask_shift]) apply (simp add: word_rep_drop) apply (subst shiftr_bl_of) apply simp+ apply (drule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD2[OF guard_mask_shift,rotated]) apply (simp add: word_rep_drop)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard\<rbrakk> \<Longrightarrow> ((of_bl ref >> radix_bits) && mask (length guard) = of_bl guard) = (guard \<le> ref) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> guard \<le> ref
 2. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard\<rbrakk> \<Longrightarrow> length ref \<le> LENGTH(32)
 2. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; of_bl (take (length ref - radix_bits) ref) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> guard \<le> ref
 3. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; of_bl (take (length ref - radix_bits) ref) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> guard \<le> ref
 2. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; of_bl (take (length ref - radix_bits) ref) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> to_bl (of_bl ref) = ?xs7 @ ref
 2. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; of_bl (take (length ref - radix_bits) ref) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> length guard \<le> length ref \<and> (of_bl ref >> length ref - length guard) && mask (length guard) = of_bl guard
 3. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; of_bl (take (length ref - radix_bits) ref) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> length guard \<le> length ref \<and> (of_bl ref >> length ref - length guard) && mask (length guard) = of_bl guard
 2. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; of_bl (take (length ref - radix_bits) ref) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> length ref \<le> LENGTH(32)
 2. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; of_bl (take (length ref - radix_bits) ref) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> length guard \<le> length ref \<and> of_bl (take (length ref - (length ref - length guard)) ref) && mask (length guard) = of_bl guard
 3. \<lbrakk>length ref \<le> 32; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (1 subgoal):
 1. \<lbrakk>radix_bits + length guard \<le> 32; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (2 subgoals):
 1. \<lbrakk>radix_bits + length guard \<le> 32; length ref = radix_bits + length guard\<rbrakk> \<Longrightarrow> to_bl (of_bl ref) = ?xs12 @ ref
 2. \<lbrakk>radix_bits + length guard \<le> 32; length ref = radix_bits + length guard; length guard \<le> length ref \<and> (of_bl ref >> length ref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal:
No subgoals!