theory ADT_IF_Refine

lemma ADT_invs: "ADT \<Turnstile> invs" apply (rule invariantI) apply (intro allI) apply (rule init_invs) apply (clarsimp simp: step_adt global_automaton_if_def) apply (elim disjE exE conjE,simp_all) apply (rule preservesE[OF kernel_call_invs]) apply (rule preservesE[OF kernel_call_invs],assumption+) apply (rule preservesE[OF kernel_call_invs_sched],assumption+) apply (rule preservesE[OF handle_preemption_invs],assumption+) apply (rule preservesE[OF schedule_invs],assumption+) apply (rule preserves'E[OF kernel_exit_invs],assumption+) apply (rule preservesE[OF check_active_irq_invs],assumption+) apply (rule preservesE[OF do_user_op_invs_entry],assumption+) apply (rule preservesE[OF check_active_irq_invs],assumption+) apply (rule preservesE[OF do_user_op_invs],assumption+) apply (rule preservesE[OF check_active_irq_invs_entry],assumption+) apply (rule preservesE[OF check_active_irq_idle_invs_entry],assumption+) apply (rule preservesE[OF check_active_irq_idle_invs],assumption+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT \<Turnstile> invs proof (prove)
goal (2 subgoals):
 1. \<forall>s. Init ADT s \<subseteq> invs
 2. \<forall>j. Step ADT j `` invs \<subseteq> invs proof (prove)
goal (2 subgoals):
 1. \<And>s. Init ADT s \<subseteq> invs
 2. \<forall>j. Step ADT j `` invs \<subseteq> invs proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step ADT j `` invs \<subseteq> invs proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), bc) \<in> invs; (\<exists>e. bc = KernelEntry e \<and> ba = KernelPreempted \<and> ((aa, bb), True, a, b) \<in> kernel_call e \<and> e \<noteq> Interrupt) \<or> (\<exists>e. bc = KernelEntry e \<and> ba = KernelSchedule (e = Interrupt) \<and> ((aa, bb), False, a, b) \<in> kernel_call e) \<or> bc = KernelPreempted \<and> ba = KernelSchedule True \<and> ((aa, bb), (), a, b) \<in> handle_preemption \<or> (\<exists>b. bc = KernelSchedule b) \<and> ba = KernelExit \<and> ((aa, bb), (), a, b) \<in> schedule \<or> bc = KernelExit \<and> ((aa, bb), ba, a, b) \<in> kernel_exit \<or> bc = InUserMode \<and> (\<exists>ab bc e. ba = KernelEntry e \<and> ((aa, bb), None, ab, bc) \<in> check_active_irq \<and> ((ab, bc), Some e, a, b) \<in> do_user_op \<and> e \<noteq> Interrupt) \<or> bc = InUserMode \<and> ba = InUserMode \<and> (\<exists>ab ba. ((aa, bb), None, ab, ba) \<in> check_active_irq \<and> ((ab, ba), None, a, b) \<in> do_user_op) \<or> bc = InUserMode \<and> ba = KernelEntry Interrupt \<and> (\<exists>i. ((aa, bb), Some i, a, b) \<in> check_active_irq) \<or> bc = InIdleMode \<and> ba = KernelEntry Interrupt \<and> (\<exists>i. ((aa, bb), Some i, a, b) \<in> check_active_irq) \<or> bc = InIdleMode \<and> ba = InIdleMode \<and> ((aa, bb), None, a, b) \<in> check_active_irq; ((a, b), ba) \<in> extras\<rbrakk> \<Longrightarrow> ((a, b), ba) \<in> invs proof (prove)
goal (10 subgoals):
 1. \<And>a b ba aa bb bc e. \<lbrakk>((aa, bb), KernelEntry e) \<in> invs; ((a, b), KernelPreempted) \<in> extras; bc = KernelEntry e; ba = KernelPreempted; ((aa, bb), True, a, b) \<in> kernel_call e; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((a, b), KernelPreempted) \<in> invs
 2. \<And>a b ba aa bb bc e. \<lbrakk>((aa, bb), KernelEntry e) \<in> invs; ((a, b), KernelSchedule (e = Interrupt)) \<in> extras; bc = KernelEntry e; ba = KernelSchedule (e = Interrupt); ((aa, bb), False, a, b) \<in> kernel_call e\<rbrakk> \<Longrightarrow> ((a, b), KernelSchedule (e = Interrupt)) \<in> invs
 3. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelPreempted) \<in> invs; ((a, b), KernelSchedule True) \<in> extras; bc = KernelPreempted; ba = KernelSchedule True; ((aa, bb), (), a, b) \<in> handle_preemption\<rbrakk> \<Longrightarrow> ((a, b), KernelSchedule True) \<in> invs
 4. \<And>a b ba aa bb bc bd. \<lbrakk>((aa, bb), KernelSchedule bd) \<in> invs; ((a, b), KernelExit) \<in> extras; bc = KernelSchedule bd; ba = KernelExit; ((aa, bb), (), a, b) \<in> schedule\<rbrakk> \<Longrightarrow> ((a, b), KernelExit) \<in> invs
 5. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelExit) \<in> invs; ((a, b), ba) \<in> extras; bc = KernelExit; ((aa, bb), ba, a, b) \<in> kernel_exit\<rbrakk> \<Longrightarrow> ((a, b), ba) \<in> invs
 6. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry e) \<in> extras; bc = InUserMode; ba = KernelEntry e; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), Some e, a, b) \<in> do_user_op; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry e) \<in> invs
 7. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 8. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 9. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 10. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (13 subgoals):
 1. \<And>a b ba aa bb bc e. \<lbrakk>((aa, bb), KernelEntry e) \<in> invs; ((a, b), KernelPreempted) \<in> extras; bc = KernelEntry e; ba = KernelPreempted; ((aa, bb), True, a, b) \<in> kernel_call e; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ?e52 a b ba aa bb bc e \<noteq> Interrupt
 2. \<And>a b ba aa bb bc e. \<lbrakk>((aa, bb), KernelEntry e) \<in> invs; ((a, b), KernelPreempted) \<in> extras; bc = KernelEntry e; ba = KernelPreempted; ((aa, bb), True, a, b) \<in> kernel_call e; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> (?s51 a b ba aa bb bc e, ?e51 a b ba aa bb bc e, ?s'51 a b ba aa bb bc e) \<in> kernel_call (?e52 a b ba aa bb bc e)
 3. \<And>a b ba aa bb bc e. \<lbrakk>((aa, bb), KernelEntry e) \<in> invs; ((a, b), KernelPreempted) \<in> extras; bc = KernelEntry e; ba = KernelPreempted; ((aa, bb), True, a, b) \<in> kernel_call e; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> (?s51 a b ba aa bb bc e, KernelEntry (?e52 a b ba aa bb bc e)) \<in> invs
 4. \<And>a b ba aa bb bc e. \<lbrakk>((aa, bb), KernelEntry e) \<in> invs; ((a, b), KernelPreempted) \<in> extras; bc = KernelEntry e; ba = KernelPreempted; ((aa, bb), True, a, b) \<in> kernel_call e; e \<noteq> Interrupt; (?s'51 a b ba aa bb bc e, KernelPreempted) \<in> invs\<rbrakk> \<Longrightarrow> ((a, b), KernelPreempted) \<in> invs
 5. \<And>a b ba aa bb bc e. \<lbrakk>((aa, bb), KernelEntry e) \<in> invs; ((a, b), KernelSchedule (e = Interrupt)) \<in> extras; bc = KernelEntry e; ba = KernelSchedule (e = Interrupt); ((aa, bb), False, a, b) \<in> kernel_call e\<rbrakk> \<Longrightarrow> ((a, b), KernelSchedule (e = Interrupt)) \<in> invs
 6. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelPreempted) \<in> invs; ((a, b), KernelSchedule True) \<in> extras; bc = KernelPreempted; ba = KernelSchedule True; ((aa, bb), (), a, b) \<in> handle_preemption\<rbrakk> \<Longrightarrow> ((a, b), KernelSchedule True) \<in> invs
 7. \<And>a b ba aa bb bc bd. \<lbrakk>((aa, bb), KernelSchedule bd) \<in> invs; ((a, b), KernelExit) \<in> extras; bc = KernelSchedule bd; ba = KernelExit; ((aa, bb), (), a, b) \<in> schedule\<rbrakk> \<Longrightarrow> ((a, b), KernelExit) \<in> invs
 8. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelExit) \<in> invs; ((a, b), ba) \<in> extras; bc = KernelExit; ((aa, bb), ba, a, b) \<in> kernel_exit\<rbrakk> \<Longrightarrow> ((a, b), ba) \<in> invs
 9. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry e) \<in> extras; bc = InUserMode; ba = KernelEntry e; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), Some e, a, b) \<in> do_user_op; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry e) \<in> invs
 10. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
A total of 13 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>a b ba aa bb bc e. \<lbrakk>((aa, bb), KernelEntry e) \<in> invs; ((a, b), KernelSchedule (e = Interrupt)) \<in> extras; bc = KernelEntry e; ba = KernelSchedule (e = Interrupt); ((aa, bb), False, a, b) \<in> kernel_call e\<rbrakk> \<Longrightarrow> ((a, b), KernelSchedule (e = Interrupt)) \<in> invs
 2. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelPreempted) \<in> invs; ((a, b), KernelSchedule True) \<in> extras; bc = KernelPreempted; ba = KernelSchedule True; ((aa, bb), (), a, b) \<in> handle_preemption\<rbrakk> \<Longrightarrow> ((a, b), KernelSchedule True) \<in> invs
 3. \<And>a b ba aa bb bc bd. \<lbrakk>((aa, bb), KernelSchedule bd) \<in> invs; ((a, b), KernelExit) \<in> extras; bc = KernelSchedule bd; ba = KernelExit; ((aa, bb), (), a, b) \<in> schedule\<rbrakk> \<Longrightarrow> ((a, b), KernelExit) \<in> invs
 4. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelExit) \<in> invs; ((a, b), ba) \<in> extras; bc = KernelExit; ((aa, bb), ba, a, b) \<in> kernel_exit\<rbrakk> \<Longrightarrow> ((a, b), ba) \<in> invs
 5. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry e) \<in> extras; bc = InUserMode; ba = KernelEntry e; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), Some e, a, b) \<in> do_user_op; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry e) \<in> invs
 6. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 7. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 8. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 9. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (8 subgoals):
 1. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelPreempted) \<in> invs; ((a, b), KernelSchedule True) \<in> extras; bc = KernelPreempted; ba = KernelSchedule True; ((aa, bb), (), a, b) \<in> handle_preemption\<rbrakk> \<Longrightarrow> ((a, b), KernelSchedule True) \<in> invs
 2. \<And>a b ba aa bb bc bd. \<lbrakk>((aa, bb), KernelSchedule bd) \<in> invs; ((a, b), KernelExit) \<in> extras; bc = KernelSchedule bd; ba = KernelExit; ((aa, bb), (), a, b) \<in> schedule\<rbrakk> \<Longrightarrow> ((a, b), KernelExit) \<in> invs
 3. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelExit) \<in> invs; ((a, b), ba) \<in> extras; bc = KernelExit; ((aa, bb), ba, a, b) \<in> kernel_exit\<rbrakk> \<Longrightarrow> ((a, b), ba) \<in> invs
 4. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry e) \<in> extras; bc = InUserMode; ba = KernelEntry e; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), Some e, a, b) \<in> do_user_op; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry e) \<in> invs
 5. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 6. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 7. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 8. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (7 subgoals):
 1. \<And>a b ba aa bb bc bd. \<lbrakk>((aa, bb), KernelSchedule bd) \<in> invs; ((a, b), KernelExit) \<in> extras; bc = KernelSchedule bd; ba = KernelExit; ((aa, bb), (), a, b) \<in> schedule\<rbrakk> \<Longrightarrow> ((a, b), KernelExit) \<in> invs
 2. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelExit) \<in> invs; ((a, b), ba) \<in> extras; bc = KernelExit; ((aa, bb), ba, a, b) \<in> kernel_exit\<rbrakk> \<Longrightarrow> ((a, b), ba) \<in> invs
 3. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry e) \<in> extras; bc = InUserMode; ba = KernelEntry e; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), Some e, a, b) \<in> do_user_op; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry e) \<in> invs
 4. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 5. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 6. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 7. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (6 subgoals):
 1. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), KernelExit) \<in> invs; ((a, b), ba) \<in> extras; bc = KernelExit; ((aa, bb), ba, a, b) \<in> kernel_exit\<rbrakk> \<Longrightarrow> ((a, b), ba) \<in> invs
 2. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry e) \<in> extras; bc = InUserMode; ba = KernelEntry e; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), Some e, a, b) \<in> do_user_op; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry e) \<in> invs
 3. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 4. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 5. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 6. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (5 subgoals):
 1. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry e) \<in> extras; bc = InUserMode; ba = KernelEntry e; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), Some e, a, b) \<in> do_user_op; e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry e) \<in> invs
 2. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 3. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 4. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 5. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (5 subgoals):
 1. \<And>a b ba aa bb bc ab bd e. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry e) \<in> extras; bc = InUserMode; ba = KernelEntry e; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), Some e, a, b) \<in> do_user_op; e \<noteq> Interrupt; ((ab, bd), InUserMode) \<in> invs\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry e) \<in> invs
 2. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 3. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 4. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 5. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (4 subgoals):
 1. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 2. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 3. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 4. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (4 subgoals):
 1. \<And>a b ba aa bb bc ab bd. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), InUserMode) \<in> extras; bc = InUserMode; ba = InUserMode; ((aa, bb), None, ab, bd) \<in> check_active_irq; ((ab, bd), None, a, b) \<in> do_user_op; ((ab, bd), InUserMode) \<in> invs\<rbrakk> \<Longrightarrow> ((a, b), InUserMode) \<in> invs
 2. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 3. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 4. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (3 subgoals):
 1. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InUserMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InUserMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 2. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 3. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb bc i. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), KernelEntry Interrupt) \<in> extras; bc = InIdleMode; ba = KernelEntry Interrupt; ((aa, bb), Some i, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), KernelEntry Interrupt) \<in> invs
 2. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb bc. \<lbrakk>((aa, bb), InIdleMode) \<in> invs; ((a, b), InIdleMode) \<in> extras; bc = InIdleMode; ba = InIdleMode; ((aa, bb), None, a, b) \<in> check_active_irq\<rbrakk> \<Longrightarrow> ((a, b), InIdleMode) \<in> invs proof (prove)
goal:
No subgoals!