theory Tcb_IF

lemma rec_del_preservation2:
  assumes "\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>"
  assumes "\<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>"
  assumes "\<And>cap b. set_cap cap b \<lbrace>Q\<rbrace>"
  assumes "\<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>"
  assumes "\<And>slot free. empty_slot slot free \<lbrace>Q\<rbrace>"
  assumes "\<And>a b. cap_swap_for_delete a b \<lbrace>Q\<rbrace>"
  assumes "\<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>"
  assumes "\<And>s. invs s \<Longrightarrow> Q s"
  assumes "\<And>s slot cap. invs s \<Longrightarrow> caps_of_state s slot = Some cap \<Longrightarrow> R cap s"
  assumes "preemption_point \<lbrace>Q\<rbrace>"
  assumes "\<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>"
  shows
    "\<lbrace>\<lambda>s :: det_state. invs s \<and> P s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace>
     rec_del call
     \<lbrace>\<lambda>r. P\<rbrace>" apply (insert assms) apply (rule_tac Q="\<lambda>s. invs s \<and> P s \<and> Q s
                                \<and> emptyable (slot_rdcall call) s
                                \<and> valid_rec_del_call call s" in hoare_pre_imp) apply simp apply (rule_tac Q="\<lambda>rv s. P s \<and> Q s" in hoare_strengthen_post) apply (rule validE_valid) apply (rule use_spec) apply (rule rec_del_preservation2' [where R=R],simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> P s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> P s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>; invs s \<and> P s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrakk> \<Longrightarrow> invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s
 2. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>; P s \<and> Q s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>; P s \<and> Q s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. invs s \<and> P s \<and> Q s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>, \<lbrace>\<lambda>rv s. P s \<and> Q s\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>; \<And>cap b. \<lbrace>Q\<rbrace> set_cap cap b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>slot free. \<lbrace>Q and P\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. P\<rbrace>; \<And>slot free. \<lbrace>Q\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. Q\<rbrace>; \<And>a b. \<lbrace>Q and P\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. P\<rbrace>; \<And>s. invs s \<Longrightarrow> Q s; \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> R cap s; \<lbrace>Q\<rbrace> preemption_point \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q and P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>; P s \<and> Q s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals!