theory Noninterference_Base

lemma Run_subset_execution:
  "\<lbrakk> no_abs; reachable s \<rbrakk> \<Longrightarrow> {s'. (s,s') \<in> Run Step as} \<subseteq> execution A s as" apply (induct as arbitrary: s rule: rev_induct) apply (simp add: execution_def steps_def Fin_Init) apply (simp add: execution_def steps_def) apply (rule subsetI) apply clarsimp apply (drule Run_mid) apply clarsimp apply (drule_tac x=s in meta_spec) apply clarsimp apply (drule_tac subsetD) apply blast apply (clarsimp simp: Image_def image_def Step_def execution_def steps_def) apply (rule_tac x=xc in exI) apply clarsimp apply (rule_tac x=xd in bexI) apply assumption apply (drule_tac x=xb in no_absD) apply (simp add: steps_def Image_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_abs; reachable s\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step as} \<subseteq> execution A s as proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>no_abs; reachable s\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step []} \<subseteq> execution A s []
 2. \<And>x xs s. \<lbrakk>\<And>s. \<lbrakk>no_abs; reachable s\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step xs} \<subseteq> execution A s xs; no_abs; reachable s\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step (xs @ [x])} \<subseteq> execution A s (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. \<lbrakk>no_abs; reachable s\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step xs} \<subseteq> execution A s xs; no_abs; reachable s\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step (xs @ [x])} \<subseteq> execution A s (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. reachable s \<Longrightarrow> {s'. (s, s') \<in> Run local.Step xs} \<subseteq> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs; no_abs; reachable s\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step (xs @ [x])} \<subseteq> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xa. \<lbrakk>\<And>s. reachable s \<Longrightarrow> {s'. (s, s') \<in> Run local.Step xs} \<subseteq> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs; no_abs; reachable s; xa \<in> {s'. (s, s') \<in> Run local.Step (xs @ [x])}\<rbrakk> \<Longrightarrow> xa \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xa. \<lbrakk>\<And>s. reachable s \<Longrightarrow> {s'. (s, s') \<in> Run local.Step xs} \<subseteq> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs; no_abs; reachable s; (s, xa) \<in> Run local.Step (xs @ [x])\<rbrakk> \<Longrightarrow> xa \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xa. \<lbrakk>\<And>s. reachable s \<Longrightarrow> {s'. (s, s') \<in> Run local.Step xs} \<subseteq> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs; no_abs; reachable s; \<exists>t. (s, t) \<in> Run local.Step xs \<and> (t, xa) \<in> Run local.Step [x]\<rbrakk> \<Longrightarrow> xa \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xa t. \<lbrakk>\<And>s. reachable s \<Longrightarrow> {s'. (s, s') \<in> Run local.Step xs} \<subseteq> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs; no_abs; reachable s; (s, t) \<in> Run local.Step xs; (t, xa) \<in> local.Step x\<rbrakk> \<Longrightarrow> xa \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xa t. \<lbrakk>no_abs; reachable s; (s, t) \<in> Run local.Step xs; (t, xa) \<in> local.Step x; reachable s \<Longrightarrow> {s'. (s, s') \<in> Run local.Step xs} \<subseteq> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs\<rbrakk> \<Longrightarrow> xa \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xa t. \<lbrakk>no_abs; reachable s; (s, t) \<in> Run local.Step xs; (t, xa) \<in> local.Step x; {s'. (s, s') \<in> Run local.Step xs} \<subseteq> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs\<rbrakk> \<Longrightarrow> xa \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (2 subgoals):
 1. \<And>x xs s xa t. \<lbrakk>no_abs; reachable s; (s, t) \<in> Run local.Step xs; (t, xa) \<in> local.Step x\<rbrakk> \<Longrightarrow> ?c15 x xs s xa t \<in> {s'. (s, s') \<in> Run local.Step xs}
 2. \<And>x xs s xa t. \<lbrakk>no_abs; reachable s; (s, t) \<in> Run local.Step xs; (t, xa) \<in> local.Step x; ?c15 x xs s xa t \<in> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs\<rbrakk> \<Longrightarrow> xa \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xa t. \<lbrakk>no_abs; reachable s; (s, t) \<in> Run local.Step xs; (t, xa) \<in> local.Step x; t \<in> Fin A ` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs\<rbrakk> \<Longrightarrow> xa \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xb xc xd. \<lbrakk>no_abs; reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>xb\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs. (xb, xa) \<in> data_type.Step A x) \<and> Fin A xc = Fin A xa proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xb xc xd. \<lbrakk>no_abs; reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> (\<exists>xa\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs. (xa, xc) \<in> data_type.Step A x) \<and> Fin A xc = Fin A xc proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xb xc xd. \<lbrakk>no_abs; reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> \<exists>xa\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs. (xa, xc) \<in> data_type.Step A x proof (prove)
goal (2 subgoals):
 1. \<And>x xs s xb xc xd. \<lbrakk>no_abs; reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> (xd, xc) \<in> data_type.Step A x
 2. \<And>x xs s xb xc xd. \<lbrakk>no_abs; reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> xd \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs s xb xc xd. \<lbrakk>no_abs; reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> xd \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs proof (prove)
goal (3 subgoals):
 1. \<And>x xs s xb xc xd. \<lbrakk>reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> reachable (?s27 x xs s xb xc xd)
 2. \<And>x xs s xb xc xd. \<lbrakk>reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> xb \<in> steps (data_type.Step A) (Init A (?s27 x xs s xb xc xd)) (?as27 x xs s xb xc xd)
 3. \<And>x xs s xb xc xd. \<lbrakk>reachable s; (s, Fin A xb) \<in> Run local.Step xs; xb \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs; xd \<in> Init A (Fin A xb); (xd, xc) \<in> data_type.Step A x; Init A (Fin A xb) = {xb}\<rbrakk> \<Longrightarrow> xd \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> data_type.Step A j}) (Init A s) xs proof (prove)
goal:
No subgoals!