theory Noninterference

lemma sub_big_steps_not_PSched:
  "\<lbrakk> (s', blah) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R\<^sup>*\<^sup>* s0 s; part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> part s' \<noteq> PSched" apply (drule tranclp_s0) apply (induct s' blah rule: sub_big_steps.induct) apply simp apply simp apply (simp add: part_def split: if_splits) apply (case_tac "sys_mode_of s", simp_all add: sys_mode_of_def) apply (case_tac "sys_mode_of s'", simp_all add: sys_mode_of_def) apply (case_tac "sys_mode_of t", simp_all add: sys_mode_of_def big_step_R_def split: if_splits) apply (rename_tac event) apply (case_tac event, simp_all) apply ((fastforce simp: ADT_A_if_def global_automaton_if_def)+)[2] apply (case_tac "sys_mode_of t", simp_all add: sys_mode_of_def big_step_R_def split: if_splits) apply (fastforce simp: ADT_A_if_def global_automaton_if_def)+ apply (case_tac "sys_mode_of t", simp_all add: sys_mode_of_def) apply (clarsimp simp: ADT_A_if_def global_automaton_if_def kernel_exit_A_if_def split: if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', blah) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R\<^sup>*\<^sup>* s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', blah) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s \<noteq> PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched proof (prove)
goal (2 subgoals):
 1. \<And>evlist t. \<lbrakk>evlist = []; t = s; \<not> big_step_R s s; part s \<noteq> PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> part t \<noteq> PSched
 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>part s \<noteq> PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; part s \<noteq> PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> part t \<noteq> PSched 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>part s \<noteq> PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched; (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; part s \<noteq> PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> part t \<noteq> PSched proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s' \<noteq> PSched; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; part s \<noteq> PSched; interrupted_modes (snd s) \<or> snd s = KernelExit\<rbrakk> \<Longrightarrow> part t \<noteq> PSched proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' s' t. \<lbrakk>interrupted_modes (snd s) \<or> snd s = KernelExit; evlist = evlist' @ [()]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<not> scheduler_modes (sys_mode_of s'); (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; \<not> scheduler_modes (sys_mode_of s)\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (sys_mode_of t) proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<not> scheduler_modes (snd s'); (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; snd s = KernelExit\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t) proof (prove)
goal (5 subgoals):
 1. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; snd s = KernelExit; snd s' = InUserMode\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 2. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; snd s = KernelExit; snd s' = InIdleMode\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 3. \<And>evlist evlist' s' t x3. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<not> scheduler_modes (KernelEntry x3); (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; snd s = KernelExit; snd s' = KernelEntry x3\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 4. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<not> x5; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; snd s = KernelExit; snd s' = KernelSchedule False\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 5. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; snd s = KernelExit; snd s' = KernelExit\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t) proof (prove)
goal (6 subgoals):
 1. \<And>evlist evlist' s' t x3. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); x3 \<noteq> Interrupt; snd s = KernelExit; snd s' = InUserMode; snd t = KernelEntry x3\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (KernelEntry x3)
 2. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); snd s = KernelExit; snd s' = InUserMode; snd t = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<not> x5
 3. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = InIdleMode\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 4. \<And>evlist evlist' s' t x3. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> scheduler_modes (KernelEntry x3); (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelEntry x3\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 5. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> x5; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelSchedule False\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 6. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelExit\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t) proof (prove)
goal (6 subgoals):
 1. \<And>evlist evlist' s' t event. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); event \<noteq> Interrupt; snd s = KernelExit; snd s' = InUserMode; snd t = KernelEntry event\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (KernelEntry event)
 2. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); snd s = KernelExit; snd s' = InUserMode; snd t = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<not> x5
 3. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = InIdleMode\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 4. \<And>evlist evlist' s' t x3. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> scheduler_modes (KernelEntry x3); (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelEntry x3\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 5. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> x5; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelSchedule False\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 6. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelExit\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t) proof (prove)
goal (5 subgoals):
 1. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); snd s = KernelExit; snd s' = InUserMode; snd t = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<not> x5
 2. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = InIdleMode\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 3. \<And>evlist evlist' s' t x3. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> scheduler_modes (KernelEntry x3); (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelEntry x3\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 4. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> x5; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelSchedule False\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 5. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelExit\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t) proof (prove)
goal (3 subgoals):
 1. \<And>evlist evlist' s' t x3. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> scheduler_modes (KernelEntry x3); (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelEntry x3\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 2. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> x5; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelSchedule False\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 3. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelExit\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t) proof (prove)
goal (4 subgoals):
 1. \<And>evlist evlist' s' t x3 x3a. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> scheduler_modes (KernelEntry x3); (s', t) \<in> data_type.Step (ADT_A_if utf) (); x3a \<noteq> Interrupt; snd s = KernelExit; snd s' = KernelEntry x3; snd t = KernelEntry x3a\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (KernelEntry x3a)
 2. \<And>evlist evlist' s' t x3 x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> scheduler_modes (KernelEntry x3); (s', t) \<in> data_type.Step (ADT_A_if utf) (); snd s = KernelExit; snd s' = KernelEntry x3; snd t = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<not> x5
 3. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; \<not> x5; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelSchedule False\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t)
 4. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelExit\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t) proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> interrupted_modes (snd t); snd s = KernelExit; snd s' = KernelExit\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (snd t) proof (prove)
goal (2 subgoals):
 1. \<And>evlist evlist' s' t x3. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); x3 \<noteq> Interrupt; snd s = KernelExit; snd s' = KernelExit; snd t = KernelEntry x3\<rbrakk> \<Longrightarrow> \<not> scheduler_modes (KernelEntry x3)
 2. \<And>evlist evlist' s' t x5. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); snd s = KernelExit; snd s' = KernelExit; snd t = KernelSchedule x5\<rbrakk> \<Longrightarrow> \<not> x5 proof (prove)
goal:
No subgoals!