kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference_Base

lemma Noninfluence:
  "\<lbrakk> confidentiality_u_weak; output_consistent; integrity_u \<rbrakk>
     \<Longrightarrow> Noninfluence" apply (rule Noninfluence_gen_Noninfluence) 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> Noninfluence 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 Noninfluence_strong:
  "\<lbrakk> confidentiality_u_weak; output_consistent; integrity_u \<rbrakk>
     \<Longrightarrow> Noninfluence_strong" apply (rule Noninfluence_Noninfluence_strong) apply (blast intro: confidentiality_u_weak) apply (blast intro: Noninfluence) done

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

lemma Noninfluence_uwr:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
     \<Longrightarrow> Noninfluence_uwr" apply (rule Noninfluence_gen_Noninfluence_uwr) apply (blast intro: Noninfluence_gen confidentiality_u_weak) done

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

lemma Noninfluence_strong_uwr:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
     \<Longrightarrow> Noninfluence_strong_uwr" apply (rule Noninfluence_uwr_Noninfluence_strong_uwr) apply (blast intro: confidentiality_u_weak) apply (blast intro: Noninfluence_uwr) done

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

lemma sources_Step_2:
  "\<lbrakk> reachable s; (dom a s, u) \<in> policy \<rbrakk>
     \<Longrightarrow> sources [a] s u = {dom a s,u}" by (auto simp: sources_Cons sources_Nil enabled_Step dest: enabled_Step)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; dom a s \<leadsto> u\<rbrakk> \<Longrightarrow> sources [a] s u = {dom a s, u}
theory Noninterference_Base

lemma execution_Nil:
  "reachable s \<Longrightarrow> execution A s [] = {s}" by (simp add: execution_Run)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> execution A s [] = {s}
theory Noninterference_Base

lemma Noninfluence_gen_confidentiality_u_weak:
  "Noninfluence_gen \<Longrightarrow> confidentiality_u_weak" apply (clarsimp simp: Noninfluence_gen_def confidentiality_u_weak_def) apply (drule_tac x=u in spec, drule_tac x="[a]" in spec) apply (drule_tac x=s in spec, drule_tac x="{t}" in spec) apply (simp add: sources_Step_2 sameFor_dom_def uwr_equiv_def Step_def
                   ipurge_Cons ipurge_Nil schedIncludesCurrentDom
            split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Noninfluence_gen \<Longrightarrow> confidentiality_u_weak proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>\<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 \<sim>schedDomain\<sim> t; dom a s \<leadsto> u; s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u; s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; \<forall>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>t\<in>ts. s \<approx>sources [a] s u\<approx> t) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s [a] t (ipurge u [a] ts) u)\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u; s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s \<and> Ball {t} reachable \<longrightarrow> (\<forall>t\<in>{t}. s \<approx>sources [a] s u\<approx> t) \<longrightarrow> (\<forall>t\<in>{t}. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>ta\<in>{t}. uwr_equiv s [a] ta (ipurge u [a] {t}) u)\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninfluence_strong_uwr_confidentiality_u_weak:
  "Noninfluence_strong_uwr \<Longrightarrow> confidentiality_u_weak" apply (clarsimp simp: Noninfluence_strong_uwr_def confidentiality_u_weak_def) apply (drule_tac x=u in spec, drule_tac x="[a]" in spec, drule_tac x="[a]" in spec) apply (drule_tac x=s in spec, drule_tac x=t in spec) apply (simp add: sources_Step_2 sameFor_dom_def uwr_equiv_def Step_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Noninfluence_strong_uwr \<Longrightarrow> confidentiality_u_weak proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>\<forall>u as bs s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u as {s} = ipurge u bs {s} \<longrightarrow> uwr_equiv s as t bs u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u; s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u; s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; \<forall>s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u [a] {s} = ipurge u [a] {s} \<longrightarrow> uwr_equiv s [a] t [a] u\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u; s \<sim>dom a s\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s \<and> reachable t \<longrightarrow> s \<approx>sources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u [a] {s} = ipurge u [a] {s} \<longrightarrow> uwr_equiv s [a] t [a] u\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninfluence_strong_uwr_integrity_u:
  "Noninfluence_strong_uwr \<Longrightarrow> integrity_u" apply (clarsimp simp: Noninfluence_strong_uwr_def integrity_u_def) apply (drule_tac x=u in spec, drule_tac x="[a]" in spec, drule_tac x="[]" in spec) apply (drule_tac x=s in spec, drule_tac x=s in spec) apply (simp add: sources_Step sameFor_dom_def uwr_refl
                   uwr_equiv_def Step_def ipurge_Cons ipurge_Nil
            split: if_splits) apply (simp add: policy_refl) apply (simp add: execution_Nil) apply (blast intro: uwr_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Noninfluence_strong_uwr \<Longrightarrow> integrity_u proof (prove)
goal (1 subgoal):
 1. \<And>a u s s'. \<lbrakk>\<forall>u as bs s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u as {s} = ipurge u bs {s} \<longrightarrow> uwr_equiv s as t bs u; reachable s; (dom a s, u) \<notin> policy; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> s' proof (prove)
goal (1 subgoal):
 1. \<And>a u s s'. \<lbrakk>reachable s; (dom a s, u) \<notin> policy; (s, s') \<in> local.Step a; \<forall>s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u [a] {s} = ipurge u [] {s} \<longrightarrow> uwr_equiv s [a] t [] u\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> s' proof (prove)
goal (1 subgoal):
 1. \<And>a u s s'. \<lbrakk>reachable s; (dom a s, u) \<notin> policy; (s, s') \<in> local.Step a; reachable s \<and> reachable s \<longrightarrow> s \<approx>sources [a] s u\<approx> s \<longrightarrow> s \<sim>schedDomain\<sim> s \<longrightarrow> ipurge u [a] {s} = ipurge u [] {s} \<longrightarrow> uwr_equiv s [a] s [] u\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> s' proof (prove)
goal (2 subgoals):
 1. \<And>a u s s'. \<lbrakk>reachable s; (u, u) \<notin> policy; s' \<in> execution A s [a]; dom a s = u\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> s'
 2. \<And>a u s s'. \<lbrakk>reachable s; (dom a s, u) \<notin> policy; s' \<in> execution A s [a]; dom a s \<noteq> u; \<forall>s' t'. s' \<in> execution A s [a] \<and> t' \<in> execution A s [] \<longrightarrow> s' \<sim>u\<sim> t'\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> s' proof (prove)
goal (1 subgoal):
 1. \<And>a u s s'. \<lbrakk>reachable s; (dom a s, u) \<notin> policy; s' \<in> execution A s [a]; dom a s \<noteq> u; \<forall>s' t'. s' \<in> execution A s [a] \<and> t' \<in> execution A s [] \<longrightarrow> s' \<sim>u\<sim> t'\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> s' proof (prove)
goal (1 subgoal):
 1. \<And>a u s s'. \<lbrakk>reachable s; (dom a s, u) \<notin> policy; s' \<in> execution A s [a]; dom a s \<noteq> u; \<forall>s'. s' \<in> execution A s [a] \<longrightarrow> s' \<sim>u\<sim> s\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> s' proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninfluence_gen_equiv_Noninfluence_strong_uwr:
  "Noninfluence_gen = Noninfluence_strong_uwr" apply (rule iffI) apply (rule Noninfluence_strong_uwr) apply (erule Noninfluence_gen_confidentiality_u_weak) apply (erule Noninfluence_gen_integrity_u) apply (rule Noninfluence_gen) apply (rule confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_integrity_u)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Noninfluence_gen = Noninfluence_strong_uwr proof (prove)
goal (2 subgoals):
 1. Noninfluence_gen \<Longrightarrow> Noninfluence_strong_uwr
 2. Noninfluence_strong_uwr \<Longrightarrow> Noninfluence_gen proof (prove)
goal (3 subgoals):
 1. Noninfluence_gen \<Longrightarrow> confidentiality_u_weak
 2. Noninfluence_gen \<Longrightarrow> integrity_u
 3. Noninfluence_strong_uwr \<Longrightarrow> Noninfluence_gen proof (prove)
goal (2 subgoals):
 1. Noninfluence_gen \<Longrightarrow> integrity_u
 2. Noninfluence_strong_uwr \<Longrightarrow> Noninfluence_gen proof (prove)
goal (1 subgoal):
 1. Noninfluence_strong_uwr \<Longrightarrow> Noninfluence_gen proof (prove)
goal (2 subgoals):
 1. Noninfluence_strong_uwr \<Longrightarrow> confidentiality_u
 2. Noninfluence_strong_uwr \<Longrightarrow> integrity_u proof (prove)
goal (3 subgoals):
 1. Noninfluence_strong_uwr \<Longrightarrow> confidentiality_u_weak
 2. Noninfluence_strong_uwr \<Longrightarrow> integrity_u
 3. Noninfluence_strong_uwr \<Longrightarrow> integrity_u proof (prove)
goal (2 subgoals):
 1. Noninfluence_strong_uwr \<Longrightarrow> integrity_u
 2. Noninfluence_strong_uwr \<Longrightarrow> integrity_u proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Alternatives

lemma in_xources_ConsD:
  "x \<in> (xources (a # as) s u)
   \<Longrightarrow> (\<forall>s'. (s,s') \<in> Step a \<longrightarrow> x \<in> xources as s' u) \<or>
       (x = dom a s \<and> (\<forall>s'. (s,s') \<in> Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u)))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> xources (a # as) s u \<Longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> x \<in> xources as s' u) \<or> x = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))
theory Noninterference_Base_Alternatives

lemma in_xources_ConsI2:
  "\<lbrakk> x = dom a s; \<forall>s'. (s,s') \<in> Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u) \<rbrakk>
     \<Longrightarrow> x \<in> xources (a # as) s u" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = dom a s; \<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u)\<rbrakk> \<Longrightarrow> x \<in> xources (a # as) s u
theory Noninterference_Base_Alternatives

lemma xources_subset_xources_Cons:
  "\<Inter>{xources as s' u | s'. (s,s') \<in> Step a} \<subseteq> xources (a # as) s u" by (fastforce simp: xources_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Inter> {xources as s' u |s'. (s, s') \<in> local.Step a} \<subseteq> xources (a # as) s u
theory Noninterference_Base_Alternatives

lemma xpurge_Nil:
  "xpurge u [] ss = []" by (auto simp: xpurge_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpurge u [] ss = []
theory Noninterference_Base_Alternatives

lemma ipurgx_Nil:
  "ipurgx u [] ss = []" by (auto simp: ipurgx_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ipurgx u [] ss = []
theory Noninterference_Base_Alternatives

lemma xpurgx_Nil:
  "xpurgx u [] ss = []" by (auto simp: xpurgx_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpurgx u [] ss = []
theory Noninterference_Base_Alternatives

lemma xpurge_Cons:
  "xpurge u (a # as) ss = (if \<exists>s \<in> ss. dom a s \<in> xources (a # as) s u
                           then a # xpurge u as (\<Union>s\<in>ss. {s'. (s,s') \<in> Step a})
                           else xpurge u as ss)" by (auto simp: xpurge_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpurge u (a # as) ss = (if \<exists>s\<in>ss. dom a s \<in> xources (a # as) s u then a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) else xpurge u as ss)
theory Noninterference_Base_Alternatives

lemma ipurgx_Cons:
  "ipurgx u (a # as) ss = (if (\<forall>s\<in>ss. dom a s \<in> sources (a # as) s u)
                           then a # ipurgx u as (\<Union>s \<in> ss. {s'. (s,s') \<in> Step a})
                           else ipurgx u as ss)" by (auto simp: ipurgx_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ipurgx u (a # as) ss = (if \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u then a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) else ipurgx u as ss)
theory Noninterference_Base_Alternatives

lemma xpurgx_Cons:
  "xpurgx u (a # as) ss = (if (\<forall>s\<in>ss. dom a s \<in> xources (a # as) s u)
                           then a # xpurgx u as (\<Union>s\<in>ss. {s'. (s,s') \<in> Step a})
                           else xpurgx u as ss)" by (auto simp: xpurgx_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpurgx u (a # as) ss = (if \<forall>s\<in>ss. dom a s \<in> xources (a # as) s u then a # xpurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) else xpurgx u as ss)
theory Noninterference_Base_Alternatives

lemma xpurge_ipurge':
  "confidentiality_u
   \<Longrightarrow> (\<forall>s\<in>ss. reachable s) \<longrightarrow> xpurge u as ss = ipurge u as ss" apply (induct as arbitrary: ss) apply (simp add: xpurge_Nil ipurge_Nil) apply (clarsimp simp: ipurge_Cons xpurge_Cons xources_sources[rule_format] intro: reachable_Step
         | safe)+ apply (drule_tac x="\<Union>s\<in>ss. {s'. (s,s') \<in> Step a}" in meta_spec) apply (fastforce intro: reachable_Step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> Ball ss reachable \<longrightarrow> xpurge u as ss = ipurge u as ss proof (prove)
goal (2 subgoals):
 1. \<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<longrightarrow> xpurge u [] ss = ipurge u [] ss
 2. \<And>a as ss. \<lbrakk>\<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<longrightarrow> xpurge u as ss = ipurge u as ss; confidentiality_u\<rbrakk> \<Longrightarrow> Ball ss reachable \<longrightarrow> xpurge u (a # as) ss = ipurge u (a # as) ss proof (prove)
goal (1 subgoal):
 1. \<And>a as ss. \<lbrakk>\<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<longrightarrow> xpurge u as ss = ipurge u as ss; confidentiality_u\<rbrakk> \<Longrightarrow> Ball ss reachable \<longrightarrow> xpurge u (a # as) ss = ipurge u (a # as) ss proof (prove)
goal (1 subgoal):
 1. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<longrightarrow> xpurge u as ss = ipurge u as ss; confidentiality_u; s \<in> ss; dom a s \<in> sources (a # as) s u; Ball ss reachable\<rbrakk> \<Longrightarrow> xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge 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>confidentiality_u; s \<in> ss; dom a s \<in> sources (a # as) s u; Ball ss reachable; Ball (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) reachable \<longrightarrow> xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Alternatives

lemma xpurge_ipurge:
  "\<lbrakk> confidentiality_u; reachable s \<rbrakk>
     \<Longrightarrow> xpurge u as {s} = ipurge u as {s}" by (subst xpurge_ipurge', auto)

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

lemma ipurgx_ipurge:
  "\<lbrakk> confidentiality_u; reachable s \<rbrakk>
     \<Longrightarrow> ipurgx u as {s} = ipurge u as {s}" apply (subst ipurgx_xpurge', (simp add: uwr_refl)+) apply (subst xpurge_ipurge', auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> ipurgx u as {s} = ipurge u as {s} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> xpurge u as {s} = ipurge u as {s} proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Alternatives

lemma xpurgx_ipurge:
  "\<lbrakk> confidentiality_u; reachable s \<rbrakk>
     \<Longrightarrow> xpurgx u as {s} = ipurge u as {s}" apply (subst ipurgx_xpurgx'[rule_format, THEN sym], simp+) apply (subst ipurgx_xpurge', (simp add: uwr_refl)+) apply (subst xpurge_ipurge', auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> xpurgx u as {s} = ipurge u as {s} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> ipurgx u as {s} = ipurge u as {s} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> xpurge u as {s} = ipurge u as {s} proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Alternatives

lemma xNoninfluence_strong_uwr_xources_ipurge_Noninfluence_strong_uwr:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
     \<Longrightarrow> xNoninfluence_strong_uwr_xources_ipurge = Noninfluence_strong_uwr" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_ipurge_def Noninfluence_strong_uwr_def) apply (frule (1) confidentiality_u_weak) apply (simp add: xources_sources) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow> xNoninfluence_strong_uwr_xources_ipurge = Noninfluence_strong_uwr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow> (\<forall>u as bs s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>xources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u as {s} = ipurge u bs {s} \<longrightarrow> uwr_equiv s as t bs u) = (\<forall>u as bs s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u as {s} = ipurge u bs {s} \<longrightarrow> uwr_equiv s as t bs u) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u; confidentiality_u\<rbrakk> \<Longrightarrow> (\<forall>u as bs s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>xources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u as {s} = ipurge u bs {s} \<longrightarrow> uwr_equiv s as t bs u) = (\<forall>u as bs s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u as {s} = ipurge u bs {s} \<longrightarrow> uwr_equiv s as t bs u) proof (prove)
goal:
No subgoals!