theory Finalise_R

lemma cancelAllSignals_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace>
   cancelAllSignals ntfn
   \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" apply (simp add: cancelAllSignals_def) apply (rule hoare_seq_ext [OF _ get_ntfn_sp']) apply (case_tac "ntfnObj ntfna", simp_all) apply (wp, simp)+ apply (wp cancelAllIPC_mapM_x_valid_inQ_queues)+ apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> cancelAllSignals ntfn \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> do ntfna <- getNotification ntfn;
case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna. \<lbrace>valid_inQ_queues and ko_at' ntfna ntfn\<rbrace> case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfna. ntfnObj ntfna = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>valid_inQ_queues and ko_at' ntfna ntfn\<rbrace> return () \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>
 2. \<And>ntfna x2. ntfnObj ntfna = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>valid_inQ_queues and ko_at' ntfna ntfn\<rbrace> return () \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>
 3. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>valid_inQ_queues and ko_at' ntfna ntfn\<rbrace> do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna);
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3;
rescheduleRequired
od \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?B14 ntfn x3 ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3 \<lbrace>\<lambda>ya. valid_inQ_queues\<rbrace>
 2. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?Q13 ntfna x3\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) \<lbrace>?B14 ntfna x3\<rbrace>
 3. \<And>ntfna x3 s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3; (valid_inQ_queues and ko_at' ntfna ntfn) s\<rbrakk> \<Longrightarrow> ?Q13 ntfna x3 s proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x3 s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3; (valid_inQ_queues and ko_at' ntfna ntfn) s\<rbrakk> \<Longrightarrow> valid_inQ_queues s proof (prove)
goal:
No subgoals!