theory Example_Valid_State

lemma Sys1AgentMap_simps:
  "Sys1AgentMap Low_cnode_ptr = partition_label Low"
      "Sys1AgentMap High_cnode_ptr = partition_label High"
      "Sys1AgentMap ntfn_ptr = partition_label High"
      "Sys1AgentMap irq_cnode_ptr = partition_label IRQ0"
      "Sys1AgentMap Silc_cnode_ptr = SilcLabel"
      "Sys1AgentMap Low_pd_ptr = partition_label Low"
      "Sys1AgentMap High_pd_ptr = partition_label High"
      "Sys1AgentMap Low_pt_ptr = partition_label Low"
      "Sys1AgentMap High_pt_ptr = partition_label High"
      "Sys1AgentMap Low_tcb_ptr = partition_label Low"
      "Sys1AgentMap High_tcb_ptr = partition_label High"
      "Sys1AgentMap idle_tcb_ptr = partition_label Low"
      "\<And>p. p \<in> ptr_range shared_page_ptr_virt pageBits
          \<Longrightarrow> Sys1AgentMap p = partition_label Low" unfolding Sys1AgentMap_def apply simp_all by (auto simp: s0_ptr_defs ptr_range_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Sys1AgentMap Low_cnode_ptr = partition_label Low &&& Sys1AgentMap High_cnode_ptr = partition_label High &&& Sys1AgentMap ntfn_ptr = partition_label High) &&& Sys1AgentMap irq_cnode_ptr = partition_label IRQ0 &&& Sys1AgentMap Silc_cnode_ptr = SilcLabel &&& Sys1AgentMap Low_pd_ptr = partition_label Low) &&& (Sys1AgentMap High_pd_ptr = partition_label High &&& Sys1AgentMap Low_pt_ptr = partition_label Low &&& Sys1AgentMap High_pt_ptr = partition_label High) &&& (Sys1AgentMap Low_tcb_ptr = partition_label Low &&& Sys1AgentMap High_tcb_ptr = partition_label High) &&& Sys1AgentMap idle_tcb_ptr = partition_label Low &&& (\<And>p. p \<in> ptr_range shared_page_ptr_virt pageBits \<Longrightarrow> Sys1AgentMap p = partition_label Low) proof (prove)
goal (1 subgoal):
 1. ((((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) Low_cnode_ptr = partition_label Low &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) High_cnode_ptr = partition_label High &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) ntfn_ptr = partition_label High) &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) irq_cnode_ptr = partition_label IRQ0 &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) Silc_cnode_ptr = SilcLabel &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) Low_pd_ptr = partition_label Low) &&& (((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) High_pd_ptr = partition_label High &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) Low_pt_ptr = partition_label Low &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) High_pt_ptr = partition_label High) &&& (((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) Low_tcb_ptr = partition_label Low &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) High_tcb_ptr = partition_label High) &&& ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) idle_tcb_ptr = partition_label Low &&& (\<And>p. p \<in> ptr_range shared_page_ptr_virt pageBits \<Longrightarrow> ((\<lambda>p. if p \<in> ptr_range shared_page_ptr_virt pageBits then partition_label Low else partition_label IRQ0)(Low_cnode_ptr := partition_label Low, High_cnode_ptr := partition_label High, ntfn_ptr := partition_label High, irq_cnode_ptr := partition_label IRQ0, Silc_cnode_ptr := SilcLabel, Low_pd_ptr := partition_label Low, High_pd_ptr := partition_label High, Low_pt_ptr := partition_label Low, High_pt_ptr := partition_label High, Low_tcb_ptr := partition_label Low, High_tcb_ptr := partition_label High, idle_tcb_ptr := partition_label Low)) p = partition_label Low) proof (prove)
goal (1 subgoal):
 1. \<And>p. p \<in> ptr_range shared_page_ptr_virt pageBits \<Longrightarrow> p \<noteq> Low_cnode_ptr \<longrightarrow> p \<noteq> High_cnode_ptr \<and> (p \<noteq> High_cnode_ptr \<longrightarrow> p \<noteq> ntfn_ptr \<and> (p \<noteq> ntfn_ptr \<longrightarrow> p \<noteq> irq_cnode_ptr \<and> (p \<noteq> irq_cnode_ptr \<longrightarrow> p \<noteq> Silc_cnode_ptr \<and> (p \<noteq> Silc_cnode_ptr \<longrightarrow> p \<noteq> Low_pd_ptr \<longrightarrow> p \<noteq> High_pd_ptr \<and> (p \<noteq> High_pd_ptr \<longrightarrow> p \<noteq> Low_pt_ptr \<longrightarrow> p \<noteq> High_pt_ptr \<and> (p \<noteq> High_pt_ptr \<longrightarrow> p \<noteq> Low_tcb_ptr \<longrightarrow> p \<noteq> High_tcb_ptr))))))