theory Refine

lemma kernel_corres':
  "corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle)
               and (\<lambda>s. scheduler_action s = resume_cur_thread))
             (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
              (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
              (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
             (call_kernel event)
             (do _ \<leftarrow> runExceptT $
                      handleEvent event `~catchError~`
                        (\<lambda>_. withoutPreemption $ do
                               irq <- doMachineOp (getActiveIRQ True);
                               when (isJust irq) $ handleInterrupt (fromJust irq)
                             od);
                 _ \<leftarrow> ThreadDecls_H.schedule;
                 activateThread
              od)" unfolding call_kernel_def callKernel_def apply (simp add: call_kernel_def callKernel_def) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule corres_split_handle[OF handleEvent_corres]) apply simp apply (rule corres_split[OF corres_machine_op]) apply (rule corres_underlying_trivial) apply (rule no_fail_getActiveIRQ) apply clarsimp apply (rule_tac x=irq in option_corres) apply (rule_tac P=\<top> and P'=\<top> in corres_inst) apply (simp add: when_def) apply (rule corres_when[simplified dc_def], simp) apply simp apply (rule handleInterrupt_corres[simplified dc_def]) apply simp apply (wp hoare_drop_imps hoare_vcg_all_lift)[1] apply simp apply (rule_tac Q="\<lambda>irq s. invs' s \<and>
                              (\<forall>irq'. irq = Some irq' \<longrightarrow>
                                 intStateIRQTable (ksInterruptState s ) irq' \<noteq>
                                 IRQInactive)"
                      in hoare_post_imp) apply simp apply (wp doMachineOp_getActiveIRQ_IRQ_active handle_event_valid_sched | simp)+ apply (rule_tac Q="\<lambda>_. \<top>" and E="\<lambda>_. invs'" in hoare_post_impErr) apply wpsimp+ apply (simp add: invs'_def valid_state'_def) apply (rule corres_split[OF schedule_corres]) apply (rule activateThread_corres) apply (wp handle_interrupt_valid_sched[unfolded non_kernel_IRQs_def, simplified]
                 schedule_invs' hoare_vcg_if_lift2 hoare_drop_imps |simp)+ apply (rule_tac Q="\<lambda>_. valid_sched and invs and valid_list" and
                     E="\<lambda>_. valid_sched and invs and valid_list"
            in hoare_post_impErr) apply (wp handle_event_valid_sched hoare_vcg_imp_lift' |simp)+ apply (clarsimp simp: active_from_running) apply (clarsimp simp: active_from_running') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (call_kernel event) (do _ <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
_ <- ThreadDecls_H.schedule;
activateThread
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (do handle_event event <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
state_ext_sched_class.schedule;
activate_thread
od) (do _ <- runExceptT $ handleEvent event `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
_ <- ThreadDecls_H.schedule;
activateThread
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (do y <- handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od));
_ <- ThreadDecls_H.schedule;
activateThread
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do y <- handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od));
_ <- ThreadDecls_H.schedule;
activateThread
od)
 2. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres ?r'4 ?P4 ?P'4 (handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od))) (handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)))
 2. \<And>y uu_. ?r'4 y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 3. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>uu_ uua_. dc uu_ uua_ \<Longrightarrow> corres (?f9 \<oplus> dc) (?E9 uu_) (?E'9 uua_) (liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) (liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od))
 2. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E9\<rbrace>
 3. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'9\<rbrace>
 4. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 5. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>uua_. corres dc (?E9 ()) (?E'9 uua_) (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od) (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)
 2. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E9\<rbrace>
 3. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'9\<rbrace>
 4. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 5. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (11 subgoals):
 1. \<And>uua_. corres_underlying Id False True (?r'14 uua_) (?P20 ()) (?Q15 uua_) (getActiveIRQ True) (getActiveIRQ True)
 2. \<And>uua_ irq irqa. ?r'14 uua_ irq irqa \<Longrightarrow> corres dc (?R14 uua_ irq) (?R'14 uua_ irqa) (when (\<exists>y. irq = Some y) (handle_interrupt (the irq))) (when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)))
 3. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?R14 uua_\<rbrace>
 4. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>?R'14 uua_\<rbrace>
 5. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. ?P20 a \<circ> machine_state and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. ?Q15 uua_ \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 7. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 8. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>uua_. True \<Longrightarrow> no_fail (?Q15 uua_) (getActiveIRQ True)
 2. \<And>uua_ irq irqa. irq = irqa \<Longrightarrow> corres dc (?R14 uua_ irq) (?R'14 uua_ irqa) (when (\<exists>y. irq = Some y) (handle_interrupt (the irq))) (when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)))
 3. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?R14 uua_\<rbrace>
 4. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>?R'14 uua_\<rbrace>
 5. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. ?Q15 uua_ \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 7. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 8. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>uua_ irq irqa. irq = irqa \<Longrightarrow> corres dc (?R14 uua_ irq) (?R'14 uua_ irqa) (when (\<exists>y. irq = Some y) (handle_interrupt (the irq))) (when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)))
 2. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?R14 uua_\<rbrace>
 3. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>?R'14 uua_\<rbrace>
 4. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 5. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 6. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 7. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 9. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 10. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>uua_ irq. corres (\<lambda>a b. True) (?R14 uua_ irq) (?R'14 uua_ irq) (when (\<exists>y. irq = Some y) (handle_interrupt (the irq))) (when (\<exists>y. irq = Some y) (handleInterrupt (the irq)))
 2. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?R14 uua_\<rbrace>
 3. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>?R'14 uua_\<rbrace>
 4. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 5. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 6. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 7. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 9. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 10. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (12 subgoals):
 1. \<And>uua_ irq. \<lbrakk>irq = None; irq = None\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?P31 uua_ irq) (?P'31 uua_ irq) (when (\<exists>y. None = Some y) (handle_interrupt (the None))) (when (\<exists>y. None = Some y) (handleInterrupt (the None)))
 2. \<And>uua_ irq z z'. \<lbrakk>irq = Some z; irq = Some z'\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?Q31 uua_ irq z) (?Q'31 uua_ irq z') (when (\<exists>y. Some z = Some y) (handle_interrupt (the (Some z)))) (when (\<exists>y. Some z' = Some y) (handleInterrupt (the (Some z'))))
 3. \<And>_ irq. (irq = None) = (irq = None)
 4. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> ?P31 uua_ irq s) \<and> (\<forall>z. irq = Some z \<longrightarrow> ?Q31 uua_ irq z s)\<rbrace>
 5. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> ?P'31 uua_ irq s) \<and> (\<forall>z. irq = Some z \<longrightarrow> ?Q'31 uua_ irq z s)\<rbrace>
 6. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 8. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 9. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>_ irq. \<lbrakk>irq = None; irq = None\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>_. True) (when (\<exists>y. None = Some y) (handle_interrupt (the None))) (when (\<exists>y. None = Some y) (handleInterrupt (the None)))
 2. \<And>uua_ irq z z'. \<lbrakk>irq = Some z; irq = Some z'\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?Q31 uua_ irq z) (?Q'31 uua_ irq z') (when (\<exists>y. Some z = Some y) (handle_interrupt (the (Some z)))) (when (\<exists>y. Some z' = Some y) (handleInterrupt (the (Some z'))))
 3. \<And>_ irq. (irq = None) = (irq = None)
 4. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> ?Q31 uua_ irq z s)\<rbrace>
 5. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> ?Q'31 uua_ irq z s)\<rbrace>
 6. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 7. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 8. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 9. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>uua_ irq z z'. \<lbrakk>irq = Some z; irq = Some z'\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?Q31 uua_ irq z) (?Q'31 uua_ irq z') (when (\<exists>y. Some z = Some y) (handle_interrupt (the (Some z)))) (when (\<exists>y. Some z' = Some y) (handleInterrupt (the (Some z'))))
 2. \<And>_ irq. (irq = None) = (irq = None)
 3. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> ?Q31 uua_ irq z s)\<rbrace>
 4. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> ?Q'31 uua_ irq z s)\<rbrace>
 5. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 7. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 8. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>uua_ irq z z'. \<lbrakk>irq = Some z; irq = Some z'\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. True) (?P36 uua_ irq z) (?P'38 uua_ irq z') (handle_interrupt (the (Some z))) (handleInterrupt (the (Some z')))
 2. \<And>_ irq. (irq = None) = (irq = None)
 3. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> ?P36 uua_ irq z s)\<rbrace>
 4. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> ?P'38 uua_ irq z s)\<rbrace>
 5. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 7. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 8. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>uua_ irq z. irq = Some z \<Longrightarrow> corres (\<lambda>rv rv'. True) (?P36 uua_ (Some z) z) (?P'38 uua_ (Some z) z) (handle_interrupt z) (handleInterrupt z)
 2. \<And>_ irq. (irq = None) = (irq = None)
 3. \<And>uua_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> ?P36 uua_ irq z s)\<rbrace>
 4. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> ?P'38 uua_ irq z s)\<rbrace>
 5. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 6. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 7. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 8. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>_ irq. (irq = None) = (irq = None)
 2. \<And>_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> einvs s)\<rbrace>
 3. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) z \<noteq> irqstate.IRQInactive)) s)\<rbrace>
 4. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 5. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 6. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 7. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 9. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 10. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>_. \<lbrace>?Q18 ()\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> einvs s)\<rbrace>
 2. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) z \<noteq> irqstate.IRQInactive)) s)\<rbrace>
 3. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and ?Q18 a\<rbrace>
 4. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 5. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 6. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 8. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>_ z. irq_state_independent_A einvs
 2. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) z \<noteq> irqstate.IRQInactive)) s)\<rbrace>
 3. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and (\<lambda>a. True \<and> (\<forall>x. einvs a))\<rbrace>
 4. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 5. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 6. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 8. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. (irq = None \<longrightarrow> True) \<and> (\<forall>z. irq = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) z \<noteq> irqstate.IRQInactive)) s)\<rbrace>
 2. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and (\<lambda>a. True \<and> (\<forall>x. einvs a))\<rbrace>
 3. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 4. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 5. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>_ rv s. invs' s \<and> (\<forall>irq'. rv = Some irq' \<longrightarrow> intStateIRQTable (ksInterruptState s) irq' \<noteq> irqstate.IRQInactive) \<Longrightarrow> (rv = None \<longrightarrow> True) \<and> (\<forall>z. rv = Some z \<longrightarrow> (\<exists>y. Some z = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) z \<noteq> irqstate.IRQInactive)) s)
 2. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. invs' s \<and> (\<forall>irq'. irq = Some irq' \<longrightarrow> intStateIRQTable (ksInterruptState s) irq' \<noteq> irqstate.IRQInactive)\<rbrace>
 3. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and (\<lambda>a. True \<and> (\<forall>x. einvs a))\<rbrace>
 4. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 5. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 6. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 8. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>uua_. \<lbrace>?Q'14 uua_\<rbrace> doMachineOp (getActiveIRQ True) \<lbrace>\<lambda>irq s. invs' s \<and> (\<forall>irq'. irq = Some irq' \<longrightarrow> intStateIRQTable (ksInterruptState s) irq' \<noteq> irqstate.IRQInactive)\<rbrace>
 2. \<lbrace>?Q9\<rbrace> handle_event event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a. (\<lambda>a. True) \<circ> machine_state and (\<lambda>a. True \<and> (\<forall>x. einvs a))\<rbrace>
 3. \<lbrace>?Q'9\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uua_. (\<lambda>_. True) \<circ> ksMachineState and ?Q'14 uua_\<rbrace>
 4. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 5. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and ?Q9 and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ?Q'9 and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?P'86\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>
 2. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 3. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> valid_list s \<and> (invs and valid_sched and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> True) and ?Q4) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> ?P'86 s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<lbrace>?P'86\<rbrace> handleEvent event \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>rv s. True \<Longrightarrow> True
 3. \<And>e s. invs' s \<Longrightarrow> valid_irq_states' s
 4. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 5. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> valid_list s \<and> (invs and valid_sched and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> ?P'86 s) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>s. invs' s \<Longrightarrow> valid_irq_states' s
 2. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 3. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> valid_list s \<and> (invs and valid_sched and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> True) and ?Q4) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> corres dc (?R4 y) (?R'4 uu_) (do y <- state_ext_sched_class.schedule;
activate_thread
od) (do _ <- ThreadDecls_H.schedule;
activateThread
od)
 2. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> valid_list s \<and> (invs and valid_sched and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> True) and ?Q4) s
 5. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>y uu_ ya uua_. \<lbrakk>(?f9 \<oplus> dc) y uu_; dc ya uua_\<rbrakk> \<Longrightarrow> corres dc (?R101 y uu_ ya) (?R'101 y uu_ uua_) activate_thread activateThread
 2. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> \<lbrace>?Q102 y\<rbrace> state_ext_sched_class.schedule \<lbrace>?R101 y uu_\<rbrace>
 3. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> \<lbrace>?Q'103 uu_\<rbrace> ThreadDecls_H.schedule \<lbrace>?R'101 y uu_\<rbrace>
 4. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>\<lambda>y. invs and valid_sched and valid_list and ?Q102 y\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>\<lambda>uu_. invs' and ?Q'103 uu_\<rbrace>
 6. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> valid_list s \<and> (invs and valid_sched and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> True) and ?Q4) s
 7. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> True) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> \<lbrace>?Q102 y\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>ya. invs and ct_in_state activatable\<rbrace>
 2. \<And>y uu_. (?f9 \<oplus> dc) y uu_ \<Longrightarrow> \<lbrace>?Q'103 uu_\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>_. invs' and ct_in_state' activatable'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> handle_event event <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>\<lambda>y. invs and valid_sched and valid_list and ?Q102 y\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>\<lambda>uu_. invs' and ?Q'103 uu_\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> valid_list s \<and> (invs and valid_sched and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> True) and ?Q4) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'151\<rbrace> handle_event event \<lbrace>\<lambda>y s. invs s \<and> valid_sched s \<and> valid_list s \<and> invs s\<rbrace>, \<lbrace>\<lambda>rv s. valid_sched s \<and> invs s \<and> valid_list s \<and> invs s \<and> valid_sched s \<and> valid_list s \<and> invs s\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>\<lambda>_. invs' and (\<lambda>s. invs' s \<and> invs' s)\<rbrace>
 3. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> valid_list s \<and> (invs and valid_sched and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> True) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> ?P'151 s)) s
 4. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> True) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?P'151\<rbrace> handle_event event \<lbrace>\<lambda>_. valid_sched and invs and valid_list\<rbrace>, \<lbrace>\<lambda>_. valid_sched and invs and valid_list\<rbrace>
 2. \<And>rv s. (valid_sched and invs and valid_list) s \<Longrightarrow> invs s \<and> valid_sched s \<and> valid_list s \<and> invs s
 3. \<And>e s. (valid_sched and invs and valid_list) s \<Longrightarrow> valid_sched s \<and> invs s \<and> valid_list s \<and> invs s \<and> valid_sched s \<and> valid_list s \<and> invs s
 4. \<lbrace>?Q'4\<rbrace> handleEvent event <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od)) \<lbrace>\<lambda>_. invs' and (\<lambda>s. invs' s \<and> invs' s)\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> valid_list s \<and> (invs and valid_sched and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<and> True) and (\<lambda>s. (invs s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> ?P'151 s)) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<Longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> (event \<noteq> Interrupt \<longrightarrow> ct_active s)
 2. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> True) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> True) and (\<lambda>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s)) s proof (prove)
goal:
No subgoals!