theory Noninterference_Base

lemma reachable_Fin:
  "\<lbrakk> reachable s; x \<in> steps (Simulation.Step A) (Init A s) as \<rbrakk>
     \<Longrightarrow> reachable (Fin A x)" apply (cut_tac s=s in Init_inv_Fin, assumption) apply (clarsimp simp: reachable_def execution_def steps_def) apply (rule_tac x="js@as" in exI) apply (rule imageI) apply (subgoal_tac "{s'. Fin A s' = Fin A xa} = {xa}") apply simp apply (erule foldl_foldl_Step) apply blast apply (blast dest: injD[OF Fin_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; x \<in> steps (data_type.Step A) (Init A s) as\<rbrakk> \<Longrightarrow> reachable (Fin A x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; x \<in> steps (data_type.Step A) (Init A s) as; Init A s = {s'. Fin A s' = s}\<rbrakk> \<Longrightarrow> reachable (Fin A x) proof (prove)
goal (1 subgoal):
 1. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {s'. Fin A s' = Fin A xa} as; Init A (Fin A xa) = {s'. Fin A s' = Fin A xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa\<rbrakk> \<Longrightarrow> \<exists>js. Fin A x \<in> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js proof (prove)
goal (1 subgoal):
 1. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {s'. Fin A s' = Fin A xa} as; Init A (Fin A xa) = {s'. Fin A s' = Fin A xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa\<rbrakk> \<Longrightarrow> Fin A x \<in> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) (js @ as) proof (prove)
goal (1 subgoal):
 1. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {s'. Fin A s' = Fin A xa} as; Init A (Fin A xa) = {s'. Fin A s' = Fin A xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) (js @ as) proof (prove)
goal (2 subgoals):
 1. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {s'. Fin A s' = Fin A xa} as; Init A (Fin A xa) = {s'. Fin A s' = Fin A xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa; {s'. Fin A s' = Fin A xa} = {xa}\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) (js @ as)
 2. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {s'. Fin A s' = Fin A xa} as; Init A (Fin A xa) = {s'. Fin A s' = Fin A xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa\<rbrakk> \<Longrightarrow> {s'. Fin A s' = Fin A xa} = {xa} proof (prove)
goal (2 subgoals):
 1. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {xa} as; Init A (Fin A xa) = {xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa; {s'. Fin A s' = Fin A xa} = {xa}\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js) as
 2. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {s'. Fin A s' = Fin A xa} as; Init A (Fin A xa) = {s'. Fin A s' = Fin A xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa\<rbrakk> \<Longrightarrow> {s'. Fin A s' = Fin A xa} = {xa} proof (prove)
goal (2 subgoals):
 1. \<And>js x. \<lbrakk>Init A (Fin A x) = {x}; x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A x; {s'. Fin A s' = Fin A x} = {x}\<rbrakk> \<Longrightarrow> {x} \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js
 2. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {s'. Fin A s' = Fin A xa} as; Init A (Fin A xa) = {s'. Fin A s' = Fin A xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa\<rbrakk> \<Longrightarrow> {s'. Fin A s' = Fin A xa} = {xa} proof (prove)
goal (1 subgoal):
 1. \<And>js xa. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) {s'. Fin A s' = Fin A xa} as; Init A (Fin A xa) = {s'. Fin A s' = Fin A xa}; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; s = Fin A xa\<rbrakk> \<Longrightarrow> {s'. Fin A s' = Fin A xa} = {xa} proof (prove)
goal:
No subgoals!