theory Example_Valid_State

lemma valid_arch_objs_s0[simp]:
  "valid_vspace_objs s0_internal" apply (clarsimp simp: valid_vspace_objs_def obj_at_def s0_internal_def) apply (drule kh0_SomeD) apply (erule disjE | clarsimp simp: addrFromPPtr_def
         | erule vs_lookupE, force simp: arch_state0_def vs_asid_refs_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao. \<lbrakk>(rs \<rhd> p) \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; kh0 p = Some (ArchObj ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao. \<lbrakk>(rs \<rhd> p) \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; p = init_globals_frame \<and> ArchObj ao = ArchObj (DataPage False ARMSmallPage) \<or> p = init_global_pd \<and> ArchObj ao = ArchObj (PageDirectory global_pd) \<or> p = idle_tcb_ptr \<and> ArchObj ao = idle_tcb \<or> p = High_tcb_ptr \<and> ArchObj ao = High_tcb \<or> p = Low_tcb_ptr \<and> ArchObj ao = Low_tcb \<or> p = High_pt_ptr \<and> ArchObj ao = High_pt \<or> p = Low_pt_ptr \<and> ArchObj ao = Low_pt \<or> p = High_pd_ptr \<and> ArchObj ao = High_pd \<or> p = Low_pd_ptr \<and> ArchObj ao = Low_pd \<or> p = irq_cnode_ptr \<and> ArchObj ao = irq_cnode \<or> p = ntfn_ptr \<and> ArchObj ao = ntfn \<or> p = Silc_cnode_ptr \<and> ArchObj ao = Silc_cnode \<or> p = High_cnode_ptr \<and> ArchObj ao = High_cnode \<or> p = Low_cnode_ptr \<and> ArchObj ao = Low_cnode \<or> p \<in> irq_node_offs_range \<and> ArchObj ao = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr> proof (prove)
goal:
No subgoals!