theory ArchADT_IF_Refine

lemma handle_preemption_if_corres[ADT_IF_Refine_assms]:
  "corres (=) (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s))
              (invs') (handle_preemption_if tc) (handlePreemption_if tc)" apply (simp add: handlePreemption_if_def handle_preemption_if_def) apply (rule corres_guard_imp) apply (rule corres_split[where r'="(=)"]) apply (rule dmo_getActiveIRQ_corres) apply (rule corres_split[where r'="dc"]) apply (rule corres_when) apply simp apply simp apply (rule handleInterrupt_corres) apply (rule corres_stateAssert_assume_stronger[where Q=\<top> and
                      P="\<lambda>s. valid_domain_list s \<and>
                             (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)"]) apply simp apply (clarsimp simp: state_relation_def) apply (wp handle_interrupt_valid_domain_time)+ apply (rule dmo_getActiveIRQ_wp) apply (rule dmo'_getActiveIRQ_wp) apply clarsimp+ apply (clarsimp simp: invs'_def valid_state'_def irq_at_def invs_def
                        Let_def valid_irq_states'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) invs' (handle_preemption_if tc) (handlePreemption_if tc) proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) invs' (do irq <- do_machine_op (getActiveIRQ True);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return tc
od) (do irq <- doMachineOp (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handleInterrupt (the irq));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do irq <- do_machine_op (getActiveIRQ True);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return tc
od) (do irq <- doMachineOp (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handleInterrupt (the irq));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 2. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ?Q s
 3. \<And>s. invs' s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres (=) ?P4 ?P'4 (do_machine_op (getActiveIRQ True)) (doMachineOp (getActiveIRQ False))
 2. \<And>irq irqa. irq = irqa \<Longrightarrow> corres (=) (?R4 irq) (?R'4 irqa) (do y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return tc
od) (do y <- when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 3. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R'4\<rbrace>
 5. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. invs' s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>irq irqa. irq = irqa \<Longrightarrow> corres (=) (?R4 irq) (?R'4 irqa) (do y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return tc
od) (do y <- when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 2. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>irq irqa. irq = irqa \<Longrightarrow> corres dc (?P11 irq) (?P'13 irqa) (when (\<exists>y. irq = Some y) (handle_interrupt (the irq))) (when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)))
 2. \<And>irq irqa y ya. \<lbrakk>irq = irqa; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R10 irq irqa y) (?R'10 irq irqa ya) (return tc) (do y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 3. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q12 irq\<rbrace> when (\<exists>y. irq = Some y) (handle_interrupt (the irq)) \<lbrace>?R10 irq irqa\<rbrace>
 4. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q'14 irqa\<rbrace> when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)) \<lbrace>?R'10 irq irqa\<rbrace>
 5. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. ?P11 irq and ?Q12 irq\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. ?P'13 irqa and ?Q'14 irqa\<rbrace>
 7. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>irq irqa. irq = irqa \<Longrightarrow> (\<exists>y. irq = Some y) = (\<exists>y. irqa = Some y)
 2. \<And>irq irqa. irq = irqa \<Longrightarrow> corres dc (?P21 irq) (?P'23 irqa) (handle_interrupt (the irq)) (handleInterrupt (the irqa))
 3. \<And>irq irqa y ya. \<lbrakk>irq = irqa; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R10 irq irqa y) (?R'10 irq irqa ya) (return tc) (do y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 4. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q12 irq\<rbrace> when (\<exists>y. irq = Some y) (handle_interrupt (the irq)) \<lbrace>?R10 irq irqa\<rbrace>
 5. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q'14 irqa\<rbrace> when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)) \<lbrace>?R'10 irq irqa\<rbrace>
 6. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. (\<lambda>x. (\<exists>y. irq = Some y) \<longrightarrow> ?P21 irq x) and ?Q12 irq\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> ?P'23 irqa x) and ?Q'14 irqa\<rbrace>
 8. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>irq irqa. irq = irqa \<Longrightarrow> corres dc (?P21 irq) (?P'23 irqa) (handle_interrupt (the irq)) (handleInterrupt (the irqa))
 2. \<And>irq irqa y ya. \<lbrakk>irq = irqa; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R10 irq irqa y) (?R'10 irq irqa ya) (return tc) (do y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 3. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q12 irq\<rbrace> when (\<exists>y. irq = Some y) (handle_interrupt (the irq)) \<lbrace>?R10 irq irqa\<rbrace>
 4. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q'14 irqa\<rbrace> when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)) \<lbrace>?R'10 irq irqa\<rbrace>
 5. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. (\<lambda>x. (\<exists>y. irq = Some y) \<longrightarrow> ?P21 irq x) and ?Q12 irq\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> ?P'23 irqa x) and ?Q'14 irqa\<rbrace>
 7. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>irq. corres dc (?P21 irq) (?P'23 irq) (handle_interrupt (the irq)) (handleInterrupt (the irq))
 2. \<And>irq irqa y ya. \<lbrakk>irq = irqa; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R10 irq irqa y) (?R'10 irq irqa ya) (return tc) (do y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 3. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q12 irq\<rbrace> when (\<exists>y. irq = Some y) (handle_interrupt (the irq)) \<lbrace>?R10 irq irqa\<rbrace>
 4. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q'14 irqa\<rbrace> when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)) \<lbrace>?R'10 irq irqa\<rbrace>
 5. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. (\<lambda>x. (\<exists>y. irq = Some y) \<longrightarrow> ?P21 irq x) and ?Q12 irq\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> ?P'23 irqa x) and ?Q'14 irqa\<rbrace>
 7. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>irq irqa y ya. \<lbrakk>irq = irqa; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R10 irq irqa y) (?R'10 irq irqa ya) (return tc) (do y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od)
 2. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q12 irq\<rbrace> when (\<exists>y. irq = Some y) (handle_interrupt (the irq)) \<lbrace>?R10 irq irqa\<rbrace>
 3. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q'14 irqa\<rbrace> when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)) \<lbrace>?R'10 irq irqa\<rbrace>
 4. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. (\<lambda>x. (\<exists>y. irq = Some y) \<longrightarrow> einvs x) and ?Q12 irq\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) (the irqa) \<noteq> irqstate.IRQInactive)) x) and ?Q'14 irqa\<rbrace>
 6. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>irq irqa y ya. \<lbrakk>irq = irqa; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) (\<lambda>_. True) (return tc) (return tc)
 2. \<And>irq irqa y ya s s'. \<lbrakk>irq = irqa; dc y ya; (s, s') \<in> state_relation; valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread); True\<rbrakk> \<Longrightarrow> (ksDomainTime s' = 0 \<longrightarrow> ksSchedulerAction s' = ChooseNewThread) \<and> valid_domain_list' s'
 3. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q12 irq\<rbrace> when (\<exists>y. irq = Some y) (handle_interrupt (the irq)) \<lbrace>\<lambda>y s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
 4. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q'14 irqa\<rbrace> when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)) \<lbrace>\<lambda>ya _. True\<rbrace>
 5. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. (\<lambda>x. (\<exists>y. irq = Some y) \<longrightarrow> einvs x) and ?Q12 irq\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) (the irqa) \<noteq> irqstate.IRQInactive)) x) and ?Q'14 irqa\<rbrace>
 7. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>irq irqa y ya s s'. \<lbrakk>irq = irqa; dc y ya; (s, s') \<in> state_relation; valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread); True\<rbrakk> \<Longrightarrow> (ksDomainTime s' = 0 \<longrightarrow> ksSchedulerAction s' = ChooseNewThread) \<and> valid_domain_list' s'
 2. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q12 irq\<rbrace> when (\<exists>y. irq = Some y) (handle_interrupt (the irq)) \<lbrace>\<lambda>y s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
 3. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q'14 irqa\<rbrace> when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)) \<lbrace>\<lambda>ya _. True\<rbrace>
 4. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. (\<lambda>x. (\<exists>y. irq = Some y) \<longrightarrow> einvs x) and ?Q12 irq\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) (the irqa) \<noteq> irqstate.IRQInactive)) x) and ?Q'14 irqa\<rbrace>
 6. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q12 irq\<rbrace> when (\<exists>y. irq = Some y) (handle_interrupt (the irq)) \<lbrace>\<lambda>y s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>
 2. \<And>irq irqa. irq = irqa \<Longrightarrow> \<lbrace>?Q'14 irqa\<rbrace> when (\<exists>y. irqa = Some y) (handleInterrupt (the irqa)) \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. (\<lambda>x. (\<exists>y. irq = Some y) \<longrightarrow> einvs x) and ?Q12 irq\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) (the irqa) \<noteq> irqstate.IRQInactive)) x) and ?Q'14 irqa\<rbrace>
 5. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq s. ((\<exists>y. irq = Some y) \<longrightarrow> einvs s) \<and> (if \<exists>y. irq = Some y then \<lambda>a. valid_domain_list a \<and> 0 < domain_time a else (\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread))) s\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) (the irqa) \<noteq> irqstate.IRQInactive)) x) and (\<lambda>_. True)\<rbrace>
 3. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>irqa. (\<lambda>x. (\<exists>y. irqa = Some y) \<longrightarrow> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) (the irqa) \<noteq> irqstate.IRQInactive)) x) and (\<lambda>_. True)\<rbrace>
 2. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<exists>y. irq_at (irq_state_of_state s + 1) (irq_masks_of_state s) = Some y) \<longrightarrow> einvs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := irq_state_of_state s + 1\<rparr>\<rparr>)) \<and> (if \<exists>y. irq_at (irq_state_of_state s + 1) (irq_masks_of_state s) = Some y then \<lambda>a. valid_domain_list a \<and> 0 < domain_time a else (\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := irq_state_of_state s + 1\<rparr>\<rparr>))) s
 3. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<exists>y. irq_at (irq_state_of_state s + 1) (irq_masks_of_state s) = Some y) \<longrightarrow> einvs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := irq_state_of_state s + 1\<rparr>\<rparr>)) \<and> (if \<exists>y. irq_at (irq_state_of_state s + 1) (irq_masks_of_state s) = Some y then \<lambda>a. valid_domain_list a \<and> 0 < domain_time a else (\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread))) (s\<lparr>machine_state := machine_state s\<lparr>irq_state := irq_state_of_state s + 1\<rparr>\<rparr>))) s
 2. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>x. (\<exists>y. irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s)) = Some y) \<longrightarrow> (invs' and (\<lambda>sa. intStateIRQTable (ksInterruptState sa) (the (irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s)))) \<noteq> irqstate.IRQInactive)) x) and (\<lambda>_. True)) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>\<rparr>))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>invs' s; irq_at (Suc (irq_state (ksMachineState s))) (irq_masks (ksMachineState s)) = Some y; intStateIRQTable (ksInterruptState s) y = irqstate.IRQInactive\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!