theory Schedule_DR

lemma arch_switch_to_thread_dcorres:
  "dcorres dc \<top> (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs)
     (return ())
     (arch_switch_to_thread t)" apply (clarsimp simp: arch_switch_to_thread_def) apply (rule corres_dummy_return_pl) apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_set_vm_root]) apply simp apply (rule dcorres_machine_op_noop) apply (simp add: ARM.clearExMonitor_def, wp)[1] apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs) (return ()) (arch_switch_to_thread t) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs) (return ()) (do y <- set_vm_root t;
do_machine_op clearExMonitor
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs) (do return ?b;
return ()
od) (do y <- set_vm_root t;
do_machine_op clearExMonitor
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q2 ?Q'2 (do return ?b;
return ()
od) (do y <- set_vm_root t;
do_machine_op clearExMonitor
od)
 2. \<And>s. True \<Longrightarrow> ?Q2 s
 3. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs) s \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. \<And>rv y. dc rv y \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 y) (K_bind (return ()) rv) (do_machine_op clearExMonitor)
 2. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_vm_root t \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv. dcorres dc (?R6 rv) (?R'6 ()) (return ()) (do_machine_op clearExMonitor)
 2. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_vm_root t \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> clearExMonitor \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_vm_root t \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>m s. underlying_memory s = m \<Longrightarrow> underlying_memory (s\<lparr>exclusive_state := default_exclusive_state\<rparr>) = m
 2. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_vm_root t \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> t) and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal:
No subgoals!