theory Finalise_DR

lemma remove_cdt_pt_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 pt_page_relation a pg_id ptr UNIV) 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_pt_slot]) apply (rule_tac F="rv = ()" in corres_gen_asm) unfolding K_bind_def apply clarsimp apply (assumption) apply (simp|wp)+ apply (drule_tac x = s in meta_spec) apply (clarsimp simp:pt_page_relation_def dest!:page_table_at_rev) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 APageTable) 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 pt_page_relation a pg_id ptr UNIV) s; dc rv rv'; rv = ()\<rbrakk> \<Longrightarrow> dcorres dc (?P12 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 pt_page_relation a pg_id ptr UNIV) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> remove_parent (a, aptr) \<lbrace>\<lambda>rv. ?P12 rv and (\<lambda>s. rv = ())\<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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 APageTable) 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 pt_page_relation a pg_id ptr UNIV) s; dc rv rv'; rv = ()\<rbrakk> \<Longrightarrow> dcorres dc (?P12 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 pt_page_relation a pg_id ptr UNIV) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> remove_parent (a, aptr) \<lbrace>\<lambda>rv. ?P12 rv and (\<lambda>s. rv = ())\<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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 APageTable) a and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv'. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> valid_idle s \<and> pt_page_relation a pg_id ptr UNIV s\<rbrakk> \<Longrightarrow> dcorres dc (?P12 ()) (?R'6 rv') (g ()) 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 pt_page_relation a pg_id ptr UNIV) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> remove_parent (a, aptr) \<lbrace>\<lambda>rv. ?P12 rv and (\<lambda>s. rv = ())\<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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 pt_page_relation a pg_id ptr UNIV) 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 APageTable) a and ?Q'6) s proof (prove)
goal (4 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 pt_page_relation a pg_id ptr UNIV) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> remove_parent (a, aptr) \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = ())\<rbrace>
 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 pt_page_relation a pg_id ptr UNIV) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6\<rbrace> return ?b \<lbrace>\<lambda>rv'. Q\<rbrace>
 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 pt_page_relation a pg_id ptr UNIV) s; P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 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 pt_page_relation a pg_id ptr UNIV) 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 APageTable) a and ?Q'6) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; \<And>s. Q s \<longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> valid_idle s \<and> pt_page_relation a pg_id ptr UNIV s; Q s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) a s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>dcorres dc (\<lambda>_. True) Q (g ()) f; Q s; Q s \<longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> valid_idle s \<and> pt_page_relation a pg_id ptr UNIV s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) a s proof (prove)
goal:
No subgoals!