theory DetSchedSchedule_AI

lemma cancel_badged_sends_filterM_valid_blocked[wp]:
   "\<lbrace>valid_blocked\<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. valid_blocked\<rbrace>" apply (rule rev_induct[where xs=xs]) apply simp apply (clarsimp simp: filterM_append) apply (wp tcb_sched_action_enqueue_valid_blocked set_thread_state_valid_blocked_except | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<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. valid_blocked\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_blocked\<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. valid_blocked\<rbrace>
 2. \<And>x xs. \<lbrace>valid_blocked\<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. valid_blocked\<rbrace> \<Longrightarrow> \<lbrace>valid_blocked\<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. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrace>valid_blocked\<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. valid_blocked\<rbrace> \<Longrightarrow> \<lbrace>valid_blocked\<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. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrace>valid_blocked\<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. valid_blocked\<rbrace> \<Longrightarrow> \<lbrace>valid_blocked\<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. valid_blocked\<rbrace> proof (prove)
goal:
No subgoals!