theory Noninterference_Base_Alternatives

lemma ipurgx_xpurgx':
  "confidentiality_u \<Longrightarrow> (\<forall>s\<in>ss. reachable s) \<longrightarrow> ipurgx u as ss = xpurgx u as ss" apply (induct as arbitrary: ss) apply (simp add: ipurgx_Nil xpurgx_Nil) apply (clarsimp simp: xpurgx_Cons ipurgx_Cons | safe)+ apply (drule_tac x="\<Union>s\<in>ss. {s'. (s,s') \<in> Step a}" in meta_spec) apply (fastforce intro: reachable_Step) apply (simp add: xources_sources) apply (simp add: xources_sources) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss proof (prove)
goal (2 subgoals):
 1. \<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<longrightarrow> ipurgx u [] ss = xpurgx u [] ss
 2. \<And>a as ss. \<lbrakk>\<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u\<rbrakk> \<Longrightarrow> Ball ss reachable \<longrightarrow> ipurgx u (a # as) ss = xpurgx u (a # as) ss proof (prove)
goal (1 subgoal):
 1. \<And>a as ss. \<lbrakk>\<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u\<rbrakk> \<Longrightarrow> Ball ss reachable \<longrightarrow> ipurgx u (a # as) ss = xpurgx u (a # as) ss proof (prove)
goal (3 subgoals):
 1. \<And>a as ss. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<in> xources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 2. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<notin> xources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurgx u as ss
 3. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<in> xources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> xpurgx u as ss = a # xpurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (3 subgoals):
 1. \<And>a as ss. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<in> xources (a # as) s u; Ball ss reachable; Ball (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) reachable \<longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 2. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<notin> xources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurgx u as ss
 3. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<in> xources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> xpurgx u as ss = a # xpurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (2 subgoals):
 1. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<notin> xources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurgx u as ss
 2. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<in> xources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> xpurgx u as ss = a # xpurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (1 subgoal):
 1. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> ipurgx u as ss = xpurgx u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<in> xources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> xpurgx u as ss = a # xpurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal:
No subgoals!