theory Tcb_AI

lemma unbind_notification_sym_refs[wp]:
  "\<lbrace>\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s\<rbrace>
     unbind_notification a
   \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace>" apply (simp add: unbind_notification_def) apply (rule hoare_seq_ext [OF _ gbn_sp]) apply (case_tac ntfnptr, simp_all) apply (wp, simp) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (wp | wpc | simp)+ apply (rule conjI) apply (fastforce simp: obj_at_def pred_tcb_at_def) apply (rule impI, clarsimp) apply (rule delta_sym_refs, assumption) apply (fastforce simp: obj_at_def pred_tcb_at_def ntfn_q_refs_of_def
                          state_refs_of_def
                    split: if_split_asm) apply (auto simp: valid_obj_def obj_at_def ntfn_bound_refs_def2 symreftype_inverse'
                    ntfn_q_refs_of_def tcb_ntfn_is_bound_def state_refs_of_def
                    tcb_st_refs_of_def tcb_bound_refs_def2
              split: ntfn.splits thread_state.splits if_split_asm
              dest!: sym_refs_bound_tcb_atD refs_in_ntfn_bound_refs
              elim!: obj_at_valid_objsE
              intro!: ntfn_q_refs_no_NTFNBound) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s\<rbrace> unbind_notification a \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s\<rbrace> do ntfnptr <- get_bound_notification a;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn a
od
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr. \<lbrace>bound_tcb_at ((=) ntfnptr) a and (\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s)\<rbrace> case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn a
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>bound_tcb_at ((=) None) a and (\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s)\<rbrace> return () \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace>
 2. \<And>ntfnptr aa. ntfnptr = Some aa \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some aa)) a and (\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s)\<rbrace> do ntfn <- get_notification aa;
y <- set_notification aa (ntfn_set_bound_tcb ntfn None);
set_bound_notification a None
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr aa. ntfnptr = Some aa \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some aa)) a and (\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s)\<rbrace> do ntfn <- get_notification aa;
y <- set_notification aa (ntfn_set_bound_tcb ntfn None);
set_bound_notification a None
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr aa ntfn. ntfnptr = Some aa \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) aa and (bound_tcb_at ((=) (Some aa)) a and (\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s))\<rbrace> do y <- set_notification aa (ntfn_set_bound_tcb ntfn None);
set_bound_notification a None
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr aa ntfn s. \<lbrakk>ntfnptr = Some aa; ko_at (Notification ntfn) aa s \<and> bound_tcb_at ((=) (Some aa)) a s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s\<rbrakk> \<Longrightarrow> (a = aa \<longrightarrow> sym_refs (\<lambda>a. if a = aa then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s a)) \<and> (a \<noteq> aa \<longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if b = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfnptr aa ntfn s. \<lbrakk>ntfnptr = Some aa; ko_at (Notification ntfn) aa s \<and> bound_tcb_at ((=) (Some aa)) a s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s\<rbrakk> \<Longrightarrow> a = aa \<longrightarrow> sym_refs (\<lambda>a. if a = aa then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s a)
 2. \<And>ntfnptr aa ntfn s. \<lbrakk>ntfnptr = Some aa; ko_at (Notification ntfn) aa s \<and> bound_tcb_at ((=) (Some aa)) a s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s\<rbrakk> \<Longrightarrow> a \<noteq> aa \<longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if b = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr aa ntfn s. \<lbrakk>ntfnptr = Some aa; ko_at (Notification ntfn) aa s \<and> bound_tcb_at ((=) (Some aa)) a s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> tcb_at a s\<rbrakk> \<Longrightarrow> a \<noteq> aa \<longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if b = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (1 subgoal):
 1. \<And>aa ntfn s. \<lbrakk>a \<noteq> aa; ko_at (Notification ntfn) aa s; bound_tcb_at ((=) (Some aa)) a s; sym_refs (state_refs_of s); valid_objs s; tcb_at a s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if b = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (2 subgoals):
 1. \<And>aa ntfn s x y tp. \<lbrakk>a \<noteq> aa; ko_at (Notification ntfn) aa s; bound_tcb_at ((=) (Some aa)) a s; sym_refs (state_refs_of s); valid_objs s; tcb_at a s; (y, tp) \<in> (if x = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if x = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s x); (y, tp) \<notin> state_refs_of s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if y = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y)
 2. \<And>aa ntfn s x y tp. \<lbrakk>a \<noteq> aa; ko_at (Notification ntfn) aa s; bound_tcb_at ((=) (Some aa)) a s; sym_refs (state_refs_of s); valid_objs s; tcb_at a s; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if x = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if y = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (1 subgoal):
 1. \<And>aa ntfn s x y tp. \<lbrakk>a \<noteq> aa; ko_at (Notification ntfn) aa s; bound_tcb_at ((=) (Some aa)) a s; sym_refs (state_refs_of s); valid_objs s; tcb_at a s; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if x = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = a then {r \<in> state_refs_of s a. snd r \<noteq> TCBBound} else if y = aa then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal:
No subgoals!