theory Example_Valid_State

lemma valid_global_refs_s0[simp]:
  "valid_global_refs s0_internal" apply (clarsimp simp: valid_global_refs_def valid_refs_def) apply (simp add: Invariants_AI.cte_wp_at_caps_of_state) apply clarsimp apply (drule s0_caps_of_state) apply (clarsimp simp: global_refs_def s0_internal_def arch_state0_def) apply (erule disjE | simp add: cap_range_def
                     | clarsimp simp: irq_node_offs_distinct[symmetric]
                     | simp only: s0_ptr_defs, force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_refs s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>a b. cte_wp_at (\<lambda>c. global_refs s0_internal \<inter> cap_range c \<noteq> {}) (a, b) s0_internal \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<exists>cap. caps_of_state s0_internal (a, b) = Some cap \<and> global_refs s0_internal \<inter> cap_range cap \<noteq> {} \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>caps_of_state s0_internal (a, b) = Some cap; global_refs s0_internal \<inter> cap_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>global_refs s0_internal \<inter> cap_range cap \<noteq> {}; cap = NullCap \<or> ((a, b), cap) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>idle_tcb_ptr \<in> cap_range cap \<or> init_global_pd \<in> cap_range cap \<or> range (\<lambda>x. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) x << cte_level_bits)) \<inter> cap_range cap \<noteq> {}; cap = NullCap \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 (Suc 0) \<and> cap = ThreadCap Low_tcb_ptr \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 3 \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 (Suc 0) \<and> cap = ThreadCap High_tcb_ptr \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 3 \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowRead} \<or> a = Silc_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Silc_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite} \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 4 \<and> cap = NullCap \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite} \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 4 \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!