theory Noninterference_Base

lemma Init_inv_Fin_system_Init_Fin_system:
  "Init_inv_Fin_system A s0 \<Longrightarrow> Init_Fin_system A s0" apply (unfold_locales) apply (erule Init_inv_Fin_system.s0_reachable) apply (simp add: Init_inv_Fin_system.Init_inv_Fin) apply (simp add: image_def) apply (fastforce simp: system.reachable_def execution_def) apply (cut_tac s="Fin A x" in Init_inv_Fin_system.Init_inv_Fin) apply assumption apply (blast intro: Init_inv_Fin_system.reachable_Fin) apply simp apply (rule disjI2) apply (clarsimp simp: system.no_abs_def) apply (frule Init_inv_Fin_system.Fin_inj) apply (cut_tac s="Fin A x" in Init_inv_Fin_system.Init_inv_Fin) apply assumption apply (blast intro: Init_inv_Fin_system.reachable_Fin) apply simp apply (fastforce dest: injD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system A s0 \<Longrightarrow> Init_Fin_system A s0 proof (prove)
goal (4 subgoals):
 1. Init_inv_Fin_system A s0 \<Longrightarrow> system.reachable A s0 s0
 2. \<And>s. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> Fin A ` Init A s = {s}
 3. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> x \<in> Init A (Fin A x)
 4. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> Fin A ` Init A s = {s}
 2. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> x \<in> Init A (Fin A x)
 3. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> (\<lambda>x. s) ` {s'. Fin A s' = s} = {s}
 2. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> x \<in> Init A (Fin A x)
 3. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> {y. y = s \<and> (\<exists>x. Fin A x = s)} = {s}
 2. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> x \<in> Init A (Fin A x)
 3. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (2 subgoals):
 1. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> x \<in> Init A (Fin A x)
 2. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (4 subgoals):
 1. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> Init_inv_Fin_system (?A24 s x as) (?s0.24 s x as)
 2. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> system.reachable (?A24 s x as) (?s0.24 s x as) (Fin A x)
 3. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; Init (?A24 s x as) (Fin A x) = {s'. Fin (?A24 s x as) s' = Fin A x}\<rbrakk> \<Longrightarrow> x \<in> Init A (Fin A x)
 4. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (3 subgoals):
 1. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> system.reachable A s0 (Fin A x)
 2. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; Init A (Fin A x) = {s'. Fin A s' = Fin A x}\<rbrakk> \<Longrightarrow> x \<in> Init A (Fin A x)
 3. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (2 subgoals):
 1. \<And>s x as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; Init A (Fin A x) = {s'. Fin A s' = Fin A x}\<rbrakk> \<Longrightarrow> x \<in> Init A (Fin A x)
 2. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system A s0 \<Longrightarrow> system.obs_det A \<or> system.no_abs A s0 proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system A s0 \<Longrightarrow> system.no_abs A s0 proof (prove)
goal (1 subgoal):
 1. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as\<rbrakk> \<Longrightarrow> Init A (Fin A x) = {x} proof (prove)
goal (1 subgoal):
 1. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; inj (Fin A)\<rbrakk> \<Longrightarrow> Init A (Fin A x) = {x} proof (prove)
goal (3 subgoals):
 1. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; inj (Fin A)\<rbrakk> \<Longrightarrow> Init_inv_Fin_system (?A41 x s as) (?s0.41 x s as)
 2. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; inj (Fin A)\<rbrakk> \<Longrightarrow> system.reachable (?A41 x s as) (?s0.41 x s as) (Fin A x)
 3. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; inj (Fin A); Init (?A41 x s as) (Fin A x) = {s'. Fin (?A41 x s as) s' = Fin A x}\<rbrakk> \<Longrightarrow> Init A (Fin A x) = {x} proof (prove)
goal (2 subgoals):
 1. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; inj (Fin A)\<rbrakk> \<Longrightarrow> system.reachable A s0 (Fin A x)
 2. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; inj (Fin A); Init A (Fin A x) = {s'. Fin A s' = Fin A x}\<rbrakk> \<Longrightarrow> Init A (Fin A x) = {x} proof (prove)
goal (1 subgoal):
 1. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; inj (Fin A); Init A (Fin A x) = {s'. Fin A s' = Fin A x}\<rbrakk> \<Longrightarrow> Init A (Fin A x) = {x} proof (prove)
goal (1 subgoal):
 1. \<And>x s as. \<lbrakk>Init_inv_Fin_system A s0; system.reachable A s0 s; x \<in> steps (Step A) (Init A s) as; inj (Fin A); Init A (Fin A x) = {s'. Fin A s' = Fin A x}\<rbrakk> \<Longrightarrow> {s'. Fin A s' = Fin A x} = {x} proof (prove)
goal:
No subgoals!