theory Noninterference_Base

lemma sources_unwinding_step:
  "\<lbrakk> s \<approx>(sources (a#as) s u)\<approx> t; s \<sim>schedDomain\<sim> t; confidentiality_u;
     (s,s') \<in> Step a; (t,t') \<in> Step a; reachable s; reachable t \<rbrakk>
     \<Longrightarrow> s' \<approx>(sources as s' u)\<approx> t'" apply (clarsimp simp: sameFor_dom_def sources_Cons) apply (subst (asm) confidentiality_u_def) apply (drule_tac x=a in spec) apply (drule_tac x=ua in spec) apply (drule_tac x=s in spec) apply (drule_tac x=t in spec) apply (fastforce intro: sameFor_sources_dom) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<approx>sources (a # as) s u\<approx> t; s \<sim>schedDomain\<sim> t; confidentiality_u; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s; reachable t\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> t' proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>\<forall>u\<in>\<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))}. s \<sim>u\<sim> t; s \<sim>schedDomain\<sim> t; confidentiality_u; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s; reachable t; ua \<in> sources as s' u\<rbrakk> \<Longrightarrow> s' \<sim>ua\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>\<forall>u\<in>\<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))}. s \<sim>u\<sim> t; s \<sim>schedDomain\<sim> t; \<forall>a u s t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>u\<sim> t'); (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s; reachable t; ua \<in> sources as s' u\<rbrakk> \<Longrightarrow> s' \<sim>ua\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>\<forall>u\<in>\<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))}. s \<sim>u\<sim> t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s; reachable t; ua \<in> sources as s' u; \<forall>u s t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>u\<sim> t')\<rbrakk> \<Longrightarrow> s' \<sim>ua\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>\<forall>u\<in>\<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))}. s \<sim>u\<sim> t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s; reachable t; ua \<in> sources as s' u; \<forall>s t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> ua \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>ua\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>ua\<sim> t')\<rbrakk> \<Longrightarrow> s' \<sim>ua\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>\<forall>u\<in>\<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))}. s \<sim>u\<sim> t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s; reachable t; ua \<in> sources as s' u; \<forall>t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> ua \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>ua\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>ua\<sim> t')\<rbrakk> \<Longrightarrow> s' \<sim>ua\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>\<forall>u\<in>\<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))}. s \<sim>u\<sim> t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s; reachable t; ua \<in> sources as s' u; reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> ua \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>ua\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>ua\<sim> t')\<rbrakk> \<Longrightarrow> s' \<sim>ua\<sim> t' proof (prove)
goal:
No subgoals!