theory Noninterference

lemma Step_partitionIntegrity':
  "\<lbrakk> (s, s') \<in> Simulation.Step (big_step_ADT_A_if utf) ()\<rbrakk>
     \<Longrightarrow> system.reachable (big_step_ADT_A_if utf) s0 s \<and> part s \<noteq> PSched
         \<longrightarrow> partitionIntegrity (current_aag (internal_state_if s))
                                (internal_state_if s) (internal_state_if s')" apply (simp add: Step_big_step_ADT_A_if) apply (erule big_steps.induct) apply (simp add: big_step_evmap_def) apply (intro impI | elim conjE)+ apply (rule partitionIntegrity_trans') apply (erule sub_big_steps_partitionIntegrity) apply (simp add: reachable_def execution_def) apply (clarsimp simp: big_step_ADT_A_if_def Fin_big_step_adt Fin_ADT_if steps_eq_Run) apply (rule Run_big_steps_tranclp) apply (simp add: big_step_ADT_A_if_def big_step_adt_def Init_ADT_if) apply (blast intro: small_step_reachable) apply assumption apply (erule small_Step_partitionIntegrity) apply (erule(1) sub_big_steps_reachable[OF _ small_step_reachable]) apply (rule sub_big_steps_not_PSched, simp+) apply (simp add: reachable_def execution_def) apply (clarsimp simp: big_step_ADT_A_if_def Fin_big_step_adt Fin_ADT_if steps_eq_Run) apply (rule Run_big_steps_tranclp) apply (simp add: big_step_ADT_A_if_def big_step_adt_def Init_ADT_if) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) () \<Longrightarrow> reachable s \<and> part s \<noteq> PSched \<longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap () \<Longrightarrow> reachable s \<and> part s \<noteq> PSched \<longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if s') proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t a. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a])\<rbrakk> \<Longrightarrow> reachable s \<and> part s \<noteq> PSched \<longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t\<rbrakk> \<Longrightarrow> reachable s \<and> part s \<noteq> PSched \<longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (internal_state_if t) proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable 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>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (internal_state_if s)) (internal_state_if s) (?s'9 s' as s t)
 2. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag (?s'9 s' as s t)) (?s'9 s' as s t) (internal_state_if t) proof (prove)
goal (4 subgoals):
 1. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable 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 (4 subgoals):
 1. \<And>s' s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; \<exists>js. s \<in> Fin (big_step_ADT_A_if utf) ` steps (data_type.Step (big_step_ADT_A_if utf)) (Init (big_step_ADT_A_if utf) s0) js; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable 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 (4 subgoals):
 1. \<And>a b ba aa bb bc ab bd be js ac bf bg. \<lbrakk>(((a, b), ba), (ab, bd), be) \<in> data_type.Step (ADT_A_if utf) (); big_step_R ((aa, bb), bc) ((ab, bd), be); part ((aa, bb), bc) \<noteq> PSched; ((ac, bf), bg) \<in> Init (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) s0; (((ac, bf), bg), (aa, bb), bc) \<in> Run (data_type.Step (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap)) js\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 ((aa, bb), bc)
 2. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable 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 (4 subgoals):
 1. \<And>a b ba aa bb bc ab bd be js ac bf bg. \<lbrakk>(((a, b), ba), (ab, bd), be) \<in> data_type.Step (ADT_A_if utf) (); big_step_R ((aa, bb), bc) ((ab, bd), be); part ((aa, bb), bc) \<noteq> PSched; ((ac, bf), bg) \<in> Init (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) s0; (((ac, bf), bg), (aa, bb), bc) \<in> Run (data_type.Step (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap)) js\<rbrakk> \<Longrightarrow> (s0, (aa, bb), bc) \<in> Run (big_steps (?C23 a b ba aa bb bc ab bd be js ac bf bg) big_step_R (?exmap23 a b ba aa bb bc ab bd be js ac bf bg)) (?js23 a b ba aa bb bc ab bd be js ac bf bg)
 2. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable 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 (3 subgoals):
 1. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 2. \<And>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable 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>s' as s t. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable 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>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; reachable 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>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s'
 2. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched proof (prove)
goal (2 subgoals):
 1. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched proof (prove)
goal (2 subgoals):
 1. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; \<exists>js. s \<in> Fin (big_step_ADT_A_if utf) ` steps (data_type.Step (big_step_ADT_A_if utf)) (Init (big_step_ADT_A_if utf) s0) js; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as aa bb bc ab bd be js ac bf bg. \<lbrakk>(((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((aa, bb), bc); big_step_R ((aa, bb), bc) ((ab, bd), be); part ((aa, bb), bc) \<noteq> PSched; ((ac, bf), bg) \<in> Init (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) s0; (((ac, bf), bg), (aa, bb), bc) \<in> Run (data_type.Step (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap)) js\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 ((aa, bb), bc)
 2. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as aa bb bc ab bd be js ac bf bg. \<lbrakk>(((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((aa, bb), bc); big_step_R ((aa, bb), bc) ((ab, bd), be); part ((aa, bb), bc) \<noteq> PSched; ((ac, bf), bg) \<in> Init (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) s0; (((ac, bf), bg), (aa, bb), bc) \<in> Run (data_type.Step (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap)) js\<rbrakk> \<Longrightarrow> (s0, (aa, bb), bc) \<in> Run (big_steps (?C49 a b ba as aa bb bc ab bd be js ac bf bg) big_step_R (?exmap49 a b ba as aa bb bc ab bd be js ac bf bg)) (?js49 a b ba as aa bb bc ab bd be js ac bf bg)
 2. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; big_step_R s t; reachable s; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched