theory ADT_IF

lemma schedule_if_domain_time_nonzero':
  "\<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
   schedule_if tc
   \<lbrace>(\<lambda>_ s. domain_time s > 0)\<rbrace>" apply (simp add: schedule_if_def schedule_def) apply (wpsimp wp: next_domain_domain_time_left
              simp: crunch_simps guarded_switch_to_def switch_to_thread_def
                    choose_thread_def switch_to_idle_thread_def)+ apply (wp hoare_drop_imps) apply (wp hoare_drop_imps) apply wp+ apply (wpsimp simp: choose_thread_def switch_to_idle_thread_def
                        guarded_switch_to_def switch_to_thread_def
                    wp: gts_wp)+ apply (auto simp: word_neq_0_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> schedule_if tc \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace> do y <- do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (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 <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
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 runnable ct_st \<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) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od;
y <- activate_thread;
return tc
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (13 subgoals):
 1. \<And>ct ct_st x2 it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>fastfail \<longrightarrow> highest; runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?R49 ct ct_st (switch_thread x2) x2 () it target_prio ct_prio fastfail cur_dom highest\<rbrace> get_thread_state x2 \<lbrace>\<lambda>ts s. runnable ts \<longrightarrow> (\<exists>y. get_tcb x2 s = Some y) \<longrightarrow> 0 < domain_time s\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B32 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom\<rbrace> gets (is_highest_prio cur_dom target_prio) \<lbrace>\<lambda>highest s. (fastfail \<and> \<not> highest \<longrightarrow> valid_domain_list s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> valid_domain_list s) \<and> (\<not> (runnable ct_st \<and> ct_prio = target_prio) \<longrightarrow> ?R49 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest s))\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B31 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B32 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace>
 4. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B31 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 5. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B29 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B30 ct ct_st x x2 y it target_prio\<rbrace>
 6. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B29 ct ct_st x x2 y it\<rbrace>
 7. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B27 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B28 ct ct_st x x2 y\<rbrace>
 8. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R16 ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B27 ct ct_st x x2\<rbrace>
 9. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R14 ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>y s. 0 < domain_time s\<rbrace>
 10. \<And>ct ct_st. \<lbrace>?B7 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> 0 < domain_time s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R16 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R14 ct ct_st x s)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B32 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom\<rbrace> gets (is_highest_prio cur_dom target_prio) \<lbrace>\<lambda>highest s. (fastfail \<and> \<not> highest \<longrightarrow> valid_domain_list s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> valid_domain_list s) \<and> (\<not> (runnable ct_st \<and> ct_prio = target_prio) \<longrightarrow> 0 < domain_time s))\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B31 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B32 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B31 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 4. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B29 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B30 ct ct_st x x2 y it target_prio\<rbrace>
 5. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B29 ct ct_st x x2 y it\<rbrace>
 6. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B27 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B28 ct ct_st x x2 y\<rbrace>
 7. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R16 ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B27 ct ct_st x x2\<rbrace>
 8. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R14 ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>y s. 0 < domain_time s\<rbrace>
 9. \<And>ct ct_st. \<lbrace>?B7 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> 0 < domain_time s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R16 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R14 ct ct_st x s)\<rbrace>
 10. \<And>ct. \<lbrace>?B6 ct\<rbrace> get_thread_state ct \<lbrace>?B7 ct\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B31 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom s. valid_domain_list s \<and> valid_domain_list s \<and> 0 < domain_time s\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B31 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B29 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B30 ct ct_st x x2 y it target_prio\<rbrace>
 4. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B29 ct ct_st x x2 y it\<rbrace>
 5. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B27 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B28 ct ct_st x x2 y\<rbrace>
 6. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R16 ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B27 ct ct_st x x2\<rbrace>
 7. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R14 ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>y s. 0 < domain_time s\<rbrace>
 8. \<And>ct ct_st. \<lbrace>?B7 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> 0 < domain_time s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R16 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R14 ct ct_st x s)\<rbrace>
 9. \<And>ct. \<lbrace>?B6 ct\<rbrace> get_thread_state ct \<lbrace>?B7 ct\<rbrace>
 10. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B6\<rbrace>
A total of 11 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>ct. \<lbrace>?B6 ct\<rbrace> get_thread_state ct \<lbrace>\<lambda>ct_st s. (scheduler_action s = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> 0 < domain_time s) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (if runnable ct_st then \<lambda>s. valid_domain_list s \<and> valid_domain_list s \<and> 0 < domain_time s else (\<lambda>s. valid_domain_list s \<and> valid_domain_list s \<and> 0 < domain_time s)) s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> (if runnable ct_st then valid_domain_list else valid_domain_list) s)\<rbrace>
 2. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B6\<rbrace>
 3. \<And>s. (valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) s \<Longrightarrow> ?Q1 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> 0 < domain_time s) proof (prove)
goal:
No subgoals!