theory Finalise_R

lemma isFinalCapability_corres:
  "corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv')
          (invs and cte_wp_at ((=) cap) ptr)
          (invs' and cte_wp_at' ((=) cte) (cte_map ptr))
       (is_final_cap cap) (isFinalCapability cte)" apply (cases "final_matters' (cteCap cte)") apply simp apply (erule isFinalCapability_corres') apply (subst bind_return[symmetric],
         rule corres_symb_exec_r) apply (rule corres_no_failI) apply wp apply (clarsimp simp: in_monad is_final_cap_def simpler_gets_def) apply (wp isFinalCapability_inv)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv') (invs and cte_wp_at ((=) cap) ptr) (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (is_final_cap cap) (isFinalCapability cte) proof (prove)
goal (2 subgoals):
 1. final_matters' (cteCap cte) \<Longrightarrow> corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv') (invs and cte_wp_at ((=) cap) ptr) (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (is_final_cap cap) (isFinalCapability cte)
 2. \<not> final_matters' (cteCap cte) \<Longrightarrow> corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv') (invs and cte_wp_at ((=) cap) ptr) (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (is_final_cap cap) (isFinalCapability cte) proof (prove)
goal (2 subgoals):
 1. final_matters' (cteCap cte) \<Longrightarrow> corres (=) (invs and cte_wp_at ((=) cap) ptr) (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (is_final_cap cap) (isFinalCapability cte)
 2. \<not> final_matters' (cteCap cte) \<Longrightarrow> corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv') (invs and cte_wp_at ((=) cap) ptr) (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (is_final_cap cap) (isFinalCapability cte) proof (prove)
goal (1 subgoal):
 1. \<not> final_matters' (cteCap cte) \<Longrightarrow> corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv') (invs and cte_wp_at ((=) cap) ptr) (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (is_final_cap cap) (isFinalCapability cte) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<not> final_matters' (cteCap cte) \<Longrightarrow> corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv') (invs and cte_wp_at ((=) cap) ptr) (?Q'4 rv) (is_final_cap cap) (return rv)
 2. \<not> final_matters' (cteCap cte) \<Longrightarrow> \<lbrace>invs' and cte_wp_at' ((=) cte) (cte_map ptr)\<rbrace> isFinalCapability cte \<lbrace>?Q'4\<rbrace>
 3. \<And>s. \<lbrakk>\<not> final_matters' (cteCap cte); (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> isFinalCapability cte \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<not> final_matters' (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (isFinalCapability cte) proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<lbrakk>\<not> final_matters' (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (?Q'4 rv) (return rv)
 2. \<And>rv. \<not> final_matters' (cteCap cte) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (invs and cte_wp_at ((=) cap) ptr) s \<and> ?Q'4 rv s' \<longrightarrow> (\<forall>(r', t')\<in>fst (return rv s'). \<exists>(r, t)\<in>fst (is_final_cap cap s). (t, t') \<in> state_relation \<and> (final_matters' (cteCap cte) \<longrightarrow> r = r'))
 3. \<not> final_matters' (cteCap cte) \<Longrightarrow> \<lbrace>invs' and cte_wp_at' ((=) cte) (cte_map ptr)\<rbrace> isFinalCapability cte \<lbrace>?Q'4\<rbrace>
 4. \<And>s. \<lbrakk>\<not> final_matters' (cteCap cte); (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> isFinalCapability cte \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrakk>\<not> final_matters' (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (isFinalCapability cte) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<not> final_matters' (cteCap cte) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (invs and cte_wp_at ((=) cap) ptr) s \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (return rv s'). \<exists>(r, t)\<in>fst (is_final_cap cap s). (t, t') \<in> state_relation \<and> (final_matters' (cteCap cte) \<longrightarrow> r = r'))
 2. \<not> final_matters' (cteCap cte) \<Longrightarrow> \<lbrace>invs' and cte_wp_at' ((=) cte) (cte_map ptr)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>s. \<lbrakk>\<not> final_matters' (cteCap cte); (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> isFinalCapability cte \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<not> final_matters' (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (isFinalCapability cte) proof (prove)
goal (3 subgoals):
 1. \<not> final_matters' (cteCap cte) \<Longrightarrow> \<lbrace>invs' and cte_wp_at' ((=) cte) (cte_map ptr)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>s. \<lbrakk>\<not> final_matters' (cteCap cte); (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> isFinalCapability cte \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<not> final_matters' (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) (isFinalCapability cte) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> final_matters' (cteCap cte); True; (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) s\<rbrakk> \<Longrightarrow> (valid_mdb' and cte_wp_at' ((=) cte) ?p35) s proof (prove)
goal:
No subgoals!