theory DetSchedSchedule_AI

lemma cancel_badged_sends_filterM_weak_valid_sched_action[wp]:
   "\<lbrace>weak_valid_sched_action\<rbrace>
      filterM (\<lambda>t. do st \<leftarrow> get_thread_state t;
                      if blocking_ipc_badge st = badge
                      then do y \<leftarrow> set_thread_state t Structures_A.thread_state.Restart;
                              y \<leftarrow> (tcb_sched_action tcb_sched_enqueue t);
                              return False
                      od
                      else return True
                   od) xs
   \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace>" apply (rule rev_induct[where xs=xs]) apply simp apply (clarsimp simp: filterM_append) apply (wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) xs \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>weak_valid_sched_action\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) [] \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace>
 2. \<And>x xs. \<lbrace>weak_valid_sched_action\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) xs \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace> \<Longrightarrow> \<lbrace>weak_valid_sched_action\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) (xs @ [x]) \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrace>weak_valid_sched_action\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) xs \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace> \<Longrightarrow> \<lbrace>weak_valid_sched_action\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) (xs @ [x]) \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrace>weak_valid_sched_action\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) xs \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace> \<Longrightarrow> \<lbrace>weak_valid_sched_action\<rbrace> do xs' <- filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) xs;
b <- do st <- get_thread_state x;
if blocking_ipc_badge st = badge then do y <- set_thread_state x Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (xs' @ (if b then [x] else []))
od \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace> proof (prove)
goal:
No subgoals!