theory Example_Valid_State

lemma kh0_dom:
  "dom kh0 = {init_globals_frame, init_global_pd, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr,
              High_pt_ptr, Low_pt_ptr, High_pd_ptr, Low_pd_ptr, irq_cnode_ptr, ntfn_ptr,
              Silc_cnode_ptr, High_cnode_ptr, Low_cnode_ptr} \<union>
             irq_node_offs_range" apply (rule equalityI) apply (simp add: kh0_def dom_def) apply (clarsimp simp: irq_node_offs_in_range) apply (clarsimp simp: dom_def) apply (rule conjI, clarsimp simp: kh0_def)+ apply (force simp: kh0_def cte_level_bits_def dest: irq_node_offs_range_correct) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom kh0 = {init_globals_frame, init_global_pd, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, High_pt_ptr, Low_pt_ptr, High_pd_ptr, Low_pd_ptr, irq_cnode_ptr, ntfn_ptr, Silc_cnode_ptr, High_cnode_ptr, Low_cnode_ptr} \<union> irq_node_offs_range proof (prove)
goal (2 subgoals):
 1. dom kh0 \<subseteq> {init_globals_frame, init_global_pd, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, High_pt_ptr, Low_pt_ptr, High_pd_ptr, Low_pd_ptr, irq_cnode_ptr, ntfn_ptr, Silc_cnode_ptr, High_cnode_ptr, Low_cnode_ptr} \<union> irq_node_offs_range
 2. {init_globals_frame, init_global_pd, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, High_pt_ptr, Low_pt_ptr, High_pd_ptr, Low_pd_ptr, irq_cnode_ptr, ntfn_ptr, Silc_cnode_ptr, High_cnode_ptr, Low_cnode_ptr} \<union> irq_node_offs_range \<subseteq> dom kh0 proof (prove)
goal (2 subgoals):
 1. {a. (\<forall>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> a) \<longrightarrow> a \<noteq> Low_cnode_ptr \<longrightarrow> a \<noteq> High_cnode_ptr \<longrightarrow> a \<noteq> Silc_cnode_ptr \<longrightarrow> a \<noteq> ntfn_ptr \<longrightarrow> a \<noteq> irq_cnode_ptr \<longrightarrow> a \<noteq> Low_pd_ptr \<longrightarrow> a \<noteq> High_pd_ptr \<longrightarrow> a \<noteq> Low_pt_ptr \<longrightarrow> a \<noteq> High_pt_ptr \<longrightarrow> a \<noteq> Low_tcb_ptr \<longrightarrow> a \<noteq> High_tcb_ptr \<longrightarrow> a \<noteq> idle_tcb_ptr \<longrightarrow> a \<noteq> init_globals_frame \<longrightarrow> a = init_global_pd} \<subseteq> insert init_globals_frame (insert init_global_pd (insert idle_tcb_ptr (insert High_tcb_ptr (insert Low_tcb_ptr (insert High_pt_ptr (insert Low_pt_ptr (insert High_pd_ptr (insert Low_pd_ptr (insert irq_cnode_ptr (insert ntfn_ptr (insert Silc_cnode_ptr (insert High_cnode_ptr (insert Low_cnode_ptr irq_node_offs_range)))))))))))))
 2. {init_globals_frame, init_global_pd, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, High_pt_ptr, Low_pt_ptr, High_pd_ptr, Low_pd_ptr, irq_cnode_ptr, ntfn_ptr, Silc_cnode_ptr, High_cnode_ptr, Low_cnode_ptr} \<union> irq_node_offs_range \<subseteq> dom kh0 proof (prove)
goal (1 subgoal):
 1. {init_globals_frame, init_global_pd, idle_tcb_ptr, High_tcb_ptr, Low_tcb_ptr, High_pt_ptr, Low_pt_ptr, High_pd_ptr, Low_pd_ptr, irq_cnode_ptr, ntfn_ptr, Silc_cnode_ptr, High_cnode_ptr, Low_cnode_ptr} \<union> irq_node_offs_range \<subseteq> dom kh0 proof (prove)
goal (1 subgoal):
 1. (\<exists>y. kh0 init_globals_frame = Some y) \<and> (\<exists>y. kh0 init_global_pd = Some y) \<and> (\<exists>y. kh0 idle_tcb_ptr = Some y) \<and> (\<exists>y. kh0 High_tcb_ptr = Some y) \<and> (\<exists>y. kh0 Low_tcb_ptr = Some y) \<and> (\<exists>y. kh0 High_pt_ptr = Some y) \<and> (\<exists>y. kh0 Low_pt_ptr = Some y) \<and> (\<exists>y. kh0 High_pd_ptr = Some y) \<and> (\<exists>y. kh0 Low_pd_ptr = Some y) \<and> (\<exists>y. kh0 irq_cnode_ptr = Some y) \<and> (\<exists>y. kh0 ntfn_ptr = Some y) \<and> (\<exists>y. kh0 Silc_cnode_ptr = Some y) \<and> (\<exists>y. kh0 High_cnode_ptr = Some y) \<and> (\<exists>y. kh0 Low_cnode_ptr = Some y) \<and> irq_node_offs_range \<subseteq> {a. \<exists>y. kh0 a = Some y} proof (prove)
goal (1 subgoal):
 1. irq_node_offs_range \<subseteq> {a. \<exists>y. kh0 a = Some y} proof (prove)
goal:
No subgoals!