theory Noninterference_Base_Refinement

lemma xources_subset:
  "abs.confidentiality_u \<Longrightarrow> abs.xources as s u \<subseteq> conc.xources as s u" apply(induct as arbitrary: s u) apply(simp add: abs.xources.xources_Nil conc.xources.xources_Nil) apply(simp add: abs.xources.xources_Cons conc.xources.xources_Cons) apply(rule conjI) apply(rule subsetI) apply(rule UnI1) apply(blast dest: subsetD[OF Step]) apply(rule subsetI) apply(rule UnI2) apply(blast dest: subsetD[OF Step]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs.confidentiality_u \<Longrightarrow> abs.xources as s u \<subseteq> conc.xources as s u proof (prove)
goal (2 subgoals):
 1. \<And>s u. abs.confidentiality_u \<Longrightarrow> abs.xources [] s u \<subseteq> conc.xources [] s u
 2. \<And>a as s u. \<lbrakk>\<And>s u. abs.confidentiality_u \<Longrightarrow> abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u\<rbrakk> \<Longrightarrow> abs.xources (a # as) s u \<subseteq> conc.xources (a # as) s u proof (prove)
goal (1 subgoal):
 1. \<And>a as s u. \<lbrakk>\<And>s u. abs.confidentiality_u \<Longrightarrow> abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u\<rbrakk> \<Longrightarrow> abs.xources (a # as) s u \<subseteq> conc.xources (a # as) s u proof (prove)
goal (1 subgoal):
 1. \<And>a as s u. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u\<rbrakk> \<Longrightarrow> \<Inter> {abs.xources as s' u |s'. (s, s') \<in> abs.Step a} \<subseteq> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))} \<and> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> abs.xources as s' u))} \<subseteq> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s u. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u\<rbrakk> \<Longrightarrow> \<Inter> {abs.xources as s' u |s'. (s, s') \<in> abs.Step a} \<subseteq> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))}
 2. \<And>a as s u. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> abs.xources as s' u))} \<subseteq> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s u x. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u; x \<in> \<Inter> {abs.xources as s' u |s'. (s, s') \<in> abs.Step a}\<rbrakk> \<Longrightarrow> x \<in> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))}
 2. \<And>a as s u. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> abs.xources as s' u))} \<subseteq> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s u x. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u; x \<in> \<Inter> {abs.xources as s' u |s'. (s, s') \<in> abs.Step a}\<rbrakk> \<Longrightarrow> x \<in> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a}
 2. \<And>a as s u. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> abs.xources as s' u))} \<subseteq> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<And>a as s u. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> abs.xources as s' u))} \<subseteq> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<And>a as s u x. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u; x \<in> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> abs.xources as s' u))}\<rbrakk> \<Longrightarrow> x \<in> \<Inter> {conc.xources as s' u |s'. (s, s') \<in> conc.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<And>a as s u x. \<lbrakk>\<And>s u. abs.xources as s u \<subseteq> conc.xources as s u; abs.confidentiality_u; x \<in> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> abs.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> abs.xources as s' u))}\<rbrakk> \<Longrightarrow> x \<in> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> conc.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> conc.xources as s' u))} proof (prove)
goal:
No subgoals!