theory ArchUntyped_AI

lemma delete_objects_rewrite[Untyped_AI_assms]:
  "\<lbrakk> word_size_bits \<le> sz; sz\<le> word_bits; ptr && ~~ mask sz = ptr \<rbrakk>
    \<Longrightarrow> delete_objects ptr sz =
          do y \<leftarrow> modify (clear_um {ptr + of_nat k |k. k < 2 ^ sz});
             modify (detype {ptr && ~~ mask sz..ptr + 2 ^ sz - 1})
          od" apply (clarsimp simp: delete_objects_def freeMemory_def word_size_def word_size_bits_def) apply (subgoal_tac "is_aligned (ptr &&~~ mask sz) sz") apply (subst mapM_storeWord_clear_um[simplified word_size_def word_size_bits_def]) apply (simp) apply simp apply (simp add:range_cover_def) apply clarsimp apply (rule is_aligned_neg_mask) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_size_bits \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> delete_objects ptr sz = do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr && ~~ mask sz..ptr + 2 ^ sz - 1})
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> do y <- do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ sz - 1]);
modify (detype {ptr..ptr + 2 ^ sz - 1})
od = do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> do y <- do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ sz - 1]);
modify (detype {ptr..ptr + 2 ^ sz - 1})
od = do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od
 2. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask sz) sz proof (prove)
goal (5 subgoals):
 1. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> is_aligned ptr sz
 2. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> 2 \<le> sz
 3. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> sz \<le> word_bits
 4. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od = do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od
 5. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask sz) sz proof (prove)
goal (4 subgoals):
 1. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> 2 \<le> sz
 2. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> sz \<le> word_bits
 3. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od = do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od
 4. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask sz) sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> sz \<le> word_bits
 2. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od = do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od
 3. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask sz) sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr; is_aligned (ptr && ~~ mask sz) sz\<rbrakk> \<Longrightarrow> do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od = do y <- modify (clear_um {ptr + word_of_nat k |k. k < 2 ^ sz});
modify (detype {ptr..ptr + 2 ^ sz - 1})
od
 2. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask sz) sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask sz) sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 \<le> sz; sz \<le> word_bits; ptr && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> sz \<le> sz proof (prove)
goal:
No subgoals!