theory Noninterference

lemma uwr_part_sys_mode_of_eq:
  "\<lbrakk> (s,t) \<in> uwr (part s); part t = part s; part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> sys_mode_of s = sys_mode_of t" apply (simp add: part_def split: if_split_asm) apply (simp add: partition_def) apply (cut_tac pas_wellformed_noninterference_silc
                   [OF policy_wellformed, where d="cur_domain (internal_state_if s)"]) apply (case_tac "the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))") apply (simp add: uwr_def sameFor_def) apply (erule (1) sameFor_current_partition_sys_mode_of_eq) apply (metis the_subject_of_aag_domain subject_current_aag) apply (metis the_label_of_domain_exists) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uwr2 s (part s) t; part t = part s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); uwr2 s (Partition (partition_if s)) t; \<not> scheduler_modes (sys_mode_of t); partition_if t = partition_if s\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); uwr2 s (Partition (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))))) t; \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s))))\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); uwr2 s (Partition (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))))) t; \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))); SilcLabel \<notin> pasDomainAbs initial_aag (cur_domain (internal_state_if s))\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); uwr2 s (Partition (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))))) t; \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))); SilcLabel \<notin> pasDomainAbs initial_aag (cur_domain (internal_state_if s)); the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s))) = OrdinaryLabel x1\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t
 2. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); uwr2 s (Partition (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))))) t; \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))); SilcLabel \<notin> pasDomainAbs initial_aag (cur_domain (internal_state_if s)); the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s))) = SilcLabel\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); (s, t) \<in> sameFor_subject (pasPolicy initial_aag) (pasObjectAbs initial_aag) (pasIRQAbs initial_aag) (pasASIDAbs initial_aag) (pasDomainAbs initial_aag) x1; \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = x1; the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s))) = OrdinaryLabel x1\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t
 2. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); uwr2 s (Partition (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))))) t; \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))); SilcLabel \<notin> pasDomainAbs initial_aag (cur_domain (internal_state_if s)); the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s))) = SilcLabel\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = x1; the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s))) = OrdinaryLabel x1\<rbrakk> \<Longrightarrow> OrdinaryLabel x1 \<in> pasDomainAbs initial_aag (cur_domain (internal_state_if s))
 2. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); uwr2 s (Partition (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))))) t; \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))); SilcLabel \<notin> pasDomainAbs initial_aag (cur_domain (internal_state_if s)); the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s))) = SilcLabel\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> scheduler_modes (sys_mode_of s); uwr2 s (Partition (label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))))) t; \<not> scheduler_modes (sys_mode_of t); label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if t)))) = label_of (the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))); SilcLabel \<notin> pasDomainAbs initial_aag (cur_domain (internal_state_if s)); the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s))) = SilcLabel\<rbrakk> \<Longrightarrow> sys_mode_of s = sys_mode_of t proof (prove)
goal:
No subgoals!