theory Finalise_R

lemma unbindMaybeNotification_obj_at'_bound:
  "\<lbrace>\<top>\<rbrace>
     unbindMaybeNotification r
   \<lbrace>\<lambda>_ s. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r s\<rbrace>" apply (simp add: unbindMaybeNotification_def) apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (rule hoare_pre) apply (wp obj_at_setObject2
        | wpc
        | simp add: setBoundNotification_def threadSet_def updateObject_default_def in_monad projectKOs)+ apply (simp add: setNotification_def obj_at'_real_def cong: valid_cong) apply (wp setObject_ko_wp_at, (simp add: objBits_simps')+) apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> unbindMaybeNotification r \<lbrace>\<lambda>_. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ntfn <- getNotification r;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification r (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od \<lbrace>\<lambda>_. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>(\<lambda>_. True) and ko_at' ntfn r\<rbrace> case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification r (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od \<lbrace>\<lambda>_. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q8 ntfn\<rbrace> case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification r (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od \<lbrace>\<lambda>_. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r\<rbrace>
 2. \<And>ntfn s. ((\<lambda>_. True) and ko_at' ntfn r) s \<Longrightarrow> ?Q8 ntfn s proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x2. ntfnBoundTCB ntfn = Some x2 \<Longrightarrow> \<lbrace>?R20 ntfn x2\<rbrace> setNotification r (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>a. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r\<rbrace>
 2. \<And>ntfn s. ((\<lambda>_. True) and ko_at' ntfn r) s \<Longrightarrow> (ntfnBoundTCB ntfn = None \<longrightarrow> obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r s) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x2. ntfnBoundTCB ntfn = Some x2 \<Longrightarrow> \<lbrace>?R20 ntfn x2\<rbrace> setObject r (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>a. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> ntfnBoundTCB obj = None) r\<rbrace>
 2. \<And>ntfn s. ((\<lambda>_. True) and ko_at' ntfn r) s \<Longrightarrow> (ntfnBoundTCB ntfn = None \<longrightarrow> obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r s) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> ?R20 ntfn x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. ko_at' ntfn r s \<Longrightarrow> (ntfnBoundTCB ntfn = None \<longrightarrow> obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r s) \<and> ((\<exists>x. ntfnBoundTCB ntfn = Some x) \<longrightarrow> ntfn_at' r s \<longrightarrow> ko_wp_at' (\<lambda>y. \<exists>obj. projectKO_opt (KONotification (ntfnBoundTCB_update (\<lambda>_. None) ntfn)) = Some obj \<and> ntfnBoundTCB obj = None) r s) proof (prove)
goal:
No subgoals!