theory CSpace_AI

lemma set_untyped_cap_as_full_is_final_cap':
  "\<lbrace>is_final_cap' cap' and cte_wp_at ((=) src_cap) src\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. is_final_cap' cap' s\<rbrace>" apply (simp add:set_untyped_cap_as_full_def) apply (intro conjI impI) apply (wp set_cap_final_cap_at) apply (clarsimp simp:cte_wp_at_caps_of_state) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_final_cap' cap' and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> \<lbrace>is_final_cap' cap' and cte_wp_at ((=) src_cap) src\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace>) \<and> ((obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>is_final_cap' cap' and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace>) proof (prove)
goal (2 subgoals):
 1. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>is_final_cap' cap' and cte_wp_at ((=) src_cap) src\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace>
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>is_final_cap' cap' and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; (is_final_cap' cap' and cte_wp_at ((=) src_cap) src) s\<rbrakk> \<Longrightarrow> is_final_cap' cap' s \<and> cte_wp_at (\<lambda>cap''. (gen_obj_refs cap'' \<inter> gen_obj_refs cap' \<noteq> {}) = (gen_obj_refs (max_free_index_update src_cap) \<inter> gen_obj_refs cap' \<noteq> {})) src s
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>is_final_cap' cap' and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>is_final_cap' cap' and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; (is_final_cap' cap' and cte_wp_at ((=) src_cap) src) s\<rbrakk> \<Longrightarrow> is_final_cap' cap' s proof (prove)
goal:
No subgoals!