theory CSpace_AI

lemma set_untyped_cap_as_full_has_reply_cap_neg:
  "\<lbrace>\<lambda>s. \<not> (has_reply_cap t s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. \<not> (has_reply_cap t s)\<rbrace>" apply (clarsimp simp:has_reply_cap_def is_reply_cap_to_def) apply (wp hoare_vcg_all_lift) apply (wp set_untyped_cap_as_full_cte_wp_at_neg) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule_tac x = x in spec) apply (drule_tac x = xa in spec) apply (clarsimp simp:masked_as_full_def free_index_update_def is_cap_simps split:cap.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> has_reply_cap t s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<forall>a b. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrace>?P2 a b\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s\<rbrace>
 2. \<And>s. (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s) \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x xa. ?P2 x xa s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s) \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x xa. ((x, xa) \<noteq> src \<and> \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (x, xa) s \<or> (x, xa) = src \<and> \<not> cte_wp_at (\<lambda>a. \<exists>rights. masked_as_full a cap = ReplyCap t False rights) src s) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa rights. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); caps_of_state s (x, xa) = Some src_cap; src = (x, xa); masked_as_full src_cap cap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa rights. \<lbrakk>caps_of_state s (x, xa) = Some src_cap; src = (x, xa); masked_as_full src_cap cap = ReplyCap t False rights; \<forall>b cap. caps_of_state s (x, b) = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa rights. \<lbrakk>caps_of_state s (x, xa) = Some src_cap; src = (x, xa); masked_as_full src_cap cap = ReplyCap t False rights; \<forall>cap. caps_of_state s (x, xa) = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!