theory Noninterference_Base

lemma foldl_foldl_Step:
  "\<lbrakk> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M as;
     M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js \<rbrakk>
     \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) as" apply (induct as arbitrary: x M js B rule: rev_induct) apply fastforce apply simp apply (erule ImageE) apply (drule_tac x=xb in meta_spec) apply (drule_tac x=M in meta_spec) apply simp apply (drule_tac x=js in meta_spec) apply (drule_tac x=B in meta_spec, simp) apply (blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M as; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) as proof (prove)
goal (2 subgoals):
 1. \<And>x M js B. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M []; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) []
 2. \<And>x xs xa M js B. \<lbrakk>\<And>x M js B. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M (xs @ [x]); M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa M js B. \<lbrakk>\<And>x M js B. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs; xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M (xs @ [x]); M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa M js B. \<lbrakk>\<And>x M js B. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs; xa \<in> data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) M xs; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> xa \<in> data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa M js B xb. \<lbrakk>\<And>x M js B. \<lbrakk>x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js; (xb, xa) \<in> data_type.Step A x; xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs\<rbrakk> \<Longrightarrow> xa \<in> data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa M js B xb. \<lbrakk>M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js; (xb, xa) \<in> data_type.Step A x; xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; \<And>M js B. \<lbrakk>xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs\<rbrakk> \<Longrightarrow> xa \<in> data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa M js B xb. \<lbrakk>M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js; (xb, xa) \<in> data_type.Step A x; xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; \<And>js B. \<lbrakk>xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js\<rbrakk> \<Longrightarrow> xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs\<rbrakk> \<Longrightarrow> xa \<in> data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa M js B xb. \<lbrakk>M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js; (xb, xa) \<in> data_type.Step A x; xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; \<And>js B. M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js \<Longrightarrow> xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs\<rbrakk> \<Longrightarrow> xa \<in> data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa M js B xb. \<lbrakk>M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js; (xb, xa) \<in> data_type.Step A x; xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; \<And>B. M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js \<Longrightarrow> xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs\<rbrakk> \<Longrightarrow> xa \<in> data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa M js B xb. \<lbrakk>M \<subseteq> foldl (\<lambda>S j. data_type.Step A j `` S) B js; (xb, xa) \<in> data_type.Step A x; xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) M xs; xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs\<rbrakk> \<Longrightarrow> xa \<in> data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (foldl (\<lambda>S j. data_type.Step A j `` S) B js) xs proof (prove)
goal:
No subgoals!