theory KHeap_R

lemma set_ntfn_iflive'[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s
      \<and> (live' (KONotification v) \<longrightarrow> ex_nonz_cap_to' p s)\<rbrace>
     setNotification p v
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: setNotification_def) apply (wp setObject_iflive'[where P="\<top>"]) apply simp apply (simp add: objBits_simps) apply (simp add: objBits_simps') apply (clarsimp simp: updateObject_default_def in_monad projectKOs) apply (clarsimp simp: updateObject_default_def
                         projectKOs bind_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> (live' (KONotification v) \<longrightarrow> ex_nonz_cap_to' p s)\<rbrace> setNotification p v \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfnBoundTCB v = Some y) \<longrightarrow> ex_nonz_cap_to' p s) \<and> ((\<exists>ts. ntfnObj v = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' p s)\<rbrace> setObject p v \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ko s x y n. updateObject v ko p y n s = updateObject_default v ko p y n s
 2. \<And>x. objBits x = ?n4
 3. 1 < 2 ^ ?n4
 4. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) p x n s); True; lookupAround2 p (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 5. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 6. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfnBoundTCB v = Some y) \<longrightarrow> ex_nonz_cap_to' p s) \<and> ((\<exists>ts. ntfnObj v = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (5 subgoals):
 1. \<And>x. objBits x = ?n4
 2. 1 < 2 ^ ?n4
 3. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) p x n s); True; lookupAround2 p (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 4. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 5. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfnBoundTCB v = Some y) \<longrightarrow> ex_nonz_cap_to' p s) \<and> ((\<exists>ts. ntfnObj v = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (4 subgoals):
 1. 1 < 2 ^ ntfnSizeBits
 2. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) p x n s); True; lookupAround2 p (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 3. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 4. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfnBoundTCB v = Some y) \<longrightarrow> ex_nonz_cap_to' p s) \<and> ((\<exists>ts. ntfnObj v = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (3 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) p x n s); True; lookupAround2 p (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 2. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 3. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfnBoundTCB v = Some y) \<longrightarrow> ex_nonz_cap_to' p s) \<and> ((\<exists>ts. ntfnObj v = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 2. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfnBoundTCB v = Some y) \<longrightarrow> ex_nonz_cap_to' p s) \<and> ((\<exists>ts. ntfnObj v = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<and> ((\<exists>y. ntfnBoundTCB v = Some y) \<longrightarrow> ex_nonz_cap_to' p s) \<and> ((\<exists>ts. ntfnObj v = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal:
No subgoals!