theory Untyped_R

lemma map_ensure_empty':
  "\<lbrace>\<lambda>s. (\<forall>slot \<in> set slots. cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) slot s) \<longrightarrow> P s\<rbrace>
     mapME_x ensureEmptySlot slots
   \<lbrace>\<lambda>rv s. P s \<rbrace>,-" apply (induct slots arbitrary: P) apply (simp add: mapME_x_def sequenceE_x_def) apply wp apply (simp add: mapME_x_def sequenceE_x_def) apply (rule_tac Q="\<lambda>rv s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s"
    in validE_R_sp) apply (simp add: ensureEmptySlot_def unlessE_def) apply (wp getCTE_wp') apply (clarsimp elim!: cte_wp_at_weakenE') apply (erule meta_allE) apply (erule hoare_post_imp_R) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> mapME_x ensureEmptySlot slots \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set []. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> mapME_x ensureEmptySlot [] \<lbrace>\<lambda>rv. P\<rbrace>, -
 2. \<And>a slots P. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> mapME_x ensureEmptySlot slots \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>slot\<in>set (a # slots). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> mapME_x ensureEmptySlot (a # slots) \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> returnOk () \<lbrace>\<lambda>rv. P\<rbrace>, -
 2. \<And>a slots P. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> mapME_x ensureEmptySlot slots \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>slot\<in>set (a # slots). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> mapME_x ensureEmptySlot (a # slots) \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> mapME_x ensureEmptySlot slots \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>slot\<in>set (a # slots). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> mapME_x ensureEmptySlot (a # slots) \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) a s \<and> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> doE _ <- ensureEmptySlot a;
foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ())
odE \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a slots P. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) a s \<and> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> ensureEmptySlot a \<lbrace>\<lambda>rv s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace>, -
 2. \<And>a slots P x. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a slots P. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) a s \<and> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> doE cte <- liftE (getCTE a);
if cteCap cte = capability.NullCap then returnOk () else throwError Fault_H.syscall_error.DeleteFirst
odE \<lbrace>\<lambda>rv s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace>, -
 2. \<And>a slots P x. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a slots P s. \<lbrakk>\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, -; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) a s \<and> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) a s \<longrightarrow> (cteCap cte = capability.NullCap \<longrightarrow> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> True)
 2. \<And>a slots P x. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P x. (\<And>P. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P x. \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> ?x40 a slots P x s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. ?x40 a slots P x\<rbrace>, - \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s) \<longrightarrow> P s\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensureEmptySlot slots) (returnOk ()) \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P x rv s. P s \<Longrightarrow> P s proof (prove)
goal:
No subgoals!