theory Noninterference_Base

lemma execution_subset_Run:
  "reachable s \<Longrightarrow> execution A s as \<subseteq> {s'. (s,s') \<in> Run Step 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 (rule Run_trans) apply blast apply (cut_tac x=xc and s=s and as=xs in Init_Fin, (simp add: steps_def)+) apply (clarsimp simp: Step_def execution_def steps_def) apply blast done

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