theory Finalise_AI

lemma cap_delete_one_caps_of_state:
  "\<lbrace>\<lambda>s. cte_wp_at can_fast_finalise p s
           \<longrightarrow> P ((caps_of_state s) (p \<mapsto> cap.NullCap))\<rbrace>
     cap_delete_one p
   \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: cap_delete_one_def unless_def
                   is_final_cap_def) apply (rule hoare_seq_ext [OF _ get_cap_sp]) apply (case_tac "can_fast_finalise cap") apply (wp empty_slot_caps_of_state get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state
                         fun_upd_def[symmetric]
                         fun_upd_idem) apply (simp add: fast_finalise_def2) apply wp apply (clarsimp simp: can_fast_finalise_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))\<rbrace> cap_delete_one p \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))\<rbrace> do cap <- get_cap p;
when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot p NullCap
od)
od \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrace>(\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) and cte_wp_at (\<lambda>c. c = cap) p\<rbrace> when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot p NullCap
od) \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cap. can_fast_finalise cap \<Longrightarrow> \<lbrace>(\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) and cte_wp_at (\<lambda>c. c = cap) p\<rbrace> when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot p NullCap
od) \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 2. \<And>cap. \<not> can_fast_finalise cap \<Longrightarrow> \<lbrace>(\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) and cte_wp_at (\<lambda>c. c = cap) p\<rbrace> when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot p NullCap
od) \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cap s. \<lbrakk>can_fast_finalise cap; ((\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) and cte_wp_at (\<lambda>c. c = cap) p) s\<rbrakk> \<Longrightarrow> (if cap \<noteq> NullCap then \<lambda>s. P ((caps_of_state s)(p \<mapsto> NullCap)) else (\<lambda>s. P (caps_of_state s))) s
 2. \<And>cap. \<not> can_fast_finalise cap \<Longrightarrow> \<lbrace>(\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) and cte_wp_at (\<lambda>c. c = cap) p\<rbrace> when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot p NullCap
od) \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<not> can_fast_finalise cap \<Longrightarrow> \<lbrace>(\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) and cte_wp_at (\<lambda>c. c = cap) p\<rbrace> when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot p NullCap
od) \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<not> can_fast_finalise cap \<Longrightarrow> \<lbrace>(\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) and cte_wp_at (\<lambda>c. c = cap) p\<rbrace> when (cap \<noteq> NullCap) fail \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap s. \<lbrakk>\<not> can_fast_finalise cap; ((\<lambda>s. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) and cte_wp_at (\<lambda>c. c = cap) p) s\<rbrakk> \<Longrightarrow> (if cap \<noteq> NullCap then \<lambda>_. True else (\<lambda>s. P (caps_of_state s))) s proof (prove)
goal:
No subgoals!