theory Ipc_IF

lemma possible_switch_to_equiv_but_for_labels:
  "\<lbrace>equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s)
                                  and K (pasObjectAbs aag target \<in> L) and pas_refined aag\<rbrace>
   possible_switch_to target
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" apply (simp add: possible_switch_to_def) apply (wp tcb_sched_action_equiv_but_for_labels) 
       (* possible_switch_to does not modify scheduler action if target is in different domain *)
        apply (rule hoare_pre_cont) apply (wp tcb_sched_action_equiv_but_for_labels) apply (rule hoare_pre_cont) apply (wp tcb_sched_action_equiv_but_for_labels)+ apply (clarsimp simp: etcb_at_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and K (pasObjectAbs aag target \<in> L) and pas_refined aag\<rbrace> possible_switch_to target \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and (\<lambda>y. pasObjectAbs aag target \<in> L) and pas_refined aag\<rbrace> do cur_dom <- gets cur_domain;
target_dom <- ethread_get tcb_domain target;
action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue target else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue target
od else set_scheduler_action $ switch_thread target
od \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cur_dom target_dom action. \<lbrakk>\<not> target_dom \<noteq> cur_dom; action \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 cur_dom target_dom action\<rbrace> reschedule_required \<lbrace>\<lambda>x s. equiv_but_for_labels aag L st s \<and> K (pasObjectAbs aag target \<in> L) s \<and> pas_refined aag s\<rbrace>
 2. \<And>cur_dom target_dom action. \<lbrakk>\<not> target_dom \<noteq> cur_dom; \<not> action \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?R6 cur_dom target_dom action\<rbrace> set_scheduler_action $ switch_thread target \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>
 3. \<And>cur_dom target_dom. \<lbrace>?B2 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (target_dom \<noteq> cur_dom \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag target \<in> L) and pas_refined aag) s) \<and> (\<not> target_dom \<noteq> cur_dom \<longrightarrow> (action \<noteq> resume_cur_thread \<longrightarrow> ?Q6 cur_dom target_dom action s) \<and> (\<not> action \<noteq> resume_cur_thread \<longrightarrow> ?R6 cur_dom target_dom action s))\<rbrace>
 4. \<And>cur_dom. \<lbrace>?B1 cur_dom\<rbrace> ethread_get tcb_domain target \<lbrace>?B2 cur_dom\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets cur_domain \<lbrace>?B1\<rbrace>
 6. \<And>s. (equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and (\<lambda>y. pasObjectAbs aag target \<in> L) and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cur_dom target_dom action. \<lbrakk>\<not> target_dom \<noteq> cur_dom; action \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 cur_dom target_dom action\<rbrace> reschedule_required \<lbrace>\<lambda>x s. equiv_but_for_labels aag L st s \<and> K (pasObjectAbs aag target \<in> L) s \<and> pas_refined aag s\<rbrace>
 2. \<And>cur_dom target_dom action. \<lbrakk>\<not> target_dom \<noteq> cur_dom; \<not> action \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?R6 cur_dom target_dom action\<rbrace> set_scheduler_action $ switch_thread target \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>
 3. \<And>cur_dom target_dom. \<lbrace>?B2 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (target_dom \<noteq> cur_dom \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag target \<in> L) and pas_refined aag) s) \<and> (\<not> target_dom \<noteq> cur_dom \<longrightarrow> (action \<noteq> resume_cur_thread \<longrightarrow> ?Q6 cur_dom target_dom action s) \<and> (\<not> action \<noteq> resume_cur_thread \<longrightarrow> ?R6 cur_dom target_dom action s))\<rbrace>
 4. \<And>cur_dom. \<lbrace>?B1 cur_dom\<rbrace> ethread_get tcb_domain target \<lbrace>?B2 cur_dom\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets cur_domain \<lbrace>?B1\<rbrace>
 6. \<And>s. (equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and (\<lambda>y. pasObjectAbs aag target \<in> L) and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cur_dom target_dom action. \<lbrakk>\<not> target_dom \<noteq> cur_dom; \<not> action \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?R6 cur_dom target_dom action\<rbrace> set_scheduler_action $ switch_thread target \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>
 2. \<And>cur_dom target_dom. \<lbrace>?B2 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (target_dom \<noteq> cur_dom \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag target \<in> L) and pas_refined aag) s) \<and> (\<not> target_dom \<noteq> cur_dom \<longrightarrow> (action \<noteq> resume_cur_thread \<longrightarrow> False) \<and> (\<not> action \<noteq> resume_cur_thread \<longrightarrow> ?R6 cur_dom target_dom action s))\<rbrace>
 3. \<And>cur_dom. \<lbrace>?B1 cur_dom\<rbrace> ethread_get tcb_domain target \<lbrace>?B2 cur_dom\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_domain \<lbrace>?B1\<rbrace>
 5. \<And>s. (equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and (\<lambda>y. pasObjectAbs aag target \<in> L) and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cur_dom target_dom action. \<lbrakk>\<not> target_dom \<noteq> cur_dom; \<not> action \<noteq> resume_cur_thread\<rbrakk> \<Longrightarrow> \<lbrace>?R6 cur_dom target_dom action\<rbrace> set_scheduler_action (switch_thread target) \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>
 2. \<And>cur_dom target_dom. \<lbrace>?B2 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (target_dom \<noteq> cur_dom \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag target \<in> L) and pas_refined aag) s) \<and> (\<not> target_dom \<noteq> cur_dom \<longrightarrow> (action \<noteq> resume_cur_thread \<longrightarrow> False) \<and> (\<not> action \<noteq> resume_cur_thread \<longrightarrow> ?R6 cur_dom target_dom action s))\<rbrace>
 3. \<And>cur_dom. \<lbrace>?B1 cur_dom\<rbrace> ethread_get tcb_domain target \<lbrace>?B2 cur_dom\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_domain \<lbrace>?B1\<rbrace>
 5. \<And>s. (equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and (\<lambda>y. pasObjectAbs aag target \<in> L) and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cur_dom target_dom. \<lbrace>?B2 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (target_dom \<noteq> cur_dom \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag target \<in> L) and pas_refined aag) s) \<and> (\<not> target_dom \<noteq> cur_dom \<longrightarrow> (action \<noteq> resume_cur_thread \<longrightarrow> False) \<and> (\<not> action \<noteq> resume_cur_thread \<longrightarrow> False))\<rbrace>
 2. \<And>cur_dom. \<lbrace>?B1 cur_dom\<rbrace> ethread_get tcb_domain target \<lbrace>?B2 cur_dom\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_domain \<lbrace>?B1\<rbrace>
 4. \<And>s. (equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and (\<lambda>y. pasObjectAbs aag target \<in> L) and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and (\<lambda>y. pasObjectAbs aag target \<in> L) and pas_refined aag) s \<Longrightarrow> etcb_at (\<lambda>t. (tcb_domain t \<noteq> cur_domain s \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag target \<in> L) and pas_refined aag) s) \<and> (\<not> tcb_domain t \<noteq> cur_domain s \<longrightarrow> (scheduler_action s \<noteq> resume_cur_thread \<longrightarrow> False) \<and> (\<not> scheduler_action s \<noteq> resume_cur_thread \<longrightarrow> False))) target s proof (prove)
goal:
No subgoals!