theory CSpacePre_AI

lemma set_untyped_cap_as_full_is_final_cap'_neg:
  "\<lbrace>\<lambda>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. \<not> is_final_cap' cap' s\<rbrace>" apply (rule hoare_pre) apply (simp add:is_final_cap'_def2) apply (wp hoare_vcg_all_lift hoare_vcg_ex_lift) apply (rule_tac Q = "cte_wp_at Q slot"
         and Q'="cte_wp_at ((=) src_cap) src" for Q slot in P_bool_lift' ) apply (wp set_untyped_cap_as_full_cte_wp_at) apply clarsimp apply (wp set_untyped_cap_as_full_cte_wp_at_neg) apply (clarsimp simp:cte_wp_at_caps_of_state masked_as_full_def) apply (clarsimp simp:is_final_cap'_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<not> is_final_cap' cap' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<not> is_final_cap' cap' s\<rbrace>
 2. \<And>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<forall>a b. \<exists>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs cap' \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<longrightarrow> ba \<noteq> b)\<rbrace>
 2. \<And>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrace>?P7 a b aa ba\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. gen_obj_refs cap' \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<longrightarrow> ba \<noteq> b)\<rbrace>
 2. \<And>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x xa. \<exists>xb xc. ?P7 x xa xb xc s proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrace>cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r. cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba)\<rbrace>
 2. \<And>a b aa ba. \<lbrace>(\<lambda>s. \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s) and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r s. \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s\<rbrace>
 3. \<And>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x xa. \<exists>xb xc. cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (xb, xc) s = (xb = x \<longrightarrow> xc \<noteq> xa) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s. (cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) and cte_wp_at ((=) src_cap) src) s \<Longrightarrow> ((aa, ba) \<noteq> src \<and> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s \<or> (aa, ba) = src \<and> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs (masked_as_full a cap) \<noteq> {}) src s) \<and> cte_wp_at ((=) src_cap) src s
 2. \<And>a b aa ba. \<lbrace>(\<lambda>s. \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s) and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r s. \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s\<rbrace>
 3. \<And>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x xa. \<exists>xb xc. cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (xb, xc) s = (xb = x \<longrightarrow> xc \<noteq> xa) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrace>(\<lambda>s. \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s) and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>r s. \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s\<rbrace>
 2. \<And>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x xa. \<exists>xb xc. cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (xb, xc) s = (xb = x \<longrightarrow> xc \<noteq> xa) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s. ((\<lambda>s. \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s) and cte_wp_at ((=) src_cap) src) s \<Longrightarrow> ((aa, ba) \<noteq> src \<and> \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (aa, ba) s \<or> (aa, ba) = src \<and> \<not> cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs (masked_as_full a cap) \<noteq> {}) src s) \<and> cte_wp_at ((=) src_cap) src s
 2. \<And>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x xa. \<exists>xb xc. cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (xb, xc) s = (xb = x \<longrightarrow> xc \<noteq> xa) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> is_final_cap' cap' s \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<forall>x xa. \<exists>xb xc. cte_wp_at (\<lambda>a. gen_obj_refs cap' \<inter> gen_obj_refs a \<noteq> {}) (xb, xc) s = (xb = x \<longrightarrow> xc \<noteq> xa) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal:
No subgoals!