theory Ipc_C

lemma transferCapsToSlots_local_slots:
  assumes weak: "\<And>c cap. P (maskedAsFull c cap) = P c"
  shows
  "\<lbrace> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot and K (slot \<notin> set destSlots) \<rbrace>
    transferCapsToSlots ep rcvBuffer x caps destSlots mi
   \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>" proof (rule hoare_gen_asm, induct caps arbitrary: x mi destSlots) case Nil show ?case by simp next case (Cons cp cps) show ?case using Cons.prems by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak cong: if_cong) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot and K (slot \<notin> set destSlots)\<rbrace> transferCapsToSlots ep rcvBuffer x caps destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>x mi destSlots. slot \<notin> set destSlots \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x [] destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>
 2. \<And>x1 caps x mi destSlots. \<lbrakk>\<And>x mi destSlots. slot \<notin> set destSlots \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x caps destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>; slot \<notin> set destSlots\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x (x1 # caps) destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (state)
this:
slot \<notin> set destSlots

goal (2 subgoals):
 1. \<And>x mi destSlots. slot \<notin> set destSlots \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x [] destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>
 2. \<And>x1 caps x mi destSlots. \<lbrakk>\<And>x mi destSlots. slot \<notin> set destSlots \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x caps destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>; slot \<notin> set destSlots\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x (x1 # caps) destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x [] destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (state)
this:
\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x [] destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>

goal (1 subgoal):
 1. \<And>x1 caps x mi destSlots. \<lbrakk>\<And>x mi destSlots. slot \<notin> set destSlots \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x caps destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>; slot \<notin> set destSlots\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x (x1 # caps) destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>x1 caps x mi destSlots. \<lbrakk>\<And>x mi destSlots. slot \<notin> set destSlots \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x caps destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>; slot \<notin> set destSlots\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x (x1 # caps) destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (state)
this:
slot \<notin> set ?destSlots1 \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer ?x1 cps ?destSlots1 ?mi1 \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>
slot \<notin> set destSlots

goal (1 subgoal):
 1. \<And>x1 caps x mi destSlots. \<lbrakk>\<And>x mi destSlots. slot \<notin> set destSlots \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x caps destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>; slot \<notin> set destSlots\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x (x1 # caps) destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x (cp # cps) destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
using this:
slot \<notin> set destSlots

goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x (cp # cps) destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (state)
this:
\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> transferCapsToSlots ep rcvBuffer x (cp # cps) destSlots mi \<lbrace>\<lambda>tag'. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>

goal:
No subgoals!