theory Retype_R

lemma createObjects_ret2:
  "\<lbrace>(\<lambda>s. P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits)))
                    [0..<n]))
        and K (n < 2 ^ word_bits \<and> n \<noteq> 0)\<rbrace>
      createObjects y n ko gbits \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_chain) apply (rule hoare_vcg_conj_lift) apply (rule createObjects_ret) apply simp+ apply (rule hoare_vcg_prop) defer apply (clarsimp simp: power_add mult.commute mult.left_commute | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits))) [0..<n])) and K (n < 2 ^ word_bits \<and> n \<noteq> 0)\<rbrace> createObjects y n ko gbits \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. n < 2 ^ word_bits \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits))) [0..<n])\<rbrace> createObjects y n ko gbits \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (3 subgoals):
 1. n < 2 ^ word_bits \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>?P2\<rbrace> createObjects y n ko gbits \<lbrace>?Q2\<rbrace>
 2. \<And>s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits))) [0..<n])\<rbrakk> \<Longrightarrow> ?P2 s
 3. \<And>rv s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; ?Q2 rv s\<rbrakk> \<Longrightarrow> P rv proof (prove)
goal (4 subgoals):
 1. n < 2 ^ word_bits \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>?P6\<rbrace> createObjects y n ko gbits \<lbrace>?Q6\<rbrace>
 2. n < 2 ^ word_bits \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>?P'6\<rbrace> createObjects y n ko gbits \<lbrace>?Q'6\<rbrace>
 3. \<And>s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits))) [0..<n])\<rbrakk> \<Longrightarrow> ?P6 s \<and> ?P'6 s
 4. \<And>rv s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; ?Q6 rv s \<and> ?Q'6 rv s\<rbrakk> \<Longrightarrow> P rv proof (prove)
goal (5 subgoals):
 1. n < 2 ^ word_bits \<and> n \<noteq> 0 \<Longrightarrow> n < 2 ^ word_bits
 2. n < 2 ^ word_bits \<and> n \<noteq> 0 \<Longrightarrow> n \<noteq> 0
 3. n < 2 ^ word_bits \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>?P'6\<rbrace> createObjects y n ko gbits \<lbrace>?Q'6\<rbrace>
 4. \<And>s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits))) [0..<n])\<rbrakk> \<Longrightarrow> True \<and> ?P'6 s
 5. \<And>rv s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; rv = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n] \<and> ?Q'6 rv s\<rbrakk> \<Longrightarrow> P rv proof (prove)
goal (3 subgoals):
 1. n < 2 ^ word_bits \<and> 0 < n \<Longrightarrow> \<lbrace>?P'6\<rbrace> createObjects y n ko gbits \<lbrace>?Q'6\<rbrace>
 2. \<And>s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits))) [0..<n])\<rbrakk> \<Longrightarrow> True \<and> ?P'6 s
 3. \<And>rv s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; rv = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n] \<and> ?Q'6 rv s\<rbrakk> \<Longrightarrow> P rv proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits))) [0..<n])\<rbrakk> \<Longrightarrow> True \<and> ?Q'14
 2. \<And>rv s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; rv = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n] \<and> ?Q'14\<rbrakk> \<Longrightarrow> P rv proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; rv = map (\<lambda>p. ptr_add y (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n] \<and> ?Q'14\<rbrakk> \<Longrightarrow> P rv
 2. \<And>s. \<lbrakk>n < 2 ^ word_bits \<and> n \<noteq> 0; P (map (\<lambda>p. ptr_add y (p * 2 ^ (objBitsKO ko + gbits))) [0..<n])\<rbrakk> \<Longrightarrow> True \<and> ?Q'14 proof (prove)
goal:
No subgoals!