theory Tcb_DR

lemma invoke_tcb_corres:
  "\<lbrakk> t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc) \<top> (invs and valid_pdpt_objs and Tcb_AI.tcb_inv_wf t' and valid_etcbs)
     (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (clarsimp) apply (case_tac t') apply (rule corres_guard_imp [OF invoke_tcb_corres_write_regs], assumption, auto intro:invoke_tcb_rules )[1] apply (rule corres_guard_imp [OF invoke_tcb_corres_read_regs], assumption, auto intro!:invoke_tcb_rules)[1] apply (rule corres_guard_imp [OF invoke_tcb_corres_copy_regs], assumption, auto intro!:invoke_tcb_rules)[1] apply (rule corres_guard_imp [OF invoke_tcb_corres_thread_control],assumption,auto intro!:invoke_tcb_rules)[1] apply (rule corres_guard_imp [OF invoke_tcb_corres_suspend], assumption, auto intro!:invoke_tcb_rules)[1] apply (rule corres_guard_imp [OF invoke_tcb_corres_resume], assumption, auto intro!:invoke_tcb_rules)[1] apply (rename_tac option) apply (case_tac option) apply (simp only:, rule corres_guard_imp[OF invoke_tcb_corres_unbind], simp , auto intro!: invoke_tcb_rules)[1] apply (simp only:, rule corres_guard_imp[OF invoke_tcb_corres_bind], simp , auto intro!: invoke_tcb_rules)[1] apply (rule corres_guard_imp [OF invoke_tcb_corres_setTLSBase], assumption, auto intro!:invoke_tcb_rules)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t = translate_tcb_invocation t' \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t') proof (prove)
goal (1 subgoal):
 1. t = translate_tcb_invocation t' \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.WriteRegisters x11 x12 x13 x14\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x21 x22 x23 x24. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.ReadRegisters x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 3. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 5. \<And>x5. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 6. \<And>x6. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 7. \<And>x71 x72. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 8. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (7 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.ReadRegisters x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 4. \<And>x5. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 5. \<And>x6. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 6. \<And>x71 x72. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 7. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 3. \<And>x5. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 4. \<And>x6. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 5. \<And>x71 x72. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 6. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x5. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 3. \<And>x6. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 4. \<And>x71 x72. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 5. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (4 subgoals):
 1. \<And>x5. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x6. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 3. \<And>x71 x72. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 4. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x71 x72. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 3. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (2 subgoals):
 1. \<And>x71 option. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 option\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 option; option = None\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x71 option a. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 3. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (2 subgoals):
 1. \<And>x71 option a. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t')
 2. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal (1 subgoal):
 1. \<And>x81 x82. \<lbrakk>t = translate_tcb_invocation t'; t' = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb (translate_tcb_invocation t')) (Tcb_A.invoke_tcb t') proof (prove)
goal:
No subgoals!