kings-crown/FVELER_Isabelle huggingface dataset:
theory InvariantUpdates_H

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

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

lemma ct_idle_or_in_cur_domain'_ksSchedulerAction_update[simp]:
  "b \<noteq> ResumeCurrentThread \<Longrightarrow>
   ct_idle_or_in_cur_domain' (s\<lparr>ksSchedulerAction := b\<rparr>)" apply (clarsimp simp add: ct_idle_or_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<noteq> ResumeCurrentThread \<Longrightarrow> ct_idle_or_in_cur_domain' (s\<lparr>ksSchedulerAction := b\<rparr>) proof (prove)
goal:
No subgoals!
theory InvariantUpdates_H

lemma sch_act_simple_wu [simp, intro!]:
  "sch_act_simple (ksWorkUnitsCompleted_update f s) = sch_act_simple s" by (simp add: sch_act_simple_def)

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

lemma sch_act_simple_ksPSpace_update[simp]:
  "sch_act_simple (ksPSpace_update f s) = sch_act_simple s" apply (simp add: sch_act_simple_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_simple (ksPSpace_update f s) = sch_act_simple s proof (prove)
goal:
No subgoals!
theory InvariantUpdates_H

lemma ps_clear_ksReadyQueue[simp]:
  "ps_clear x n (ksReadyQueues_update f s) = ps_clear x n s" by (simp add: ps_clear_def)

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

lemma inQ_tcbIPCBuffer_update_idem[simp]:
  "inQ d p (tcbIPCBuffer_update f ko) = inQ d p ko" by (clarsimp simp: inQ_def)

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

lemma valid_mdb_interrupts'[simp]:
  "valid_mdb' (ksInterruptState_update f s) = valid_mdb' s" by (simp add: valid_mdb'_def)

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

lemma vms_ksReadyQueues_update[simp]:
  "valid_machine_state' (ksReadyQueues_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' (ksReadyQueues_update f s) = valid_machine_state' s
theory InvariantUpdates_H

lemma ct_in_state'_ksMachineState_update[simp]:
  "ct_in_state' x (ksMachineState_update f s) = ct_in_state' x s" by (simp add: ct_in_state'_def)+

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

lemma ex_cte_cap_wp_to'_ksMachineState_update[simp]:
  "ex_cte_cap_wp_to' x y (ksMachineState_update f s) = ex_cte_cap_wp_to' x y s" by (simp add: ex_cte_cap_wp_to'_def)+

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

lemma ps_clear_ksMachineState_update[simp]:
  "ps_clear a b (ksMachineState_update f s) = ps_clear a b s" by (simp add: ps_clear_def)

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

lemma valid_arch_state'_interrupt[simp]:
  "valid_arch_state' (ksInterruptState_update f s) = valid_arch_state' s" by (simp add: valid_arch_state'_def cong: option.case_cong)

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

lemma valid_bitmapQ_ksSchedulerAction_upd[simp]:
  "valid_bitmapQ (ksSchedulerAction_update f s) = valid_bitmapQ s" unfolding bitmapQ_defs by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bitmapQ (ksSchedulerAction_update f s) = valid_bitmapQ s proof (prove)
goal (1 subgoal):
 1. (\<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> [])) = (\<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []))
theory InvariantUpdates_H

lemma bitmapQ_no_L2_orphans_ksSchedulerAction_upd[simp]:
  "bitmapQ_no_L2_orphans (ksSchedulerAction_update f s) = bitmapQ_no_L2_orphans s" unfolding bitmapQ_defs by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bitmapQ_no_L2_orphans (ksSchedulerAction_update f s) = bitmapQ_no_L2_orphans s proof (prove)
goal (1 subgoal):
 1. (\<forall>d i j. ksReadyQueuesL2Bitmap (ksSchedulerAction_update f s) (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap (ksSchedulerAction_update f s) d !! i) = (\<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i)
theory InvariantUpdates_H

lemma cur_tcb'_ksReadyQueuesL1Bitmap_upd[simp]:
  "cur_tcb' (ksReadyQueuesL1Bitmap_update f s) = cur_tcb' s" unfolding cur_tcb'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_tcb' (ksReadyQueuesL1Bitmap_update f s) = cur_tcb' s proof (prove)
goal (1 subgoal):
 1. tcb_at' (ksCurThread (ksReadyQueuesL1Bitmap_update f s)) (ksReadyQueuesL1Bitmap_update f s) = tcb_at' (ksCurThread s) s
theory InvariantUpdates_H

lemma cur_tcb'_ksReadyQueuesL2Bitmap_upd[simp]:
  "cur_tcb' (ksReadyQueuesL2Bitmap_update f s) = cur_tcb' s" unfolding cur_tcb'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_tcb' (ksReadyQueuesL2Bitmap_update f s) = cur_tcb' s proof (prove)
goal (1 subgoal):
 1. tcb_at' (ksCurThread (ksReadyQueuesL2Bitmap_update f s)) (ksReadyQueuesL2Bitmap_update f s) = tcb_at' (ksCurThread s) s
theory InvariantUpdates_H

lemma ex_cte_cap_wp_to'_ksReadyQueuesL1Bitmap[simp]:
   "ex_cte_cap_wp_to' P p (ksReadyQueuesL1Bitmap_update f s) = ex_cte_cap_wp_to' P p s" unfolding ex_cte_cap_wp_to'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to' P p (ksReadyQueuesL1Bitmap_update f s) = ex_cte_cap_wp_to' P p s proof (prove)
goal (1 subgoal):
 1. (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' (ksReadyQueuesL1Bitmap_update f s))) cref (ksReadyQueuesL1Bitmap_update f s)) = (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s)
theory InvariantUpdates_H

lemma ex_cte_cap_wp_to'_ksReadyQueuesL2Bitmap[simp]:
   "ex_cte_cap_wp_to' P p (ksReadyQueuesL2Bitmap_update f s) = ex_cte_cap_wp_to' P p s" unfolding ex_cte_cap_wp_to'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to' P p (ksReadyQueuesL2Bitmap_update f s) = ex_cte_cap_wp_to' P p s proof (prove)
goal (1 subgoal):
 1. (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' (ksReadyQueuesL2Bitmap_update f s))) cref (ksReadyQueuesL2Bitmap_update f s)) = (\<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s)
theory InvariantUpdates_H

lemma sch_act_simple_readyQueue[simp]:
  "sch_act_simple (ksReadyQueues_update f s) = sch_act_simple s" apply (simp add: sch_act_simple_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_simple (ksReadyQueues_update f s) = sch_act_simple s proof (prove)
goal:
No subgoals!
theory InvariantUpdates_H

lemma sch_act_simple_ksReadyQueuesL1Bitmap[simp]:
  "sch_act_simple (ksReadyQueuesL1Bitmap_update f s) = sch_act_simple s" apply (simp add: sch_act_simple_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_simple (ksReadyQueuesL1Bitmap_update f s) = sch_act_simple s proof (prove)
goal:
No subgoals!
theory InvariantUpdates_H

lemma sch_act_simple_ksReadyQueuesL2Bitmap[simp]:
  "sch_act_simple (ksReadyQueuesL2Bitmap_update f s) = sch_act_simple s" apply (simp add: sch_act_simple_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_simple (ksReadyQueuesL2Bitmap_update f s) = sch_act_simple s proof (prove)
goal:
No subgoals!
theory InvariantUpdates_H

lemma ksDomainTime_invs[simp]:
  "invs' (ksDomainTime_update f s) = invs' s" by (simp add:invs'_def valid_state'_def
    cur_tcb'_def ct_not_inQ_def ct_idle_or_in_cur_domain'_def
    tcb_in_cur_domain'_def valid_machine_state'_def)

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

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

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

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

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

lemma sch_act_sane_ksMachineState[simp]:
  "sch_act_sane (ksMachineState_update f s) = sch_act_sane s" by (simp add: sch_act_sane_def)

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

lemma invs'_update_cnt[elim!]:
  "invs' s \<Longrightarrow> invs' (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)" by (clarsimp simp: invs'_def valid_state'_def valid_queues_def valid_queues'_def
                      valid_irq_node'_def cur_tcb'_def ct_idle_or_in_cur_domain'_def
                      tcb_in_cur_domain'_def valid_queues_no_bitmap_def
                      bitmapQ_no_L2_orphans_def bitmapQ_no_L1_orphans_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> invs' (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)
theory StateRelation

lemma obj_relation_cuts_def2:
  "obj_relation_cuts ko x =
   (case ko of CNode sz cs \<Rightarrow> if well_formed_cnode_n sz cs
                             then {(cte_map (x, y), cte_relation y) | y. y \<in> dom cs}
                             else {(x, \<bottom>\<bottom>)}
             | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pte_relation y))
                                           ` (UNIV :: word8 set)
             | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pde_relation y))
                                           ` (UNIV :: 12 word set)
             | ArchObj (DataPage dev sz)      \<Rightarrow>
                 {(x + n * 2 ^ pageBits,  \<lambda>_ obj. obj =(if dev then KOUserDataDevice else KOUserData)) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
             | _ \<Rightarrow> {(x, other_obj_relation)})" by (simp split: Structures_A.kernel_object.split
                  ARM_A.arch_kernel_obj.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_relation_cuts ko x = (case ko of CNode sz cs \<Rightarrow> if well_formed_cnode_n sz cs then {(cte_map (x, y), cte_relation y) |y. y \<in> dom cs} else {(x, \<lambda>_ _. False)} | ArchObj (arch_kernel_obj.ASIDPool fun) \<Rightarrow> {(x, other_obj_relation)} | ArchObj (PageTable pt) \<Rightarrow> range (\<lambda>y. (x + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y)) | ArchObj (PageDirectory pd) \<Rightarrow> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)) | ArchObj (DataPage dev sz) \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = (if dev then KOUserDataDevice else KOUserData)) |n. n < 2 ^ (pageBitsForSize sz - pageBits)} | _ \<Rightarrow> {(x, other_obj_relation)})
theory StateRelation

lemma obj_relation_cuts_def3:
  "obj_relation_cuts ko x =
  (case (a_type ko) of
     ACapTable n \<Rightarrow> {(cte_map (x, y), cte_relation y) | y. length y = n}
   | AArch APageTable \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pte_relation y))
                            ` (UNIV :: word8 set)
   | AArch APageDirectory \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pde_relation y))
                            ` (UNIV :: 12 word set)
   | AArch (AUserData sz)  \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserData) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
   | AArch (ADeviceData sz)  \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserDataDevice ) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
   | AGarbage _ \<Rightarrow> {(x, \<bottom>\<bottom>)}
   | _ \<Rightarrow> {(x, other_obj_relation)})" apply (simp add: obj_relation_cuts_def2 a_type_def
            split: Structures_A.kernel_object.split
                  ARM_A.arch_kernel_obj.split) apply (clarsimp simp: well_formed_cnode_n_def length_set_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_relation_cuts ko x = (case a_type ko of ACapTable n \<Rightarrow> {(cte_map (x, y), cte_relation y) |y. length y = n} | AGarbage xa \<Rightarrow> {(x, \<lambda>_ _. False)} | AArch AASIDPool \<Rightarrow> {(x, other_obj_relation)} | AArch APageTable \<Rightarrow> range (\<lambda>y. (x + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y)) | AArch APageDirectory \<Rightarrow> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)) | AArch (AUserData sz) \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserData) |n. n < 2 ^ (pageBitsForSize sz - pageBits)} | AArch (ADeviceData sz) \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserDataDevice) |n. n < 2 ^ (pageBitsForSize sz - pageBits)} | _ \<Rightarrow> {(x, other_obj_relation)}) proof (prove)
goal (1 subgoal):
 1. \<forall>x11 x12. well_formed_cnode_n x11 x12 \<longrightarrow> ko = CNode x11 x12 \<longrightarrow> {(cte_map (x, y), cte_relation y) |y. y \<in> dom x12} = {(cte_map (x, y), cte_relation y) |y. length y = x11} proof (prove)
goal:
No subgoals!
theory StateRelation

lemma is_other_obj_relation_type_CapTable:
  "\<not> is_other_obj_relation_type (ACapTable n)" by (simp add: is_other_obj_relation_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_other_obj_relation_type (ACapTable n)
theory StateRelation

lemma is_other_obj_relation_type_UserData:
  "\<not> is_other_obj_relation_type (AArch (AUserData sz))" unfolding is_other_obj_relation_type_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_other_obj_relation_type (AArch (AUserData sz)) proof (prove)
goal (1 subgoal):
 1. \<not> (case AArch (AUserData sz) of ACapTable n \<Rightarrow> False | AGarbage x \<Rightarrow> False | AArch AASIDPool \<Rightarrow> True | AArch _ \<Rightarrow> False | _ \<Rightarrow> True)
theory StateRelation

lemma is_other_obj_relation_type_DeviceData:
  "\<not> is_other_obj_relation_type (AArch (ADeviceData sz))" unfolding is_other_obj_relation_type_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_other_obj_relation_type (AArch (ADeviceData sz)) proof (prove)
goal (1 subgoal):
 1. \<not> (case AArch (ADeviceData sz) of ACapTable n \<Rightarrow> False | AGarbage x \<Rightarrow> False | AArch AASIDPool \<Rightarrow> True | AArch _ \<Rightarrow> False | _ \<Rightarrow> True)
theory StateRelation

lemma is_other_obj_relation_type:
  "is_other_obj_relation_type (a_type ko) \<Longrightarrow>
   obj_relation_cuts ko x = {(x, other_obj_relation)}" by (simp add: obj_relation_cuts_def3 is_other_obj_relation_type_def
         split: a_type.splits aa_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_other_obj_relation_type (a_type ko) \<Longrightarrow> obj_relation_cuts ko x = {(x, other_obj_relation)}
theory StateRelation

lemma eq_trans_helper:
  "\<lbrakk> x = y; P y = Q \<rbrakk> \<Longrightarrow> P x = Q" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; P y = Q\<rbrakk> \<Longrightarrow> P x = Q
theory StateRelation

lemma cap_relation_case':
  "cap_relation cap cap'
     = (case cap of cap.ArchObjectCap arch_cap.ASIDControlCap \<Rightarrow> cap_relation cap cap'
            | _ \<Rightarrow> cap_relation cap cap')" by (simp split: cap.split arch_cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation cap cap' = (case cap of cap.ArchObjectCap (arch_cap.ASIDPoolCap word1 word2) \<Rightarrow> cap_relation cap cap' | cap.ArchObjectCap _ \<Rightarrow> cap_relation cap cap' | _ \<Rightarrow> cap_relation cap cap')
theory StateRelation

lemma mi_map_label[simp]: "msgLabel (message_info_map mi) = mi_label mi" by (cases mi, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msgLabel (message_info_map mi) = mi_label mi
theory StateRelation

lemma curthread_relation:
  "(a, b) \<in> state_relation \<Longrightarrow> ksCurThread b = cur_thread a" by (simp add: state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> state_relation \<Longrightarrow> ksCurThread b = cur_thread a
theory StateRelation

lemma state_relation_pspace_relation[elim!]:
  "(s,s') \<in> state_relation \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')" by (simp add: state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> state_relation \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
theory StateRelation

lemma state_relation_ekheap_relation[elim!]:
  "(s,s') \<in> state_relation \<Longrightarrow> ekheap_relation (ekheap s) (ksPSpace s')" by (simp add: state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> state_relation \<Longrightarrow> ekheap_relation (ekheap s) (ksPSpace s')
theory StateRelation

lemma state_relationE [elim?]:
  assumes sr:  "(s, s') \<in> state_relation"
  and rl: "\<lbrakk>pspace_relation (kheap s) (ksPSpace s');
  ekheap_relation (ekheap s) (ksPSpace s');
  sched_act_relation (scheduler_action s) (ksSchedulerAction s');
  ready_queues_relation (ready_queues s) (ksReadyQueues s');
  ghost_relation (kheap s) (gsUserPages s') (gsCNodes s');
  cdt_relation (swp cte_at s) (cdt s) (ctes_of s') \<and>
  revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s');
  cdt_list_relation (cdt_list s) (cdt s) (ctes_of s');
  (arch_state s, ksArchState s') \<in> arch_state_relation;
  interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s');
  cur_thread s = ksCurThread s';
  idle_thread s = ksIdleThread s';
  machine_state s = ksMachineState s';
  work_units_completed s = ksWorkUnitsCompleted s';
  domain_index s = ksDomScheduleIdx s';
  domain_list s = ksDomSchedule s';
  cur_domain s = ksCurDomain s';
  domain_time s = ksDomainTime s' \<rbrakk> \<Longrightarrow> R"
  shows "R" using sr by (blast intro!: rl dest: state_relationD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. R
theory StateRelation

lemma isCNodeCap_cap_map [simp]:
  "cap_relation c c' \<Longrightarrow> isCNodeCap c' = is_cnode_cap c" apply (cases c, simp_all add: isCap_defs split: sum.splits) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> isCNodeCap c' = is_cnode_cap c proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<not> (case c' of capability.CNodeCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!
theory StateRelation

lemma sts_rel_idle :
  "thread_state_relation st IdleThreadState = (st = Structures_A.IdleThreadState)" by (cases st, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_state_relation st Structures_H.thread_state.IdleThreadState = idle st
theory StateRelation

lemma pspace_dom_revE:
  "\<lbrakk> x \<in> pspace_dom ps; \<And>ko y P. \<lbrakk> ps y = Some ko; (x, P) \<in> obj_relation_cuts ko y \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by (clarsimp simp add: pspace_dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> pspace_dom ps; \<And>ko y P. \<lbrakk>ps y = Some ko; (x, P) \<in> obj_relation_cuts ko y\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory StateRelation

lemma pspace_dom_relatedE:
  "\<lbrakk> s' x = Some ko'; pspace_relation s s';
     \<And>y ko P. \<lbrakk> s y = Some ko; (x, P) \<in> obj_relation_cuts ko y; P ko ko' \<rbrakk> \<Longrightarrow> R
        \<rbrakk> \<Longrightarrow> R" apply (rule pspace_dom_revE [OF in_related_pspace_dom],
         assumption+) apply (frule(1) pspace_relation_absD) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' x = Some ko'; pspace_relation s s'; \<And>y ko P. \<lbrakk>s y = Some ko; (x, P) \<in> obj_relation_cuts ko y; P ko ko'\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>ko y P. \<lbrakk>s' x = Some ko'; pspace_relation s s'; \<And>y ko P. \<lbrakk>s y = Some ko; (x, P) \<in> obj_relation_cuts ko y; P ko ko'\<rbrakk> \<Longrightarrow> R; s y = Some ko; (x, P) \<in> obj_relation_cuts ko y\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>ko y P. \<lbrakk>s' x = Some ko'; pspace_relation s s'; \<And>y ko P. \<lbrakk>s y = Some ko; (x, P) \<in> obj_relation_cuts ko y; P ko ko'\<rbrakk> \<Longrightarrow> R; s y = Some ko; (x, P) \<in> obj_relation_cuts ko y; \<forall>(x', P)\<in>obj_relation_cuts ko y. \<exists>z. s' x' = Some z \<and> P ko z\<rbrakk> \<Longrightarrow> R proof (prove)
goal:
No subgoals!
theory StateRelation

lemma ghost_relation_typ_at:
  "ghost_relation (kheap s) ups cns \<equiv>
   (\<forall>a sz. data_at sz a s = (ups a = Some sz)) \<and>
   (\<forall>a n. typ_at (ACapTable n) a s = (cns a = Some n))" apply (rule eq_reflection) apply (clarsimp simp: ghost_relation_def typ_at_eq_kheap_obj data_at_def) apply (intro conjI impI iffI allI; force) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ghost_relation (kheap s) ups cns \<equiv> (\<forall>a sz. data_at sz a s = (ups a = Some sz)) \<and> (\<forall>a n. typ_at (ACapTable n) a s = (cns a = Some n)) proof (prove)
goal (1 subgoal):
 1. ghost_relation (kheap s) ups cns = ((\<forall>a sz. data_at sz a s = (ups a = Some sz)) \<and> (\<forall>a n. typ_at (ACapTable n) a s = (cns a = Some n))) proof (prove)
goal (1 subgoal):
 1. ((\<forall>a sz. (\<exists>dev. kheap s a = Some (ArchObj (DataPage dev sz))) = (ups a = Some sz)) \<and> (\<forall>a n. (\<exists>cs. kheap s a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns a = Some n))) = ((\<forall>a sz. (kheap s a = Some (ArchObj (DataPage False sz)) \<or> kheap s a = Some (ArchObj (DataPage True sz))) = (ups a = Some sz)) \<and> (\<forall>a n. (\<exists>cs. kheap s a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns a = Some n))) proof (prove)
goal:
No subgoals!