theory DetSchedSchedule_AI

lemma invoke_tcb_valid_sched[wp]:
  "\<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf ti\<rbrace>
     invoke_tcb ti
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (cases ti, simp_all only:) apply (wp mapM_x_wp | simp | rule subset_refl | rule reschedule_preserves_valid_sched |
               clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap |
               intro impI conjI)+ apply (rename_tac option) apply (case_tac option) apply (wp mapM_x_wp | simp | rule subset_refl |
            clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap |
            rule reschedule_preserves_valid_sched | intro impI conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf ti\<rbrace> invoke_tcb ti \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (WriteRegisters x11 x12 x13 x14)\<rbrace> invoke_tcb (WriteRegisters x11 x12 x13 x14) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (ReadRegisters x21 x22 x23 x24)\<rbrace> invoke_tcb (ReadRegisters x21 x22 x23 x24) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (CopyRegisters x31 x32 x33 x34 x35 x36 x37)\<rbrace> invoke_tcb (CopyRegisters x31 x32 x33 x34 x35 x36 x37) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)\<rbrace> invoke_tcb (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>x5. ti = Suspend x5 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (Suspend x5)\<rbrace> invoke_tcb (Suspend x5) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>x6. ti = Resume x6 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (Resume x6)\<rbrace> invoke_tcb (Resume x6) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (NotificationControl x71 x72)\<rbrace> invoke_tcb (NotificationControl x71 x72) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (SetTLSBase x81 x82)\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>?Q256 x71 x72\<rbrace> invoke_tcb (NotificationControl x71 x72) \<lbrace>\<lambda>rv. valid_sched\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x71 x72 s. \<lbrakk>ti = NotificationControl x71 x72; (invs and valid_sched and simple_sched_action and tcb_inv_wf (NotificationControl x71 x72)) s\<rbrakk> \<Longrightarrow> ?Q256 x71 x72 s
 3. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (SetTLSBase x81 x82)\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. ti = NotificationControl x71 option \<Longrightarrow> \<lbrace>?Q256 x71 option\<rbrace> invoke_tcb (NotificationControl x71 option) \<lbrace>\<lambda>rv. valid_sched\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x71 x72 s. \<lbrakk>ti = NotificationControl x71 x72; (invs and valid_sched and simple_sched_action and tcb_inv_wf (NotificationControl x71 x72)) s\<rbrakk> \<Longrightarrow> ?Q256 x71 x72 s
 3. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (SetTLSBase x81 x82)\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x71 option. \<lbrakk>ti = NotificationControl x71 option; option = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q256 x71 option\<rbrace> invoke_tcb (NotificationControl x71 option) \<lbrace>\<lambda>rv. valid_sched\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x71 option a. \<lbrakk>ti = NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q256 x71 option\<rbrace> invoke_tcb (NotificationControl x71 option) \<lbrace>\<lambda>rv. valid_sched\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>x71 x72 s. \<lbrakk>ti = NotificationControl x71 x72; (invs and valid_sched and simple_sched_action and tcb_inv_wf (NotificationControl x71 x72)) s\<rbrakk> \<Longrightarrow> ?Q256 x71 x72 s
 4. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf (SetTLSBase x81 x82)\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!