theory TcbAcc_R

lemma lift_neg_pred_tcb_at':
  assumes typat: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>"
      and sttcb: "\<And>S p. \<lbrace>pred_tcb_at' proj S p\<rbrace> f \<lbrace>\<lambda>_. pred_tcb_at' proj S p\<rbrace>"
    shows "\<lbrace>\<lambda>s. P (pred_tcb_at' proj S p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (pred_tcb_at' proj S p s)\<rbrace>" apply (rule_tac P=P in P_bool_lift) apply (rule sttcb) apply (simp add: pred_tcb_at'_def not_obj_at') apply (wp hoare_convert_imp) apply (rule typat) prefer 2 apply assumption apply (rule hoare_chain [OF sttcb]) apply (fastforce simp: pred_tcb_at'_def comp_def) apply (clarsimp simp: pred_tcb_at'_def elim!: obj_at'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (pred_tcb_at' proj S p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (pred_tcb_at' proj S p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>pred_tcb_at' proj S p\<rbrace> f \<lbrace>\<lambda>r. pred_tcb_at' proj S p\<rbrace>
 2. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj S p s\<rbrace> f \<lbrace>\<lambda>r s. \<not> pred_tcb_at' proj S p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> pred_tcb_at' proj S p s\<rbrace> f \<lbrace>\<lambda>r s. \<not> pred_tcb_at' proj S p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. typ_at' TCBT p s \<longrightarrow> obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p s\<rbrace> f \<lbrace>\<lambda>r s. typ_at' TCBT p s \<longrightarrow> obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> ?P3 s\<rbrace> f \<lbrace>\<lambda>r s. \<not> typ_at' TCBT p s\<rbrace>
 2. \<lbrace>?R3\<rbrace> f \<lbrace>\<lambda>rv. obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p\<rbrace>
 3. \<And>s. typ_at' TCBT p s \<longrightarrow> obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p s \<Longrightarrow> ?P3 s \<longrightarrow> ?R3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R3\<rbrace> f \<lbrace>\<lambda>rv. obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p\<rbrace>
 2. \<And>s. typ_at' TCBT p s \<longrightarrow> obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p s \<Longrightarrow> typ_at' TCBT p s \<longrightarrow> ?R3 s proof (prove)
goal (2 subgoals):
 1. \<And>s. typ_at' TCBT p s \<longrightarrow> obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p s \<Longrightarrow> typ_at' TCBT p s \<longrightarrow> ?R3 s
 2. \<lbrace>?R3\<rbrace> f \<lbrace>\<lambda>rv. obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p\<rbrace> f \<lbrace>\<lambda>rv. obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p s \<Longrightarrow> pred_tcb_at' proj ?S6 ?p6 s
 2. \<And>rv s. pred_tcb_at' proj ?S6 ?p6 s \<Longrightarrow> obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. pred_tcb_at' proj (\<lambda>a. \<not> S a) p s \<Longrightarrow> obj_at' (Not \<circ> (\<lambda>ko. S (proj (tcb_to_itcb' ko)))) p s proof (prove)
goal:
No subgoals!