kings-crown/FVELER_Isabelle huggingface dataset:
theory Example_Valid_State

lemma domains_of_state_s0[simp]:
  "domains_of_state s0_internal = {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}" apply(rule equalityI) apply(rule subsetI) apply clarsimp apply (erule domains_of_state_aux.cases) apply (clarsimp simp: s0_internal_def exst0_def ekh0_obj_def split: if_split_asm) apply clarsimp apply (force simp: s0_internal_def exst0_def ekh0_obj_def intro: domains_of_state_aux.domtcbs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domains_of_state s0_internal = {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)} proof (prove)
goal (2 subgoals):
 1. domains_of_state s0_internal \<subseteq> {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}
 2. {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)} \<subseteq> domains_of_state s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> domains_of_state s0_internal \<Longrightarrow> x \<in> {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}
 2. {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)} \<subseteq> domains_of_state s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> domains_of_state s0_internal; a = High_tcb_ptr \<longrightarrow> b \<noteq> High_domain; a = idle_tcb_ptr \<longrightarrow> b \<noteq> default_domain\<rbrakk> \<Longrightarrow> a = Low_tcb_ptr \<and> b = Low_domain
 2. {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)} \<subseteq> domains_of_state s0_internal proof (prove)
goal (2 subgoals):
 1. \<And>a b ptr etcb d. \<lbrakk>a = High_tcb_ptr \<longrightarrow> b \<noteq> High_domain; a = idle_tcb_ptr \<longrightarrow> b \<noteq> default_domain; a = ptr; b = d; ekheap s0_internal ptr = Some etcb; d = tcb_domain etcb\<rbrakk> \<Longrightarrow> a = Low_tcb_ptr \<and> b = Low_domain
 2. {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)} \<subseteq> domains_of_state s0_internal proof (prove)
goal (1 subgoal):
 1. {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)} \<subseteq> domains_of_state s0_internal proof (prove)
goal (1 subgoal):
 1. (High_tcb_ptr, High_domain) \<in> domains_of_state s0_internal \<and> (Low_tcb_ptr, Low_domain) \<in> domains_of_state s0_internal \<and> (idle_tcb_ptr, default_domain) \<in> domains_of_state s0_internal proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma Sys1_pas_cur_domain:
  "pas_cur_domain Sys1PAS s0_internal" by (simp add: s0_internal_def exst0_def Sys1PAS_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_cur_domain Sys1PAS s0_internal
theory Example_Valid_State

lemma Sys1_current_subject_idemp:
  "Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr> = Sys1PAS" apply (simp add: Sys1PAS_def s0_internal_def exst0_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr> = Sys1PAS proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma pasMaySendIrqs_Sys1PAS[simp]:
  "pasMaySendIrqs Sys1PAS = False" by(auto simp: Sys1PAS_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasMaySendIrqs Sys1PAS = False
theory Example_Valid_State

lemma Sys1_pas_domains_distinct:
  "pas_domains_distinct Sys1PAS" apply (clarsimp simp: Sys1PAS_def pas_domains_distinct_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_domains_distinct Sys1PAS proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma Sys1_pas_wellformed_noninterference:
  "pas_wellformed_noninterference Sys1PAS" apply (simp add: pas_wellformed_noninterference_def) apply (intro conjI ballI allI) apply (blast intro: Sys1_wellformed) apply (clarsimp simp: Sys1PAS_def policy_wellformed_def Sys1AuthGraph_def) apply (rule Sys1_pas_domains_distinct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_wellformed_noninterference Sys1PAS proof (prove)
goal (1 subgoal):
 1. (\<forall>l\<in>range (pasObjectAbs Sys1PAS) \<union> \<Union> (range (pasDomainAbs Sys1PAS)) - {SilcLabel}. policy_wellformed (pasPolicy Sys1PAS) False (range (pasIRQAbs Sys1PAS)) l) \<and> (\<forall>d. SilcLabel \<notin> pasDomainAbs Sys1PAS d) \<and> pas_domains_distinct Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>l. l \<in> range (pasObjectAbs Sys1PAS) \<union> \<Union> (range (pasDomainAbs Sys1PAS)) - {SilcLabel} \<Longrightarrow> policy_wellformed (pasPolicy Sys1PAS) False (range (pasIRQAbs Sys1PAS)) l
 2. \<And>d. SilcLabel \<notin> pasDomainAbs Sys1PAS d
 3. pas_domains_distinct Sys1PAS proof (prove)
goal (2 subgoals):
 1. \<And>d. SilcLabel \<notin> pasDomainAbs Sys1PAS d
 2. pas_domains_distinct Sys1PAS proof (prove)
goal (1 subgoal):
 1. pas_domains_distinct Sys1PAS proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma only_timer_irq_s0:
  "only_timer_irq timer_irq s0_internal" apply (clarsimp simp: only_timer_irq_def s0_internal_def irq_is_recurring_def is_irq_at_def
                        irq_at_def Let_def irq_oracle_def machine_state0_def timer_irq_def) apply presburger done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_timer_irq timer_irq s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>n. \<exists>m. (n + m) mod 10 = 0 proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma domain_sep_inv_s0:
  "domain_sep_inv False s0_internal s0_internal" apply (clarsimp simp: domain_sep_inv_def) apply (force dest: cte_wp_at_caps_of_state' s0_caps_of_state
        | rule conjI allI | clarsimp simp: s0_internal_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain_sep_inv False s0_internal s0_internal proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s0_internal) \<and> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s0_internal \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s0_internal \<and> interrupt_states s0_internal irq \<noteq> IRQSignal \<and> interrupt_states s0_internal irq \<noteq> IRQReserved) proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma only_timer_irq_inv_s0:
  "only_timer_irq_inv timer_irq s0_internal s0_internal" by (simp add: only_timer_irq_inv_def only_timer_irq_s0 domain_sep_inv_s0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_timer_irq_inv timer_irq s0_internal s0_internal
theory Example_Valid_State

lemma Sys1_guarded_pas_domain:
  "guarded_pas_domain Sys1PAS s0_internal" by (clarsimp simp: guarded_pas_domain_def Sys1PAS_def s0_internal_def
                     exst0_def Sys1AgentMap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guarded_pas_domain Sys1PAS s0_internal
theory Example_Valid_State

lemma well_formed_cnode_n_s0_caps[simp]:
  "well_formed_cnode_n 10 High_caps"
  "well_formed_cnode_n 10 Low_caps"
  "well_formed_cnode_n 10 Silc_caps"
  "\<not> well_formed_cnode_n 10 [[] \<mapsto> NullCap]" apply ((force simp: High_caps_def Low_caps_def Silc_caps_def well_formed_cnode_n_def
                  the_nat_to_bl_def nat_to_bl_def dom_empty_cnode)+)[3] apply (clarsimp simp: well_formed_cnode_n_def) apply (drule eqset_imp_iff[where x="[]"]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (well_formed_cnode_n 10 High_caps &&& well_formed_cnode_n 10 Low_caps) &&& well_formed_cnode_n 10 Silc_caps &&& \<not> well_formed_cnode_n 10 [[] \<mapsto> NullCap] proof (prove)
goal (1 subgoal):
 1. \<not> well_formed_cnode_n 10 [[] \<mapsto> NullCap] proof (prove)
goal (1 subgoal):
 1. {[]} = {x. length x = 10} \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. ([] \<in> {[]}) = ([] \<in> {x. length x = 10}) \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma valid_caps_s0[simp]:
  "s0_internal \<turnstile> ThreadCap Low_tcb_ptr"
  "s0_internal \<turnstile> ThreadCap High_tcb_ptr"
  "s0_internal \<turnstile> CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2)"
  "s0_internal \<turnstile> CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2)"
  "s0_internal \<turnstile> CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl_10 2)"
  "s0_internal \<turnstile> ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))"
  "s0_internal \<turnstile> ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))"
  "s0_internal \<turnstile> NotificationCap ntfn_ptr 0 {AllowWrite}"
  "s0_internal \<turnstile> NotificationCap ntfn_ptr 0 {AllowRead}"
  "s0_internal \<turnstile> ReplyCap Low_tcb_ptr True {AllowGrant,AllowWrite}"
  "s0_internal \<turnstile> ReplyCap High_tcb_ptr True {AllowGrant,AllowWrite}" by (simp_all add: valid_cap_def s0_internal_def s0_ptr_defs cap_aligned_def is_aligned_def
                       word_bits_def cte_level_bits_def the_nat_to_bl_def
                       nat_to_bl_def Low_asid_def High_asid_def asid_low_bits_def asid_bits_def
                       obj_at_def kh0_def kh0_obj_def is_tcb_def is_cap_table_def a_type_def
                       is_ntfn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((s0_internal \<turnstile> ThreadCap Low_tcb_ptr &&& s0_internal \<turnstile> ThreadCap High_tcb_ptr) &&& s0_internal \<turnstile> CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) &&& s0_internal \<turnstile> CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) &&& s0_internal \<turnstile> CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)) &&& (s0_internal \<turnstile> ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) &&& s0_internal \<turnstile> ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) &&& s0_internal \<turnstile> NotificationCap ntfn_ptr 0 {AllowWrite}) &&& s0_internal \<turnstile> NotificationCap ntfn_ptr 0 {AllowRead} &&& s0_internal \<turnstile> ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite} &&& s0_internal \<turnstile> ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}
theory Example_Valid_State

lemma pspace_aligned_s0:
  "pspace_aligned s0_internal" apply (clarsimp simp: pspace_aligned_def s0_internal_def) apply (drule kh0_SomeD) apply (erule disjE
         | (subst is_aligned_def,
           fastforce simp: s0_ptr_defs cte_level_bits_def kh0_def kh0_obj_def))+ apply (clarsimp simp: cte_level_bits_def) apply (drule irq_node_offs_range_correct) apply (clarsimp simp: s0_ptr_defs cte_level_bits_def) apply (rule is_aligned_add[OF _ is_aligned_shift]) apply (simp add: is_aligned_def s0_ptr_defs cte_level_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_aligned s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>x y. kh0 x = Some y \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = init_globals_frame \<and> y = ArchObj (DataPage False ARMSmallPage) \<or> x = init_global_pd \<and> y = ArchObj (PageDirectory global_pd) \<or> x = idle_tcb_ptr \<and> y = idle_tcb \<or> x = High_tcb_ptr \<and> y = High_tcb \<or> x = Low_tcb_ptr \<and> y = Low_tcb \<or> x = High_pt_ptr \<and> y = High_pt \<or> x = Low_pt_ptr \<and> y = Low_pt \<or> x = High_pd_ptr \<and> y = High_pd \<or> x = Low_pd_ptr \<and> y = Low_pd \<or> x = irq_cnode_ptr \<and> y = irq_cnode \<or> x = ntfn_ptr \<and> y = ntfn \<or> x = Silc_cnode_ptr \<and> y = Silc_cnode \<or> x = High_cnode_ptr \<and> y = High_cnode \<or> x = Low_cnode_ptr \<and> y = Low_cnode \<or> x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0) \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0) \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> irq_node_offs_range \<Longrightarrow> is_aligned x 4 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>irq. x = init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<Longrightarrow> is_aligned x 4 proof (prove)
goal (1 subgoal):
 1. \<And>irq. is_aligned (0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4)) 4 proof (prove)
goal (1 subgoal):
 1. \<And>irq. is_aligned 0xE0008000 4 proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma descendants_s0[simp]:
  "descendants_of (a, b) (cdt s0_internal) = {}" apply (rule set_eqI) apply clarsimp apply (drule descendants_of_NoneD[rotated]) apply (simp add: s0_internal_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of (a, b) (cdt s0_internal) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of (a, b) (cdt s0_internal)) = (x \<in> {}) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. (aa, ba) \<in> descendants_of (a, b) (cdt s0_internal) \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. cdt s0_internal (a, b) = None
 2. \<And>a b. False \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma valid_ioc_s0[simp]:
  "valid_ioc s0_internal" by (clarsimp simp: cte_wp_at_cases tcb_cap_cases_def valid_ioc_def
                        s0_internal_def kh0_def kh0_obj_def split: if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioc s0_internal
theory Example_Valid_State

lemma valid_idle_s0[simp]:
  "valid_idle s0_internal" apply (clarsimp simp: valid_idle_def st_tcb_at_tcb_states_of_state_eq
                        thread_bounds_of_state_s0
                        identity_eq[symmetric] tcb_states_of_state_s0
                        valid_arch_idle_def) by (simp add: s0_ptr_defs s0_internal_def idle_thread_ptr_def pred_tcb_at_def obj_at_def kh0_def idle_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle s0_internal proof (prove)
goal (1 subgoal):
 1. idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None)) (idle_thread s0_internal) s0_internal \<and> idle_thread s0_internal = idle_thread_ptr
theory Example_Valid_State

lemma only_idle_s0[simp]:
  "only_idle s0_internal" apply (clarsimp simp: only_idle_def st_tcb_at_tcb_states_of_state_eq
                        identity_eq[symmetric] tcb_states_of_state_s0) apply (simp add: s0_ptr_defs s0_internal_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_idle s0_internal proof (prove)
goal (1 subgoal):
 1. idle_tcb_ptr = idle_thread s0_internal proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma valid_reply_masters_s0[simp]:
  "valid_reply_masters s0_internal" apply (clarsimp simp: valid_reply_masters_def) apply (force dest: s0_caps_of_state
               simp: Invariants_AI.cte_wp_at_caps_of_state  is_master_reply_cap_to_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_reply_masters s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>a b t. cte_wp_at (is_master_reply_cap_to t) (a, b) s0_internal \<Longrightarrow> a = t \<and> b = tcb_cnode_index 2 proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma valid_irq_handlers_s0[simp]:
  "valid_irq_handlers s0_internal" apply (clarsimp simp: valid_irq_handlers_def ran_def) apply (force dest: s0_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_handlers s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>cap irq a b. \<lbrakk>irq \<in> cap_irqs cap; caps_of_state s0_internal (a, b) = Some cap\<rbrakk> \<Longrightarrow> irq_issued irq s0_internal proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma valid_irq_state_s0[simp]:
  "valid_irq_states s0_internal" apply (clarsimp simp: valid_irq_states_def valid_irq_masks_def s0_internal_def machine_state0_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_states s0_internal proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma valid_machine_state_s0[simp]:
  "valid_machine_state s0_internal" apply (clarsimp simp: valid_machine_state_def s0_internal_def machine_state0_def in_user_frame_def obj_at_def const_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_machine_state s0_internal proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma valid_global_objs_s0[simp]:
  "valid_global_objs s0_internal" apply (clarsimp simp: valid_global_objs_def s0_internal_def arch_state0_def) apply (force simp: valid_vso_at_def obj_at_def kh0_def kh0_obj_def
                     is_aligned_addrFromPPtr kernel_base_aligned_pageBits
                     kernel_mapping_slots_def empty_table_def pde_ref_def valid_pde_mappings_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_objs s0_internal proof (prove)
goal (1 subgoal):
 1. valid_vso_at init_global_pd \<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 = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = init_global_pd, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = exst0\<rparr> \<and> obj_at (empty_table (set (second_level_tables \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = init_global_pd, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>))) init_global_pd \<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 = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = \<lambda>x. None, arm_next_asid = 0, arm_asid_map = \<lambda>x. None, arm_global_pd = init_global_pd, arm_global_pts = [], arm_kernel_vspace = \<lambda>ref. if kernel_base \<le> ref \<and> ref \<le> kernel_base + mask 20 then ArmVSpaceKernelWindow else ArmVSpaceInvalidRegion\<rparr>, exst = exst0\<rparr> proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma equal_kernel_mappings_s0[simp]:
  "equal_kernel_mappings s0_internal" apply (clarsimp simp: equal_kernel_mappings_def obj_at_def s0_internal_def) apply (drule kh0_SomeD)+ apply (force simp: kh0_obj_def High_pd'_def Low_pd'_def s0_ptr_defs kernel_mapping_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equal_kernel_mappings s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>x y pd pd' w. \<lbrakk>w \<in> kernel_mapping_slots; kh0 x = Some (ArchObj (PageDirectory pd)); kh0 y = Some (ArchObj (PageDirectory pd'))\<rbrakk> \<Longrightarrow> pd w = pd' w proof (prove)
goal (1 subgoal):
 1. \<And>x y pd pd' w. \<lbrakk>w \<in> kernel_mapping_slots; x = init_globals_frame \<and> ArchObj (PageDirectory pd) = ArchObj (DataPage False ARMSmallPage) \<or> x = init_global_pd \<and> ArchObj (PageDirectory pd) = ArchObj (PageDirectory global_pd) \<or> x = idle_tcb_ptr \<and> ArchObj (PageDirectory pd) = idle_tcb \<or> x = High_tcb_ptr \<and> ArchObj (PageDirectory pd) = High_tcb \<or> x = Low_tcb_ptr \<and> ArchObj (PageDirectory pd) = Low_tcb \<or> x = High_pt_ptr \<and> ArchObj (PageDirectory pd) = High_pt \<or> x = Low_pt_ptr \<and> ArchObj (PageDirectory pd) = Low_pt \<or> x = High_pd_ptr \<and> ArchObj (PageDirectory pd) = High_pd \<or> x = Low_pd_ptr \<and> ArchObj (PageDirectory pd) = Low_pd \<or> x = irq_cnode_ptr \<and> ArchObj (PageDirectory pd) = irq_cnode \<or> x = ntfn_ptr \<and> ArchObj (PageDirectory pd) = ntfn \<or> x = Silc_cnode_ptr \<and> ArchObj (PageDirectory pd) = Silc_cnode \<or> x = High_cnode_ptr \<and> ArchObj (PageDirectory pd) = High_cnode \<or> x = Low_cnode_ptr \<and> ArchObj (PageDirectory pd) = Low_cnode \<or> x \<in> irq_node_offs_range \<and> ArchObj (PageDirectory pd) = CNode 0 (empty_cnode 0); y = init_globals_frame \<and> ArchObj (PageDirectory pd') = ArchObj (DataPage False ARMSmallPage) \<or> y = init_global_pd \<and> ArchObj (PageDirectory pd') = ArchObj (PageDirectory global_pd) \<or> y = idle_tcb_ptr \<and> ArchObj (PageDirectory pd') = idle_tcb \<or> y = High_tcb_ptr \<and> ArchObj (PageDirectory pd') = High_tcb \<or> y = Low_tcb_ptr \<and> ArchObj (PageDirectory pd') = Low_tcb \<or> y = High_pt_ptr \<and> ArchObj (PageDirectory pd') = High_pt \<or> y = Low_pt_ptr \<and> ArchObj (PageDirectory pd') = Low_pt \<or> y = High_pd_ptr \<and> ArchObj (PageDirectory pd') = High_pd \<or> y = Low_pd_ptr \<and> ArchObj (PageDirectory pd') = Low_pd \<or> y = irq_cnode_ptr \<and> ArchObj (PageDirectory pd') = irq_cnode \<or> y = ntfn_ptr \<and> ArchObj (PageDirectory pd') = ntfn \<or> y = Silc_cnode_ptr \<and> ArchObj (PageDirectory pd') = Silc_cnode \<or> y = High_cnode_ptr \<and> ArchObj (PageDirectory pd') = High_cnode \<or> y = Low_cnode_ptr \<and> ArchObj (PageDirectory pd') = Low_cnode \<or> y \<in> irq_node_offs_range \<and> ArchObj (PageDirectory pd') = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> pd w = pd' w proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma valid_asid_map_s0[simp]:
  "valid_asid_map s0_internal" apply (clarsimp simp: valid_asid_map_def s0_internal_def arch_state0_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_map s0_internal proof (prove)
goal:
No subgoals!