theory ArchTcb_AI

lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
  "\<lbrace>no_cap_to_obj_dr_emp cap\<rbrace>
     cap_delete slot
   \<lbrace>\<lambda>rv. no_cap_to_obj_dr_emp cap\<rbrace>" apply (simp add: cap_delete_def
                   no_cap_to_obj_with_diff_ref_ran_caps_form) apply wp apply (rule use_spec) apply (rule rec_del_all_caps_in_range) apply (simp add: table_cap_ref_def[simplified, split_simps cap.split]
              | rule obj_ref_none_no_asid)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_dr_emp cap\<rbrace> cap_delete slot \<lbrace>\<lambda>rv. no_cap_to_obj_dr_emp cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap\<rbrace> doE y <- rec_del (CTEDeleteCall slot True);
returnOk ()
odE \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> rec_del (CTEDeleteCall slot True) \<lbrace>\<lambda>y a. \<forall>cp\<in>ran (caps_of_state a). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap\<rbrace>
 2. \<And>s. \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>?Q\<rbrace> rec_del (CTEDeleteCall slot True) \<lbrace>\<lambda>y a. \<forall>cp\<in>ran (caps_of_state a). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap\<rbrace>
 2. \<And>s. \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>s. obj_refs NullCap = obj_refs cap \<longrightarrow> table_cap_ref NullCap = table_cap_ref cap
 2. \<And>s x n zt. obj_refs (ThreadCap x) = obj_refs cap \<longrightarrow> table_cap_ref (ThreadCap x) = table_cap_ref cap \<Longrightarrow> obj_refs (Zombie x zt n) = obj_refs cap \<longrightarrow> table_cap_ref (Zombie x zt n) = table_cap_ref cap
 3. \<And>s x y gd n zt. obj_refs (CNodeCap x y gd) = obj_refs cap \<longrightarrow> table_cap_ref (CNodeCap x y gd) = table_cap_ref cap \<Longrightarrow> obj_refs (Zombie x zt n) = obj_refs cap \<longrightarrow> table_cap_ref (Zombie x zt n) = table_cap_ref cap
 4. \<And>s x zt zt' n m. obj_refs (Zombie x zt n) = obj_refs cap \<longrightarrow> table_cap_ref (Zombie x zt n) = table_cap_ref cap \<Longrightarrow> obj_refs (Zombie x zt' m) = obj_refs cap \<longrightarrow> table_cap_ref (Zombie x zt' m) = table_cap_ref cap
 5. \<And>s. \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap \<Longrightarrow> \<forall>cp\<in>ran (caps_of_state s). obj_refs cp = obj_refs cap \<longrightarrow> table_cap_ref cp = table_cap_ref cap proof (prove)
goal:
No subgoals!