theory VSpacePre_AI

lemma arch_update_cap_zombies:
  "\<lbrace>\<lambda>s. cte_wp_at (is_arch_update cap) p s \<and> zombies_final s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. zombies_final s\<rbrace>" apply (simp add: zombies_final_def2 cte_wp_at_caps_of_state del: split_paired_All) apply wp apply (intro allI impI) apply (elim conjE exE) apply (simp del: split_paired_All add: is_arch_update_def split: if_split_asm) apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply simp apply (frule master_cap_obj_refs) apply (drule cap_master_cap_zombie) apply clarsimp apply (erule_tac x=pa in allE) apply (erule_tac x=p in allE) apply simp apply (frule master_cap_obj_refs) apply (drule cap_master_cap_zombie) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (is_arch_update cap) p s \<and> zombies_final s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>capa. caps_of_state s p = Some capa \<and> is_arch_update cap capa) \<and> (\<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap')\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>capa. caps_of_state s p = Some capa \<and> is_arch_update cap capa) \<and> (\<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap') \<Longrightarrow> \<forall>pa p' capa cap'. ((caps_of_state s)(p \<mapsto> cap)) pa = Some capa \<and> ((caps_of_state s)(p \<mapsto> cap)) p' = Some cap' \<and> obj_refs capa \<inter> obj_refs cap' \<noteq> {} \<and> pa \<noteq> p' \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s pa p' capa cap'. \<lbrakk>(\<exists>capa. caps_of_state s p = Some capa \<and> is_arch_update cap capa) \<and> (\<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'); ((caps_of_state s)(p \<mapsto> cap)) pa = Some capa \<and> ((caps_of_state s)(p \<mapsto> cap)) p' = Some cap' \<and> obj_refs capa \<inter> obj_refs cap' \<noteq> {} \<and> pa \<noteq> p'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; ((caps_of_state s)(p \<mapsto> cap)) pa = Some capa; ((caps_of_state s)(p \<mapsto> cap)) p' = Some cap'; obj_refs capa \<inter> obj_refs cap' \<noteq> {}; pa \<noteq> p'; caps_of_state s p = Some capaa; is_arch_update cap capaa\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (2 subgoals):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>caps_of_state s p' = Some cap'; obj_refs capa \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; caps_of_state s p = Some capaa; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; pa = p; is_arch_cap capa; cap_master_cap capa = cap_master_cap capaa; cap = capa\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap'
 2. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (2 subgoals):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>caps_of_state s p' = Some cap'; obj_refs capa \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; caps_of_state s p = Some capaa; pa = p; is_arch_cap capa; cap_master_cap capa = cap_master_cap capaa; cap = capa; \<forall>p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap'
 2. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (2 subgoals):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>caps_of_state s p' = Some cap'; obj_refs capa \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; caps_of_state s p = Some capaa; pa = p; is_arch_cap capa; cap_master_cap capa = cap_master_cap capaa; cap = capa; \<forall>cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap'
 2. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (2 subgoals):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>caps_of_state s p' = Some cap'; obj_refs capa \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; caps_of_state s p = Some capaa; pa = p; is_arch_cap capa; cap_master_cap capa = cap_master_cap capaa; cap = capa; obj_refs capaa \<inter> obj_refs cap' \<noteq> {} \<longrightarrow> \<not> is_zombie capaa \<and> \<not> is_zombie cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap'
 2. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (2 subgoals):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>caps_of_state s p' = Some cap'; obj_refs capa \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; caps_of_state s p = Some capaa; pa = p; is_arch_cap capa; cap_master_cap capa = cap_master_cap capaa; cap = capa; obj_refs capaa \<inter> obj_refs cap' \<noteq> {} \<longrightarrow> \<not> is_zombie capaa \<and> \<not> is_zombie cap'; obj_refs capa = obj_refs capaa\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap'
 2. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (2 subgoals):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>caps_of_state s p' = Some cap'; obj_refs capa \<inter> obj_refs cap' \<noteq> {}; p \<noteq> p'; caps_of_state s p = Some capaa; pa = p; is_arch_cap capa; cap = capa; obj_refs capaa \<inter> obj_refs cap' \<noteq> {} \<longrightarrow> \<not> is_zombie capaa \<and> \<not> is_zombie cap'; obj_refs capa = obj_refs capaa; is_zombie capa = is_zombie capaa\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap'
 2. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'; \<forall>p' cap cap'. caps_of_state s pa = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> pa \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'; \<forall>cap cap'. caps_of_state s pa = Some cap \<and> caps_of_state s p = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> pa \<noteq> p \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'; obj_refs capa \<inter> obj_refs capaa \<noteq> {} \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie capaa\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; pa \<noteq> p; is_arch_cap cap'; cap_master_cap cap' = cap_master_cap capaa; caps_of_state s pa = Some capa; p' = p; cap = cap'; obj_refs capa \<inter> obj_refs capaa \<noteq> {} \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie capaa; obj_refs cap' = obj_refs capaa\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal (1 subgoal):
 1. \<And>s pa p' capa cap' capaa. \<lbrakk>obj_refs capa \<inter> obj_refs cap' \<noteq> {}; caps_of_state s p = Some capaa; pa \<noteq> p; is_arch_cap cap'; caps_of_state s pa = Some capa; p' = p; cap = cap'; obj_refs capa \<inter> obj_refs capaa \<noteq> {} \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie capaa; obj_refs cap' = obj_refs capaa; is_zombie cap' = is_zombie capaa\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap' proof (prove)
goal:
No subgoals!