kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_H

lemma sch_act_wf_arch [simp]:
  "sch_act_wf sa (ksArchState_update f s) = sch_act_wf sa s" by (cases sa) (simp_all add: ct_in_state'_def  tcb_in_cur_domain'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_wf sa (ksArchState_update f s) = sch_act_wf sa s
theory Invariants_H

lemma valid_queues_arch [simp]:
  "valid_queues (ksArchState_update f s) = valid_queues s" by (simp add: valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues (ksArchState_update f s) = valid_queues s
theory Invariants_H

lemma if_unsafe_then_cap_arch' [simp]:
  "if_unsafe_then_cap' (ksArchState_update f s) = if_unsafe_then_cap' s" by (simp add: if_unsafe_then_cap'_def ex_cte_cap_to'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap' (ksArchState_update f s) = if_unsafe_then_cap' s
theory Invariants_H

lemma valid_idle_arch' [simp]:
  "valid_idle' (ksArchState_update f s) = valid_idle' s" by (simp add: valid_idle'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle' (ksArchState_update f s) = valid_idle' s
theory Invariants_H

lemma valid_irq_node_arch' [simp]:
  "valid_irq_node' w (ksArchState_update f s) = valid_irq_node' w s" by (simp add: valid_irq_node'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_node' w (ksArchState_update f s) = valid_irq_node' w s
theory Invariants_H

lemma sch_act_wf_machine_state [simp]:
  "sch_act_wf sa (ksMachineState_update f s) = sch_act_wf sa s" by (cases sa) (simp_all add: ct_in_state'_def  tcb_in_cur_domain'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_wf sa (ksMachineState_update f s) = sch_act_wf sa s
theory Invariants_H

lemma valid_queues_machine_state [simp]:
  "valid_queues (ksMachineState_update f s) = valid_queues s" by (simp add: valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues (ksMachineState_update f s) = valid_queues s
theory Invariants_H

lemma valid_queues_arch' [simp]:
  "valid_queues' (ksArchState_update f s) = valid_queues' s" by (simp add: valid_queues'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues' (ksArchState_update f s) = valid_queues' s
theory Invariants_H

lemma valid_queues_machine_state' [simp]:
  "valid_queues' (ksMachineState_update f s) = valid_queues' s" by (simp add: valid_queues'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues' (ksMachineState_update f s) = valid_queues' s
theory Invariants_H

lemma valid_irq_node'_machine_state [simp]:
  "valid_irq_node' x (ksMachineState_update f s) = valid_irq_node' x s" by (simp add: valid_irq_node'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_node' x (ksMachineState_update f s) = valid_irq_node' x s
theory Invariants_H

lemma no_0_ko_wp' [elim!]:
  "\<lbrakk> ko_wp_at' Q 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" by (simp add: ko_wp_at'_def no_0_obj'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_wp_at' Q 0 s; no_0_obj' s\<rbrakk> \<Longrightarrow> P
theory Invariants_H

lemma no_0_obj_at' [elim!]:
  "\<lbrakk> obj_at' Q 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" by (simp add: obj_at'_def no_0_obj'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' Q 0 s; no_0_obj' s\<rbrakk> \<Longrightarrow> P
theory Invariants_H

lemma no_0_typ_at' [elim!]:
  "\<lbrakk> typ_at' T 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" by (clarsimp simp: typ_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at' T 0 s; no_0_obj' s\<rbrakk> \<Longrightarrow> P
theory Invariants_H

lemma no_0_ko_wp'_eq [simp]:
  "no_0_obj' s \<Longrightarrow> ko_wp_at' P 0 s = False" by (simp add: ko_wp_at'_def no_0_obj'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0_obj' s \<Longrightarrow> ko_wp_at' P 0 s = False
theory Invariants_H

lemma no_0_obj_at'_eq [simp]:
  "no_0_obj' s \<Longrightarrow> obj_at' P 0 s = False" by (simp add: obj_at'_def no_0_obj'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0_obj' s \<Longrightarrow> obj_at' P 0 s = False
theory Invariants_H

lemma no_0_typ_at'_eq [simp]:
  "no_0_obj' s \<Longrightarrow> typ_at' P 0 s = False" by (simp add: typ_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0_obj' s \<Longrightarrow> typ_at' P 0 s = False
theory Invariants_H

lemma valid_pspace_valid_objs'[elim!]:
  "valid_pspace' s \<Longrightarrow> valid_objs' s" by (simp add: valid_pspace'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace' s \<Longrightarrow> valid_objs' s
theory Invariants_H

lemma simple_sane_strg:
  "sch_act_simple s \<longrightarrow> sch_act_sane s" by (simp add: sch_act_sane_def sch_act_simple_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_simple s \<longrightarrow> sch_act_sane s
theory Invariants_H

lemma sch_act_wf_cases:
  "sch_act_wf action = (case action of
    ResumeCurrentThread \<Rightarrow> ct_in_state' activatable'
  | ChooseNewThread     \<Rightarrow> \<top>
  | SwitchToThread t    \<Rightarrow> \<lambda>s. st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s)" by (cases action) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_wf action = (case action of ResumeCurrentThread \<Rightarrow> ct_in_state' activatable' | ChooseNewThread \<Rightarrow> \<lambda>_. True | SwitchToThread t \<Rightarrow> \<lambda>s. st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s)
theory Invariants_H

lemma vms_sch_act_update'[iff]:
  "valid_machine_state' (ksSchedulerAction_update f s) =
   valid_machine_state' s" by (simp add: valid_machine_state'_def )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_machine_state' (ksSchedulerAction_update f s) = valid_machine_state' s
theory Invariants_H

lemma objBitsT_koTypeOf :
  "(objBitsT (koTypeOf ko)) = objBitsKO ko" apply (cases ko; simp add: objBits_simps objBitsT_simps) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp add: archObjSize_def objBitsT_simps
                                                pteBits_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. objBitsT (koTypeOf ko) = objBitsKO ko proof (prove)
goal (1 subgoal):
 1. \<And>x8. ko = KOArch x8 \<Longrightarrow> objBitsT (ArchT (archTypeOf x8)) = archObjSize x8 proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_object. ko = KOArch arch_kernel_object \<Longrightarrow> objBitsT (ArchT (archTypeOf arch_kernel_object)) = archObjSize arch_kernel_object proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma st_tcb_at'_runnable_is_activatable:
  "st_tcb_at' runnable' t s \<Longrightarrow> st_tcb_at' activatable' t s" by (simp add: st_tcb_at'_def)
     (fastforce elim: obj_at'_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' runnable' t s \<Longrightarrow> st_tcb_at' activatable' t s
theory Invariants_H

lemma tcb_at'_has_tcbPriority:
 "tcb_at' t s \<Longrightarrow> \<exists>p. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s" by (clarsimp simp add: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' t s \<Longrightarrow> \<exists>p. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s
theory Invariants_H

lemma pred_tcb_at'_Not:
  "pred_tcb_at' f (Not o P) t s = (tcb_at' t s \<and> \<not> pred_tcb_at' f P t s)" by (auto simp: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at' f (Not \<circ> P) t s = (tcb_at' t s \<and> \<not> pred_tcb_at' f P t s)
theory Invariants_H

lemma obj_at'_conj_distrib:
  "obj_at' (\<lambda>ko. P ko \<and> Q ko) p s \<Longrightarrow> obj_at' P p s \<and> obj_at' Q p s" by (auto simp: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (\<lambda>ko. P ko \<and> Q ko) p s \<Longrightarrow> obj_at' P p s \<and> obj_at' Q p s
theory Invariants_H

lemma obj_at'_conj:
  "obj_at' (\<lambda>ko. P ko \<and> Q ko) p s = (obj_at' P p s \<and> obj_at' Q p s)" using obj_at'_conj_distrib obj_at_conj' by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (\<lambda>ko. P ko \<and> Q ko) p s = (obj_at' P p s \<and> obj_at' Q p s) proof (prove)
using this:
obj_at' (\<lambda>ko. ?P ko \<and> ?Q ko) ?p ?s \<Longrightarrow> obj_at' ?P ?p ?s \<and> obj_at' ?Q ?p ?s
\<lbrakk>obj_at' ?P ?p ?s; obj_at' ?Q ?p ?s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>k. ?P k \<and> ?Q k) ?p ?s

goal (1 subgoal):
 1. obj_at' (\<lambda>ko. P ko \<and> Q ko) p s = (obj_at' P p s \<and> obj_at' Q p s)
theory Invariants_H

lemma not_obj_at'_strengthen:
  "obj_at' (Not \<circ> P) p s \<Longrightarrow> \<not> obj_at' P p s" by (clarsimp simp: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (Not \<circ> P) p s \<Longrightarrow> \<not> obj_at' P p s
theory Invariants_H

lemma not_pred_tcb_at'_strengthen:
  "pred_tcb_at' f (Not \<circ> P) p s \<Longrightarrow> \<not> pred_tcb_at' f P p s" by (clarsimp simp: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at' f (Not \<circ> P) p s \<Longrightarrow> \<not> pred_tcb_at' f P p s
theory Invariants_H

lemma valid_queues_no_bitmap_def':
  "valid_queues_no_bitmap =
     (\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)).
                  obj_at' (inQ d p) t s \<and> st_tcb_at' runnable' t s) \<and>
                  distinct (ksReadyQueues s (d, p)) \<and> (d > maxDomain \<or> p > maxPriority \<longrightarrow> ksReadyQueues s (d,p) = []))" apply (rule ext, rule iffI) apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_and pred_tcb_at'_def o_def
                  elim!: obj_at'_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues_no_bitmap = (\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s \<and> st_tcb_at' runnable' t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_queues_no_bitmap s \<Longrightarrow> \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s \<and> st_tcb_at' runnable' t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])
 2. \<And>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s \<and> st_tcb_at' runnable' t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []) \<Longrightarrow> valid_queues_no_bitmap s proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma valid_refs'_cteCaps:
  "valid_refs' S (ctes_of s) = (\<forall>c \<in> ran (cteCaps_of s). S \<inter> capRange c = {})" by (fastforce simp: valid_refs'_def cteCaps_of_def elim!: ranE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_refs' S (ctes_of s) = (\<forall>c\<in>ran (cteCaps_of s). S \<inter> capRange c = {})
theory Invariants_H

lemma cte_at_valid_cap_sizes_0:
  "valid_cap_sizes' n ctes \<Longrightarrow> ctes p = Some cte \<Longrightarrow> 0 < n" apply (clarsimp simp: valid_cap_sizes'_def) apply (drule bspec, erule ranI) apply (rule Suc_le_lessD, erule order_trans[rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap_sizes' n ctes; ctes p = Some cte\<rbrakk> \<Longrightarrow> 0 < n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cte\<in>ran ctes. 2 ^ capBits (cteCap cte) \<le> n; ctes p = Some cte\<rbrakk> \<Longrightarrow> 0 < n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes p = Some cte; 2 ^ capBits (cteCap cte) \<le> n\<rbrakk> \<Longrightarrow> 0 < n proof (prove)
goal (1 subgoal):
 1. ctes p = Some cte \<Longrightarrow> Suc 0 \<le> 2 ^ capBits (cteCap cte) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma invs_valid_stateI' [elim!]:
  "invs' s \<Longrightarrow> valid_state' s" by (simp add: invs'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_state' s
theory Invariants_H

lemma tcb_at_invs' [elim!]:
  "invs' s \<Longrightarrow> tcb_at' (ksCurThread s) s" by (simp add: invs'_def cur_tcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> tcb_at' (ksCurThread s) s
theory Invariants_H

lemma invs_valid_objs' [elim!]:
  "invs' s \<Longrightarrow> valid_objs' s" by (simp add: invs'_def valid_state'_def valid_pspace'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_objs' s
theory Invariants_H

lemma invs_pspace_aligned' [elim!]:
  "invs' s \<Longrightarrow> pspace_aligned' s" by (simp add: invs'_def valid_state'_def valid_pspace'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> pspace_aligned' s
theory Invariants_H

lemma invs_pspace_distinct' [elim!]:
  "invs' s \<Longrightarrow> pspace_distinct' s" by (simp add: invs'_def valid_state'_def valid_pspace'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> pspace_distinct' s
theory Invariants_H

lemma invs_valid_pspace' [elim!]:
  "invs' s \<Longrightarrow> valid_pspace' s" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_pspace' s
theory Invariants_H

lemma invs_cur' [elim!]:
  "invs' s \<Longrightarrow> cur_tcb' s" by (simp add: invs'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> cur_tcb' s
theory Invariants_H

lemma invs_mdb' [elim!]:
  "invs' s \<Longrightarrow> valid_mdb' s" by (simp add: invs'_def valid_state'_def valid_pspace'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_mdb' s
theory Invariants_H

lemma valid_mdb_no_loops [elim!]:
  "valid_mdb_ctes m \<Longrightarrow> no_loops m" by (auto intro: mdb_chain_0_no_loops)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb_ctes m \<Longrightarrow> no_loops m
theory Invariants_H

lemma invs_no_loops [elim!]:
  "invs' s \<Longrightarrow> no_loops (ctes_of s)" apply (rule valid_mdb_no_loops) apply (simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> no_loops (ctes_of s) proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_mdb_ctes (ctes_of s) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma invs_iflive'[elim!]:
  "invs' s \<Longrightarrow> if_live_then_nonz_cap' s" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> if_live_then_nonz_cap' s
theory Invariants_H

lemma invs_unsafe_then_cap' [elim!]:
  "invs' s \<Longrightarrow> if_unsafe_then_cap' s" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> if_unsafe_then_cap' s
theory Invariants_H

lemma invs_sym' [elim!]:
  "invs' s \<Longrightarrow> sym_refs (state_refs_of' s)" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> sym_refs (state_refs_of' s)
theory Invariants_H

lemma invs_sch_act_wf' [elim!]:
  "invs' s \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s
theory Invariants_H

lemma invs_queues [elim!]:
  "invs' s \<Longrightarrow> valid_queues s" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_queues s
theory Invariants_H

lemma invs_valid_idle'[elim!]:
  "invs' s \<Longrightarrow> valid_idle' s" by (fastforce simp: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_idle' s
theory Invariants_H

lemma invs_valid_global'[elim!]:
  "invs' s \<Longrightarrow> valid_global_refs' s" by (fastforce simp: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_global_refs' s
theory Invariants_H

lemma invs'_invs_no_cicd:
  "invs' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s" by (simp add: invs'_to_invs_no_cicd'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s
theory Invariants_H

lemma invs'_bitmapQ_no_L1_orphans:
  "invs' s \<Longrightarrow> bitmapQ_no_L1_orphans s" by (drule invs_queues, simp add: valid_queues_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> bitmapQ_no_L1_orphans s
theory Invariants_H

lemma invs_ksCurDomain_maxDomain' [elim!]:
  "invs' s \<Longrightarrow> ksCurDomain s \<le> maxDomain" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> ksCurDomain s \<le> maxDomain
theory Invariants_H

lemma simple_st_tcb_at_state_refs_ofD':
  "st_tcb_at' simple' t s \<Longrightarrow> bound_tcb_at' (\<lambda>x. tcb_bound_refs' x = state_refs_of' s t) t s" by (fastforce simp: pred_tcb_at'_def obj_at'_def state_refs_of'_def
                      projectKO_eq project_inject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' simple' t s \<Longrightarrow> bound_tcb_at' (\<lambda>x. tcb_bound_refs' x = state_refs_of' s t) t s
theory Invariants_H

lemma cur_tcb_arch' [iff]:
  "cur_tcb' (ksArchState_update f s) = cur_tcb' s" by (simp add: cur_tcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_tcb' (ksArchState_update f s) = cur_tcb' s
theory Invariants_H

lemma cur_tcb'_machine_state [simp]:
  "cur_tcb' (ksMachineState_update f s) = cur_tcb' s" by (simp add: cur_tcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_tcb' (ksMachineState_update f s) = cur_tcb' s
theory Invariants_H

lemma invs_no_0_obj'[elim!]:
  "invs' s \<Longrightarrow> no_0_obj' s" by (simp add: invs'_def valid_state'_def valid_pspace'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> no_0_obj' s
theory Invariants_H

lemma pred_tcb'_neq_contra:
  "\<lbrakk> pred_tcb_at' proj P p s; pred_tcb_at' proj Q p s; \<And>st. P st \<noteq> Q st \<rbrakk> \<Longrightarrow> False" by (clarsimp simp: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_tcb_at' proj P p s; pred_tcb_at' proj Q p s; \<And>st. P st \<noteq> Q st\<rbrakk> \<Longrightarrow> False
theory Invariants_H

lemma invs'_ksDomSchedule:
  "invs' s \<Longrightarrow> KernelStateData_H.ksDomSchedule s = KernelStateData_H.ksDomSchedule (newKernelState undefined)" unfolding invs'_def valid_state'_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s) and cur_tcb') s \<Longrightarrow> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined)
theory Invariants_H

lemma invs'_ksDomScheduleIdx:
  "invs' s \<Longrightarrow> KernelStateData_H.ksDomScheduleIdx s < length (KernelStateData_H.ksDomSchedule (newKernelState undefined))" unfolding invs'_def valid_state'_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s) and cur_tcb') s \<Longrightarrow> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined))
theory Invariants_H

lemma valid_bitmap_valid_bitmapQ_exceptE:
  "\<lbrakk> valid_bitmapQ_except d p s ; (bitmapQ d p s \<longleftrightarrow> ksReadyQueues s (d,p) \<noteq> []) ;
     bitmapQ_no_L2_orphans s \<rbrakk>
   \<Longrightarrow> valid_bitmapQ s" unfolding valid_bitmapQ_def valid_bitmapQ_except_def by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_bitmapQ_except d p s; bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> []); bitmapQ_no_L2_orphans s\<rbrakk> \<Longrightarrow> valid_bitmapQ s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>da pa. da \<noteq> d \<or> pa \<noteq> p \<longrightarrow> bitmapQ da pa s = (ksReadyQueues s (da, pa) \<noteq> []); bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> []); bitmapQ_no_L2_orphans s\<rbrakk> \<Longrightarrow> \<forall>d p. bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])
theory Invariants_H

lemma valid_bitmap_valid_bitmapQ_exceptI[intro]:
  "valid_bitmapQ s \<Longrightarrow> valid_bitmapQ_except d p s" unfolding valid_bitmapQ_except_def valid_bitmapQ_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bitmapQ s \<Longrightarrow> valid_bitmapQ_except d p s proof (prove)
goal (1 subgoal):
 1. \<forall>d p. bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> []) \<Longrightarrow> \<forall>da pa. da \<noteq> d \<or> pa \<noteq> p \<longrightarrow> bitmapQ da pa s = (ksReadyQueues s (da, pa) \<noteq> [])
theory Invariants_H

lemma pdBits_eq: "pdBits = pd_bits" by (simp add: pd_bits_def pdBits_def pdeBits_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pdBits = pd_bits
theory Invariants_H

lemma ptBits_eq: "ptBits = pt_bits" by (simp add: pt_bits_def ptBits_def pteBits_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptBits = pt_bits
theory Invariants_H

lemma largePagePTE_offset_eq:  "largePagePTE_offsets = largePagePTEOffsets" by (simp add: largePagePTE_offsets_def largePagePTEOffsets_def pteBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. largePagePTE_offsets = largePagePTEOffsets
theory Invariants_H

lemma superSectionPDE_offsets_eq:  "superSectionPDE_offsets = superSectionPDEOffsets" by (simp add: superSectionPDE_offsets_def superSectionPDEOffsets_def pdeBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. superSectionPDE_offsets = superSectionPDEOffsets