theory ArchCSpace_AI

lemma set_cap_valid_arch_caps_simple:
  "\<lbrace>\<lambda>s. valid_arch_caps s
      \<and> valid_objs s
      \<and> cte_wp_at (Not o is_arch_cap) ptr s
      \<and> (obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap)
      \<and> \<not> (is_arch_cap cap)\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" apply (wp ARM.set_cap_valid_arch_caps) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule(1) caps_of_state_valid_cap) apply (rename_tac cap') apply (subgoal_tac "\<forall>x \<in> {cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x") apply simp apply (rule conjI) apply (clarsimp simp: ARM.vs_cap_ref_def is_cap_simps) apply (erule impCE) apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
                          cte_wp_at_caps_of_state
                          ARM.obj_ref_none_no_asid) apply (rule ARM.no_cap_to_obj_with_diff_ref_triv, simp_all) apply (rule ccontr, clarsimp simp: ARM.table_cap_ref_def is_cap_simps) apply (auto simp: ARM.is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_arch_caps s \<and> valid_objs s \<and> cte_wp_at (Not \<circ> is_arch_cap) ptr s \<and> (obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap) \<and> \<not> is_arch_cap cap\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_caps s \<and> valid_objs s \<and> cte_wp_at (Not \<circ> is_arch_cap) ptr s \<and> (obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap) \<and> \<not> is_arch_cap cap \<Longrightarrow> valid_arch_caps s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> ARM.vs_cap_ref cap' = Some vref \<longrightarrow> ARM.vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> ARM.reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<and> (ARM.is_pt_cap cap \<or> ARM.is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pt_cap cap \<or> ARM.is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> ARM.is_pt_cap cap \<and> ARM.is_pt_cap oldcap \<or> ARM.is_pd_cap cap \<and> ARM.is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap cap' \<or> ARM.is_pt_cap cap \<and> ARM.is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some capa; \<not> is_arch_cap capa\<rbrakk> \<Longrightarrow> (\<forall>vref. ARM.vs_cap_ref capa = Some vref \<longrightarrow> ARM.vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> ARM.reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<and> (ARM.is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pt_cap cap \<longrightarrow> (ARM.is_pt_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap capa \<or> ARM.is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = ptr)) \<and> (ARM.is_pd_cap cap \<longrightarrow> (ARM.is_pt_cap cap \<and> ARM.is_pt_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<and> (ARM.is_pd_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (ARM.is_pd_cap capa \<or> ARM.is_pt_cap cap \<and> ARM.is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some capa; \<not> is_arch_cap capa; s \<turnstile> capa\<rbrakk> \<Longrightarrow> (\<forall>vref. ARM.vs_cap_ref capa = Some vref \<longrightarrow> ARM.vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> ARM.reachable_pg_cap capa s \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<and> (ARM.is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pt_cap cap \<longrightarrow> (ARM.is_pt_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap capa \<or> ARM.is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = ptr)) \<and> (ARM.is_pd_cap cap \<longrightarrow> (ARM.is_pt_cap cap \<and> ARM.is_pt_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<and> (ARM.is_pd_cap capa \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid capa = None) \<longrightarrow> obj_refs capa \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (ARM.is_pd_cap capa \<or> ARM.is_pt_cap cap \<and> ARM.is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> (\<forall>vref. ARM.vs_cap_ref cap' = Some vref \<longrightarrow> ARM.vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> ARM.reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<and> (ARM.is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pt_cap cap \<longrightarrow> (ARM.is_pt_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap capa \<or> ARM.is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = ptr)) \<and> (ARM.is_pd_cap cap \<longrightarrow> (ARM.is_pt_cap cap \<and> ARM.is_pt_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<and> (ARM.is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (ARM.is_pd_cap capa \<or> ARM.is_pt_cap cap \<and> ARM.is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = ptr)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<forall>x\<in>{cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x\<rbrakk> \<Longrightarrow> (\<forall>vref. ARM.vs_cap_ref cap' = Some vref \<longrightarrow> ARM.vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> ARM.reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<and> (ARM.is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (ARM.second_level_tables (arch_state s)))) r s)) \<and> (ARM.is_pt_cap cap \<longrightarrow> (ARM.is_pt_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (ARM.is_pd_cap cap \<and> ARM.is_pd_cap capa \<or> ARM.is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = ptr)) \<and> (ARM.is_pd_cap cap \<longrightarrow> (ARM.is_pt_cap cap \<and> ARM.is_pt_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<and> (ARM.is_pd_cap cap' \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid cap' = None) \<longrightarrow> obj_refs cap' \<noteq> obj_refs cap) \<longrightarrow> (\<forall>a b. (\<exists>capa. caps_of_state s (a, b) = Some capa \<and> obj_refs capa = obj_refs cap \<and> (ARM.is_pd_cap capa \<or> ARM.is_pt_cap cap \<and> ARM.is_pt_cap capa) \<and> (cap_asid cap = None \<or> cap_asid capa = None)) \<longrightarrow> (a, b) = ptr))
 2. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> \<forall>x\<in>{cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x proof (prove)
goal (2 subgoals):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap'\<rbrakk> \<Longrightarrow> (\<forall>vref. ARM.vs_cap_ref cap' = Some vref \<longrightarrow> ARM.vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> ARM.reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s
 2. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> \<forall>x\<in>{cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x proof (prove)
goal (3 subgoals):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap'\<rbrakk> \<Longrightarrow> \<forall>vref. ARM.vs_cap_ref cap' = Some vref \<longrightarrow> ARM.vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> ARM.reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)
 2. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap'\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap {ptr} s
 3. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> \<forall>x\<in>{cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x proof (prove)
goal (2 subgoals):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap'\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap {ptr} s
 2. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> \<forall>x\<in>{cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x proof (prove)
goal (3 subgoals):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap'; \<not> obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap {ptr} s
 2. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap'; s \<turnstile> cap\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap {ptr} s
 3. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> \<forall>x\<in>{cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x proof (prove)
goal (2 subgoals):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap'; s \<turnstile> cap\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap {ptr} s
 2. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> \<forall>x\<in>{cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x proof (prove)
goal (2 subgoals):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'; \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap'; s \<turnstile> cap\<rbrakk> \<Longrightarrow> table_cap_ref cap = None
 2. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap' proof (prove)
goal (1 subgoal):
 1. \<And>s cap'. \<lbrakk>valid_arch_caps s; valid_objs s; obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap; \<not> is_arch_cap cap; caps_of_state s ptr = Some cap'; \<not> is_arch_cap cap'; s \<turnstile> cap'\<rbrakk> \<Longrightarrow> \<not> ARM.is_pt_cap cap \<and> \<not> ARM.is_pd_cap cap \<and> \<not> ARM.is_pt_cap cap' \<and> \<not> ARM.is_pd_cap cap' proof (prove)
goal:
No subgoals!