theory Example_Valid_State

lemma valid_kernel_mappings_s0[simp]:
  "valid_kernel_mappings s0_internal" apply (clarsimp simp: valid_kernel_mappings_def s0_internal_def ran_def
                 valid_kernel_mappings_if_pd_def split: kernel_object.splits
                                                        arch_kernel_obj.splits) apply (drule kh0_SomeD) apply (clarsimp simp: arch_state0_def kernel_mapping_slots_def) apply (erule disjE | simp add: pde_ref_def s0_ptr_defs kh0_obj_def High_pd'_def Low_pd'_def
                          split: if_split_asm pde.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_kernel_mappings s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>x3 a x r. \<lbrakk>kh0 a = Some (ArchObj (PageDirectory x3)); pde_ref (x3 x) = Some r\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts arch_state0)) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>x3 a x r. \<lbrakk>pde_ref (x3 x) = Some r; a = init_globals_frame \<and> ArchObj (PageDirectory x3) = ArchObj (DataPage False ARMSmallPage) \<or> a = init_global_pd \<and> ArchObj (PageDirectory x3) = ArchObj (PageDirectory global_pd) \<or> a = idle_tcb_ptr \<and> ArchObj (PageDirectory x3) = idle_tcb \<or> a = High_tcb_ptr \<and> ArchObj (PageDirectory x3) = High_tcb \<or> a = Low_tcb_ptr \<and> ArchObj (PageDirectory x3) = Low_tcb \<or> a = High_pt_ptr \<and> ArchObj (PageDirectory x3) = High_pt \<or> a = Low_pt_ptr \<and> ArchObj (PageDirectory x3) = Low_pt \<or> a = High_pd_ptr \<and> ArchObj (PageDirectory x3) = High_pd \<or> a = Low_pd_ptr \<and> ArchObj (PageDirectory x3) = Low_pd \<or> a = irq_cnode_ptr \<and> ArchObj (PageDirectory x3) = irq_cnode \<or> a = ntfn_ptr \<and> ArchObj (PageDirectory x3) = ntfn \<or> a = Silc_cnode_ptr \<and> ArchObj (PageDirectory x3) = Silc_cnode \<or> a = High_cnode_ptr \<and> ArchObj (PageDirectory x3) = High_cnode \<or> a = Low_cnode_ptr \<and> ArchObj (PageDirectory x3) = Low_cnode \<or> a \<in> irq_node_offs_range \<and> ArchObj (PageDirectory x3) = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> (r \<in> set (arm_global_pts arch_state0)) = (x \<in> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>x3 a x r. \<lbrakk>pde_ref (x3 x) = Some r; a = init_global_pd \<and> x3 = (\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {}) \<or> a = idle_tcb_ptr \<and> ArchObj (PageDirectory x3) = idle_tcb \<or> a = High_tcb_ptr \<and> ArchObj (PageDirectory x3) = High_tcb \<or> a = Low_tcb_ptr \<and> ArchObj (PageDirectory x3) = Low_tcb \<or> a = High_pt_ptr \<and> ArchObj (PageDirectory x3) = High_pt \<or> a = Low_pt_ptr \<and> ArchObj (PageDirectory x3) = Low_pt \<or> a = High_pd_ptr \<and> ArchObj (PageDirectory x3) = High_pd \<or> a = Low_pd_ptr \<and> ArchObj (PageDirectory x3) = Low_pd \<or> a = irq_cnode_ptr \<and> ArchObj (PageDirectory x3) = irq_cnode \<or> a = ntfn_ptr \<and> ArchObj (PageDirectory x3) = ntfn \<or> a = Silc_cnode_ptr \<and> ArchObj (PageDirectory x3) = Silc_cnode \<or> a = High_cnode_ptr \<and> ArchObj (PageDirectory x3) = High_cnode \<or> a = Low_cnode_ptr \<and> ArchObj (PageDirectory x3) = Low_cnode; UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!