theory Invariants_AI

lemma valid_reply_caps_st_cte_lift:
  assumes ctes: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
  assumes tcbs: "\<And>P t. \<lbrace>st_tcb_at P t\<rbrace> f \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>"
  shows "\<lbrace>valid_reply_caps\<rbrace> f \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>" unfolding valid_reply_caps_def apply (rule hoare_vcg_conj_lift) apply (rule hoare_vcg_all_lift) apply (subst disj_not1 [THEN sym])+ apply (rule hoare_vcg_disj_lift) apply (rule has_reply_cap_cte_lift) apply (rule ctes) apply (rule tcbs) apply (rule ctes) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> f \<lbrace>\<lambda>_. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s\<rbrace>
 2. \<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrace>\<lambda>s. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s\<rbrace> f \<lbrace>\<lambda>rv s. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s\<rbrace>
 2. \<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrace>\<lambda>s. \<not> has_reply_cap t s \<or> st_tcb_at awaiting_reply t s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s \<or> st_tcb_at awaiting_reply t s\<rbrace>
 2. \<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>\<lambda>s. \<not> has_reply_cap t s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace>
 2. \<And>t. \<lbrace>st_tcb_at awaiting_reply t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at awaiting_reply t\<rbrace>
 3. \<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 2. \<And>t. \<lbrace>st_tcb_at awaiting_reply t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at awaiting_reply t\<rbrace>
 3. \<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrace>st_tcb_at awaiting_reply t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at awaiting_reply t\<rbrace>
 2. \<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!