theory Noninterference_Base

lemma Run_mid[rule_format]:
  "(s,u) \<in> Run Stepf (as @ bs) \<longrightarrow> (\<exists>t. (s,t) \<in> Run Stepf as \<and> (t,u) \<in> Run Stepf bs)" proof (induct as arbitrary: s u bs) case Nil show ?case by (clarsimp) next case (Cons a as) show ?case apply (clarsimp simp: relcomp_def) apply (drule "Cons.hyps"[rule_format]) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, u) \<in> Run Stepf (as @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf as \<and> (t, u) \<in> Run Stepf bs) proof (state)
goal (2 subgoals):
 1. \<And>s u bs. (s, u) \<in> Run Stepf ([] @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf [] \<and> (t, u) \<in> Run Stepf bs)
 2. \<And>a as s u bs. (\<And>s u bs. (s, u) \<in> Run Stepf (as @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf as \<and> (t, u) \<in> Run Stepf bs)) \<Longrightarrow> (s, u) \<in> Run Stepf ((a # as) @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf (a # as) \<and> (t, u) \<in> Run Stepf bs) proof (state)
this:


goal (2 subgoals):
 1. \<And>s u bs. (s, u) \<in> Run Stepf ([] @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf [] \<and> (t, u) \<in> Run Stepf bs)
 2. \<And>a as s u bs. (\<And>s u bs. (s, u) \<in> Run Stepf (as @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf as \<and> (t, u) \<in> Run Stepf bs)) \<Longrightarrow> (s, u) \<in> Run Stepf ((a # as) @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf (a # as) \<and> (t, u) \<in> Run Stepf bs) proof (prove)
goal (1 subgoal):
 1. (s, u) \<in> Run Stepf ([] @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf [] \<and> (t, u) \<in> Run Stepf bs) proof (state)
this:
(s, u) \<in> Run Stepf ([] @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf [] \<and> (t, u) \<in> Run Stepf bs)

goal (1 subgoal):
 1. \<And>a as s u bs. (\<And>s u bs. (s, u) \<in> Run Stepf (as @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf as \<and> (t, u) \<in> Run Stepf bs)) \<Longrightarrow> (s, u) \<in> Run Stepf ((a # as) @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf (a # as) \<and> (t, u) \<in> Run Stepf bs) proof (state)
goal (1 subgoal):
 1. \<And>a as s u bs. (\<And>s u bs. (s, u) \<in> Run Stepf (as @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf as \<and> (t, u) \<in> Run Stepf bs)) \<Longrightarrow> (s, u) \<in> Run Stepf ((a # as) @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf (a # as) \<and> (t, u) \<in> Run Stepf bs) proof (state)
this:
(?s, ?u) \<in> Run Stepf (as @ ?bs) \<longrightarrow> (\<exists>t. (?s, t) \<in> Run Stepf as \<and> (t, ?u) \<in> Run Stepf ?bs)

goal (1 subgoal):
 1. \<And>a as s u bs. (\<And>s u bs. (s, u) \<in> Run Stepf (as @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf as \<and> (t, u) \<in> Run Stepf bs)) \<Longrightarrow> (s, u) \<in> Run Stepf ((a # as) @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf (a # as) \<and> (t, u) \<in> Run Stepf bs) proof (prove)
goal (1 subgoal):
 1. (s, u) \<in> Run Stepf ((a # as) @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf (a # as) \<and> (t, u) \<in> Run Stepf bs) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(s, b) \<in> Stepf a; (b, u) \<in> Run Stepf (as @ bs)\<rbrakk> \<Longrightarrow> \<exists>t. ((\<lambda>x xa. (x, xa) \<in> Stepf a) OO (\<lambda>x xa. (x, xa) \<in> Run Stepf as)) s t \<and> (t, u) \<in> Run Stepf bs proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(s, b) \<in> Stepf a; \<exists>t. (b, t) \<in> Run Stepf as \<and> (t, u) \<in> Run Stepf bs\<rbrakk> \<Longrightarrow> \<exists>t. ((\<lambda>x xa. (x, xa) \<in> Stepf a) OO (\<lambda>x xa. (x, xa) \<in> Run Stepf as)) s t \<and> (t, u) \<in> Run Stepf bs proof (prove)
goal:
No subgoals! proof (state)
this:
(s, u) \<in> Run Stepf ((a # as) @ bs) \<longrightarrow> (\<exists>t. (s, t) \<in> Run Stepf (a # as) \<and> (t, u) \<in> Run Stepf bs)

goal:
No subgoals!