theory Noninterference

lemma small_Step_partitionIntegrity:
  notes active_from_running[simp]
  assumes step: "(s, t) \<in> data_type.Step (ADT_A_if utf) ()"
    and reachable: "system.reachable (ADT_A_if utf) s0 s"
    and sched: "part s \<noteq> PSched"
  shows "partitionIntegrity (current_aag (internal_state_if s))
                            (internal_state_if s) (internal_state_if t)" proof (cases "sys_mode_of s") case InUserMode with assms show ?thesis by (fastforce dest: ADT_A_if_reachable_invs_if
                  simp: invs_if_def part_def global_automaton_if_def
                        Step_ADT_A_if_def_global_automaton_if
                 intro: user_small_Step_partitionIntegrity check_active_irq_A_if_partitionIntegrity) next case InIdleMode with assms show ?thesis by (fastforce simp: Step_ADT_A_if_def_global_automaton_if global_automaton_if_def
                 intro: check_active_irq_A_if_partitionIntegrity) next case KernelEntry with assms show ?thesis by (fastforce dest: ADT_A_if_reachable_invs_if
                 simp: invs_if_def part_def Step_ADT_A_if_def_global_automaton_if
                       global_automaton_if_def not_schedule_modes_KernelEntry
                intro: kernel_call_A_if_partitionIntegrity) next case KernelExit with assms show ?thesis apply (clarsimp simp: Step_ADT_A_if_def_global_automaton_if
                          global_automaton_if_def kernel_exit_A_if_def) apply (safe; simp) apply (erule use_valid) apply wp apply (rule partitionIntegrity_refl) done next case KernelPreempted with assms show ?thesis by (simp add: part_def) next case KernelSchedule with assms show ?thesis apply (clarsimp simp: part_def Step_ADT_A_if_def_global_automaton_if
                          global_automaton_if_def kernel_schedule_if_def) apply (safe; simp) apply (erule use_valid) apply (wp schedule_if_partitionIntegrity[OF current_domains_distinct]) apply (clarsimp simp: partitionIntegrity_refl) apply (drule ADT_A_if_reachable_invs_if) apply (clarsimp simp: invs_if_def Invs_def silc_inv_refl current_aag_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
goal (6 subgoals):
 1. sys_mode_of s = InUserMode \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. sys_mode_of s = InIdleMode \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. \<And>x3. sys_mode_of s = KernelEntry x3 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 4. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 5. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 6. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
sys_mode_of s = InUserMode

goal (6 subgoals):
 1. sys_mode_of s = InUserMode \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. sys_mode_of s = InIdleMode \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. \<And>x3. sys_mode_of s = KernelEntry x3 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 4. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 5. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 6. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (chain)
picking this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = InUserMode proof (prove)
using this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = InUserMode

goal (1 subgoal):
 1. partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)

goal (5 subgoals):
 1. sys_mode_of s = InIdleMode \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x3. sys_mode_of s = KernelEntry x3 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 4. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 5. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
goal (5 subgoals):
 1. sys_mode_of s = InIdleMode \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x3. sys_mode_of s = KernelEntry x3 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 4. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 5. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
sys_mode_of s = InIdleMode

goal (5 subgoals):
 1. sys_mode_of s = InIdleMode \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x3. sys_mode_of s = KernelEntry x3 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 4. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 5. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (chain)
picking this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = InIdleMode proof (prove)
using this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = InIdleMode

goal (1 subgoal):
 1. partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)

goal (4 subgoals):
 1. \<And>x3. sys_mode_of s = KernelEntry x3 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 4. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
goal (4 subgoals):
 1. \<And>x3. sys_mode_of s = KernelEntry x3 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 4. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
sys_mode_of s = KernelEntry x3_

goal (4 subgoals):
 1. \<And>x3. sys_mode_of s = KernelEntry x3 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 4. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (chain)
picking this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = KernelEntry x3_ proof (prove)
using this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = KernelEntry x3_

goal (1 subgoal):
 1. partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)

goal (3 subgoals):
 1. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
goal (3 subgoals):
 1. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
sys_mode_of s = KernelExit

goal (3 subgoals):
 1. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 3. sys_mode_of s = KernelExit \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (chain)
picking this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = KernelExit proof (prove)
using this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = KernelExit

goal (1 subgoal):
 1. partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched; sys_mode_of s = KernelExit; (\<exists>a b aa ba e. s = ((a, b), KernelEntry e) \<and> t = ((aa, ba), KernelPreempted) \<and> ((a, b), True, aa, ba) \<in> kernel_call_A_if e \<and> e \<noteq> Interrupt) \<or> (\<exists>a b aa ba e. s = ((a, b), KernelEntry e) \<and> t = ((aa, ba), KernelSchedule (e = Interrupt)) \<and> ((a, b), False, aa, ba) \<in> kernel_call_A_if e) \<or> (\<exists>a b. s = ((a, b), KernelPreempted) \<and> (\<exists>aa ba. t = ((aa, ba), KernelSchedule True) \<and> ((a, b), (), aa, ba) \<in> kernel_handle_preemption_if)) \<or> (\<exists>a b. (\<exists>ba. s = ((a, b), KernelSchedule ba)) \<and> (\<exists>aa ba. t = ((aa, ba), KernelExit) \<and> ((a, b), (), aa, ba) \<in> kernel_schedule_if)) \<or> (\<exists>a b. s = ((a, b), KernelExit) \<and> (\<exists>aa ba. t = ((aa, ba), if ct_running ba then InUserMode else InIdleMode) \<and> (aa, ba) \<in> fst (kernel_exit_if a b))) \<or> (\<exists>a b. s = ((a, b), InUserMode) \<and> (\<exists>aa ba ab bb e. t = ((ab, bb), KernelEntry e) \<and> ((a, b), None, aa, ba) \<in> check_active_irq_A_if \<and> ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf \<and> e \<noteq> Interrupt)) \<or> (\<exists>a b. s = ((a, b), InUserMode) \<and> (\<exists>aa ba ab bb. t = ((ab, bb), InUserMode) \<and> ((a, b), None, aa, ba) \<in> check_active_irq_A_if \<and> ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf)) \<or> (\<exists>a b. s = ((a, b), InUserMode) \<and> (\<exists>aa ba. t = ((aa, ba), KernelEntry Interrupt) \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if))) \<or> (\<exists>a b. s = ((a, b), InIdleMode) \<and> (\<exists>aa ba. t = ((aa, ba), KernelEntry Interrupt) \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if))) \<or> (\<exists>a b. s = ((a, b), InIdleMode) \<and> (\<exists>aa ba. t = ((aa, ba), InIdleMode) \<and> ((a, b), None, aa, ba) \<in> check_active_irq_A_if)); step_restrict t\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelExit); part ((a, b), KernelExit) \<noteq> PSched; step_restrict ((aa, ba), if ct_running ba then InUserMode else InIdleMode); s = ((a, b), KernelExit); (aa, ba) \<in> fst (kernel_exit_if a b); t = ((aa, ba), if ct_running ba then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelExit); part ((a, b), KernelExit) \<noteq> PSched; step_restrict ((aa, ba), if ct_running ba then InUserMode else InIdleMode); s = ((a, b), KernelExit); t = ((aa, ba), if ct_running ba then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> \<lbrace>?P150 a b aa ba\<rbrace> kernel_exit_if a \<lbrace>\<lambda>a. partitionIntegrity (current_aag b) b\<rbrace>
 2. \<And>a b aa ba. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelExit); part ((a, b), KernelExit) \<noteq> PSched; step_restrict ((aa, ba), if ct_running ba then InUserMode else InIdleMode); s = ((a, b), KernelExit); t = ((aa, ba), if ct_running ba then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> ?P150 a b aa ba b proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelExit); part ((a, b), KernelExit) \<noteq> PSched; step_restrict ((aa, ba), if ct_running ba then InUserMode else InIdleMode); s = ((a, b), KernelExit); t = ((aa, ba), if ct_running ba then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b b proof (prove)
goal:
No subgoals! proof (state)
this:
partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)

goal (2 subgoals):
 1. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
goal (2 subgoals):
 1. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
sys_mode_of s = KernelPreempted

goal (2 subgoals):
 1. sys_mode_of s = KernelPreempted \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 2. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (chain)
picking this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = KernelPreempted proof (prove)
using this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = KernelPreempted

goal (1 subgoal):
 1. partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)

goal (1 subgoal):
 1. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
goal (1 subgoal):
 1. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (state)
this:
sys_mode_of s = KernelSchedule x5_

goal (1 subgoal):
 1. \<And>x5. sys_mode_of s = KernelSchedule x5 \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (chain)
picking this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = KernelSchedule x5_ proof (prove)
using this:
(s, t) \<in> data_type.Step (ADT_A_if utf) ()
system.reachable (ADT_A_if utf) s0 s
part s \<noteq> PSched
sys_mode_of s = KernelSchedule x5_

goal (1 subgoal):
 1. partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (if x5_ then PSched else Partition (partition_if s)) \<noteq> PSched; sys_mode_of s = KernelSchedule x5_; (\<exists>a b aa ba e. s = ((a, b), KernelEntry e) \<and> t = ((aa, ba), KernelPreempted) \<and> ((a, b), True, aa, ba) \<in> kernel_call_A_if e \<and> e \<noteq> Interrupt) \<or> (\<exists>a b aa ba e. s = ((a, b), KernelEntry e) \<and> t = ((aa, ba), KernelSchedule (e = Interrupt)) \<and> ((a, b), False, aa, ba) \<in> kernel_call_A_if e) \<or> (\<exists>a b. s = ((a, b), KernelPreempted) \<and> (\<exists>aa ba. t = ((aa, ba), KernelSchedule True) \<and> ((a, b), (), aa, ba) \<in> kernel_handle_preemption_if)) \<or> (\<exists>a b. (\<exists>ba. s = ((a, b), KernelSchedule ba)) \<and> (\<exists>aa ba. t = ((aa, ba), KernelExit) \<and> (aa, ba) \<in> fst (schedule_if a b))) \<or> (\<exists>a b. s = ((a, b), KernelExit) \<and> (\<exists>aa ba m. t = ((aa, ba), m) \<and> ((a, b), m, aa, ba) \<in> kernel_exit_A_if)) \<or> (\<exists>a b. s = ((a, b), InUserMode) \<and> (\<exists>aa ba ab bb e. t = ((ab, bb), KernelEntry e) \<and> ((a, b), None, aa, ba) \<in> check_active_irq_A_if \<and> ((aa, ba), Some e, ab, bb) \<in> do_user_op_A_if utf \<and> e \<noteq> Interrupt)) \<or> (\<exists>a b. s = ((a, b), InUserMode) \<and> (\<exists>aa ba ab bb. t = ((ab, bb), InUserMode) \<and> ((a, b), None, aa, ba) \<in> check_active_irq_A_if \<and> ((aa, ba), None, ab, bb) \<in> do_user_op_A_if utf)) \<or> (\<exists>a b. s = ((a, b), InUserMode) \<and> (\<exists>aa ba. t = ((aa, ba), KernelEntry Interrupt) \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if))) \<or> (\<exists>a b. s = ((a, b), InIdleMode) \<and> (\<exists>aa ba. t = ((aa, ba), KernelEntry Interrupt) \<and> (\<exists>i. ((a, b), Some i, aa, ba) \<in> check_active_irq_A_if))) \<or> (\<exists>a b. s = ((a, b), InIdleMode) \<and> (\<exists>aa ba. t = ((aa, ba), InIdleMode) \<and> ((a, b), None, aa, ba) \<in> check_active_irq_A_if)); step_restrict t\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelSchedule x5_); (if x5_ then PSched else Partition (partition_if ((a, b), KernelSchedule ba))) \<noteq> PSched; ba = x5_; step_restrict ((aa, bb), KernelExit); s = ((a, b), KernelSchedule x5_); (aa, bb) \<in> fst (schedule_if a b); t = ((aa, bb), KernelExit)\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b bb proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bb. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelSchedule x5_); (if x5_ then PSched else Partition (partition_if ((a, b), KernelSchedule ba))) \<noteq> PSched; ba = x5_; step_restrict ((aa, bb), KernelExit); s = ((a, b), KernelSchedule x5_); t = ((aa, bb), KernelExit)\<rbrakk> \<Longrightarrow> \<lbrace>?P151 a b ba aa bb\<rbrace> schedule_if a \<lbrace>\<lambda>a. partitionIntegrity (current_aag b) b\<rbrace>
 2. \<And>a b ba aa bb. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelSchedule x5_); (if x5_ then PSched else Partition (partition_if ((a, b), KernelSchedule ba))) \<noteq> PSched; ba = x5_; step_restrict ((aa, bb), KernelExit); s = ((a, b), KernelSchedule x5_); t = ((aa, bb), KernelExit)\<rbrakk> \<Longrightarrow> ?P151 a b ba aa bb b proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelSchedule x5_); (if x5_ then PSched else Partition (partition_if ((a, b), KernelSchedule ba))) \<noteq> PSched; ba = x5_; step_restrict ((aa, bb), KernelExit); s = ((a, b), KernelSchedule x5_); t = ((aa, bb), KernelExit)\<rbrakk> \<Longrightarrow> (partitionIntegrity (current_aag b) b and guarded_pas_domain (current_aag b) and pas_cur_domain (current_aag b) and (\<lambda>s. domain_time s \<noteq> 0) and silc_inv (current_aag b) b and einvs and pas_refined (current_aag b)) b proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb. \<lbrakk>system.reachable (ADT_A_if utf) s0 ((a, b), KernelSchedule x5_); (if x5_ then PSched else Partition (partition_if ((a, b), KernelSchedule x5_))) \<noteq> PSched; step_restrict ((aa, bb), KernelExit); s = ((a, b), KernelSchedule x5_); t = ((aa, bb), KernelExit)\<rbrakk> \<Longrightarrow> guarded_pas_domain (current_aag b) b \<and> pas_cur_domain (current_aag b) b \<and> domain_time b \<noteq> 0 \<and> silc_inv (current_aag b) b b \<and> invs b \<and> valid_list b \<and> valid_sched b \<and> pas_refined (current_aag b) b proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb. \<lbrakk>(if x5_ then PSched else Partition (partition_if ((a, b), KernelSchedule x5_))) \<noteq> PSched; step_restrict ((aa, bb), KernelExit); s = ((a, b), KernelSchedule x5_); t = ((aa, bb), KernelExit); invs_if ((a, b), KernelSchedule x5_)\<rbrakk> \<Longrightarrow> guarded_pas_domain (current_aag b) b \<and> pas_cur_domain (current_aag b) b \<and> domain_time b \<noteq> 0 \<and> silc_inv (current_aag b) b b \<and> invs b \<and> valid_list b \<and> valid_sched b \<and> pas_refined (current_aag b) b proof (prove)
goal:
No subgoals! proof (state)
this:
partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)

goal:
No subgoals!