theory StateRelation

lemma state_relationD:
  assumes sr:  "(s, s') \<in> state_relation"
  shows "pspace_relation (kheap s) (ksPSpace s') \<and>
  ekheap_relation (ekheap s) (ksPSpace s') \<and>
  sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and>
  ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and>
  ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and>
  cdt_relation (swp cte_at s) (cdt s) (ctes_of s') \<and>
  cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and>
  revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and>
  (arch_state s, ksArchState s') \<in> arch_state_relation \<and>
  interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and>
  cur_thread s = ksCurThread s' \<and>
  idle_thread s = ksIdleThread s' \<and>
  machine_state s = ksMachineState s' \<and>
  work_units_completed s = ksWorkUnitsCompleted s' \<and>
  domain_index s = ksDomScheduleIdx s' \<and>
  domain_list s = ksDomSchedule s' \<and>
  cur_domain s = ksCurDomain s' \<and>
  domain_time s = ksDomainTime s'" using sr unfolding state_relation_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule s' \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s' proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule s' \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s' proof (prove)
using this:
(s, s') \<in> {(s, s'). pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule s' \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s'}

goal (1 subgoal):
 1. pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule s' \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s'