theory Scheduler_IF

lemma switch_to_idle_thread_midstrength_reads_respects_scheduler[wp]:
  "midstrength_reads_respects_scheduler aag l (invs and pas_refined aag)
     (switch_to_idle_thread >>= (\<lambda>_. set_scheduler_action resume_cur_thread))" apply (simp add: switch_to_idle_thread_def) apply (rule equiv_valid_guard_imp) apply (simp add: bind_assoc double_gets_drop_regets) apply (rule bind_ev_general) apply (rule bind_ev_general) apply (rule store_cur_thread_midstrength_reads_respects) apply (rule_tac P="\<top>" and P'="\<top>" in equiv_valid_inv_unobservable) apply (rule hoare_pre) apply (rule scheduler_equiv_lift'[where P=\<top>]) apply (wp globals_equiv_scheduler_inv silc_dom_lift | simp)+ apply (wp midstrength_scheduler_affects_equiv_unobservable
                | simp | (rule hoare_pre, wps))+ apply (wp cur_thread_update_not_subject_reads_respects_scheduler arch_stit_invs
               | assumption | simp | fastforce)+ apply (clarsimp simp: scheduler_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag) (do _ <- switch_to_idle_thread;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag) (do _ <- do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (2 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q (do _ <- do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od;
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q (do x <- gets idle_thread;
xa <- arch_switch_to_idle_thread;
_ <- modify (cur_thread_update (\<lambda>_. x));
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid (scheduler_equiv aag) ?B3 (scheduler_affects_equiv aag l) (?Q3 rv) (do x <- arch_switch_to_idle_thread;
_ <- modify (cur_thread_update (\<lambda>_. rv));
set_scheduler_action resume_cur_thread
od)
 2. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B3 ?P'3 (gets idle_thread)
 3. \<lbrace>?P''3\<rbrace> gets idle_thread \<lbrace>?Q3\<rbrace>
 4. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. equiv_valid (scheduler_equiv aag) (?B7 rv) (scheduler_affects_equiv aag l) (?Q7 rv rva) (do _ <- modify (cur_thread_update (\<lambda>_. rv));
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv. equiv_valid (scheduler_equiv aag) ?B3 (?B7 rv) (?P'7 rv) arch_switch_to_idle_thread
 3. \<And>rv. \<lbrace>?P''7 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>?Q7 rv\<rbrace>
 4. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B3 ?P'3 (gets idle_thread)
 5. \<lbrace>?P''3\<rbrace> gets idle_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (5 subgoals):
 1. \<And>rv. equiv_valid (scheduler_equiv aag) ?B3 (midstrength_scheduler_affects_equiv aag l) (?P'7 rv) arch_switch_to_idle_thread
 2. \<And>rv. \<lbrace>?P''7 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rva. invs and (\<lambda>s. rv = idle_thread s)\<rbrace>
 3. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B3 ?P'3 (gets idle_thread)
 4. \<lbrace>?P''3\<rbrace> gets idle_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 5. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (9 subgoals):
 1. \<And>rv st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>rv st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>rv. \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 4. \<And>rv. \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
 5. \<And>rv s. ?P'7 rv s \<Longrightarrow> True \<and> True
 6. \<And>rv. \<lbrace>?P''7 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rva. invs and (\<lambda>s. rv = idle_thread s)\<rbrace>
 7. equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?P'3 (gets idle_thread)
 8. \<lbrace>?P''3\<rbrace> gets idle_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 9. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (10 subgoals):
 1. \<And>rv st. \<lbrace>?Q21 rv st\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>rv st s. ((\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st) s \<Longrightarrow> ?Q21 rv st s
 3. \<And>rv st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>rv. \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 5. \<And>rv. \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
 6. \<And>rv s. ?P'7 rv s \<Longrightarrow> True \<and> True
 7. \<And>rv. \<lbrace>?P''7 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rva. invs and (\<lambda>s. rv = idle_thread s)\<rbrace>
 8. equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?P'3 (gets idle_thread)
 9. \<lbrace>?P''3\<rbrace> gets idle_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 10. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (15 subgoals):
 1. \<And>rv st sta. \<lbrace>(\<lambda>_. True) and globals_equiv_scheduler sta\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>rv st Q. \<lbrace>(\<lambda>_. True) and (\<lambda>s. Q (cur_domain s))\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>rv st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>rv st Q. \<lbrace>(\<lambda>_. True) and (\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s))\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>rv st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>rv st sta. \<lbrace>(\<lambda>_. True) and silc_dom_equiv aag sta\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>rv st s. ((\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st) s \<Longrightarrow> ((\<lambda>_. True) and scheduler_equiv aag st) s
 8. \<And>rv st. \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>rv. \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 10. \<And>rv. \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
A total of 15 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>st. \<lbrace>scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>rv. \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 3. \<And>rv. \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
 4. \<And>rv s. ?P'7 rv s \<Longrightarrow> True \<and> True
 5. \<And>rv. \<lbrace>?P''7 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rva. invs and (\<lambda>s. rv = idle_thread s)\<rbrace>
 6. equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?P'3 (gets idle_thread)
 7. \<lbrace>?P''3\<rbrace> gets idle_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 8. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (7 subgoals):
 1. \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 2. \<And>rv. \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
 3. \<And>rv s. ?P'7 rv s \<Longrightarrow> True \<and> True
 4. \<And>rv. \<lbrace>?P''7 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rva. invs and (\<lambda>s. rv = idle_thread s)\<rbrace>
 5. equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?P'3 (gets idle_thread)
 6. \<lbrace>?P''3\<rbrace> gets idle_thread \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 7. \<And>s. (invs and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> pas_refined aag s \<Longrightarrow> \<forall>s t. scheduler_equiv aag s t \<and> midstrength_scheduler_affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t proof (prove)
goal:
No subgoals!