theory Scheduler_IF

lemma switch_to_thread_midstrength_reads_respects_scheduler[wp]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "midstrength_reads_respects_scheduler aag l
     (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)))
     (switch_to_thread t >>= (\<lambda>_. set_scheduler_action resume_cur_thread))" apply (simp add: switch_to_thread_def) apply (subst oblivious_modify_swap[symmetric, OF tcb_action_oblivious_cur_thread]) apply (simp add: bind_assoc) apply (simp add: set_scheduler_action_def) apply (subst oblivious_modify_swap[symmetric, OF tcb_action_oblivious_schact]) apply (rule equiv_valid_get_assert) apply (rule equiv_valid_guard_imp) apply (simp add: bind_assoc[symmetric]) apply (rule bind_ev_general) apply (rule tcb_action_reads_respects_scheduler[OF domains_distinct]) apply (simp add: bind_assoc) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do _ <- switch_to_thread t;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do _ <- do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do _ <- do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
rv <- modify (cur_thread_update (\<lambda>_. t));
tcb_sched_action tcb_sched_dequeue t
od;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do x <- get;
x <- assert (\<exists>y. get_tcb t x = Some y);
x <- arch_switch_to_thread t;
x <- modify (cur_thread_update (\<lambda>_. t));
_ <- tcb_sched_action tcb_sched_dequeue t;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do x <- get;
x <- assert (\<exists>y. get_tcb t x = Some y);
x <- arch_switch_to_thread t;
x <- modify (cur_thread_update (\<lambda>_. t));
_ <- tcb_sched_action tcb_sched_dequeue t;
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do x <- get;
x <- assert (\<exists>y. get_tcb t x = Some y);
x <- arch_switch_to_thread t;
x <- modify (cur_thread_update (\<lambda>_. t));
rv <- modify (scheduler_action_update (\<lambda>_. resume_cur_thread));
tcb_sched_action tcb_sched_dequeue t
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do x <- arch_switch_to_thread t;
x <- modify (cur_thread_update (\<lambda>_. t));
rv <- modify (scheduler_action_update (\<lambda>_. resume_cur_thread));
tcb_sched_action tcb_sched_dequeue t
od) proof (prove)
goal (2 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q2 (do x <- arch_switch_to_thread t;
x <- modify (cur_thread_update (\<lambda>_. t));
rv <- modify (scheduler_action_update (\<lambda>_. resume_cur_thread));
tcb_sched_action tcb_sched_dequeue t
od)
 2. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q2 (do rv <- do x <- do x <- arch_switch_to_thread t;
modify (cur_thread_update (\<lambda>_. t))
od;
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od;
tcb_sched_action tcb_sched_dequeue t
od)
 2. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid (scheduler_equiv aag) ?B5 (scheduler_affects_equiv aag l) (?Q5 rv) (tcb_sched_action tcb_sched_dequeue t)
 2. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B5 ?P'5 (do x <- do x <- arch_switch_to_thread t;
modify (cur_thread_update (\<lambda>_. t))
od;
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 3. \<lbrace>?P''5\<rbrace> do x <- do x <- arch_switch_to_thread t;
modify (cur_thread_update (\<lambda>_. t))
od;
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od \<lbrace>?Q5\<rbrace>
 4. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> ?P'5 s \<and> ?P''5 s proof (prove)
goal (3 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?P'5 (do x <- do x <- arch_switch_to_thread t;
modify (cur_thread_update (\<lambda>_. t))
od;
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 2. \<lbrace>?P''5\<rbrace> do x <- do x <- arch_switch_to_thread t;
modify (cur_thread_update (\<lambda>_. t))
od;
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 3. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> ?P'5 s \<and> ?P''5 s proof (prove)
goal (3 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?P'5 (do x <- arch_switch_to_thread t;
x <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 2. \<lbrace>?P''5\<rbrace> do x <- do x <- arch_switch_to_thread t;
modify (cur_thread_update (\<lambda>_. t))
od;
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>
 3. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> ?P'5 s \<and> ?P''5 s proof (prove)
goal:
No subgoals!