theory IpcCancel_R

lemma cancelAllSignals_valid_objs'[wp]:
  "\<lbrace>valid_objs'\<rbrace> cancelAllSignals ntfn \<lbrace>\<lambda>rv. valid_objs'\<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, simp) apply (rename_tac list) apply (rule_tac Q="\<lambda>rv s. valid_objs' s \<and> (\<forall>x\<in>set list. tcb_at' x s)"
                  in hoare_post_imp) apply (simp add: valid_ntfn'_def) apply (simp add: Ball_def) apply (wp setSchedulerAction_valid_objs' mapM_x_wp'
            sts_valid_objs' hoare_vcg_all_lift hoare_vcg_const_imp_lift
       | simp)+ apply (simp add: valid_tcb_state'_def) apply (wp set_ntfn_valid_objs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) apply clarsimp apply (frule(1) ko_at_valid_objs') apply (simp add: projectKOs) apply (clarsimp simp: valid_obj'_def valid_ntfn'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> cancelAllSignals ntfn \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<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_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna. \<lbrace>valid_objs' 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_objs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfna. ntfnObj ntfna = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>valid_objs' and ko_at' ntfna ntfn\<rbrace> return () \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>ntfna x2. ntfnObj ntfna = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>valid_objs' and ko_at' ntfna ntfn\<rbrace> return () \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 3. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>valid_objs' 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_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfna x2. ntfnObj ntfna = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>valid_objs' and ko_at' ntfna ntfn\<rbrace> return () \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>valid_objs' 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_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>valid_objs' 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_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna list. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<Longrightarrow> \<lbrace>valid_objs' 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) list;
rescheduleRequired
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn list rv s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn list; valid_objs' s \<and> (\<forall>x\<in>set list. tcb_at' x s)\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>ntfna list. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<Longrightarrow> \<lbrace>valid_objs' 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) list;
rescheduleRequired
od \<lbrace>\<lambda>rv s. valid_objs' s \<and> (\<forall>x\<in>set list. tcb_at' x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna list. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<Longrightarrow> \<lbrace>valid_objs' 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) list;
rescheduleRequired
od \<lbrace>\<lambda>rv s. valid_objs' s \<and> (\<forall>x\<in>set list. tcb_at' x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna list. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<Longrightarrow> \<lbrace>valid_objs' 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) list;
rescheduleRequired
od \<lbrace>\<lambda>rv s. valid_objs' s \<and> (\<forall>x. x \<in> set list \<longrightarrow> tcb_at' x s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn list x s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn list; x \<in> set list; valid_objs' s \<and> (\<forall>x. x \<in> set list \<longrightarrow> tcb_at' x s)\<rbrakk> \<Longrightarrow> valid_tcb_state' Structures_H.thread_state.Restart s
 2. \<And>ntfna list. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<Longrightarrow> \<lbrace>?Q15 ntfna list\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) \<lbrace>\<lambda>y s. valid_objs' s \<and> (\<forall>x. x \<in> set list \<longrightarrow> tcb_at' x s)\<rbrace>
 3. \<And>ntfna list s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list; (valid_objs' and ko_at' ntfna ntfn) s\<rbrakk> \<Longrightarrow> ?Q15 ntfna list s proof (prove)
goal (2 subgoals):
 1. \<And>ntfna list. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<Longrightarrow> \<lbrace>?Q15 ntfna list\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) \<lbrace>\<lambda>y s. valid_objs' s \<and> (\<forall>x. x \<in> set list \<longrightarrow> tcb_at' x s)\<rbrace>
 2. \<And>ntfna list s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list; (valid_objs' and ko_at' ntfna ntfn) s\<rbrakk> \<Longrightarrow> ?Q15 ntfna list s proof (prove)
goal (1 subgoal):
 1. \<And>ntfna list s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list; (valid_objs' and ko_at' ntfna ntfn) s\<rbrakk> \<Longrightarrow> (valid_objs' and valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna)) s \<and> (\<forall>x. x \<in> set list \<longrightarrow> tcb_at' x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna list s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list; valid_objs' s; ko_at' ntfna ntfn s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) s \<and> (\<forall>x. x \<in> set list \<longrightarrow> tcb_at' x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfna list s ko. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list; valid_objs' s; ko_at' ntfna ntfn s; projectKO_opt ko = Some ntfna\<rbrakk> \<Longrightarrow> injectKO ntfna = ko
 2. \<And>ntfna list s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list; valid_objs' s; ko_at' ntfna ntfn s; valid_obj' (injectKO ntfna) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) s \<and> (\<forall>x. x \<in> set list \<longrightarrow> tcb_at' x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna list s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list; valid_objs' s; ko_at' ntfna ntfn s; valid_obj' (injectKO ntfna) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) s \<and> (\<forall>x. x \<in> set list \<longrightarrow> tcb_at' x s) proof (prove)
goal:
No subgoals!