theory TcbAcc_R

lemma threadSet_pred_tcb_no_state:
  assumes "\<And>tcb. proj (tcb_to_itcb' (f tcb)) = proj (tcb_to_itcb' tcb)"
  shows   "\<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace>" proof - have pos: "\<And>P' t' t.
            \<lbrace>pred_tcb_at' proj P' t'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. pred_tcb_at' proj P' t'\<rbrace>" apply (simp add: pred_tcb_at'_def) apply (wp threadSet_obj_at'_strongish) apply clarsimp apply (erule obj_at'_weakenE) apply (insert assms) apply clarsimp done show ?thesis apply (rule_tac P=P in P_bool_lift) apply (rule pos) apply (rule_tac Q="\<lambda>_ s. \<not> tcb_at' t' s \<or> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s"
             in hoare_post_imp) apply (erule disjE) apply (clarsimp dest!: pred_tcb_at') apply (clarsimp) apply (frule_tac P=P' and Q="\<lambda>tcb. \<not> P' tcb" in pred_tcb_at_conj') apply (clarsimp)+ apply (wp hoare_convert_imp) apply (simp add: typ_at_tcb' [symmetric]) apply (wp pos)+ apply (clarsimp simp: pred_tcb_at'_def not_obj_at' elim!: obj_at'_weakenE) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P' t' t. \<lbrace>pred_tcb_at' proj P' t'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. pred_tcb_at' proj P' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P' t' t. \<lbrace>obj_at' (\<lambda>ko. P' (proj (tcb_to_itcb' ko))) t'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P' (proj (tcb_to_itcb' ko))) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P' t' t s. obj_at' (\<lambda>ko. P' (proj (tcb_to_itcb' ko))) t' s \<Longrightarrow> obj_at' (\<lambda>obj. if t = t' then P' (proj (tcb_to_itcb' (f obj))) else P' (proj (tcb_to_itcb' obj))) t' s proof (prove)
goal (1 subgoal):
 1. \<And>P' t' t s. obj_at' (\<lambda>ko. P' (proj (tcb_to_itcb' ko))) t' s \<Longrightarrow> obj_at' (\<lambda>obj. (t = t' \<longrightarrow> P' (proj (tcb_to_itcb' (f obj)))) \<and> (t \<noteq> t' \<longrightarrow> P' (proj (tcb_to_itcb' obj)))) t' s proof (prove)
goal (1 subgoal):
 1. \<And>P' t' t s k. P' (proj (tcb_to_itcb' k)) \<Longrightarrow> (t = t' \<longrightarrow> P' (proj (tcb_to_itcb' (f k)))) \<and> (t \<noteq> t' \<longrightarrow> P' (proj (tcb_to_itcb' k))) proof (prove)
goal (1 subgoal):
 1. \<And>P' t' t s k. \<lbrakk>P' (proj (tcb_to_itcb' k)); \<And>tcb. proj (tcb_to_itcb' (f tcb)) = proj (tcb_to_itcb' tcb)\<rbrakk> \<Longrightarrow> (t = t' \<longrightarrow> P' (proj (tcb_to_itcb' (f k)))) \<and> (t \<noteq> t' \<longrightarrow> P' (proj (tcb_to_itcb' k))) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pred_tcb_at' proj ?P' ?t'\<rbrace> threadSet f ?t \<lbrace>\<lambda>rv. pred_tcb_at' proj ?P' ?t'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>pred_tcb_at' proj P' t'\<rbrace> threadSet f t \<lbrace>\<lambda>r. pred_tcb_at' proj P' t'\<rbrace>
 2. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P' t' s\<rbrace> threadSet f t \<lbrace>\<lambda>r s. \<not> pred_tcb_at' proj P' t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P' t' s\<rbrace> threadSet f t \<lbrace>\<lambda>r s. \<not> pred_tcb_at' proj P' t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<not> tcb_at' t' s \<or> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s \<Longrightarrow> \<not> pred_tcb_at' proj P' t' s
 2. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P' t' s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. \<not> tcb_at' t' s \<or> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<not> tcb_at' t' s \<Longrightarrow> \<not> pred_tcb_at' proj P' t' s
 2. \<And>rv s. pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s \<Longrightarrow> \<not> pred_tcb_at' proj P' t' s
 3. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P' t' s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. \<not> tcb_at' t' s \<or> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s \<Longrightarrow> \<not> pred_tcb_at' proj P' t' s
 2. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P' t' s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. \<not> tcb_at' t' s \<or> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s; pred_tcb_at' proj P' t' s\<rbrakk> \<Longrightarrow> False
 2. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P' t' s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. \<not> tcb_at' t' s \<or> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s; pred_tcb_at' proj P' t' s\<rbrakk> \<Longrightarrow> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s
 2. \<And>s. \<lbrakk>pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s; pred_tcb_at' proj P' t' s; pred_tcb_at' proj (\<lambda>a. P' a \<and> \<not> P' a) t' s\<rbrakk> \<Longrightarrow> False
 3. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P' t' s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. \<not> tcb_at' t' s \<or> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj P' t' s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. tcb_at' t' s \<longrightarrow> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> ?P18 s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. \<not> tcb_at' t' s\<rbrace>
 2. \<lbrace>?R18\<rbrace> threadSet f t \<lbrace>\<lambda>rv. pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t'\<rbrace>
 3. \<And>s. \<not> pred_tcb_at' proj P' t' s \<Longrightarrow> ?P18 s \<longrightarrow> ?R18 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> ?P18 s\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. \<not> typ_at' TCBT t' s\<rbrace>
 2. \<lbrace>?R18\<rbrace> threadSet f t \<lbrace>\<lambda>rv. pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t'\<rbrace>
 3. \<And>s. \<not> pred_tcb_at' proj P' t' s \<Longrightarrow> ?P18 s \<longrightarrow> ?R18 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> pred_tcb_at' proj P' t' s \<Longrightarrow> typ_at' TCBT t' s \<longrightarrow> pred_tcb_at' proj (\<lambda>tcb. \<not> P' tcb) t' s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace>

goal:
No subgoals!