theory Detype_R

lemma valid_objs: "valid_objs' s"
  and        pa: "pspace_aligned' s"
  and        pd: "pspace_distinct' s"
  and        vq: "valid_queues s"
  and       vq': "valid_queues' s"
  and  sym_refs: "sym_refs (state_refs_of' s)"
  and    iflive: "if_live_then_nonz_cap' s"
  and  ifunsafe: "if_unsafe_then_cap' s"
  and     dlist: "valid_dlist (ctes_of s)"
  and      no_0: "no_0 (ctes_of s)"
  and   chain_0: "mdb_chain_0 (ctes_of s)"
  and    badges: "valid_badges (ctes_of s)"
  and contained: "caps_contained' (ctes_of s)"
  and   chunked: "mdb_chunked (ctes_of s)"
  and      umdb: "untyped_mdb' (ctes_of s)"
  and      uinc: "untyped_inc' (ctes_of s)"
  and  nullcaps: "valid_nullcaps (ctes_of s)"
  and    ut_rev: "ut_revocable' (ctes_of s)"
  and    dist_z: "distinct_zombies (ctes_of s)"
  and  irq_ctrl: "irq_control (ctes_of s)"
  and    clinks: "class_links (ctes_of s)"
  and  rep_r_fb: "reply_masters_rvk_fb (ctes_of s)"
  and      idle: "valid_idle' s"
  and      refs: "valid_global_refs' s"
  and      arch: "valid_arch_state' s"
  and      virq: "valid_irq_node' (irq_node' s) s"
  and     virqh: "valid_irq_handlers' s"
  and     virqs: "valid_irq_states' s"
  and no_0_objs: "no_0_obj' s"
  and  ctnotinQ: "ct_not_inQ s"
  and  pde_maps: "valid_pde_mappings' s"
  and irqs_masked: "irqs_masked' s"
  and      ctcd: "ct_idle_or_in_cur_domain' s"
  and       cdm: "ksCurDomain s \<le> maxDomain"
  and       vds: "valid_dom_schedule' s" using invs by (auto simp add: invs'_def valid_state'_def valid_pspace'_def
                    valid_mdb'_def valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((((valid_objs' s &&& pspace_aligned' s) &&& pspace_distinct' s &&& Invariants_H.valid_queues s) &&& (valid_queues' s &&& sym_refs (state_refs_of' s)) &&& if_live_then_nonz_cap' s &&& if_unsafe_then_cap' s) &&& ((valid_dlist (ctes_of s) &&& no_0 (ctes_of s)) &&& mdb_chain_0 (ctes_of s) &&& valid_badges (ctes_of s)) &&& (caps_contained' (ctes_of s) &&& mdb_chunked (ctes_of s)) &&& untyped_mdb' (ctes_of s) &&& untyped_inc' (ctes_of s) &&& valid_nullcaps (ctes_of s)) &&& (((ut_revocable' (ctes_of s) &&& distinct_zombies (ctes_of s)) &&& irq_control (ctes_of s) &&& class_links (ctes_of s)) &&& (reply_masters_rvk_fb (ctes_of s) &&& valid_idle' s) &&& valid_global_refs' s &&& valid_arch_state' s &&& valid_irq_node' (irq_node' s) s) &&& ((valid_irq_handlers' s &&& valid_irq_states' s) &&& no_0_obj' s &&& ct_not_inQ s) &&& (valid_pde_mappings' s &&& irqs_masked' s) &&& ct_idle_or_in_cur_domain' s &&& ksCurDomain s \<le> maxDomain &&& valid_dom_schedule' s proof (prove)
using this:
invs' s

goal (1 subgoal):
 1. ((((valid_objs' s &&& pspace_aligned' s) &&& pspace_distinct' s &&& Invariants_H.valid_queues s) &&& (valid_queues' s &&& sym_refs (state_refs_of' s)) &&& if_live_then_nonz_cap' s &&& if_unsafe_then_cap' s) &&& ((valid_dlist (ctes_of s) &&& no_0 (ctes_of s)) &&& mdb_chain_0 (ctes_of s) &&& valid_badges (ctes_of s)) &&& (caps_contained' (ctes_of s) &&& mdb_chunked (ctes_of s)) &&& untyped_mdb' (ctes_of s) &&& untyped_inc' (ctes_of s) &&& valid_nullcaps (ctes_of s)) &&& (((ut_revocable' (ctes_of s) &&& distinct_zombies (ctes_of s)) &&& irq_control (ctes_of s) &&& class_links (ctes_of s)) &&& (reply_masters_rvk_fb (ctes_of s) &&& valid_idle' s) &&& valid_global_refs' s &&& valid_arch_state' s &&& valid_irq_node' (irq_node' s) s) &&& ((valid_irq_handlers' s &&& valid_irq_states' s) &&& no_0_obj' s &&& ct_not_inQ s) &&& (valid_pde_mappings' s &&& irqs_masked' s) &&& ct_idle_or_in_cur_domain' s &&& ksCurDomain s \<le> maxDomain &&& valid_dom_schedule' s