theory Fastpath_Equiv

lemma possibleSwitchTo_rewrite:
  "monadic_rewrite True True
          (\<lambda>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s
              \<and> ksSchedulerAction s = ResumeCurrentThread
              \<and> ksCurThread s = thread
              \<and> ksCurDomain s = curDom
              \<and> destDom = curDom)
    (possibleSwitchTo t) (setSchedulerAction (SwitchToThread t))" supply if_split[split del] apply (simp add: possibleSwitchTo_def) 
  (* under current preconditions both branch conditions are false *)
   apply (monadic_rewrite_l monadic_rewrite_if_l_False \<open>wpsimp wp: threadGet_wp cd_wp\<close>) apply (monadic_rewrite_l monadic_rewrite_if_l_False \<open>wpsimp wp: threadGet_wp cd_wp\<close>) 
   (* discard unused getters before setSchedulerAction *)
    apply (simp add: getCurThread_def curDomain_def gets_bind_ign getSchedulerAction_def) apply (monadic_rewrite_symb_exec_l_drop, rule monadic_rewrite_refl) apply (auto simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom) (possibleSwitchTo t) (setSchedulerAction (SwitchToThread t)) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom) (possibleSwitchTo t) (setSchedulerAction (SwitchToThread t)) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom) (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od) (setSchedulerAction (SwitchToThread t)) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom) (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od) (setSchedulerAction (SwitchToThread t)) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q7 (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od) (setSchedulerAction (SwitchToThread t))
 2. \<And>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom \<Longrightarrow> ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> tcbDomain tcb \<noteq> ksCurDomain s) and (\<lambda>_. True)) s) and ?Q7) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q49 (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
setSchedulerAction (SwitchToThread t)
od) (setSchedulerAction (SwitchToThread t))
 2. \<And>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom \<Longrightarrow> ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> tcbDomain tcb \<noteq> ksCurDomain s) and (\<lambda>_. True)) s) and ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> ksSchedulerAction s \<noteq> ResumeCurrentThread) and (\<lambda>_. True)) s) and ?Q49)) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q49 (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
setSchedulerAction (SwitchToThread t)
od) (setSchedulerAction (SwitchToThread t))
 2. \<And>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom \<Longrightarrow> ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> tcbDomain tcb \<noteq> ksCurDomain s) and (\<lambda>_. True)) s) and ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> ksSchedulerAction s \<noteq> ResumeCurrentThread) and (\<lambda>_. True)) s) and ?Q49)) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q49 (do targetDom <- threadGet tcbDomain t;
setSchedulerAction (SwitchToThread t)
od) (setSchedulerAction (SwitchToThread t))
 2. \<And>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom \<Longrightarrow> ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> tcbDomain tcb \<noteq> ksCurDomain s) and (\<lambda>_. True)) s) and ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> ksSchedulerAction s \<noteq> ResumeCurrentThread) and (\<lambda>_. True)) s) and ?Q49)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. tcbPriority tcb = destPrio \<and> tcbDomain tcb = destDom) t s \<and> ksSchedulerAction s = ResumeCurrentThread \<and> ksCurThread s = thread \<and> ksCurDomain s = curDom \<and> destDom = curDom \<Longrightarrow> ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> tcbDomain tcb \<noteq> ksCurDomain s) and (\<lambda>_. True)) s) and ((\<lambda>s. \<forall>tcb. ko_at' tcb t s \<longrightarrow> ((\<lambda>_. \<not> ksSchedulerAction s \<noteq> ResumeCurrentThread) and (\<lambda>_. True)) s) and (\<lambda>_. True))) s proof (prove)
goal:
No subgoals!