theory Schedule_DR

lemma change_current_domain_and_switch_to_idle_thread_dcorres:
  "dcorres dc \<top> (invs and valid_etcbs)
                (do _ \<leftarrow> change_current_domain;
                    Schedule_D.switch_to_thread None
                 od)
                switch_to_idle_thread" including no_pre apply (clarsimp simp: Schedule_D.switch_to_thread_def switch_to_idle_thread_def) apply (rule dcorres_symb_exec_r) apply (rule corres_guard_imp) apply (rule corres_symb_exec_l) apply (rule_tac R=\<top> in corres_split_noop_rhs) apply (rule dcorres_arch_switch_to_idle_thread_return) apply (clarsimp simp: corres_underlying_def gets_def modify_def get_def put_def do_machine_op_def select_f_def split_def bind_def in_return) apply (clarsimp simp: transform_def transform_current_thread_def transform_asid_table_def) apply assumption apply (wp change_current_domain_same | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (do _ <- change_current_domain;
Schedule_D.switch_to_thread None
od) switch_to_idle_thread proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (do _ <- change_current_domain;
Schedule_D.switch_to_thread None
od) switch_to_idle_thread proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (do _ <- change_current_domain;
modify (cdl_current_thread_update (\<lambda>_. None))
od) (do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (?Q' rv) (do _ <- change_current_domain;
modify (cdl_current_thread_update (\<lambda>_. None))
od) (do y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. rv))
od)
 2. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv. dcorres dc (?Q4 rv) (?Q'4 rv) (do _ <- change_current_domain;
modify (cdl_current_thread_update (\<lambda>_. None))
od) (do y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. rv))
od)
 2. \<And>rv s. True \<Longrightarrow> ?Q4 rv s
 3. \<And>rv s. ?Q' rv s \<Longrightarrow> ?Q'4 rv s
 4. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv uu_. dcorres dc (?Q8 rv uu_) (?Q'4 rv) (modify (cdl_current_thread_update (\<lambda>_. None))) (do y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. rv))
od)
 2. \<And>rv s. ?Q4 rv s \<Longrightarrow> \<lbrace>(=) s\<rbrace> change_current_domain \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv. \<lbrace>?Q4 rv\<rbrace> change_current_domain \<lbrace>?Q8 rv\<rbrace>
 4. \<And>rv. False \<Longrightarrow> no_fail (?Q4 rv) change_current_domain
 5. \<And>rv s. True \<Longrightarrow> ?Q4 rv s
 6. \<And>rv s. ?Q' rv s \<Longrightarrow> ?Q'4 rv s
 7. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>rv uu_. dcorres dc (?P13 rv uu_) (?P'15 rv) (return ()) arch_switch_to_idle_thread
 2. \<And>rv uu_. dcorres dc (\<lambda>_. True) (?R'13 rv uu_) (modify (cdl_current_thread_update (\<lambda>_. None))) (modify (cur_thread_update (\<lambda>_. rv)))
 3. \<And>rv uu_. \<lbrace>?Q'16 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x. ?R'13 rv uu_\<rbrace>
 4. \<And>rv s. ?Q4 rv s \<Longrightarrow> \<lbrace>(=) s\<rbrace> change_current_domain \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv. \<lbrace>?Q4 rv\<rbrace> change_current_domain \<lbrace>\<lambda>uu_. ?P13 rv uu_ and (\<lambda>a. True)\<rbrace>
 6. \<And>rv. False \<Longrightarrow> no_fail (?Q4 rv) change_current_domain
 7. \<And>rv s. True \<Longrightarrow> ?Q4 rv s
 8. \<And>rv s. ?Q' rv s \<Longrightarrow> (?P'15 rv and ?Q'16 rv) s
 9. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv uu_. dcorres dc (\<lambda>_. True) (?R'13 rv uu_) (modify (cdl_current_thread_update (\<lambda>_. None))) (modify (cur_thread_update (\<lambda>_. rv)))
 2. \<And>rv uu_. \<lbrace>?Q'16 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x. ?R'13 rv uu_\<rbrace>
 3. \<And>rv s. ?Q4 rv s \<Longrightarrow> \<lbrace>(=) s\<rbrace> change_current_domain \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv. \<lbrace>?Q4 rv\<rbrace> change_current_domain \<lbrace>\<lambda>_. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 5. \<And>rv. False \<Longrightarrow> no_fail (?Q4 rv) change_current_domain
 6. \<And>rv s. True \<Longrightarrow> ?Q4 rv s
 7. \<And>rv s. ?Q' rv s \<Longrightarrow> ((\<lambda>_. True) and ?Q'16 rv) s
 8. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv b. ?R'13 rv () b \<Longrightarrow> transform (b\<lparr>cur_thread := rv\<rparr>) = transform b\<lparr>cdl_current_thread := None\<rparr>
 2. \<And>rv uu_. \<lbrace>?Q'16 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x. ?R'13 rv uu_\<rbrace>
 3. \<And>rv s. ?Q4 rv s \<Longrightarrow> \<lbrace>(=) s\<rbrace> change_current_domain \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv. \<lbrace>?Q4 rv\<rbrace> change_current_domain \<lbrace>\<lambda>_. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 5. \<And>rv. False \<Longrightarrow> no_fail (?Q4 rv) change_current_domain
 6. \<And>rv s. True \<Longrightarrow> ?Q4 rv s
 7. \<And>rv s. ?Q' rv s \<Longrightarrow> ((\<lambda>_. True) and ?Q'16 rv) s
 8. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv b. ?R'13 rv () b \<Longrightarrow> rv = idle_thread b
 2. \<And>rv uu_. \<lbrace>?Q'16 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x. ?R'13 rv uu_\<rbrace>
 3. \<And>rv s. ?Q4 rv s \<Longrightarrow> \<lbrace>(=) s\<rbrace> change_current_domain \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv. \<lbrace>?Q4 rv\<rbrace> change_current_domain \<lbrace>\<lambda>_. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 5. \<And>rv. False \<Longrightarrow> no_fail (?Q4 rv) change_current_domain
 6. \<And>rv s. True \<Longrightarrow> ?Q4 rv s
 7. \<And>rv s. ?Q' rv s \<Longrightarrow> ((\<lambda>_. True) and ?Q'16 rv) s
 8. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv _. \<lbrace>?Q'16 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x a. rv = idle_thread a\<rbrace>
 2. \<And>rv s. ?Q4 rv s \<Longrightarrow> \<lbrace>(=) s\<rbrace> change_current_domain \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv. \<lbrace>?Q4 rv\<rbrace> change_current_domain \<lbrace>\<lambda>_. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 4. \<And>rv. False \<Longrightarrow> no_fail (?Q4 rv) change_current_domain
 5. \<And>rv s. True \<Longrightarrow> ?Q4 rv s
 6. \<And>rv s. ?Q' rv s \<Longrightarrow> ((\<lambda>_. True) and ?Q'16 rv) s
 7. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!