theory Noninterference_Base

lemma sources_eq':
  "confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t
   \<longrightarrow> sources as s u = sources as t u" proof (induct as arbitrary: s t) case Nil show ?case by (simp add: sources_Nil) next case (Cons a as) show ?case apply (clarsimp simp: sources_Cons) apply (rule un_eq) apply (simp only: Union_eq, simp only: UNION_eq[symmetric]) apply (rule Un_eq, clarsimp) apply (metis "Cons.hyps"[rule_format] sched_equiv_preserved reachable_Step) apply (fastforce intro: enabled_Step) apply (fastforce intro: enabled_Step) apply (clarsimp simp: schedIncludesCurrentDom) apply (rule Collect_cong) apply (rule conj_cong, rule refl) apply (rule iff_exI) apply (metis "Cons.hyps"[rule_format] sched_equiv_preserved reachable_Step enabled_Step) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources as s u = sources as t u proof (state)
goal (2 subgoals):
 1. \<And>s t. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources [] s u = sources [] t u
 2. \<And>a as s t. (\<And>s t. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources as s u = sources as t u) \<Longrightarrow> confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources (a # as) s u = sources (a # as) t u proof (state)
this:


goal (2 subgoals):
 1. \<And>s t. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources [] s u = sources [] t u
 2. \<And>a as s t. (\<And>s t. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources as s u = sources as t u) \<Longrightarrow> confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources (a # as) s u = sources (a # as) t u proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources [] s u = sources [] t u proof (state)
this:
confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources [] s u = sources [] t u

goal (1 subgoal):
 1. \<And>a as s t. (\<And>s t. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources as s u = sources as t u) \<Longrightarrow> confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources (a # as) s u = sources (a # as) t u proof (state)
goal (1 subgoal):
 1. \<And>a as s t. (\<And>s t. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources as s u = sources as t u) \<Longrightarrow> confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources (a # as) s u = sources (a # as) t u proof (state)
this:
confidentiality_u \<and> ?s \<sim>schedDomain\<sim> ?t \<and> reachable ?s \<and> reachable ?t \<longrightarrow> sources as ?s u = sources as ?t u

goal (1 subgoal):
 1. \<And>a as s t. (\<And>s t. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources as s u = sources as t u) \<Longrightarrow> confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources (a # as) s u = sources (a # as) t u proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources (a # as) s u = sources (a # as) t u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> \<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))} = \<Union> {sources as s' u |s'. (t, s') \<in> local.Step a} \<union> {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> \<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} = \<Union> {sources as s' u |s'. (t, s') \<in> local.Step a}
 2. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> {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))} = {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> (\<Union>x\<in>{sources as s' u |s'. (s, s') \<in> local.Step a}. x) = (\<Union>x\<in>{sources as s' u |s'. (t, s') \<in> local.Step a}. x)
 2. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> {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))} = {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (4 subgoals):
 1. \<And>s' s'a. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t; (s, s') \<in> local.Step a; (t, s'a) \<in> local.Step a\<rbrakk> \<Longrightarrow> sources as s' u = sources as s'a u
 2. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {sources as s' u |s'. (s, s') \<in> local.Step a}
 3. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {sources as s' u |s'. (t, s') \<in> local.Step a}
 4. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> {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))} = {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {sources as s' u |s'. (s, s') \<in> local.Step a}
 2. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {sources as s' u |s'. (t, s') \<in> local.Step a}
 3. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> {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))} = {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {sources as s' u |s'. (t, s') \<in> local.Step a}
 2. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> {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))} = {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> {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))} = {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} = {w. w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> (w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))) = (w = dom a t \<and> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u))) proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t; w = dom a t\<rbrakk> \<Longrightarrow> (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)) = (\<exists>v. dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u)) proof (prove)
goal (1 subgoal):
 1. \<And>w v. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t; w = dom a t\<rbrakk> \<Longrightarrow> (dom a t \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)) = (dom a t \<leadsto> v \<and> (\<exists>s'. (t, s') \<in> local.Step a \<and> v \<in> sources as s' u)) proof (prove)
goal:
No subgoals! proof (state)
this:
confidentiality_u \<and> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t \<longrightarrow> sources (a # as) s u = sources (a # as) t u

goal:
No subgoals!