theory Noninterference

lemma step_from_interrupt_to_schedule:
  "\<lbrakk> (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s;
     evs \<noteq> []; interrupted_modes (sys_mode_of s) \<rbrakk>
     \<Longrightarrow> (s,s') \<in> data_type.Step (ADT_A_if utf) () \<and> (sys_mode_of s') = KernelSchedule True" apply (induct rule: sub_big_steps.induct) apply simp apply (case_tac "evlist'") apply simp 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)+)[2] apply simp apply simp apply (elim conjE) apply (erule schedule_step[rotated],assumption) apply (simp add: big_step_R_def sys_mode_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; evs \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True proof (prove)
goal (2 subgoals):
 1. \<And>evlist t. \<lbrakk>evlist = []; t = s; \<not> big_step_R s s; evlist \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True
 2. \<And>evlist evlist' e s' t. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' e s' t. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (2 subgoals):
 1. \<And>evlist evlist' e s' t. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s); evlist' = []\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True
 2. \<And>evlist evlist' e s' t a list. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s); evlist' = a # list\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (2 subgoals):
 1. \<And>evlist evlist' s' t. \<lbrakk>evlist = [()]; (s', []) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = []\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True
 2. \<And>evlist evlist' e s' t a list. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s); evlist' = a # list\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (3 subgoals):
 1. \<And>evlist evlist' s' t evlista ta. \<lbrakk>evlist = [()]; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = []; s' = ta; [] = evlista; evlista = []; ta = s; \<not> big_step_R s s\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True
 2. \<And>evlist evlist' s' t evlista evlist'a e s'a ta. \<lbrakk>evlist = [()]; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = []; s' = ta; [] = evlista; evlista = evlist'a @ [e]; (s'a, evlist'a) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s ta\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True
 3. \<And>evlist evlist' e s' t a list. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s); evlist' = a # list\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (3 subgoals):
 1. \<And>evlist evlist' s' t evlista ta. \<lbrakk>evlist = [()]; (s, t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = []; s' = s; evlista = []; ta = s; \<not> big_step_R s s\<rbrakk> \<Longrightarrow> sys_mode_of t = KernelSchedule True
 2. \<And>evlist evlist' s' t evlista evlist'a e s'a ta. \<lbrakk>evlist = [()]; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = []; s' = ta; [] = evlista; evlista = evlist'a @ [e]; (s'a, evlist'a) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s ta\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True
 3. \<And>evlist evlist' e s' t a list. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s); evlist' = a # list\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (4 subgoals):
 1. \<And>evlist evlist' s' t evlista ta r. \<lbrakk>evlist = [()]; (s, t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; evlist' = []; s' = s; evlista = []; ta = s; \<not> big_step_R s s; (r, internal_state_if t) \<in> fst (kernel_entry_if Interrupt (user_context_of s) (internal_state_if s)); sys_mode_of s = KernelEntry Interrupt; sys_mode_of t = KernelSchedule True; snd r = user_context_of s; snd r = user_context_of t; cur_domain (internal_state_if t) = cur_domain (internal_state_if s)\<rbrakk> \<Longrightarrow> sys_mode_of t = KernelSchedule True
 2. \<And>evlist evlist' s' t evlista ta r. \<lbrakk>evlist = [()]; (s, t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; evlist' = []; s' = s; evlista = []; ta = s; \<not> big_step_R s s; (r, internal_state_if t) \<in> fst (handle_preemption_if (user_context_of s) (internal_state_if s)); sys_mode_of s = KernelPreempted; sys_mode_of t = KernelSchedule True; r = user_context_of s; r = user_context_of t; cur_domain (internal_state_if t) = cur_domain (internal_state_if s)\<rbrakk> \<Longrightarrow> sys_mode_of t = KernelSchedule True
 3. \<And>evlist evlist' s' t evlista evlist'a e s'a ta. \<lbrakk>evlist = [()]; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = []; s' = ta; [] = evlista; evlista = evlist'a @ [e]; (s'a, evlist'a) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s ta\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True
 4. \<And>evlist evlist' e s' t a list. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s); evlist' = a # list\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (2 subgoals):
 1. \<And>evlist evlist' s' t evlista evlist'a e s'a ta. \<lbrakk>evlist = [()]; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = []; s' = ta; [] = evlista; evlista = evlist'a @ [e]; (s'a, evlist'a) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s ta\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True
 2. \<And>evlist evlist' e s' t a list. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s); evlist' = a # list\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' e s' t a list. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<lbrakk>evlist' \<noteq> []; interrupted_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; evlist \<noteq> []; interrupted_modes (sys_mode_of s); evlist' = a # list\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' s' t list. \<lbrakk>evlist = () # list @ [()]; (s', () # list) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s, s') \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of s' = KernelSchedule True; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = () # list\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' s' t list. \<lbrakk>evlist = () # list @ [()]; (s', () # list) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = () # list; (s, s') \<in> data_type.Step (ADT_A_if utf) (); sys_mode_of s' = KernelSchedule True\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' s' t list r. \<lbrakk>evlist = () # list @ [()]; (s', () # list) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; interrupted_modes (sys_mode_of s); evlist' = () # list; (s, s') \<in> data_type.Step (ADT_A_if utf) (); (r, internal_state_if t) \<in> fst (schedule_if (user_context_of s') (internal_state_if s')); sys_mode_of t = KernelExit; r = user_context_of s'; r = user_context_of t\<rbrakk> \<Longrightarrow> (s, t) \<in> data_type.Step (ADT_A_if utf) () \<and> sys_mode_of t = KernelSchedule True proof (prove)
goal:
No subgoals!