theory TCB_DP

lemma update_thread_current_thread_inv[wp]:
  "\<lbrace>\<lambda>s. P (cdl_current_thread s)\<rbrace>
  update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. x)) \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>" apply (clarsimp simp: update_thread_def) apply (wp) apply (case_tac t) apply (clarsimp)+ apply (wp) apply (clarsimp)+ apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_thread s)\<rbrace> update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. x)) \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_thread s)\<rbrace> do t <- get_object target_tcb;
case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_object target_tcb \<lbrace>?B1\<rbrace>
 3. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (12 subgoals):
 1. \<And>t. t = Endpoint \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 2. \<And>t. t = Notification \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 3. \<And>t x3. t = Tcb x3 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 4. \<And>t x4. t = CNode x4 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 5. \<And>t x5. t = AsidPool x5 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 6. \<And>t x6. t = PageTable x6 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 7. \<And>t x7. t = PageDirectory x7 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 8. \<And>t x8. t = Frame x8 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 9. \<And>t. t = Untyped \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 10. \<And>t x10. t = IRQNode x10 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x3. \<lbrace>?B1 (Tcb x3)\<rbrace> set_object target_tcb (Tcb (x3\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 2. \<And>t x4. t = CNode x4 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 3. \<And>t x5. t = AsidPool x5 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 4. \<And>t x6. t = PageTable x6 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 5. \<And>t x7. t = PageDirectory x7 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 6. \<And>t x8. t = Frame x8 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 7. \<And>t. t = Untyped \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 8. \<And>t x10. t = IRQNode x10 \<Longrightarrow> \<lbrace>?B1 t\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 9. \<lbrace>?Q\<rbrace> get_object target_tcb \<lbrace>?B1\<rbrace>
 10. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>t x4. t = CNode x4 \<Longrightarrow> \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 2. \<And>t x5. t = AsidPool x5 \<Longrightarrow> \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 3. \<And>t x6. t = PageTable x6 \<Longrightarrow> \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 4. \<And>t x7. t = PageDirectory x7 \<Longrightarrow> \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 5. \<And>t x8. t = Frame x8 \<Longrightarrow> \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 6. \<And>t. t = Untyped \<Longrightarrow> \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 7. \<And>t x10. t = IRQNode x10 \<Longrightarrow> \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> case t of Tcb tcb \<Rightarrow> set_object target_tcb (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) | _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 8. \<lbrace>?Q\<rbrace> get_object target_tcb \<lbrace>\<lambda>a b. P (cdl_current_thread b)\<rbrace>
 9. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_object target_tcb \<lbrace>\<lambda>a b. P (cdl_current_thread b)\<rbrace>
 2. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cdl_current_thread s) \<Longrightarrow> cdl_objects s target_tcb \<noteq> None \<longrightarrow> P (cdl_current_thread s) proof (prove)
goal:
No subgoals!