theory Schedule_DR

lemma switch_to_idle_thread_dcorres:
  "dcorres dc \<top> (invs and valid_etcbs) (Schedule_D.switch_to_thread None) switch_to_idle_thread" apply (clarsimp simp: Schedule_D.switch_to_thread_def switch_to_idle_thread_def) apply (rule dcorres_symb_exec_r) apply (rule corres_guard_imp) apply (rule corres_split_noop_rhs) apply (rule dcorres_arch_switch_to_idle_thread_return) apply (clarsimp simp: corres_underlying_def gets_def modify_def get_def put_def do_machine_op_def select_f_def split_def bind_def in_return) apply (clarsimp simp: transform_def transform_current_thread_def transform_asid_table_def) apply assumption apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (Schedule_D.switch_to_thread None) switch_to_idle_thread proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (modify (cdl_current_thread_update (\<lambda>_. None))) (do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (?Q' rv) (modify (cdl_current_thread_update (\<lambda>_. None))) (do y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. rv))
od)
 2. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv. dcorres dc (?Q4 rv) (?Q'4 rv) (modify (cdl_current_thread_update (\<lambda>_. None))) (do y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. rv))
od)
 2. \<And>rv s. True \<Longrightarrow> ?Q4 rv s
 3. \<And>rv s. ?Q' rv s \<Longrightarrow> ?Q'4 rv s
 4. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv. dcorres dc (?P8 rv) (?P'8 rv) (return ()) arch_switch_to_idle_thread
 2. \<And>rv. dcorres dc (?R8 rv) (?R'8 rv) (modify (cdl_current_thread_update (\<lambda>_. None))) (modify (cur_thread_update (\<lambda>_. rv)))
 3. \<And>rv. \<lbrace>?Q'8 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x. ?R'8 rv\<rbrace>
 4. \<And>rv s. True \<Longrightarrow> (?P8 rv and ?R8 rv) s
 5. \<And>rv s. ?Q' rv s \<Longrightarrow> (?P'8 rv and ?Q'8 rv) s
 6. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv. dcorres dc (?R8 rv) (?R'8 rv) (modify (cdl_current_thread_update (\<lambda>_. None))) (modify (cur_thread_update (\<lambda>_. rv)))
 2. \<And>rv. \<lbrace>?Q'8 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x. ?R'8 rv\<rbrace>
 3. \<And>rv s. True \<Longrightarrow> ((\<lambda>_. True) and ?R8 rv) s
 4. \<And>rv s. ?Q' rv s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8 rv) s
 5. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv b. \<lbrakk>?R8 rv (transform b); ?R'8 rv b\<rbrakk> \<Longrightarrow> transform (b\<lparr>cur_thread := rv\<rparr>) = transform b\<lparr>cdl_current_thread := None\<rparr>
 2. \<And>rv. \<lbrace>?Q'8 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x. ?R'8 rv\<rbrace>
 3. \<And>rv s. True \<Longrightarrow> ((\<lambda>_. True) and ?R8 rv) s
 4. \<And>rv s. ?Q' rv s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8 rv) s
 5. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv b. \<lbrakk>?R8 rv \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects b, cdl_cdt = transform_cdt b, cdl_current_thread = if cur_thread b \<noteq> idle_thread b then Some (cur_thread b) else None, cdl_irq_node = interrupt_irq_node b, cdl_asid_table = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table b), cdl_current_domain = cur_domain b\<rparr>; ?R'8 rv b\<rbrakk> \<Longrightarrow> rv = idle_thread b
 2. \<And>rv. \<lbrace>?Q'8 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x. ?R'8 rv\<rbrace>
 3. \<And>rv s. True \<Longrightarrow> ((\<lambda>_. True) and ?R8 rv) s
 4. \<And>rv s. ?Q' rv s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8 rv) s
 5. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<lbrace>?Q'8 rv\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>x b. rv = idle_thread b\<rbrace>
 2. \<And>rv s. True \<Longrightarrow> ((\<lambda>_. True) and ?R8 rv) s
 3. \<And>rv s. ?Q' rv s \<Longrightarrow> ((\<lambda>_. True) and ?Q'8 rv) s
 4. \<lbrace>invs and valid_etcbs\<rbrace> gets idle_thread \<lbrace>?Q'\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets idle_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!