theory ADT_IF_Refine

lemma schedule_if_domain_time_left:
  "\<lbrace>\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
   schedule_if tc
   \<lbrace>\<lambda>rv s. 0 < domain_time s\<rbrace>" unfolding schedule_if_def schedule_det_ext_ext_def schedule_switch_thread_fastfail_def supply ethread_get_wp[wp del] supply if_split[split del] supply nonzero_gt_zero[simp] gt_zero_nonzero[simp] apply (rule hoare_pre) apply (wpsimp simp: ethread_get_when_def wp: gts_wp
          | wp hoare_drop_imp[where f="ethread_get a b" for a b]
               hoare_drop_imp[where f="tcb_sched_action a b" for a b])+ apply (auto split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> schedule_if tc \<lbrace>\<lambda>rv s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> do do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- if ct \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od;
activate_thread;
return tc
od \<lbrace>\<lambda>rv s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> do do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- if ct \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od;
activate_thread;
return tc
od \<lbrace>\<lambda>rv s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> do do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- if ct \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od;
activate_thread;
return tc
od \<lbrace>\<lambda>rv s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> do do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- if ct \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od;
activate_thread;
return tc
od \<lbrace>\<lambda>rv s. 0 < domain_time s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- if ct \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od;
activate_thread;
return tc
od \<lbrace>\<lambda>rv s. 0 < domain_time s\<rbrace>
 2. \<And>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s st. \<lbrakk>valid_domain_list s; domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread; st_tcb_at ((=) st) (cur_thread s) s\<rbrakk> \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> (runnable st \<longrightarrow> 0 < domain_time s) \<and> (cur_thread s = idle_thread s \<longrightarrow> 0 < domain_time s)) \<and> ((\<exists>x. scheduler_action s = switch_thread x) \<longrightarrow> (if runnable st then \<lambda>a. (valid_domain_list a \<and> 0 < domain_time a) \<and> valid_domain_list a \<and> 0 < domain_time a else (\<lambda>sa. (cur_thread s \<noteq> idle_thread sa \<longrightarrow> valid_domain_list sa \<and> valid_domain_list sa \<and> 0 < domain_time sa) \<and> valid_domain_list sa \<and> valid_domain_list sa \<and> 0 < domain_time sa)) s) proof (prove)
goal:
No subgoals!