theory Ipc_DR

lemma possible_switch_to_dcorres:
  "dcorres dc P P' (return ()) (possible_switch_to t)" apply (clarsimp simp: possible_switch_to_def cong: if_cong) apply (rule dcorres_symb_exec_r)+ apply (rule corres_guard1_imp, rule corres_if_rhs) apply (rule tcb_sched_action_dcorres[THEN corres_trivial]) apply (rule corres_if_rhs) apply (rule dcorres_symb_exec_r)+ apply (rule tcb_sched_action_dcorres[THEN corres_trivial]) apply (wp set_scheduler_action_transform_inv tcb_sched_action_transform_inv
                 | simp add: reschedule_required_def
                 | wpc
                 | rule set_scheduler_action_dcorres[THEN corres_trivial])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (possible_switch_to t) proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (do cur_dom <- gets cur_domain;
target_dom <- ethread_get tcb_domain t;
action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue t else if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)
od) proof (prove)
goal (7 subgoals):
 1. \<And>rv rva rvb. dcorres dc P (?Q'14 rv rva rvb) (return ()) (if rva \<noteq> rv then tcb_sched_action tcb_sched_enqueue t else if rvb \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t))
 2. \<And>rv rva. \<lbrace>?Q'10 rv rva\<rbrace> gets scheduler_action \<lbrace>?Q'14 rv rva\<rbrace>
 3. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv. \<lbrace>?Q'6 rv\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'10 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>P'\<rbrace> gets cur_domain \<lbrace>?Q'6\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb. rva \<noteq> rv \<Longrightarrow> dcorres dc (?P21 rv rva rvb) (?Q21 rv rva rvb) (return ()) (tcb_sched_action tcb_sched_enqueue t)
 2. \<And>rv rva rvb. \<not> rva \<noteq> rv \<Longrightarrow> dcorres dc (?P'21 rv rva rvb) (?Q'21 rv rva rvb) (return ()) (if rvb \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t))
 3. \<And>rv rva rvb s. P s \<Longrightarrow> (rva \<noteq> rv \<longrightarrow> ?P21 rv rva rvb s) \<and> (\<not> rva \<noteq> rv \<longrightarrow> ?P'21 rv rva rvb s)
 4. \<And>rv rva. \<lbrace>?Q'10 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. (rva \<noteq> rv \<longrightarrow> ?Q21 rv rva r s) \<and> (\<not> rva \<noteq> rv \<longrightarrow> ?Q'21 rv rva r s)\<rbrace>
 5. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv. \<lbrace>?Q'6 rv\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'10 rv\<rbrace>
 7. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>P'\<rbrace> gets cur_domain \<lbrace>?Q'6\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb. \<not> rva \<noteq> rv \<Longrightarrow> dcorres dc (?P'21 rv rva rvb) (?Q'21 rv rva rvb) (return ()) (if rvb \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t))
 2. \<And>rv rva rvb s. P s \<Longrightarrow> (rva \<noteq> rv \<longrightarrow> True) \<and> (\<not> rva \<noteq> rv \<longrightarrow> ?P'21 rv rva rvb s)
 3. \<And>rv rva. \<lbrace>?Q'10 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. (rva \<noteq> rv \<longrightarrow> True) \<and> (\<not> rva \<noteq> rv \<longrightarrow> ?Q'21 rv rva r s)\<rbrace>
 4. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>rv. \<lbrace>?Q'6 rv\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'10 rv\<rbrace>
 6. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>P'\<rbrace> gets cur_domain \<lbrace>?Q'6\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb. \<lbrakk>\<not> rva \<noteq> rv; rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> dcorres dc (?P26 rv rva rvb) (?Q26 rv rva rvb) (return ()) (do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od)
 2. \<And>rv rva rvb. \<lbrakk>\<not> rva \<noteq> rv; \<not> rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> dcorres dc (?P'26 rv rva rvb) (?Q'26 rv rva rvb) (return ()) (set_scheduler_action (switch_thread t))
 3. \<And>rv rva rvb s. P s \<Longrightarrow> (rva \<noteq> rv \<longrightarrow> True) \<and> (\<not> rva \<noteq> rv \<longrightarrow> (rvb \<noteq> resume_cur_thread \<longrightarrow> ?P26 rv rva rvb s) \<and> (\<not> rvb \<noteq> resume_cur_thread \<longrightarrow> ?P'26 rv rva rvb s))
 4. \<And>rv rva. \<lbrace>?Q'10 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. (rva \<noteq> rv \<longrightarrow> True) \<and> (\<not> rva \<noteq> rv \<longrightarrow> (r \<noteq> resume_cur_thread \<longrightarrow> ?Q26 rv rva r s) \<and> (\<not> r \<noteq> resume_cur_thread \<longrightarrow> ?Q'26 rv rva r s))\<rbrace>
 5. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>rv. \<lbrace>?Q'6 rv\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'10 rv\<rbrace>
 7. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>P'\<rbrace> gets cur_domain \<lbrace>?Q'6\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>rv rva rvb rvc. \<lbrakk>\<not> rva \<noteq> rv; rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> dcorres dc (?P26 rv rva rvb) (?Q'29 rv rva rvb rvc) (return ()) (tcb_sched_action tcb_sched_enqueue t)
 2. \<And>rv rva rvb. \<lbrakk>\<not> rva \<noteq> rv; rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 rv rva rvb\<rbrace> reschedule_required \<lbrace>?Q'29 rv rva rvb\<rbrace>
 3. \<And>rv rva rvb cs. \<lbrakk>\<not> rva \<noteq> rv; rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reschedule_required \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv rva rvb. \<lbrakk>\<not> rva \<noteq> rv; \<not> rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> dcorres dc (?P'26 rv rva rvb) (?Q'26 rv rva rvb) (return ()) (set_scheduler_action (switch_thread t))
 5. \<And>rv rva rvb s. P s \<Longrightarrow> (rva \<noteq> rv \<longrightarrow> True) \<and> (\<not> rva \<noteq> rv \<longrightarrow> (rvb \<noteq> resume_cur_thread \<longrightarrow> ?P26 rv rva rvb s) \<and> (\<not> rvb \<noteq> resume_cur_thread \<longrightarrow> ?P'26 rv rva rvb s))
 6. \<And>rv rva. \<lbrace>?Q'10 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. (rva \<noteq> rv \<longrightarrow> True) \<and> (\<not> rva \<noteq> rv \<longrightarrow> (r \<noteq> resume_cur_thread \<longrightarrow> ?Q26 rv rva r s) \<and> (\<not> r \<noteq> resume_cur_thread \<longrightarrow> ?Q'26 rv rva r s))\<rbrace>
 7. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<And>rv. \<lbrace>?Q'6 rv\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'10 rv\<rbrace>
 9. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 10. \<lbrace>P'\<rbrace> gets cur_domain \<lbrace>?Q'6\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb. \<lbrakk>\<not> rva \<noteq> rv; rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 rv rva rvb\<rbrace> reschedule_required \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>rv rva rvb cs. \<lbrakk>\<not> rva \<noteq> rv; rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reschedule_required \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rv rva rvb. \<lbrakk>\<not> rva \<noteq> rv; \<not> rvb \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> dcorres dc (?P'26 rv rva rvb) (?Q'26 rv rva rvb) (return ()) (set_scheduler_action (switch_thread t))
 4. \<And>rv rva rvb s. P s \<Longrightarrow> (rva \<noteq> rv \<longrightarrow> True) \<and> (\<not> rva \<noteq> rv \<longrightarrow> (rvb \<noteq> resume_cur_thread \<longrightarrow> True) \<and> (\<not> rvb \<noteq> resume_cur_thread \<longrightarrow> ?P'26 rv rva rvb s))
 5. \<And>rv rva. \<lbrace>?Q'10 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. (rva \<noteq> rv \<longrightarrow> True) \<and> (\<not> rva \<noteq> rv \<longrightarrow> (r \<noteq> resume_cur_thread \<longrightarrow> ?Q26 rv rva r s) \<and> (\<not> r \<noteq> resume_cur_thread \<longrightarrow> ?Q'26 rv rva r s))\<rbrace>
 6. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<And>rv. \<lbrace>?Q'6 rv\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'10 rv\<rbrace>
 8. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 9. \<lbrace>P'\<rbrace> gets cur_domain \<lbrace>?Q'6\<rbrace>
 10. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_domain \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!