theory TcbAcc_R

lemma threadSet_obj_at'_really_strongest:
  "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj)
    t' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>" apply (simp add: threadSet_def) apply (rule hoare_wp_splits) apply (rule setObject_tcb_strongest) apply (simp only: imp_conv_disj) apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift) apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"]) apply simp apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift) apply (rule getObject_inv_tcb) apply (rule hoare_strengthen_post [OF getObject_ko_at]) apply simp apply (simp add: objBits_simps') apply (erule obj_at'_weakenE) apply simp apply (cases "t = t'", simp_all) apply (rule OMG_getObject_tcb) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj) t' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. (t = t' \<longrightarrow> P (f obj)) \<and> (t \<noteq> t' \<longrightarrow> P obj)) t' s\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>?B10 tcb\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>
 2. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. (t = t' \<longrightarrow> P (f obj)) \<and> (t \<noteq> t' \<longrightarrow> P obj)) t' s\<rbrace> getObject t \<lbrace>?B10\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. (t = t' \<longrightarrow> P (f obj)) \<and> (t \<noteq> t' \<longrightarrow> P obj)) t' s\<rbrace> getObject t \<lbrace>\<lambda>tcb s. if t = t' then P (f tcb) else obj_at' P t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> tcb_at' t s \<or> obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t' s\<rbrace> getObject t \<lbrace>\<lambda>tcb s. if t = t' then P (f tcb) else obj_at' P t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<not> tcb_at' t s\<rbrace> getObject t \<lbrace>\<lambda>rv s. False\<rbrace>
 2. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<not> tcb_at' t s \<and> tcb_at' t s \<Longrightarrow> False
 2. \<lbrace>\<lambda>s. \<not> tcb_at' t s\<rbrace> getObject t \<lbrace>\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s\<rbrace>
 3. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<not> tcb_at' t s\<rbrace> getObject t \<lbrace>\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s\<rbrace>
 2. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> tcb_at' t s\<rbrace> getObject t \<lbrace>\<lambda>rv s. \<not> tcb_at' t s\<rbrace>
 2. \<lbrace>\<lambda>s. True\<rbrace> getObject t \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 3. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. True\<rbrace> getObject t \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 2. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>q n ko. loadObject t q n ko = loadObject_default t q n ko
 2. \<And>v. 1 < 2 ^ objBits v
 3. \<And>rv s. ko_at' rv t s \<Longrightarrow> tcb_at' t s
 4. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>v. 1 < 2 ^ objBits v
 2. \<And>rv s. ko_at' rv t s \<Longrightarrow> tcb_at' t s
 3. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ko_at' rv t s \<Longrightarrow> tcb_at' t s
 2. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s k. k = rv \<Longrightarrow> True
 2. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>obj. (t \<noteq> t' \<or> P (f obj)) \<and> (\<not> t \<noteq> t' \<or> P obj)) t'\<rbrace> getObject t \<lbrace>\<lambda>rv s. if t = t' then P (f rv) else obj_at' P t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>obj_at' (\<lambda>obj. P (f obj)) t'\<rbrace> getObject t' \<lbrace>\<lambda>rv s. P (f rv)\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> getObject t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> getObject t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal:
No subgoals!