theory IpcCancel_R

lemma (in delete_one) suspend_corres:
  "corres dc (einvs and tcb_at t) (invs' and tcb_at' t)
        (IpcCancel_A.suspend t) (ThreadDecls_H.suspend t)" apply (simp add: IpcCancel_A.suspend_def Thread_H.suspend_def) apply (rule corres_guard_imp) apply (rule corres_split_nor[OF cancel_ipc_corres]) apply (rule corres_split[OF getThreadState_corres]) apply (rule corres_split_nor) apply (rule corres_if) apply (case_tac state; simp) apply (simp add: update_restart_pc_def updateRestartPC_def) apply (rule asUser_corres') apply (simp add: ARM.nextInstructionRegister_def ARM.faultRegister_def
                             ARM_H.nextInstructionRegister_def ARM_H.faultRegister_def) apply (simp add: ARM_H.Register_def) apply (subst unit_dc_is_eq) apply (rule corres_underlying_trivial) apply (wpsimp simp: ARM.setRegister_def ARM.getRegister_def) apply (rule corres_return_trivial) apply (rule corres_split_nor[OF setThreadState_corres]) apply simp apply (rule tcbSchedDequeue_corres') apply (wpsimp simp: update_restart_pc_def updateRestartPC_def)+ apply (rule hoare_post_imp[where Q = "\<lambda>rv s. tcb_at t s \<and> is_etcb_at t s"]) apply simp apply wp apply (rule hoare_post_imp[where Q = "\<lambda>rv s. tcb_at' t s \<and> valid_inQ_queues s"]) apply (wpsimp simp: valid_queues_inQ_queues) apply wp+ apply (force simp: valid_sched_def tcb_at_is_etcb_at) apply (clarsimp simp add: invs'_def valid_state'_def valid_queues_inQ_queues) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (IpcCancel_A.suspend t) (ThreadDecls_H.suspend t) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do y <- cancel_ipc t;
state <- get_thread_state t;
y <- if state = Structures_A.thread_state.Running then update_restart_pc t else return ();
y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do y <- cancel_ipc t;
state <- get_thread_state t;
y <- if state = Structures_A.thread_state.Running then update_restart_pc t else return ();
y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 2. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. corres dc ?R4 ?R'4 (do state <- get_thread_state t;
y <- if state = Structures_A.thread_state.Running then update_restart_pc t else return ();
y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 2. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. ?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. ?R'4\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R9 state) (?R'9 statea) (do y <- if state = Structures_A.thread_state.Running then update_restart_pc t else return ();
y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- if statea = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 2. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>?R9\<rbrace>
 3. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>?R'9\<rbrace>
 4. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?P15 state) (?P'17 statea) (if state = Structures_A.thread_state.Running then update_restart_pc t else return ()) (if statea = Structures_H.thread_state.Running then updateRestartPC t else return ())
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 5. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. ?P15 state and ?Q16 state\<rbrace>
 6. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. ?P'17 statea and ?Q'18 statea\<rbrace>
 7. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 9. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 10. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (12 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> (state = Structures_A.thread_state.Running) = (statea = Structures_H.thread_state.Running)
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?P25 state) (?P'28 statea) (update_restart_pc t) (updateRestartPC t)
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 6. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 7. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then ?P25 state else ?Q26 state) and ?Q16 state\<rbrace>
 8. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then ?P'28 statea else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 9. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?P25 state) (?P'28 statea) (update_restart_pc t) (updateRestartPC t)
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 6. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then ?P25 state else ?Q26 state) and ?Q16 state\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then ?P'28 statea else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 8. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?P25 state) (?P'28 statea) (as_user t (getRegister IpcCancel_A.nextInstructionRegister >>= setRegister IpcCancel_A.faultRegister)) (asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister))
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 6. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then ?P25 state else ?Q26 state) and ?Q16 state\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then ?P'28 statea else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 8. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (getRegister IpcCancel_A.nextInstructionRegister >>= setRegister IpcCancel_A.faultRegister) (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister)
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 6. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else ?Q26 state) and ?Q16 state\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 8. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (getRegister ARM.NextIP >>= setRegister ARM.FaultIP) (getRegister (ARM_H.Register ARM.NextIP) >>= setRegister (ARM_H.Register ARM.FaultIP))
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 6. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else ?Q26 state) and ?Q16 state\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 8. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (getRegister ARM.NextIP >>= setRegister ARM.FaultIP) (getRegister ARM.NextIP >>= setRegister ARM.FaultIP)
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 6. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else ?Q26 state) and ?Q16 state\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 8. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) (getRegister ARM.NextIP >>= setRegister ARM.FaultIP) (getRegister ARM.NextIP >>= setRegister ARM.FaultIP)
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 6. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else ?Q26 state) and ?Q16 state\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 8. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state statea. \<lbrakk>thread_state_relation state statea; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (getRegister ARM.NextIP >>= setRegister ARM.FaultIP)
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 6. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else ?Q26 state) and ?Q16 state\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 8. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?Q26 state) (?Q'29 statea) (return ()) (return ())
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 5. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else ?Q26 state) and ?Q16 state\<rbrace>
 6. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else ?Q'29 statea) and ?Q'18 statea\<rbrace>
 7. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 9. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 10. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R14 state statea) (?R'14 state statea) (do y <- set_thread_state t Structures_A.thread_state.Inactive;
tcb_sched_action tcb_sched_dequeue t
od) (do y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od)
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. ?R14 state statea\<rbrace>
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. ?R'14 state statea\<rbrace>
 4. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else (\<lambda>_. True)) and ?Q16 state\<rbrace>
 5. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and ?Q'18 statea\<rbrace>
 6. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 8. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 9. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (12 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> thread_state_relation Structures_A.thread_state.Inactive Structures_H.thread_state.Inactive
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R83 state statea) (?R'83 state statea) (tcb_sched_action tcb_sched_dequeue t) (tcbSchedDequeue t)
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q83 state statea\<rbrace> set_thread_state t Structures_A.thread_state.Inactive \<lbrace>\<lambda>x. ?R83 state statea\<rbrace>
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'83 state statea\<rbrace> setThreadState Structures_H.thread_state.Inactive t \<lbrace>\<lambda>x. ?R'83 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. tcb_at t and ?Q83 state statea\<rbrace>
 6. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. tcb_at' t and ?Q'83 state statea\<rbrace>
 7. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else (\<lambda>_. True)) and ?Q16 state\<rbrace>
 8. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and ?Q'18 statea\<rbrace>
 9. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R83 state statea) (?R'83 state statea) (tcb_sched_action tcb_sched_dequeue t) (tcbSchedDequeue t)
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q83 state statea\<rbrace> set_thread_state t Structures_A.thread_state.Inactive \<lbrace>\<lambda>x. ?R83 state statea\<rbrace>
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'83 state statea\<rbrace> setThreadState Structures_H.thread_state.Inactive t \<lbrace>\<lambda>x. ?R'83 state statea\<rbrace>
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. tcb_at t and ?Q83 state statea\<rbrace>
 5. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. tcb_at' t and ?Q'83 state statea\<rbrace>
 6. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else (\<lambda>_. True)) and ?Q16 state\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and ?Q'18 statea\<rbrace>
 8. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q83 state statea\<rbrace> set_thread_state t Structures_A.thread_state.Inactive \<lbrace>\<lambda>x. is_etcb_at t\<rbrace>
 2. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'83 state statea\<rbrace> setThreadState Structures_H.thread_state.Inactive t \<lbrace>\<lambda>x. tcb_at' t and valid_inQ_queues\<rbrace>
 3. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q16 state\<rbrace> if state = Structures_A.thread_state.Running then update_restart_pc t else return () \<lbrace>\<lambda>x. tcb_at t and ?Q83 state statea\<rbrace>
 4. \<And>state statea. thread_state_relation state statea \<Longrightarrow> \<lbrace>?Q'18 statea\<rbrace> if statea = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>\<lambda>x. tcb_at' t and ?Q'83 state statea\<rbrace>
 5. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then tcb_at t else (\<lambda>_. True)) and ?Q16 state\<rbrace>
 6. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and ?Q'18 statea\<rbrace>
 7. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 9. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 10. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (if state = Structures_A.thread_state.Running then tcb_at t else (\<lambda>_. True)) s \<and> tcb_at t s \<and> is_etcb_at t s\<rbrace>
 2. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and (\<lambda>s. (statea = Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> valid_inQ_queues s) \<and> (statea \<noteq> Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> tcb_at' t s \<and> valid_inQ_queues s))\<rbrace>
 3. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv s. tcb_at t s \<and> is_etcb_at t s \<Longrightarrow> (if rv = Structures_A.thread_state.Running then tcb_at t else (\<lambda>_. True)) s \<and> tcb_at t s \<and> is_etcb_at t s
 2. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. tcb_at t s \<and> is_etcb_at t s\<rbrace>
 3. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and (\<lambda>s. (statea = Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> valid_inQ_queues s) \<and> (statea \<noteq> Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> tcb_at' t s \<and> valid_inQ_queues s))\<rbrace>
 4. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q9\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. tcb_at t s \<and> is_etcb_at t s\<rbrace>
 2. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and (\<lambda>s. (statea = Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> valid_inQ_queues s) \<and> (statea \<noteq> Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> tcb_at' t s \<and> valid_inQ_queues s))\<rbrace>
 3. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and ?Q9\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>statea. (if statea = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and (\<lambda>s. (statea = Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> valid_inQ_queues s) \<and> (statea \<noteq> Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> tcb_at' t s \<and> valid_inQ_queues s))\<rbrace>
 2. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and (\<lambda>s. tcb_at t s \<and> is_etcb_at t s)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. tcb_at' t s \<and> valid_inQ_queues s \<Longrightarrow> ((if rv = Structures_H.thread_state.Running then tcb_at' t else (\<lambda>_. True)) and (\<lambda>s. (rv = Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> valid_inQ_queues s) \<and> (rv \<noteq> Structures_H.thread_state.Running \<longrightarrow> tcb_at' t s \<and> tcb_at' t s \<and> valid_inQ_queues s))) s
 2. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. tcb_at' t s \<and> valid_inQ_queues s\<rbrace>
 3. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and (\<lambda>s. tcb_at t s \<and> is_etcb_at t s)\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'9\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. tcb_at' t s \<and> valid_inQ_queues s\<rbrace>
 2. \<lbrace>?Q4\<rbrace> cancel_ipc t \<lbrace>\<lambda>x. tcb_at t and (\<lambda>s. tcb_at t s \<and> is_etcb_at t s)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> cancelIPC t \<lbrace>\<lambda>x. tcb_at' t and ?Q'9\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (einvs and tcb_at t and (\<lambda>s. tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s)) s
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and (\<lambda>s. tcb_at' t s \<and> tcb_at' t s \<and> valid_inQ_queues s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (invs' and tcb_at' t and (\<lambda>s. tcb_at' t s \<and> tcb_at' t s \<and> valid_inQ_queues s)) s proof (prove)
goal:
No subgoals!