theory Finalise_IF

lemma suspend_globals_equiv[ wp]:
  "\<lbrace>globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state\<rbrace>
   suspend t
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding suspend_def update_restart_pc_def apply (wp tcb_sched_action_extended.globals_equiv dxo_wp_weak) apply simp apply (wp set_thread_state_globals_equiv) apply wp+ apply clarsimp apply (rule hoare_vcg_conj_lift) prefer 2 apply (rule hoare_drop_imps) apply wp+ apply (rule hoare_drop_imps) apply wp+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state\<rbrace> suspend t \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state\<rbrace> do cancel_ipc t;
state <- get_thread_state t;
if state = Running then as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) else return ();
set_thread_state t Inactive;
do_extended_op (tcb_sched_action tcb_sched_dequeue t)
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x state xa xb s f. globals_equiv st (trans_state f s) = globals_equiv st s
 2. \<And>x state xa. \<lbrace>?B4 x state xa\<rbrace> set_thread_state t Inactive \<lbrace>\<lambda>xb. globals_equiv st\<rbrace>
 3. \<And>x state. \<lbrace>?B3 x state\<rbrace> if state = Running then as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) else return () \<lbrace>?B4 x state\<rbrace>
 4. \<And>x. \<lbrace>?B1 x\<rbrace> get_thread_state t \<lbrace>?B3 x\<rbrace>
 5. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 6. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x state xa. \<lbrace>?B4 x state xa\<rbrace> set_thread_state t Inactive \<lbrace>\<lambda>xb. globals_equiv st\<rbrace>
 2. \<And>x state. \<lbrace>?B3 x state\<rbrace> if state = Running then as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) else return () \<lbrace>?B4 x state\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> get_thread_state t \<lbrace>?B3 x\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 5. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x state. \<lbrace>?B3 x state\<rbrace> if state = Running then as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) else return () \<lbrace>\<lambda>xa. globals_equiv st and valid_arch_state\<rbrace>
 2. \<And>x. \<lbrace>?B1 x\<rbrace> get_thread_state t \<lbrace>?B3 x\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 4. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B1 x\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s)) s \<and> valid_arch_state s) \<and> (state \<noteq> Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 3. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> t \<noteq> idle_thread s \<and> valid_arch_state s) \<and> (state \<noteq> Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 3. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P24 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. rv = Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> t \<noteq> idle_thread s \<and> valid_arch_state s\<rbrace>
 2. \<lbrace>?P'23 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. rv \<noteq> Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>\<lambda>a b. ?P24 a b \<and> ?P'23 a b\<rbrace>
 4. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'23 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. rv \<noteq> Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s\<rbrace>
 2. \<lbrace>?P24 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. rv = Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> t \<noteq> idle_thread s \<and> valid_arch_state s\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>\<lambda>a b. ?P24 a b \<and> ?P'23 a b\<rbrace>
 4. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'23 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. globals_equiv st s \<and> valid_arch_state s\<rbrace>
 2. \<lbrace>?P24 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. rv = Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> t \<noteq> idle_thread s \<and> valid_arch_state s\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>\<lambda>a b. ?P24 a b \<and> ?P'23 a b\<rbrace>
 4. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P24 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. rv = Running \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> t \<noteq> idle_thread s \<and> valid_arch_state s\<rbrace>
 2. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>\<lambda>a b. ?P24 a b \<and> globals_equiv st b \<and> valid_arch_state b\<rbrace>
 3. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P24 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. globals_equiv st s \<and> valid_arch_state s \<and> t \<noteq> idle_thread s \<and> valid_arch_state s\<rbrace>
 2. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>\<lambda>a b. ?P24 a b \<and> globals_equiv st b \<and> valid_arch_state b\<rbrace>
 3. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state) s \<Longrightarrow> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s \<and> t \<noteq> idle_thread s \<and> valid_arch_state s \<and> (globals_equiv st and valid_arch_state) s \<and> valid_arch_state s proof (prove)
goal:
No subgoals!