theory CNodeInv_AI

lemma cap_swap_reply_masters:
  "\<lbrace>valid_reply_masters and K(\<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')\<rbrace>
   cap_swap c p c' p' \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" apply (simp add: valid_reply_masters_def is_master_reply_cap_to_def cte_wp_at_caps_of_state) apply (rule hoare_pre) apply (simp only: imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift cap_swap_caps_of_state
             cap_swap_typ_at tcb_at_typ_at) apply (simp add: is_cap_simps) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and K (\<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>_. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2) and (\<lambda>y. \<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>_ s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q5\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>_ s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2) and (\<lambda>y. \<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')) s \<Longrightarrow> ?Q5 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q5\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>_ s. \<forall>a b t. (\<nexists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<or> a = t \<and> b = tcb_cnode_index 2\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2) and (\<lambda>y. \<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')) s \<Longrightarrow> ?Q5 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2) and (\<lambda>y. \<not> is_master_reply_cap c \<and> \<not> is_master_reply_cap c')) s \<Longrightarrow> \<forall>x xa xb. (\<nexists>cap. ((caps_of_state s)(p \<mapsto> c', p' \<mapsto> c)) (x, xa) = Some cap \<and> (\<exists>rights. cap = ReplyCap xb True rights)) \<or> x = xb \<and> xa = tcb_cnode_index 2 proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2) \<and> (\<forall>x R. c \<noteq> ReplyCap x True R) \<and> (\<forall>x R. c' \<noteq> ReplyCap x True R) \<Longrightarrow> \<forall>x xa. (x, xa) \<noteq> p \<longrightarrow> (x, xa) \<noteq> p' \<longrightarrow> (\<forall>xb. (\<forall>cap. caps_of_state s (x, xa) = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap xb True rights)) \<or> x = xb \<and> xa = tcb_cnode_index 2) proof (prove)
goal:
No subgoals!