kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference_Base

lemma Noninfluence_uwr_Noninfluence:
  "\<lbrakk> output_consistent; Noninfluence_uwr \<rbrakk> \<Longrightarrow> Noninfluence" apply (clarsimp simp: Noninfluence_def) apply (erule obs_equivI) apply (auto simp: Noninfluence_uwr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_consistent; Noninfluence_uwr\<rbrakk> \<Longrightarrow> Noninfluence proof (prove)
goal (1 subgoal):
 1. \<And>u as s t. \<lbrakk>output_consistent; Noninfluence_uwr; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t\<rbrakk> \<Longrightarrow> obs_equiv s as t (ipurge u as {t}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s t. \<lbrakk>Noninfluence_uwr; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t\<rbrakk> \<Longrightarrow> uwr_equiv s as t (ipurge u as {t}) u proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninfluence_strong_uwr_Noninfluence_strong:
  "\<lbrakk> output_consistent; Noninfluence_strong_uwr \<rbrakk> \<Longrightarrow> Noninfluence_strong" apply (clarsimp simp: Noninfluence_strong_def) apply (erule obs_equivI) apply (auto simp: Noninfluence_strong_uwr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_consistent; Noninfluence_strong_uwr\<rbrakk> \<Longrightarrow> Noninfluence_strong proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>output_consistent; Noninfluence_strong_uwr; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>Noninfluence_strong_uwr; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}\<rbrakk> \<Longrightarrow> uwr_equiv s as t bs u proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma sched_equiv_preserved_left:
  "\<lbrakk> integrity_u; s \<sim>schedDomain\<sim> t;
     dom a s \<noteq> schedDomain; (s,s') \<in> Step a; reachable s \<rbrakk>
     \<Longrightarrow> s' \<sim>schedDomain\<sim> t" by (blast intro: integrity_uD schedNotGlobalChannel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; s \<sim>schedDomain\<sim> t; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a; reachable s\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
theory Noninterference_Base

lemma Noninfluence_gen_Noninterference:
  "\<lbrakk> output_consistent; Noninfluence_gen \<rbrakk> \<Longrightarrow> Noninterference" apply (clarsimp simp: Noninterference_def Noninfluence_gen_def) apply (erule_tac x=u in allE) apply (erule_tac x=as in allE) apply (erule_tac x=s in allE) apply (erule_tac x="{s}" in allE) apply (clarsimp simp: sameFor_dom_def uwr_refl) apply (blast intro: obs_equivI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_consistent; Noninfluence_gen\<rbrakk> \<Longrightarrow> Noninterference proof (prove)
goal (1 subgoal):
 1. \<And>u as s. \<lbrakk>output_consistent; \<forall>u as s ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u); reachable s\<rbrakk> \<Longrightarrow> obs_equiv s as s (ipurge u as {s}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s. \<lbrakk>output_consistent; reachable s; \<forall>as s ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)\<rbrakk> \<Longrightarrow> obs_equiv s as s (ipurge u as {s}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s. \<lbrakk>output_consistent; reachable s; \<forall>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)\<rbrakk> \<Longrightarrow> obs_equiv s as s (ipurge u as {s}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s. \<lbrakk>output_consistent; reachable s; \<forall>ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)\<rbrakk> \<Longrightarrow> obs_equiv s as s (ipurge u as {s}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s. \<lbrakk>output_consistent; reachable s; reachable s \<and> Ball {s} reachable \<longrightarrow> (\<forall>t\<in>{s}. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>{s}. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>{s}. uwr_equiv s as t (ipurge u as {s}) u)\<rbrakk> \<Longrightarrow> obs_equiv s as s (ipurge u as {s}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s. \<lbrakk>output_consistent; reachable s; uwr_equiv s as s (ipurge u as {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s as s (ipurge u as {s}) u proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninfluence_gen_Noninfluence:
  "\<lbrakk> output_consistent; Noninfluence_gen \<rbrakk> \<Longrightarrow> Noninfluence" apply (clarsimp simp: Noninfluence_def Noninfluence_gen_def) apply (erule_tac x=u in allE) apply (erule_tac x=as in allE) apply (erule_tac x=s in allE) apply (erule_tac x="{t}" in allE) apply (blast intro: obs_equivI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_consistent; Noninfluence_gen\<rbrakk> \<Longrightarrow> Noninfluence proof (prove)
goal (1 subgoal):
 1. \<And>u as s t. \<lbrakk>output_consistent; \<forall>u as s ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u); reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t\<rbrakk> \<Longrightarrow> obs_equiv s as t (ipurge u as {t}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s t. \<lbrakk>output_consistent; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; \<forall>as s ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)\<rbrakk> \<Longrightarrow> obs_equiv s as t (ipurge u as {t}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s t. \<lbrakk>output_consistent; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; \<forall>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)\<rbrakk> \<Longrightarrow> obs_equiv s as t (ipurge u as {t}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s t. \<lbrakk>output_consistent; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; \<forall>ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)\<rbrakk> \<Longrightarrow> obs_equiv s as t (ipurge u as {t}) u proof (prove)
goal (1 subgoal):
 1. \<And>u as s t. \<lbrakk>output_consistent; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; reachable s \<and> Ball {t} reachable \<longrightarrow> (\<forall>t\<in>{t}. s \<approx>sources as s u\<approx> t) \<longrightarrow> (\<forall>t\<in>{t}. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>ta\<in>{t}. uwr_equiv s as ta (ipurge u as {t}) u)\<rbrakk> \<Longrightarrow> obs_equiv s as t (ipurge u as {t}) u proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninfluence_gen_Noninfluence_uwr:
  "Noninfluence_gen \<Longrightarrow> Noninfluence_uwr" by (clarsimp simp: Noninfluence_uwr_def Noninfluence_gen_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Noninfluence_gen \<Longrightarrow> Noninfluence_uwr
theory Noninterference_Base

lemma Noninfluence_gen_Noninterference_strong:
  "\<lbrakk> output_consistent; Noninfluence_gen \<rbrakk> \<Longrightarrow> Noninterference_strong" apply (rule Noninterference_Noninterference_strong) apply (blast intro: Noninfluence_gen_Noninterference) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_consistent; Noninfluence_gen\<rbrakk> \<Longrightarrow> Noninterference_strong proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_consistent; Noninfluence_gen\<rbrakk> \<Longrightarrow> Noninterference proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma sources_refl:
  "reachable s \<Longrightarrow> u \<in> sources as s u" apply (induct as arbitrary: s) apply (simp add: sources_Nil) apply (simp add: sources_Cons) apply (frule_tac a=a in enabled_Step) apply (auto simp: reachable_Step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> u \<in> sources as s u proof (prove)
goal (2 subgoals):
 1. \<And>s. reachable s \<Longrightarrow> u \<in> sources [] s u
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<Longrightarrow> u \<in> sources as s u; reachable s\<rbrakk> \<Longrightarrow> u \<in> sources (a # as) s u proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<Longrightarrow> u \<in> sources as s u; reachable s\<rbrakk> \<Longrightarrow> u \<in> sources (a # as) s u proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<Longrightarrow> u \<in> sources as s u; reachable s\<rbrakk> \<Longrightarrow> (\<exists>x. (\<exists>s'. x = sources as s' u \<and> (s, s') \<in> local.Step a) \<and> u \<in> x) \<or> u = 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)) proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<Longrightarrow> u \<in> sources as s u; reachable s; \<exists>s'. (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (\<exists>x. (\<exists>s'. x = sources as s' u \<and> (s, s') \<in> local.Step a) \<and> u \<in> x) \<or> u = 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)) proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma schedDomain_in_sources_Cons:
  "\<lbrakk> reachable s; dom a s = schedDomain \<rbrakk>
     \<Longrightarrow> dom a s \<in> sources (a#as) s u" apply (unfold sources_Cons) apply (erule ssubst) apply (rule UnI2) apply (clarsimp) apply (rule_tac x=u in exI) apply (safe) apply (rule schedFlowsToAll) apply (frule_tac a=a in enabled_Step) apply (fastforce dest: sources_refl reachable_Step) done

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

lemma sources_eq:
  "\<lbrakk> confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t \<rbrakk>
     \<Longrightarrow> sources as s u = sources as t u" by (rule sources_eq'[rule_format], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; s \<sim>schedDomain\<sim> t; reachable s; reachable t\<rbrakk> \<Longrightarrow> sources as s u = sources as t u
theory Noninterference_Base

lemma ipurge_eq:
  "\<lbrakk> s \<sim>schedDomain\<sim> t; reachable s; reachable t; confidentiality_u \<rbrakk>
     \<Longrightarrow> ipurge u as {s} = ipurge u as {t}" by (rule ipurge_eq'[rule_format], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<sim>schedDomain\<sim> t; reachable s; reachable t; confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as {s} = ipurge u as {t}
theory Noninterference_Base

lemma dom_in_sources_Cons:
  "\<lbrakk> confidentiality_u; reachable s; reachable t; s \<approx>(sources (a#as) s u)\<approx> t;
     s \<sim>schedDomain\<sim> t; (dom a s \<in> sources (a#as) s u) \<rbrakk>
     \<Longrightarrow> (dom a t \<in> sources (a#as) t u)" apply (subgoal_tac "dom a s = dom a t") apply (fastforce dest: sources_eq) apply (blast intro: schedIncludesCurrentDom) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources (a # as) s u\<approx> t; s \<sim>schedDomain\<sim> t; dom a s \<in> sources (a # as) s u\<rbrakk> \<Longrightarrow> dom a t \<in> sources (a # as) t u proof (prove)
goal (2 subgoals):
 1. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources (a # as) s u\<approx> t; s \<sim>schedDomain\<sim> t; dom a s \<in> sources (a # as) s u; dom a s = dom a t\<rbrakk> \<Longrightarrow> dom a t \<in> sources (a # as) t u
 2. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources (a # as) s u\<approx> t; s \<sim>schedDomain\<sim> t; dom a s \<in> sources (a # as) s u\<rbrakk> \<Longrightarrow> dom a s = dom a t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources (a # as) s u\<approx> t; s \<sim>schedDomain\<sim> t; dom a s \<in> sources (a # as) s u\<rbrakk> \<Longrightarrow> dom a s = dom a t proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma uwr_equiv_Cons_bothI:
  "\<lbrakk> reachable s; reachable t;
      \<forall>s' t'. (s,s') \<in> Step a \<and> (t,t') \<in> Step b \<longrightarrow> uwr_equiv s' as t' bs u \<rbrakk>
     \<Longrightarrow> uwr_equiv s (a # as) t (b # bs) u" by (fastforce simp: uwr_equiv_def execution_Run reachable_Step)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; reachable t; \<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step b \<longrightarrow> uwr_equiv s' as t' bs u\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (b # bs) u
theory Noninterference_Base

lemma notin_policyI':
  "\<lbrakk> reachable s; dom a s \<notin> sources (a # list) s u; (s,s') \<in> Step a; ua \<in> sources list s' u \<rbrakk>
     \<Longrightarrow> (dom a s,ua) \<notin> policy" apply (rule notin_policyI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; dom a s \<notin> sources (a # list) s u; (s, s') \<in> local.Step a; ua \<in> sources list s' u\<rbrakk> \<Longrightarrow> (dom a s, ua) \<notin> policy proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; dom a s \<notin> sources (a # list) s u; (s, s') \<in> local.Step a; ua \<in> sources list s' u\<rbrakk> \<Longrightarrow> dom a s \<notin> sources (a # ?list) s ?u
 2. \<lbrakk>reachable s; dom a s \<notin> sources (a # list) s u; (s, s') \<in> local.Step a; ua \<in> sources list s' u\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> local.Step a \<and> ua \<in> sources ?list s' ?u proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma sources_eq_Step:
  "\<lbrakk> integrity_u; confidentiality_u; reachable s; (s,s') \<in> Step a; dom a s \<noteq> schedDomain \<rbrakk>
     \<Longrightarrow> (sources as s' u) = (sources as s u)" apply (rule sources_eq, simp+) apply (rule_tac t=s and s=s and a=a in sched_equiv_preserved_left) apply (auto simp add: uwr_refl reachable_Step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> sources as s' u = sources as s u proof (prove)
goal (3 subgoals):
 1. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> s
 2. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> reachable s'
 3. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> reachable s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> integrity_u
 2. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s
 3. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> dom a s \<noteq> schedDomain
 4. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> (s, s') \<in> local.Step a
 5. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> reachable s
 6. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> reachable s'
 7. \<lbrakk>integrity_u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> reachable s proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma sources_equiv_preserved_left:
  "\<lbrakk> integrity_u; confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t;
     dom a s \<notin> sources (a#as) s u; s \<approx>sources (a#as) s u\<approx> t; (s,s') \<in> Step a;
     dom a s \<noteq> schedDomain \<rbrakk>
     \<Longrightarrow> s' \<approx>sources as s' u\<approx> t" apply (clarsimp simp: sameFor_dom_def) apply (rename_tac v) apply (case_tac "(dom a s, v) \<in> policy") apply (fastforce simp: sources_Cons) apply (fastforce dest: integrity_uD simp: sources_Cons) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<notin> sources (a # as) s u; s \<approx>sources (a # as) s u\<approx> t; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> t proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>integrity_u; confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<notin> sources (a # as) s u; \<forall>u\<in>sources (a # as) s u. s \<sim>u\<sim> t; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; ua \<in> sources as s' u\<rbrakk> \<Longrightarrow> s' \<sim>ua\<sim> t proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>integrity_u; confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<notin> sources (a # as) s u; \<forall>u\<in>sources (a # as) s u. s \<sim>u\<sim> t; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> s' \<sim>v\<sim> t proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>integrity_u; confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<notin> sources (a # as) s u; \<forall>u\<in>sources (a # as) s u. s \<sim>u\<sim> t; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; v \<in> sources as s' u; dom a s \<leadsto> v\<rbrakk> \<Longrightarrow> s' \<sim>v\<sim> t
 2. \<And>v. \<lbrakk>integrity_u; confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<notin> sources (a # as) s u; \<forall>u\<in>sources (a # as) s u. s \<sim>u\<sim> t; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; v \<in> sources as s' u; (dom a s, v) \<notin> policy\<rbrakk> \<Longrightarrow> s' \<sim>v\<sim> t proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>integrity_u; confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<notin> sources (a # as) s u; \<forall>u\<in>sources (a # as) s u. s \<sim>u\<sim> t; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; v \<in> sources as s' u; (dom a s, v) \<notin> policy\<rbrakk> \<Longrightarrow> s' \<sim>v\<sim> t proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninterference:
  "\<lbrakk> confidentiality_u_weak; output_consistent; integrity_u \<rbrakk>
     \<Longrightarrow> Noninterference" apply (rule Noninfluence_gen_Noninterference) apply assumption apply (blast intro: Noninfluence_gen confidentiality_u_weak) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow> Noninterference proof (prove)
goal (2 subgoals):
 1. \<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow> output_consistent
 2. \<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow> Noninfluence_gen proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow> Noninfluence_gen proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninterference_strong:
  "\<lbrakk> confidentiality_u_weak; output_consistent; integrity_u \<rbrakk>
     \<Longrightarrow> Noninterference_strong" apply (rule Noninfluence_gen_Noninterference_strong) apply assumption apply (blast intro: Noninfluence_gen confidentiality_u_weak) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow> Noninterference_strong proof (prove)
goal (2 subgoals):
 1. \<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow> output_consistent
 2. \<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow> Noninfluence_gen proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; output_consistent; integrity_u\<rbrakk> \<Longrightarrow> Noninfluence_gen proof (prove)
goal:
No subgoals!