theory Untyped_R

lemma corres_check_no_children:
  "corres (\<lambda>x y. x = y) (cte_at slot)
     (pspace_aligned' and pspace_distinct' and valid_mdb' and
      cte_wp_at' (\<lambda>_. True) (cte_map slot))
     (const_on_failure x
        (doE z \<leftarrow> ensure_no_children slot;
             returnOk y
         odE))
     (constOnFailure x
        (doE z \<leftarrow> ensureNoChildren (cte_map slot);
             returnOk y
         odE))" apply (clarsimp simp:const_on_failure_def constOnFailure_def) apply (rule corres_guard_imp) apply (rule corres_split_catch[where E = dc and E'=dc]) apply (rule corres_guard_imp[OF corres_splitEE]) apply (rule ensureNoChildren_corres) apply simp apply (rule corres_returnOkTT) apply simp apply wp+ apply simp+ apply (clarsimp simp:dc_def,wp)+ apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) (const_on_failure x (doE z <- ensure_no_children slot;
returnOk y
odE)) (constOnFailure x (doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE)) proof (prove)
goal (1 subgoal):
 1. corres (=) (cte_wp_at (\<lambda>_. True) slot) (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) (doE z <- ensure_no_children slot;
returnOk y
odE <catch> (\<lambda>xa. return x)) (doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE <catch> const (return x)) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (doE z <- ensure_no_children slot;
returnOk y
odE <catch> (\<lambda>xa. return x)) (doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE <catch> const (return x))
 2. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres (?f4 \<oplus> (=)) ?P4 ?P'4 (doE z <- ensure_no_children slot;
returnOk y
odE) (doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE)
 2. \<And>xa ft'. ?f4 xa ft' \<Longrightarrow> corres (=) (dc xa) (dc ft') (return x) (const (return x) ft')
 3. \<lbrace>?Q4\<rbrace> doE z <- ensure_no_children slot;
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 5. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (11 subgoals):
 1. corres (?f4 \<oplus> ?r'10) ?P10 ?P'10 (ensure_no_children slot) (ensureNoChildren (cte_map slot))
 2. \<And>z za. ?r'10 z za \<Longrightarrow> corres (?f4 \<oplus> (=)) (?R10 z) (?R'10 za) (returnOk y) (returnOk y)
 3. \<lbrace>?Q10\<rbrace> ensure_no_children slot \<lbrace>?R10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> ensureNoChildren (cte_map slot) \<lbrace>?R'10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. ?P4 s \<Longrightarrow> (?P10 and ?Q10) s
 6. \<And>s. ?P'4 s \<Longrightarrow> (?P'10 and ?Q'10) s
 7. \<And>xa ft'. ?f4 xa ft' \<Longrightarrow> corres (=) (dc xa) (dc ft') (return x) (const (return x) ft')
 8. \<lbrace>?Q4\<rbrace> doE z <- ensure_no_children slot;
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 10. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (?P4 and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. cte_map slot = cte_map slot
 2. \<And>z za. dc z za \<Longrightarrow> corres (ser \<oplus> (=)) (?R10 z) (?R'10 za) (returnOk y) (returnOk y)
 3. \<lbrace>?Q10\<rbrace> ensure_no_children slot \<lbrace>?R10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> ensureNoChildren (cte_map slot) \<lbrace>?R'10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. ?P4 s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q10) s
 6. \<And>s. ?P'4 s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb' and ?Q'10) s
 7. \<And>xa ft'. ser xa ft' \<Longrightarrow> corres (=) (dc xa) (dc ft') (return x) (const (return x) ft')
 8. \<lbrace>?Q4\<rbrace> doE z <- ensure_no_children slot;
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 10. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (?P4 and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>z za. dc z za \<Longrightarrow> corres (ser \<oplus> (=)) (?R10 z) (?R'10 za) (returnOk y) (returnOk y)
 2. \<lbrace>?Q10\<rbrace> ensure_no_children slot \<lbrace>?R10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'10\<rbrace> ensureNoChildren (cte_map slot) \<lbrace>?R'10\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. ?P4 s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q10) s
 5. \<And>s. ?P'4 s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb' and ?Q'10) s
 6. \<And>xa ft'. ser xa ft' \<Longrightarrow> corres (=) (dc xa) (dc ft') (return x) (const (return x) ft')
 7. \<lbrace>?Q4\<rbrace> doE z <- ensure_no_children slot;
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (?P4 and ?Q4) s
 10. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>z za. dc z za \<Longrightarrow> y = y
 2. \<lbrace>?Q10\<rbrace> ensure_no_children slot \<lbrace>\<lambda>z _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'10\<rbrace> ensureNoChildren (cte_map slot) \<lbrace>\<lambda>za _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. ?P4 s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q10) s
 5. \<And>s. ?P'4 s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb' and ?Q'10) s
 6. \<And>xa ft'. ser xa ft' \<Longrightarrow> corres (=) (dc xa) (dc ft') (return x) (const (return x) ft')
 7. \<lbrace>?Q4\<rbrace> doE z <- ensure_no_children slot;
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (?P4 and ?Q4) s
 10. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<lbrace>?Q10\<rbrace> ensure_no_children slot \<lbrace>\<lambda>z _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>?Q'10\<rbrace> ensureNoChildren (cte_map slot) \<lbrace>\<lambda>za _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. ?P4 s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q10) s
 4. \<And>s. ?P'4 s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb' and ?Q'10) s
 5. \<And>xa ft'. ser xa ft' \<Longrightarrow> corres (=) (dc xa) (dc ft') (return x) (const (return x) ft')
 6. \<lbrace>?Q4\<rbrace> doE z <- ensure_no_children slot;
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 8. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (?P4 and ?Q4) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>s. ?P4 s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and (\<lambda>s. True \<and> True)) s
 2. \<And>s. ?P'4 s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map slot) and valid_mdb' and (\<lambda>s. True \<and> True)) s
 3. \<And>xa ft'. ser xa ft' \<Longrightarrow> corres (=) (dc xa) (dc ft') (return x) (const (return x) ft')
 4. \<lbrace>?Q4\<rbrace> doE z <- ensure_no_children slot;
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 6. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (?P4 and ?Q4) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> doE z <- ensure_no_children slot;
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> doE z <- ensureNoChildren (cte_map slot);
returnOk y
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 3. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q4) s
 4. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> ((\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<and> valid_mdb' s) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and (\<lambda>s. True \<and> True)) s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> ((\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<and> valid_mdb' s) and (\<lambda>s. True \<and> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and valid_mdb' and cte_wp_at' (\<lambda>_. True) (cte_map slot)) s \<Longrightarrow> ((\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<and> valid_mdb' s) and (\<lambda>s. True \<and> True)) s proof (prove)
goal:
No subgoals!