theory Noninterference

lemma scheduler_steps:
  assumes big_step: "(s,s'') \<in> data_type.Step (big_step_ADT_A_if utf) ()"
  assumes interrupted: "part s = PSched"
  obtains s' where "(s,s') \<in> data_type.Step (ADT_A_if utf) ()"
                   "sys_mode_of s' = KernelSchedule True"
                   "(s',s'') \<in> data_type.Step (ADT_A_if utf) ()" apply (insert big_step interrupted) apply (simp add: Step_big_step_ADT_A_if) apply (simp add: big_steps.simps) apply clarsimp apply (subgoal_tac "interrupted_modes (sys_mode_of s)") prefer 2 apply (clarsimp simp add: big_step_R_def part_def sys_mode_of_def split: if_split_asm) apply (case_tac "snd s",simp_all) apply (case_tac "as = []") apply (erule sub_big_steps.cases) apply simp apply (erule interrupt_step[rotated,rotated],assumption) apply ((simp add: big_step_R_def sys_mode_of_def)+)[3] apply (frule step_from_interrupt_to_schedule) by clarsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); sys_mode_of s' = KernelSchedule True; (s', s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); sys_mode_of s' = KernelSchedule True; (s', s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; (s, s'') \<in> data_type.Step (big_step_ADT_A_if utf) (); part s = PSched\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); sys_mode_of s' = KernelSchedule True; (s', s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; (s, s'') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap (); part s = PSched\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. \<lbrakk>(s, s') \<in> data_type.Step (ADT_A_if utf) (); sys_mode_of s' = KernelSchedule True; (s', s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; \<exists>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) () \<and> big_step_R s s''; part s = PSched\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''\<rbrakk> \<Longrightarrow> interrupted_modes (sys_mode_of s) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''\<rbrakk> \<Longrightarrow> interrupted_modes (sys_mode_of s)
 2. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as. \<lbrakk>(((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) (\<lambda>s s'. snd s = KernelExit \<and> interrupted_modes (snd s') \<or> interrupted_modes (snd s) \<and> snd s' = KernelExit) s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); snd s = KernelExit \<and> interrupted_modes (snd s'') \<or> interrupted_modes (snd s) \<and> snd s'' = KernelExit; \<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; scheduler_modes (snd s)\<rbrakk> \<Longrightarrow> interrupted_modes (snd s)
 2. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as = []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as \<noteq> []\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (3 subgoals):
 1. \<And>a b ba as evlist t. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as = []; ((a, b), ba) = t; as = evlist; evlist = []; t = s; \<not> big_step_R s s\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b ba as evlist evlist' e s' t. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as = []; ((a, b), ba) = t; as = evlist; evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t\<rbrakk> \<Longrightarrow> thesis
 3. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as \<noteq> []\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (3 subgoals):
 1. \<And>a b ba as evlist t. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (s, s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); ((a, b), ba) = s; as = []; evlist = []; t = s; \<not> big_step_R s s\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b ba as evlist evlist' e s' t. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as = []; ((a, b), ba) = t; as = evlist; evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t\<rbrakk> \<Longrightarrow> thesis
 3. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as \<noteq> []\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (4 subgoals):
 1. \<And>a b ba as evlist t r. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (s, s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; ((a, b), ba) = s; as = []; evlist = []; t = s; \<not> big_step_R s s; (r, internal_state_if s'') \<in> fst (kernel_entry_if Interrupt (user_context_of s) (internal_state_if s)); sys_mode_of s = KernelEntry Interrupt; sys_mode_of s'' = KernelSchedule True; snd r = user_context_of s; snd r = user_context_of s''; cur_domain (internal_state_if s'') = cur_domain (internal_state_if s)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b ba as evlist t r. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (s, s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; ((a, b), ba) = s; as = []; evlist = []; t = s; \<not> big_step_R s s; (r, internal_state_if s'') \<in> fst (handle_preemption_if (user_context_of s) (internal_state_if s)); sys_mode_of s = KernelPreempted; sys_mode_of s'' = KernelSchedule True; r = user_context_of s; r = user_context_of s''; cur_domain (internal_state_if s'') = cur_domain (internal_state_if s)\<rbrakk> \<Longrightarrow> thesis
 3. \<And>a b ba as evlist evlist' e s' t. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as = []; ((a, b), ba) = t; as = evlist; evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t\<rbrakk> \<Longrightarrow> thesis
 4. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as \<noteq> []\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as \<noteq> []\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (3 subgoals):
 1. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as \<noteq> []\<rbrakk> \<Longrightarrow> as \<noteq> []
 2. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as \<noteq> []\<rbrakk> \<Longrightarrow> interrupted_modes (sys_mode_of s)
 3. \<And>a b ba as. \<lbrakk>\<And>a b ba. \<lbrakk>(s, (a, b), KernelSchedule True) \<in> data_type.Step (ADT_A_if utf) (); ba = KernelSchedule True; (((a, b), KernelSchedule True), s'') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> thesis; part s = PSched; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (((a, b), ba), s'') \<in> data_type.Step (ADT_A_if utf) (); big_step_R s s''; interrupted_modes (sys_mode_of s); as \<noteq> []; (s, (a, b), ba) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of ((a, b), ba) = KernelSchedule True\<rbrakk> \<Longrightarrow> thesis