kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_H

lemma mask_wordRadix_less_wordBits:
  assumes sz: "wordRadix \<le> size w"
  shows "unat ((w::'a::len word) && mask wordRadix) < wordBits" using word_unat_mask_lt[where m=wordRadix and w=w] assms by (simp add: wordRadix_def wordBits_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (w && mask wordRadix) < wordBits proof (prove)
using this:
wordRadix \<le> size w \<Longrightarrow> unat (w && mask wordRadix) < 2 ^ wordRadix
wordRadix \<le> size w

goal (1 subgoal):
 1. unat (w && mask wordRadix) < wordBits
theory Invariants_H

lemma priority_mask_wordRadix_size:
  "unat ((w::priority) && mask wordRadix) < wordBits" by (rule mask_wordRadix_less_wordBits, simp add: wordRadix_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (w && mask wordRadix) < wordBits
theory Invariants_H

lemma ko_at_defn_rewr:
  "ko_at'_defn ko p s \<Longrightarrow> (obj_at' P p s = P ko)" unfolding ko_at'_defn_def by (auto simp: obj_at'_def)

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

lemma ko_at_defn_uniqueD:
  "ko_at'_defn ko p s \<Longrightarrow> ko_at'_defn ko' p s \<Longrightarrow> ko' = ko" unfolding ko_at'_defn_def by (auto simp: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at'_defn ko p s; ko_at'_defn ko' p s\<rbrakk> \<Longrightarrow> ko' = ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko p s; ko_at' ko' p s\<rbrakk> \<Longrightarrow> ko' = ko
theory Invariants_H

lemma ko_at_defn_pred_tcb_at':
  "ko_at'_defn ko p s \<Longrightarrow> (pred_tcb_at' proj P p s = P (proj (tcb_to_itcb' ko)))" by (auto simp: pred_tcb_at'_def ko_at_defn_rewr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at'_defn ko p s \<Longrightarrow> pred_tcb_at' proj P p s = P (proj (tcb_to_itcb' ko))
theory Invariants_H

lemma ko_at_defn_ko_wp_at':
  "ko_at'_defn ko p s \<Longrightarrow> (ko_wp_at' P p s = P (injectKO ko))" by (clarsimp simp: ko_at'_defn_def obj_at'_real_def
                     ko_wp_at'_def project_inject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at'_defn ko p s \<Longrightarrow> ko_wp_at' P p s = P (injectKO ko)
theory Invariants_H

lemma neq_out_intv:
  "\<lbrakk> a \<noteq> b; b \<notin> {a..a + c - 1} - {a} \<rbrakk> \<Longrightarrow> b \<notin> {a..a + c - 1}" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b \<notin> {a..a + c - (1::'a)} - {a}\<rbrakk> \<Longrightarrow> b \<notin> {a..a + c - (1::'a)}
theory Invariants_H

lemma rule_out_intv:
  "\<lbrakk> ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; a \<noteq> b \<rbrakk>
   \<Longrightarrow> b \<notin> mask_range a (objBitsKO obj)" apply (drule(1) pspace_distinctD') apply (subst (asm) ps_clear_def) apply (drule_tac x = b in orthD2) apply fastforce apply (drule neq_out_intv) apply (simp add: mask_def add_diff_eq) apply (simp add: mask_def add_diff_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; a \<noteq> b\<rbrakk> \<Longrightarrow> b \<notin> mask_range a (objBitsKO obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s b = Some obj'; pspace_distinct' s; a \<noteq> b; ps_clear a (objBitsKO obj) s\<rbrakk> \<Longrightarrow> b \<notin> mask_range a (objBitsKO obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s b = Some obj'; pspace_distinct' s; a \<noteq> b; ({a..a + (1 << objBitsKO obj) - 1} - {a}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> b \<notin> mask_range a (objBitsKO obj) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s b = Some obj'; pspace_distinct' s; a \<noteq> b\<rbrakk> \<Longrightarrow> b \<in> dom (ksPSpace s)
 2. \<lbrakk>ksPSpace s b = Some obj'; pspace_distinct' s; a \<noteq> b; b \<notin> {a..a + (1 << objBitsKO obj) - 1} - {a}\<rbrakk> \<Longrightarrow> b \<notin> mask_range a (objBitsKO obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s b = Some obj'; pspace_distinct' s; a \<noteq> b; b \<notin> {a..a + (1 << objBitsKO obj) - 1} - {a}\<rbrakk> \<Longrightarrow> b \<notin> mask_range a (objBitsKO obj) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s b = Some obj'; pspace_distinct' s; b \<notin> {a..a + (1 << objBitsKO obj) - 1} - {a}\<rbrakk> \<Longrightarrow> b \<notin> {a..a + ?c10 - 1} - {a}
 2. \<lbrakk>ksPSpace s b = Some obj'; pspace_distinct' s; b \<notin> {a..a + (1 << objBitsKO obj) - 1} - {a}; b \<notin> {a..a + ?c10 - 1}\<rbrakk> \<Longrightarrow> b \<notin> mask_range a (objBitsKO obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s b = Some obj'; pspace_distinct' s; b \<notin> {a..a + (1 << objBitsKO obj) - 1} - {a}; b \<notin> {a..a + 2 ^ objBitsKO obj - 1}\<rbrakk> \<Longrightarrow> b \<notin> mask_range a (objBitsKO obj) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma ptr_range_mask_range:
  "{ptr..ptr + 2 ^ bits - 1} = mask_range ptr bits" unfolding mask_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {ptr..ptr + 2 ^ bits - 1} = mask_range ptr bits proof (prove)
goal (1 subgoal):
 1. {ptr..ptr + 2 ^ bits - 1} = {ptr..ptr + ((1 << bits) - 1)}
theory Invariants_H

lemma distinct_obj_range'_not_subset:
  "\<lbrakk> ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s;
     pspace_aligned' s; a \<noteq> b \<rbrakk>
   \<Longrightarrow> \<not> obj_range' b obj' \<subseteq> obj_range' a obj" unfolding obj_range'_def apply (frule_tac x=a in pspace_alignedD') apply assumption apply (frule_tac x=b in pspace_alignedD') apply assumption apply (frule (3) rule_out_intv) by (fastforce simp: is_aligned_no_overflow_mask ptr_range_mask_range word_add_increasing)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b\<rbrakk> \<Longrightarrow> \<not> obj_range' b obj' \<subseteq> obj_range' a obj proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b\<rbrakk> \<Longrightarrow> \<not> {b..b + 2 ^ objBitsKO obj' - 1} \<subseteq> {a..a + 2 ^ objBitsKO obj - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj)\<rbrakk> \<Longrightarrow> \<not> {b..b + 2 ^ objBitsKO obj' - 1} \<subseteq> {a..a + 2 ^ objBitsKO obj - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj)\<rbrakk> \<Longrightarrow> \<not> {b..b + 2 ^ objBitsKO obj' - 1} \<subseteq> {a..a + 2 ^ objBitsKO obj - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj)\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj); is_aligned b (objBitsKO obj')\<rbrakk> \<Longrightarrow> \<not> {b..b + 2 ^ objBitsKO obj' - 1} \<subseteq> {a..a + 2 ^ objBitsKO obj - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj); is_aligned b (objBitsKO obj')\<rbrakk> \<Longrightarrow> \<not> {b..b + 2 ^ objBitsKO obj' - 1} \<subseteq> {a..a + 2 ^ objBitsKO obj - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; pspace_aligned' s; a \<noteq> b; is_aligned a (objBitsKO obj); is_aligned b (objBitsKO obj'); b \<notin> mask_range a (objBitsKO obj)\<rbrakk> \<Longrightarrow> \<not> {b..b + 2 ^ objBitsKO obj' - 1} \<subseteq> {a..a + 2 ^ objBitsKO obj - 1}
theory InvariantUpdates_H

lemma ps_clear_domE[elim?]:
  "\<lbrakk> ps_clear x n s; dom (ksPSpace s) = dom (ksPSpace s') \<rbrakk> \<Longrightarrow> ps_clear x n s'" by (simp add: ps_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear x n s; dom (ksPSpace s) = dom (ksPSpace s')\<rbrakk> \<Longrightarrow> ps_clear x n s'
theory InvariantUpdates_H

lemma ps_clear_upd:
  "ksPSpace s y = Some v \<Longrightarrow>
    ps_clear x n (ksPSpace_update (\<lambda>a. (ksPSpace s)(y \<mapsto> v')) s') = ps_clear x n s" by (rule iffI | clarsimp elim!: ps_clear_domE | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace s y = Some v \<Longrightarrow> ps_clear x n (s'\<lparr>ksPSpace := (ksPSpace s)(y \<mapsto> v')\<rparr>) = ps_clear x n s
theory InvariantUpdates_H

lemma ct_not_inQ_ksMachineState_update[simp]:
  "ct_not_inQ (ksMachineState_update f s) = ct_not_inQ s" by (simp add: ct_not_inQ_def)

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

lemma ct_in_current_domain_ksMachineState[simp]:
  "ct_idle_or_in_cur_domain' (ksMachineState_update p s) = ct_idle_or_in_cur_domain' s" by (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_idle_or_in_cur_domain' (ksMachineState_update p s) = ct_idle_or_in_cur_domain' s
theory InvariantUpdates_H

lemma invs'_machine:
  assumes mask: "irq_masks (f (ksMachineState s)) =
                 irq_masks (ksMachineState s)"
  assumes vms: "valid_machine_state' (ksMachineState_update f s) =
                valid_machine_state' s"
  shows "invs' (ksMachineState_update f s) = invs' s" proof - show ?thesis apply (cases "ksSchedulerAction s") apply (simp_all add: invs'_def valid_state'_def cur_tcb'_def ct_in_state'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def
                    valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs
                    vms ct_not_inQ_def
                    state_refs_of'_def ps_clear_def
                    valid_irq_node'_def mask
              cong: option.case_cong) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' (ksMachineState_update f s) = invs' s proof (state)
goal (1 subgoal):
 1. invs' (ksMachineState_update f s) = invs' s proof (prove)
goal (1 subgoal):
 1. invs' (ksMachineState_update f s) = invs' s proof (prove)
goal (3 subgoals):
 1. ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> invs' (ksMachineState_update f s) = invs' s
 2. ksSchedulerAction s = ChooseNewThread \<Longrightarrow> invs' (ksMachineState_update f s) = invs' s
 3. \<And>x3. ksSchedulerAction s = SwitchToThread x3 \<Longrightarrow> invs' (ksMachineState_update f s) = invs' s proof (prove)
goal:
No subgoals! proof (state)
this:
invs' (ksMachineState_update f s) = invs' s

goal:
No subgoals!
theory InvariantUpdates_H

lemma pspace_no_overlap_queues [simp]:
  "pspace_no_overlap' w sz (ksReadyQueues_update f s) = pspace_no_overlap' w sz s" by (simp add: pspace_no_overlap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' w sz (ksReadyQueues_update f s) = pspace_no_overlap' w sz s
theory InvariantUpdates_H

lemma pspace_no_overlap'_ksSchedulerAction[simp]:
  "pspace_no_overlap' a b (ksSchedulerAction_update f s) =
   pspace_no_overlap' a b s" by (simp add: pspace_no_overlap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' a b (ksSchedulerAction_update f s) = pspace_no_overlap' a b s
theory InvariantUpdates_H

lemma ksReadyQueues_update_id[simp]:
  "ksReadyQueues_update id s = s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksReadyQueues_update id s = s
theory InvariantUpdates_H

lemma ct_not_inQ_ksReadyQueues_update[simp]:
  "ct_not_inQ (ksReadyQueues_update f s) = ct_not_inQ s" by (simp add: ct_not_inQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_not_inQ (ksReadyQueues_update f s) = ct_not_inQ s
theory InvariantUpdates_H

lemma inQ_context[simp]:
  "inQ d p (tcbArch_update f tcb) = inQ d p tcb" by (cases tcb, simp add: inQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inQ d p (tcbArch_update f tcb) = inQ d p tcb
theory InvariantUpdates_H

lemma valid_tcb'_tcbQueued[simp]:
  "valid_tcb' (tcbQueued_update f tcb) = valid_tcb' tcb" by (cases tcb, rule ext, simp add: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb' (tcbQueued_update f tcb) = valid_tcb' tcb
theory InvariantUpdates_H

lemma valid_tcb'_tcbFault_update[simp]:
  "valid_tcb' tcb s \<Longrightarrow> valid_tcb' (tcbFault_update f tcb) s" by (clarsimp simp: valid_tcb'_def  tcb_cte_cases_def cteSizeBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb' tcb s \<Longrightarrow> valid_tcb' (tcbFault_update f tcb) s
theory InvariantUpdates_H

lemma valid_tcb'_tcbTimeSlice_update[simp]:
  "valid_tcb' (tcbTimeSlice_update f tcb) s = valid_tcb' tcb s" by (simp add:valid_tcb'_def tcb_cte_cases_def cteSizeBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb' (tcbTimeSlice_update f tcb) s = valid_tcb' tcb s
theory InvariantUpdates_H

lemma valid_queues_ksSchedulerAction_update[simp]:
  "valid_queues (ksSchedulerAction_update f s) = valid_queues s" unfolding valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues (ksSchedulerAction_update f s) = valid_queues s proof (prove)
goal (1 subgoal):
 1. ((\<forall>d p. (\<forall>t\<in>set (ksReadyQueues (ksSchedulerAction_update f s) (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t (ksSchedulerAction_update f s)) \<and> distinct (ksReadyQueues (ksSchedulerAction_update f s) (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues (ksSchedulerAction_update f s) (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap (ksSchedulerAction_update f s) d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap (ksSchedulerAction_update f s) (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues (ksSchedulerAction_update f s) (d, p) \<noteq> [])) \<and> (\<forall>d i j. ksReadyQueuesL2Bitmap (ksSchedulerAction_update f s) (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap (ksSchedulerAction_update f s) d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap (ksSchedulerAction_update f s) d !! i \<longrightarrow> ksReadyQueuesL2Bitmap (ksSchedulerAction_update f s) (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize)) = ((\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> (\<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])) \<and> (\<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i) \<and> (\<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize))
theory InvariantUpdates_H

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

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

lemma ex_cte_cap_wp_to'_gsCNodes_update[simp]:
  "ex_cte_cap_wp_to' P p (gsCNodes_update f s') = ex_cte_cap_wp_to' P p s'" by (simp add: ex_cte_cap_wp_to'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to' P p (gsCNodes_update f s') = ex_cte_cap_wp_to' P p s'
theory InvariantUpdates_H

lemma ex_cte_cap_wp_to'_gsUserPages_update[simp]:
  "ex_cte_cap_wp_to' P p (gsUserPages_update f s') = ex_cte_cap_wp_to' P p s'" by (simp add: ex_cte_cap_wp_to'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to' P p (gsUserPages_update f s') = ex_cte_cap_wp_to' P p s'
theory InvariantUpdates_H

lemma pspace_no_overlap'_gsCNodes_update[simp]:
  "pspace_no_overlap' p b (gsCNodes_update f s') = pspace_no_overlap' p b s'" by (simp add: pspace_no_overlap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' p b (gsCNodes_update f s') = pspace_no_overlap' p b s'
theory InvariantUpdates_H

lemma pspace_no_overlap'_gsUserPages_update[simp]:
  "pspace_no_overlap' p b (gsUserPages_update f s') = pspace_no_overlap' p b s'" by (simp add: pspace_no_overlap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' p b (gsUserPages_update f s') = pspace_no_overlap' p b s'
theory InvariantUpdates_H

lemma pspace_no_overlap'_ksMachineState_update[simp]:
  "pspace_no_overlap' p n (ksMachineState_update f s) =
   pspace_no_overlap' p n s" by (simp add: pspace_no_overlap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' p n (ksMachineState_update f s) = pspace_no_overlap' p n s
theory InvariantUpdates_H

lemma pspace_no_overlap_gsUntypedZeroRanges[simp]:
  "pspace_no_overlap' ptr n (gsUntypedZeroRanges_update f s)
    = pspace_no_overlap' ptr n s" by (simp add: pspace_no_overlap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' ptr n (gsUntypedZeroRanges_update f s) = pspace_no_overlap' ptr n s
theory InvariantUpdates_H

lemma vms'_ct[simp]:
  "valid_machine_state' (ksCurThread_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' (ksCurThread_update f s) = valid_machine_state' s
theory InvariantUpdates_H

lemma tcb_in_cur_domain_ct[simp]:
  "tcb_in_cur_domain' t  (ksCurThread_update f s) = tcb_in_cur_domain' t s" by (fastforce simp: tcb_in_cur_domain'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_in_cur_domain' t (ksCurThread_update f s) = tcb_in_cur_domain' t s
theory InvariantUpdates_H

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

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

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

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

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

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

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

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

lemma valid_queues_ksCurDomain[simp]:
  "valid_queues (ksCurDomain_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 (ksCurDomain_update f s) = valid_queues s
theory InvariantUpdates_H

lemma valid_queues_ksDomScheduleIdx[simp]:
  "valid_queues (ksDomScheduleIdx_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 (ksDomScheduleIdx_update f s) = valid_queues s
theory InvariantUpdates_H

lemma valid_queues_ksDomSchedule[simp]:
  "valid_queues (ksDomSchedule_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 (ksDomSchedule_update f s) = valid_queues s
theory InvariantUpdates_H

lemma valid_queues_ksDomainTime[simp]:
  "valid_queues (ksDomainTime_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 (ksDomainTime_update f s) = valid_queues s
theory InvariantUpdates_H

lemma valid_queues_ksWorkUnitsCompleted[simp]:
  "valid_queues (ksWorkUnitsCompleted_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 (ksWorkUnitsCompleted_update f s) = valid_queues s
theory InvariantUpdates_H

lemma valid_irq_node'_ksCurDomain[simp]:
  "valid_irq_node' w (ksCurDomain_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 (ksCurDomain_update f s) = valid_irq_node' w s
theory InvariantUpdates_H

lemma valid_irq_node'_ksDomScheduleIdx[simp]:
  "valid_irq_node' w (ksDomScheduleIdx_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 (ksDomScheduleIdx_update f s) = valid_irq_node' w s
theory InvariantUpdates_H

lemma valid_irq_node'_ksDomSchedule[simp]:
  "valid_irq_node' w (ksDomSchedule_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 (ksDomSchedule_update f s) = valid_irq_node' w s
theory InvariantUpdates_H

lemma valid_irq_node'_ksDomainTime[simp]:
  "valid_irq_node' w (ksDomainTime_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 (ksDomainTime_update f s) = valid_irq_node' w s
theory InvariantUpdates_H

lemma valid_irq_node'_ksWorkUnitsCompleted[simp]:
  "valid_irq_node' w (ksWorkUnitsCompleted_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 (ksWorkUnitsCompleted_update f s) = valid_irq_node' w s
theory InvariantUpdates_H

lemma ct_in_current_domain_ArchState_update[simp]:
  "ct_idle_or_in_cur_domain' (ksArchState_update f s) = ct_idle_or_in_cur_domain' s" by (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)

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

lemma pspace_no_overlap_queuesL1 [simp]:
  "pspace_no_overlap' w sz (ksReadyQueuesL1Bitmap_update f s) = pspace_no_overlap' w sz s" by (simp add: pspace_no_overlap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' w sz (ksReadyQueuesL1Bitmap_update f s) = pspace_no_overlap' w sz s
theory InvariantUpdates_H

lemma pspace_no_overlap_queuesL2 [simp]:
  "pspace_no_overlap' w sz (ksReadyQueuesL2Bitmap_update f s) = pspace_no_overlap' w sz s" by (simp add: pspace_no_overlap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap' w sz (ksReadyQueuesL2Bitmap_update f s) = pspace_no_overlap' w sz s