theory CNodeInv_AI

lemma cap_move_has_reply_cap_neg:
  "\<lbrace>\<lambda>s. \<not> has_reply_cap t s \<and>
    cte_wp_at (weak_derived c) p s \<and>
    cte_wp_at ((=) cap.NullCap) p' s \<and>
    p \<noteq> p'\<rbrace>
   cap_move c p p' \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace>" apply (simp add: has_reply_cap_def is_reply_cap_to_def cte_wp_at_caps_of_state
              del: split_paired_All split_paired_Ex) apply (wp cap_move_caps_of_state) apply (elim conjE exE) apply (drule(1) cap_swap_no_reply_caps[where cs="caps_of_state _"]) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> has_reply_cap t s \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at ((=) NullCap) p' s \<and> p \<noteq> p'\<rbrace> cap_move c p p' \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)) \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> weak_derived c cap) \<and> caps_of_state s p' = Some NullCap \<and> p \<noteq> p'\<rbrace> cap_move c p p' \<lbrace>\<lambda>rv s. \<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)) \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> weak_derived c cap) \<and> caps_of_state s p' = Some NullCap \<and> p \<noteq> p' \<Longrightarrow> \<forall>pa cap. ((caps_of_state s)(p' \<mapsto> c, p \<mapsto> NullCap)) pa = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); caps_of_state s p' = Some NullCap; p \<noteq> p'; caps_of_state s p = Some cap; weak_derived c cap\<rbrakk> \<Longrightarrow> \<forall>pa cap. ((caps_of_state s)(p' \<mapsto> c, p \<mapsto> NullCap)) pa = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights) proof (prove)
goal (4 subgoals):
 1. \<And>s cap. \<lbrakk>\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); p \<noteq> p'; caps_of_state s p = Some cap; weak_derived c cap\<rbrakk> \<Longrightarrow> weak_derived (?c8 s cap) NullCap
 2. \<And>s cap. \<lbrakk>\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); p \<noteq> p'; caps_of_state s p = Some cap; weak_derived c cap\<rbrakk> \<Longrightarrow> weak_derived (?c'8 s cap) cap
 3. \<And>s cap. \<lbrakk>\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); p \<noteq> p'; caps_of_state s p = Some cap; weak_derived c cap\<rbrakk> \<Longrightarrow> \<forall>sl R. caps_of_state s sl \<noteq> Some (ReplyCap (?t8 s cap) False R)
 4. \<And>s cap. \<lbrakk>\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); p \<noteq> p'; caps_of_state s p = Some cap; weak_derived c cap; \<forall>sl R. ((caps_of_state s)(p' \<mapsto> ?c'8 s cap, p \<mapsto> ?c8 s cap)) sl \<noteq> Some (ReplyCap (?t8 s cap) False R)\<rbrakk> \<Longrightarrow> \<forall>pa cap. ((caps_of_state s)(p' \<mapsto> c, p \<mapsto> NullCap)) pa = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights) proof (prove)
goal:
No subgoals!