theory TcbAcc_AI

lemma sts_reply [wp]:
  "\<lbrace>\<lambda>s. valid_reply_caps s \<and>
       (\<not> awaiting_reply st \<longrightarrow> \<not> has_reply_cap p s)\<rbrace>
   set_thread_state p st \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>" apply (simp only: valid_reply_caps_def imp_conv_disj
                    cte_wp_at_caps_of_state has_reply_cap_def) apply (rule hoare_pre, wp hoare_vcg_all_lift
                            hoare_vcg_disj_lift
                            sts_st_tcb_at_cases) apply clarsimp apply (frule_tac x=x in spec) apply (elim disjE, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_reply_caps s \<and> (st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap p s)\<rbrace> set_thread_state p st \<lbrace>\<lambda>_. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ((\<forall>t. (\<nexists>p cap. caps_of_state s p = Some cap \<and> is_reply_cap_to t cap) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)) \<and> (\<not> st \<noteq> BlockedOnReply \<or> (\<nexists>pa cap. caps_of_state s pa = Some cap \<and> is_reply_cap_to p cap))\<rbrace> set_thread_state p st \<lbrace>\<lambda>_ s. (\<forall>t. (\<nexists>p cap. caps_of_state s p = Some cap \<and> is_reply_cap_to t cap) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<forall>t. (\<nexists>p cap. caps_of_state s p = Some cap \<and> is_reply_cap_to t cap) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)) \<and> (\<not> st \<noteq> BlockedOnReply \<or> (\<nexists>pa cap. caps_of_state s pa = Some cap \<and> is_reply_cap_to p cap)) \<Longrightarrow> (\<forall>x. (\<nexists>p cap. caps_of_state s p = Some cap \<and> is_reply_cap_to x cap) \<or> (p = x \<longrightarrow> awaiting_reply st) \<and> (p \<noteq> x \<longrightarrow> st_tcb_at awaiting_reply x s)) \<and> unique_reply_caps (caps_of_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b cap. \<lbrakk>\<forall>t. (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> \<not> is_reply_cap_to t cap) \<or> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); awaiting_reply st \<or> (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> \<not> is_reply_cap_to p cap); p = x \<and> st \<noteq> BlockedOnReply \<or> p \<noteq> x \<and> \<not> st_tcb_at awaiting_reply x s; caps_of_state s (a, b) = Some cap; is_reply_cap_to x cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x a b cap. \<lbrakk>\<forall>t. (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> \<not> is_reply_cap_to t cap) \<or> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); awaiting_reply st \<or> (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> \<not> is_reply_cap_to p cap); p = x \<and> st \<noteq> BlockedOnReply \<or> p \<noteq> x \<and> \<not> st_tcb_at awaiting_reply x s; caps_of_state s (a, b) = Some cap; is_reply_cap_to x cap; (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> \<not> is_reply_cap_to x cap) \<or> st_tcb_at awaiting_reply x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!