theory Noninterference

lemma sub_big_steps_reachable:
  "\<lbrakk> (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s;
     system.reachable (ADT_A_if utf) s0 s \<rbrakk>
     \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s'" apply (rule_tac s=s and js=evlist' in Step_system.reachable_execution[OF ADT_A_if_Step_system]) apply assumption apply (drule sub_big_steps_Run) apply (clarsimp simp: execution_def image_def) apply (subst Bex_def) apply (simp only: steps_eq_Run) apply (rule_tac x="s'" in exI) apply (rule conjI) apply (rule_tac x=s in exI) apply (clarsimp simp: system.reachable_def) apply (frule execution_invs) apply (frule invs_if_full_invs_if) apply (frule execution_restrict) apply (simp add: ADT_A_if_def) apply (simp add: ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; system.reachable (ADT_A_if utf) s0 s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; system.reachable (ADT_A_if utf) s0 s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 2. \<lbrakk>(s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; system.reachable (ADT_A_if utf) s0 s\<rbrakk> \<Longrightarrow> s' \<in> execution (ADT_A_if utf) s evlist' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; system.reachable (ADT_A_if utf) s0 s\<rbrakk> \<Longrightarrow> s' \<in> execution (ADT_A_if utf) s evlist' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist' \<and> \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s' \<in> execution (ADT_A_if utf) s evlist' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>steps (data_type.Step (ADT_A_if utf)) (Init (ADT_A_if utf) s) evlist'. s' = Fin (ADT_A_if utf) x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> steps (data_type.Step (ADT_A_if utf)) (Init (ADT_A_if utf) s) evlist' \<and> s' = Fin (ADT_A_if utf) x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init (ADT_A_if utf) s \<and> (s0', x) \<in> Run (data_type.Step (ADT_A_if utf)) evlist') \<and> s' = Fin (ADT_A_if utf) x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> (\<exists>s0'. s0' \<in> Init (ADT_A_if utf) s \<and> (s0', s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist') \<and> s' = Fin (ADT_A_if utf) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> \<exists>s0'. s0' \<in> Init (ADT_A_if utf) s \<and> (s0', s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'
 2. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s' = Fin (ADT_A_if utf) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s \<in> Init (ADT_A_if utf) s \<and> (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'
 2. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s' = Fin (ADT_A_if utf) s' proof (prove)
goal (2 subgoals):
 1. \<And>js. \<lbrakk>(s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'; s \<in> execution (ADT_A_if utf) s0 js\<rbrakk> \<Longrightarrow> s \<in> Init (ADT_A_if utf) s
 2. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s' = Fin (ADT_A_if utf) s' proof (prove)
goal (2 subgoals):
 1. \<And>js. \<lbrakk>(s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'; s \<in> execution (ADT_A_if utf) s0 js; invs_if s\<rbrakk> \<Longrightarrow> s \<in> Init (ADT_A_if utf) s
 2. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s' = Fin (ADT_A_if utf) s' proof (prove)
goal (2 subgoals):
 1. \<And>js. \<lbrakk>(s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'; s \<in> execution (ADT_A_if utf) s0 js; invs_if s; s \<in> full_invs_if\<rbrakk> \<Longrightarrow> s \<in> Init (ADT_A_if utf) s
 2. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s' = Fin (ADT_A_if utf) s' proof (prove)
goal (2 subgoals):
 1. \<And>js. \<lbrakk>(s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'; s \<in> execution (ADT_A_if utf) s0 js; invs_if s; s \<in> full_invs_if; step_restrict s\<rbrakk> \<Longrightarrow> s \<in> Init (ADT_A_if utf) s
 2. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s' = Fin (ADT_A_if utf) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; (s, s') \<in> Run (data_type.Step (ADT_A_if utf)) evlist'; \<not> big_step_R s s'\<rbrakk> \<Longrightarrow> s' = Fin (ADT_A_if utf) s' proof (prove)
goal:
No subgoals!