theory Finalise_AI

lemma (in Finalise_AI_1) finalise_cap_cases:
  "\<lbrace>\<lambda>(s :: 'a state). final \<longrightarrow> is_final_cap' cap s
         \<and> cte_wp_at ((=) cap) slot s\<rbrace>
     finalise_cap cap final
   \<lbrace>\<lambda>rv (s :: 'a state). fst rv = cap.NullCap
            \<and> snd rv = (if final then cap_cleanup_opt cap else NullCap)
            \<and> (snd rv \<noteq> NullCap \<longrightarrow> is_final_cap' cap s)
     \<or>
       is_zombie (fst rv) \<and> is_final_cap' cap s
        \<and> is_final_cap' (fst rv) s
        \<and> snd rv = NullCap
        \<and> appropriate_cte_cap (fst rv) = appropriate_cte_cap cap
        \<and> cte_refs (fst rv) = cte_refs cap
        \<and> gen_obj_refs (fst rv) = gen_obj_refs cap
        \<and> obj_size (fst rv) = obj_size cap
        \<and> fst_cte_ptrs (fst rv) = fst_cte_ptrs cap
        \<and> vs_cap_ref cap = None\<rbrace>" apply (rule hoare_strengthen_post,
         rule finalise_cap_cases1) apply (erule disjEI) apply (auto simp: is_final_cap'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. final \<longrightarrow> is_final_cap' cap s \<and> cte_wp_at ((=) cap) slot s\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv s. fst rv = NullCap \<and> snd rv = (if final then cap_cleanup_opt cap else NullCap) \<and> (snd rv \<noteq> NullCap \<longrightarrow> is_final_cap' cap s) \<or> is_zombie (fst rv) \<and> is_final_cap' cap s \<and> is_final_cap' (fst rv) s \<and> snd rv = NullCap \<and> appropriate_cte_cap (fst rv) = appropriate_cte_cap cap \<and> cte_refs (fst rv) = cte_refs cap \<and> gen_obj_refs (fst rv) = gen_obj_refs cap \<and> obj_size (fst rv) = obj_size cap \<and> fst_cte_ptrs (fst rv) = fst_cte_ptrs cap \<and> vs_cap_ref cap = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. fst rv = NullCap \<and> snd rv = (if final then cap_cleanup_opt cap else NullCap) \<and> (snd rv \<noteq> NullCap \<longrightarrow> is_final_cap' cap s) \<or> is_zombie (fst rv) \<and> is_final_cap' cap s \<and> snd rv = NullCap \<and> appropriate_cte_cap (fst rv) = appropriate_cte_cap cap \<and> cte_refs (fst rv) = cte_refs cap \<and> gen_obj_refs (fst rv) = gen_obj_refs cap \<and> obj_size (fst rv) = obj_size cap \<and> fst_cte_ptrs (fst rv) = fst_cte_ptrs cap \<and> vs_cap_ref cap = None \<Longrightarrow> fst rv = NullCap \<and> snd rv = (if final then cap_cleanup_opt cap else NullCap) \<and> (snd rv \<noteq> NullCap \<longrightarrow> is_final_cap' cap s) \<or> is_zombie (fst rv) \<and> is_final_cap' cap s \<and> is_final_cap' (fst rv) s \<and> snd rv = NullCap \<and> appropriate_cte_cap (fst rv) = appropriate_cte_cap cap \<and> cte_refs (fst rv) = cte_refs cap \<and> gen_obj_refs (fst rv) = gen_obj_refs cap \<and> obj_size (fst rv) = obj_size cap \<and> fst_cte_ptrs (fst rv) = fst_cte_ptrs cap \<and> vs_cap_ref cap = None proof (prove)
goal (2 subgoals):
 1. \<And>rv s. fst rv = NullCap \<and> snd rv = (if final then cap_cleanup_opt cap else NullCap) \<and> (snd rv \<noteq> NullCap \<longrightarrow> is_final_cap' cap s) \<Longrightarrow> fst rv = NullCap \<and> snd rv = (if final then cap_cleanup_opt cap else NullCap) \<and> (snd rv \<noteq> NullCap \<longrightarrow> is_final_cap' cap s)
 2. \<And>rv s. is_zombie (fst rv) \<and> is_final_cap' cap s \<and> snd rv = NullCap \<and> appropriate_cte_cap (fst rv) = appropriate_cte_cap cap \<and> cte_refs (fst rv) = cte_refs cap \<and> gen_obj_refs (fst rv) = gen_obj_refs cap \<and> obj_size (fst rv) = obj_size cap \<and> fst_cte_ptrs (fst rv) = fst_cte_ptrs cap \<and> vs_cap_ref cap = None \<Longrightarrow> is_zombie (fst rv) \<and> is_final_cap' cap s \<and> is_final_cap' (fst rv) s \<and> snd rv = NullCap \<and> appropriate_cte_cap (fst rv) = appropriate_cte_cap cap \<and> cte_refs (fst rv) = cte_refs cap \<and> gen_obj_refs (fst rv) = gen_obj_refs cap \<and> obj_size (fst rv) = obj_size cap \<and> fst_cte_ptrs (fst rv) = fst_cte_ptrs cap \<and> vs_cap_ref cap = None proof (prove)
goal:
No subgoals!