theory DetSchedSchedule_AI

lemma unbind_maybe_notification_sym_refs[wp]:
  "\<lbrace>\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s\<rbrace>
     unbind_maybe_notification a
   \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace>" apply (simp add: unbind_maybe_notification_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp | wpc | clarsimp)+ apply (rule conjI) apply clarsimp apply (rule delta_sym_refs, assumption) apply (clarsimp split: if_split_asm) apply (frule ko_at_state_refs_ofD, simp) apply (clarsimp split: if_split_asm) apply (frule ko_at_state_refs_ofD, simp) apply (fastforce simp: symreftype_inverse' dest!: refs_in_ntfn_q_refs) apply clarsimp apply (rule delta_sym_refs, assumption) apply (clarsimp split: if_split_asm, frule ko_at_state_refs_ofD, simp)+ apply (frule_tac P="(=) (Some a)" in ntfn_bound_tcb_at, simp_all add: obj_at_def)[1] apply (fastforce simp: ntfn_q_refs_no_NTFNBound obj_at_def is_tcb state_refs_of_def
                          tcb_st_refs_of_no_NTFNBound tcb_bound_refs_def2 tcb_ntfn_is_bound_def
                          tcb_st_refs_no_TCBBound
                   dest!: pred_tcb_at_tcb_at bound_tcb_at_state_refs_ofD) apply (frule ko_at_state_refs_ofD, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s\<rbrace> unbind_maybe_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\<rbrace> do ntfn <- get_notification a;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) a and (\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s)\<rbrace> case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q8 ntfn\<rbrace> case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of s)\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) a and (\<lambda>s. sym_refs (state_refs_of s) \<and> valid_objs s)) s \<Longrightarrow> ?Q8 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> (x = a \<longrightarrow> ntfn_bound_tcb ntfn = Some a \<longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s b)) \<and> (x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x = a \<longrightarrow> ntfn_bound_tcb ntfn = Some a \<longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s b)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; ntfn_bound_tcb ntfn = Some a\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s b)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; ntfn_bound_tcb ntfn = Some a; (y, tp) \<in> (if x = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} 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> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s y)
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; ntfn_bound_tcb ntfn = Some a; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s y)
 3. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s y tp. \<lbrakk>(y, tp) \<notin> state_refs_of s a; ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; ntfn_bound_tcb ntfn = Some a; (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn); tp \<noteq> TCBBound\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<and> symreftype tp \<noteq> TCBBound) \<and> (y \<noteq> a \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s y)
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; ntfn_bound_tcb ntfn = Some a; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s y)
 3. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; ntfn_bound_tcb ntfn = Some a; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = a then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s y)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; ntfn_bound_tcb ntfn = Some a; (y, tp) \<in> state_refs_of s a; (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> tp = TCBBound\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> a \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; ntfn_bound_tcb ntfn = Some a; y = a \<and> tp = NTFNBound \<or> (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn); (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> tp = TCBBound; state_refs_of s a = insert (a, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn))\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> a \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s\<rbrakk> \<Longrightarrow> x \<noteq> a \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; x \<noteq> a; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if b = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s b) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; x \<noteq> a; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> (if xa = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if xa = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s xa); (y, tp) \<notin> state_refs_of s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if y = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y)
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; x \<noteq> a; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if xa = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if y = a then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; x \<noteq> a; ntfn_bound_tcb ntfn = Some x; (y, TCBBound) \<in> state_refs_of s x; state_refs_of s a = insert (x, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn))\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (x, NTFNBound) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of s x) \<and> (y \<noteq> x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of s y))
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; x \<noteq> a; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s a; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = x \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y. \<lbrakk>kheap s a = Some (Notification ntfn); sym_refs (state_refs_of s); valid_objs s; x \<noteq> a; ntfn_bound_tcb ntfn = Some x; (y, TCBBound) \<in> state_refs_of s x; state_refs_of s a = insert (x, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)); bound_tcb_at ((=) (Some a)) x s\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (x, NTFNBound) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of s x) \<and> (y \<noteq> x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of s y))
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; x \<noteq> a; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s a; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = x \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) a s; sym_refs (state_refs_of s); valid_objs s; x \<noteq> a; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s a; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> a \<longrightarrow> (y = x \<longrightarrow> (a, symreftype tp) \<in> state_refs_of s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (a, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal:
No subgoals!