theory Finalise_DR

lemma remove_cdt_pd_slot_exec:
  "\<lbrakk>dcorres dc \<top> Q (g ()) f;
   \<And>s. Q s\<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and page_directory_at a) s\<rbrakk>
    \<Longrightarrow> dcorres dc P Q
    (remove_parent (a ,aptr) >>= g) f" apply (rule corres_dummy_return_pr) apply (rule corres_guard_imp) apply (rule corres_split[OF dummy_remove_cdt_pd_slot]) unfolding K_bind_def apply (simp|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s\<rbrakk> \<Longrightarrow> dcorres dc P Q (remove_parent (a, aptr) >>= g) f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s\<rbrakk> \<Longrightarrow> dcorres dc P Q (remove_parent (a, aptr) >>= g) (do return ?b;
f
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s\<rbrakk> \<Longrightarrow> dcorres dc ?Q2 ?Q'2 (remove_parent (a, aptr) >>= g) (do return ?b;
f
od)
 2. \<And>s. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s; Q s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (g rv) (K_bind f rv')
 2. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> remove_parent (a, aptr) \<lbrace>?R6\<rbrace>
 3. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> return ?b \<lbrace>?R'6\<rbrace>
 4. \<And>s. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s; P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s; Q s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (g rv) f
 2. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> remove_parent (a, aptr) \<lbrace>?R6\<rbrace>
 3. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> return ?b \<lbrace>?R'6\<rbrace>
 4. \<And>s. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s; P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s; Q s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a and ?Q'6) s proof (prove)
goal:
No subgoals!