theory Noninterference

lemma sub_big_steps_partitionIntegrity:
  "\<lbrakk> (t, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s;
     big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s))
                            (internal_state_if s) (internal_state_if t)" apply (induct t as rule: sub_big_steps.induct) apply (simp add: partitionIntegrity_def globals_equiv_scheduler_refl
                    silc_dom_equiv_def equiv_for_refl domain_fields_equiv_def) apply simp apply (erule partitionIntegrity_trans') apply (erule small_Step_partitionIntegrity) apply (blast intro: sub_big_steps_reachable) apply (rule sub_big_steps_not_PSched, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(t, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (prove)
goal (2 subgoals):
 1. \<And>evlist t. \<lbrakk>evlist = []; t = s; \<not> big_step_R s s; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t)
 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>big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) 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>big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); (s', t) \<in> data_type.Step (ADT_A_if utf) e; \<not> big_step_R s t; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if 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; partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s'); (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if 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; (s', t) \<in> data_type.Step (ADT_A_if utf) (); \<not> big_step_R s t; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s')) (internal_state_if s') (internal_state_if t) proof (prove)
goal (2 subgoals):
 1. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<not> big_step_R s t; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s'
 2. \<And>evlist evlist' s' t. \<lbrakk>evlist = evlist' @ [()]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<not> big_step_R s t; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s' \<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; \<not> big_step_R s t; big_step_R\<^sup>*\<^sup>* s0 s; system.reachable (ADT_A_if utf) s0 s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched proof (prove)
goal:
No subgoals!