theory CNodeInv_AI

lemma rec_del_delete_cases:
  "\<And>sl ex.
    \<lbrace>\<top> :: 'state_ext state \<Rightarrow> bool\<rbrace>
      rec_del (CTEDeleteCall sl ex)
    \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. c = cap.NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>,-" subgoal for sl ex using rec_del_abort_cases [where args="FinaliseSlotCall sl ex"] apply (subst rec_del_simps_ext, simp add: split_def) apply wp apply (rule hoare_strengthen_post [OF empty_slot_deletes]) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule use_spec, rule spec_strengthen_postE, assumption) apply (clarsimp simp: cte_wp_at_caps_of_state) apply assumption done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sl ex. \<lbrace>\<lambda>_. True\<rbrace> rec_del (CTEDeleteCall sl ex) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rec_del (CTEDeleteCall sl ex) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl\<rbrace>, - proof (prove)
using this:
case FinaliseSlotCall sl ex of FinaliseSlotCall sl ex \<Rightarrow> ?s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> | _ \<Rightarrow> True

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rec_del (CTEDeleteCall sl ex) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE p <- rec_del (FinaliseSlotCall sl ex);
y <- liftE (when (ex \<or> fst p) (empty_slot sl (snd p)));
returnOk undefined
odE \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; ex \<or> fst p\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 p\<rbrace> empty_slot sl (snd p) \<lbrace>\<lambda>y. cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl\<rbrace>
 2. (\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> \<lbrace>?P'4\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>p s. True \<and> (if ex \<or> fst p then ?Q12 p else cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; True\<rbrakk> \<Longrightarrow> ?P'4 s proof (prove)
goal (3 subgoals):
 1. \<And>p rv s. \<lbrakk>\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; ex \<or> fst p; cte_wp_at (\<lambda>c. c = NullCap) sl s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s
 2. (\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> \<lbrace>?P'4\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>p s. True \<and> (if ex \<or> fst p then \<lambda>_. True else cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; True\<rbrakk> \<Longrightarrow> ?P'4 s proof (prove)
goal (2 subgoals):
 1. (\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<Longrightarrow> \<lbrace>?P'4\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>p s. True \<and> (if ex \<or> fst p then \<lambda>_. True else cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. \<lbrakk>\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; True\<rbrakk> \<Longrightarrow> ?P'4 s proof (prove)
goal (2 subgoals):
 1. \<And>s sa r. \<lbrakk>\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; fst sa \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl r\<rbrakk> \<Longrightarrow> True \<and> (if ex \<or> fst sa then \<lambda>_. True else cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> ex \<and> is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl) r
 2. \<And>s. \<lbrakk>\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; True\<rbrakk> \<Longrightarrow> True proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> rec_del (FinaliseSlotCall sl ex) \<lbrace>\<lambda>rv s. fst rv \<or> \<not> ex \<and> cte_wp_at (\<lambda>c. is_zombie c \<and> sl \<in> fst_cte_ptrs c) sl s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; True\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!