theory CSpaceInv_AI

lemma set_cap_iflive:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>p'\<in>(zobj_refs cap' - zobj_refs cap). obj_at (Not \<circ> live) p' s) p s
        \<and> if_live_then_nonz_cap s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>" apply (simp add: if_live_then_nonz_cap_def) apply (simp only: imp_conv_disj) apply (rule hoare_pre, wp hoare_vcg_all_lift hoare_vcg_disj_lift set_cap_cap_to) apply (clarsimp simp: cte_wp_at_def) apply (rule ccontr) apply (drule bspec) apply simp apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) p s \<and> if_live_then_nonz_cap s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) p s \<and> (\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) p s \<and> (\<forall>ptr. \<not> obj_at live ptr s \<or> ex_nonz_cap_to ptr s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> obj_at live ptr s \<or> ex_nonz_cap_to ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>cap'. \<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) p s \<and> (\<forall>ptr. \<not> obj_at live ptr s \<or> ex_nonz_cap_to ptr s) \<Longrightarrow> \<forall>x. \<not> obj_at live x s \<or> cte_wp_at (\<lambda>cap'. x \<notin> zobj_refs cap' - zobj_refs cap) p s \<and> ex_nonz_cap_to x s proof (prove)
goal (1 subgoal):
 1. \<And>s x capa. \<lbrakk>\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s; fst (get_cap p s) = {(capa, s)}; \<forall>p'\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p' s; obj_at live x s; x \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> x \<in> zobj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>s x capa. \<lbrakk>\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s; fst (get_cap p s) = {(capa, s)}; \<forall>p'\<in>zobj_refs capa - zobj_refs cap. obj_at (Not \<circ> live) p' s; obj_at live x s; x \<in> zobj_refs capa; x \<notin> zobj_refs cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s x capa. \<lbrakk>\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s; fst (get_cap p s) = {(capa, s)}; obj_at live x s; x \<in> zobj_refs capa; x \<notin> zobj_refs cap\<rbrakk> \<Longrightarrow> ?p'17 s x capa \<in> zobj_refs capa - zobj_refs cap
 2. \<And>s x capa. \<lbrakk>\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s; fst (get_cap p s) = {(capa, s)}; obj_at live x s; x \<in> zobj_refs capa; x \<notin> zobj_refs cap; obj_at (Not \<circ> live) (?p'17 s x capa) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x capa. \<lbrakk>\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s; fst (get_cap p s) = {(capa, s)}; obj_at live x s; x \<in> zobj_refs capa; x \<notin> zobj_refs cap; obj_at (Not \<circ> live) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!