theory Interrupt_R

lemma is_irq_active_corres:
  "corres (=) \<top> \<top> (is_irq_active irq) (isIRQActive irq)" apply (simp add: is_irq_active_def isIRQActive_def get_irq_state_def
                   getIRQState_def getInterruptState_def) apply (clarsimp simp: state_relation_def interrupt_state_relation_def) apply (drule_tac x=irq in spec)+ apply (simp add: irq_state_relation_def
            split: irqstate.split_asm irq_state.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (is_irq_active irq) (isIRQActive irq) proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> (interrupt_states s irq = irq_state.IRQInactive) = (intStateIRQTable (ksInterruptState s') irq = irqstate.IRQInactive) proof (prove)
goal (1 subgoal):
 1. \<And>s s' node irqs'. \<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_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; cur_thread s = ksCurThread s'; ksInterruptState s' = InterruptState node irqs'; idle_thread s = ksIdleThread s'; \<forall>irq. interrupt_irq_node s irq = node + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits); \<forall>irq. irq_state_relation (interrupt_states s irq) (irqs' irq); 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> (interrupt_states s irq = irq_state.IRQInactive) = (irqs' irq = irqstate.IRQInactive) proof (prove)
goal (1 subgoal):
 1. \<And>s s' node irqs'. \<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_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; cur_thread s = ksCurThread s'; ksInterruptState s' = InterruptState node irqs'; 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'; interrupt_irq_node s irq = node + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits); irq_state_relation (interrupt_states s irq) (irqs' irq)\<rbrakk> \<Longrightarrow> (interrupt_states s irq = irq_state.IRQInactive) = (irqs' irq = irqstate.IRQInactive) proof (prove)
goal:
No subgoals!