theory KHeap_DR

lemma branch_map_simp2:
  " \<lbrakk>length cref \<le> 32; 0 < nata;nata + length list < length cref; list \<le> cref\<rbrakk>
  \<Longrightarrow> unat ((((of_bl cref)::word32) >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))" apply (subgoal_tac "take nata (drop (length list) cref) \<le> drop (length list) cref") apply (frule_tac iffD2[OF guard_mask_shift,rotated,where cref1="drop (length list) cref" and cref'1="of_bl cref::word32"]) defer apply clarsimp apply (subgoal_tac "nata\<le> length cref - length list") apply (drule min.absorb2[where b = nata]) apply simp apply (clarsimp simp: add.commute) apply (simp only: unat_def) apply (rule iffD2[OF eq_nat_nat_iff]) apply (simp add:bl_to_bin_ge0 )+ apply (subst bl_to_bin_rep_F[symmetric]) apply (subst to_bl_bin[symmetric]) apply (rule arg_cong[where f = bl_to_bin]) apply (simp add:word_rep_drop)+ apply (clarsimp simp:List.take_drop prefix_def less_eq_list_def) apply (rule_tac x = "(drop nata zs)" in exI) apply simp apply (simp add:word_rep_drop) apply (rule take_drop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; length (take nata (drop (length list) cref)) \<le> length (drop (length list) cref) \<and> (of_bl cref >> length (drop (length list) cref) - length (take nata (drop (length list) cref))) && mask (length (take nata (drop (length list) cref))) = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; length (take nata (drop (length list) cref)) \<le> length (drop (length list) cref) \<and> (of_bl cref >> length (drop (length list) cref) - length (take nata (drop (length list) cref))) && mask (length (take nata (drop (length list) cref))) = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list; min (length cref - length list) nata = nata\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> unat (of_bl (take nata (drop (length list) cref))) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> nat (uint (of_bl (take nata (drop (length list) cref)))) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (6 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> 0 \<le> uint (of_bl (take nata (drop (length list) cref)))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> 0 \<le> bl_to_bin (take nata (drop (length list) cref))
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> uint (of_bl (take nata (drop (length list) cref))) = bl_to_bin (take nata (drop (length list) cref))
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 5. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 6. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> uint (of_bl (take nata (drop (length list) cref))) = bl_to_bin (take nata (drop (length list) cref))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> uint (of_bl (take nata (drop (length list) cref))) = bl_to_bin (replicate ?n44 False @ take nata (drop (length list) cref))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> bl_to_bin (to_bl (of_bl (take nata (drop (length list) cref)))) = bl_to_bin (replicate ?n44 False @ take nata (drop (length list) cref))
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; (of_bl cref >> length cref - (nata + length list)) && mask nata = of_bl (take nata (drop (length list) cref)); nata \<le> length cref - length list\<rbrakk> \<Longrightarrow> to_bl (of_bl (take nata (drop (length list) cref))) = replicate ?n44 False @ take nata (drop (length list) cref)
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref; nata \<le> length cref - length list; (of_bl cref >> length cref - (length list + nata)) && mask nata = of_bl (take nata (drop (length list) cref))\<rbrakk> \<Longrightarrow> nata \<le> length cref - length list
 3. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 4. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> take nata (drop (length list) cref) \<le> drop (length list) cref
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (2 subgoals):
 1. \<And>zs. \<lbrakk>length list + length zs \<le> 32; 0 < nata; nata < length zs; cref = list @ zs\<rbrakk> \<Longrightarrow> \<exists>zsa. zs = take nata zs @ zsa
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (2 subgoals):
 1. \<And>zs. \<lbrakk>length list + length zs \<le> 32; 0 < nata; nata < length zs; cref = list @ zs\<rbrakk> \<Longrightarrow> zs = take nata zs @ drop nata zs
 2. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> to_bl (of_bl cref) = ?xs1 @ drop (length list) cref proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cref \<le> 32; 0 < nata; nata + length list < length cref; list \<le> cref; take nata (drop (length list) cref) \<le> drop (length list) cref\<rbrakk> \<Longrightarrow> replicate (32 - length cref) False @ cref = ?xs1 @ drop (length list) cref proof (prove)
goal:
No subgoals!