theory Tcb_R

lemma tcbinv_invs':
  "\<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti\<rbrace>
     invokeTCB ti
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (case_tac ti, simp_all only:) apply (simp add: invokeTCB_def) apply wp apply (clarsimp simp: invs'_def valid_state'_def
                         dest!: global'_no_ex_cap) apply (simp add: invokeTCB_def) apply (wp restart_invs') apply (clarsimp simp: invs'_def valid_state'_def
                        dest!: global'_no_ex_cap) apply (wp tc_invs') apply (clarsimp split: option.split dest!: isCapDs) apply (wp writereg_invs' readreg_invs' copyreg_invs' tcbntfn_invs'
             | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' ti\<rbrace> invokeTCB ti \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1. ti = tcbinvocation.Suspend x1 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Suspend x1)\<rbrace> invokeTCB (tcbinvocation.Suspend x1) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Resume x2)\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1. ti = tcbinvocation.Suspend x1 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x1 and ex_nonz_cap_to' x1)\<rbrace> liftE (do y <- ThreadDecls_H.suspend x1;
return []
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Resume x2)\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1 s. \<lbrakk>ti = tcbinvocation.Suspend x1; (invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x1 and ex_nonz_cap_to' x1)) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and tcb_at' x1 and (\<lambda>s. x1 \<noteq> ksIdleThread s)) s
 2. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Resume x2)\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.Resume x2)\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2. ti = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x2 and ex_nonz_cap_to' x2)\<rbrace> liftE (do y <- ThreadDecls_H.restart x2;
return []
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2 s. \<lbrakk>ti = tcbinvocation.Resume x2; (invs' and sch_act_simple and ct_in_state' runnable' and (tcb_at' x2 and ex_nonz_cap_to' x2)) s\<rbrakk> \<Longrightarrow> (invs' and ex_nonz_cap_to' x2 and (\<lambda>s. x2 \<noteq> ksIdleThread s)) s
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 x38. ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 x38 s. \<lbrakk>ti = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38; (invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38)) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and tcb_at' x31 and ex_nonz_cap_to' x31 and K (valid_option_prio x35 \<and> valid_option_prio x34) and (case x36 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case x36 of None \<Rightarrow> True | Some x \<Rightarrow> (isCNodeCap \<circ> fst) x) and (case x37 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case x37 of None \<Rightarrow> True | Some x \<Rightarrow> (isValidVTableRoot \<circ> fst) x) and (case case x38 of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_cap' x) and K (case case x38 of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> True | Some x \<Rightarrow> isArchObjectCap x) and K (case x38 of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned msg_align_bits \<circ> fst) x)) s
 2. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42. ti = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.NotificationControl x41 x42)\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x51 x52 x53 x54. ti = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.WriteRegisters x51 x52 x53 x54)\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x61 x62 x63 x64. ti = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.ReadRegisters x61 x62 x63 x64)\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x71 x72 x73 x74 x75 x76 x77. ti = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77)\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>x81 x82. ti = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and ct_in_state' runnable' and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!