theory Schedule_DR

lemma dcorres_dummy_set_thread_state_runnable:
  "dcorres dc \<top>
  (not_idle_thread ptr and st_tcb_at (\<lambda>t. (infer_tcb_pending_op ptr t) = (infer_tcb_pending_op ptr st)) ptr)
  (return ())
  (set_thread_state ptr st)" supply option.case_cong[cong] if_cong[cong] apply (rule wp_to_dcorres) apply (clarsimp simp:set_thread_state_def not_idle_thread_def set_object_def get_object_def | wp)+ apply (clarsimp simp:transform_def transform_current_thread_def st_tcb_at_def obj_at_def
       | rule ext)+ apply (clarsimp simp:transform_objects_def not_idle_thread_def dest!:get_tcb_SomeD) apply (case_tac "x = ptr") apply (clarsimp simp:transform_tcb_def) apply (clarsimp simp:restrict_map_def Map.map_add_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread ptr and st_tcb_at (\<lambda>t. infer_tcb_pending_op ptr t = infer_tcb_pending_op ptr st) ptr) (return ()) (set_thread_state ptr st) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread ptr and st_tcb_at (\<lambda>t. infer_tcb_pending_op ptr t = infer_tcb_pending_op ptr st) ptr) (return ()) (set_thread_state ptr st) proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrace>\<lambda>s. (not_idle_thread ptr and st_tcb_at (\<lambda>t. infer_tcb_pending_op ptr t = infer_tcb_pending_op ptr st) ptr) s \<and> transform s = cs\<rbrace> set_thread_state ptr st \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>ptr \<noteq> idle_thread s; st_tcb_at (\<lambda>t. infer_tcb_pending_op ptr t = infer_tcb_pending_op ptr st) ptr s; get_tcb ptr s = Some y; kheap s ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform (update_kheap (\<lambda>a. if a = ptr then Some (TCB (update_tcb_state st y)) else kheap s a) s) = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb x. \<lbrakk>ptr \<noteq> idle_thread s; infer_tcb_pending_op ptr (tcb_state tcb) = infer_tcb_pending_op ptr st; get_tcb ptr s = Some y; kheap s ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap (\<lambda>a. if a = ptr then Some (TCB (update_tcb_state st y)) else kheap s a) s) x = transform_objects s x proof (prove)
goal (1 subgoal):
 1. \<And>s tcb x. \<lbrakk>ptr \<noteq> idle_thread s; infer_tcb_pending_op ptr (tcb_state tcb) = infer_tcb_pending_op ptr st; kheap s ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptra. map_option (transform_object (machine_state s) ptra ((ekheap s |` (- {idle_thread s})) ptra)) (((\<lambda>a. if a = ptr then Some (TCB (update_tcb_state st tcb)) else kheap s a) |` (- {idle_thread s})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) x proof (prove)
goal (2 subgoals):
 1. \<And>s tcb x. \<lbrakk>ptr \<noteq> idle_thread s; infer_tcb_pending_op ptr (tcb_state tcb) = infer_tcb_pending_op ptr st; kheap s ptr = Some (TCB tcb); x = ptr\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptra. map_option (transform_object (machine_state s) ptra ((ekheap s |` (- {idle_thread s})) ptra)) (((\<lambda>a. if a = ptr then Some (TCB (update_tcb_state st tcb)) else kheap s a) |` (- {idle_thread s})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) x
 2. \<And>s tcb x. \<lbrakk>ptr \<noteq> idle_thread s; infer_tcb_pending_op ptr (tcb_state tcb) = infer_tcb_pending_op ptr st; kheap s ptr = Some (TCB tcb); x \<noteq> ptr\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptra. map_option (transform_object (machine_state s) ptra ((ekheap s |` (- {idle_thread s})) ptra)) (((\<lambda>a. if a = ptr then Some (TCB (update_tcb_state st tcb)) else kheap s a) |` (- {idle_thread s})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) x proof (prove)
goal (1 subgoal):
 1. \<And>s tcb x. \<lbrakk>ptr \<noteq> idle_thread s; infer_tcb_pending_op ptr (tcb_state tcb) = infer_tcb_pending_op ptr st; kheap s ptr = Some (TCB tcb); x \<noteq> ptr\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptra. map_option (transform_object (machine_state s) ptra ((ekheap s |` (- {idle_thread s})) ptra)) (((\<lambda>a. if a = ptr then Some (TCB (update_tcb_state st tcb)) else kheap s a) |` (- {idle_thread s})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) x proof (prove)
goal:
No subgoals!