kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference_Base_Alternatives

lemma xNoninfluence_strong_uwr_sources_xpurge_Noninfluence_strong_uwr:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
     \<Longrightarrow> xNoninfluence_strong_uwr_sources_xpurge = Noninfluence_strong_uwr" apply (clarsimp simp: xNoninfluence_strong_uwr_sources_xpurge_def Noninfluence_strong_uwr_def) apply (frule (1) confidentiality_u_weak) apply (simp add: xpurge_ipurge) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow> xNoninfluence_strong_uwr_sources_xpurge = 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>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> xpurge u as {s} = xpurge 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>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> xpurge u as {s} = xpurge 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!
theory Noninterference_Base_Alternatives

lemma xNoninfluence_strong_uwr_xources_xpurge_Noninfluence_strong_uwr:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
    \<Longrightarrow> xNoninfluence_strong_uwr_xources_xpurge = Noninfluence_strong_uwr" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_xpurge_def Noninfluence_strong_uwr_def) apply (frule (1) confidentiality_u_weak) apply (simp add: xources_sources xpurge_ipurge) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow> xNoninfluence_strong_uwr_xources_xpurge = 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> xpurge u as {s} = xpurge 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> xpurge u as {s} = xpurge 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!
theory Noninterference_Base_Alternatives

lemma xNoninfluence_strong_uwr_sources_xpurgx_Noninfluence_strong_uwr:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
     \<Longrightarrow> xNoninfluence_strong_uwr_sources_xpurgx = Noninfluence_strong_uwr" apply (clarsimp simp: xNoninfluence_strong_uwr_sources_xpurgx_def Noninfluence_strong_uwr_def) apply (frule (1) confidentiality_u_weak) apply (simp add: xpurgx_ipurge) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow> xNoninfluence_strong_uwr_sources_xpurgx = 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>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> xpurgx u as {s} = xpurgx 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>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> xpurgx u as {s} = xpurgx 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!
theory Noninterference_Base_Alternatives

lemma xNoninfluence_strong_uwr_xources_xpurgx_Noninfluence_strong_uwr:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
     \<Longrightarrow> xNoninfluence_strong_uwr_xources_xpurgx = Noninfluence_strong_uwr" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_xpurgx_def Noninfluence_strong_uwr_def) apply (frule (1) confidentiality_u_weak) apply (simp add: xpurgx_ipurge xources_sources) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow> xNoninfluence_strong_uwr_xources_xpurgx = 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> xpurgx u as {s} = xpurgx 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> xpurgx u as {s} = xpurgx 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!
theory Noninterference_Base_Alternatives

lemma Noninfluence_strong_uwr_pg_Noninfluence_strong_uwr:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
     \<Longrightarrow> Noninfluence_strong_uwr_pg = Noninfluence_strong_uwr" apply (clarsimp simp: Noninfluence_strong_uwr_pg_def Noninfluence_strong_uwr_def) apply (frule (1) confidentiality_u_weak) apply (simp add: ipurge_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow> Noninfluence_strong_uwr_pg = 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>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u as {s} = ipurge u bs {t} \<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>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurge u as {s} = ipurge u bs {t} \<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!
theory Noninterference_Base_Alternatives

lemma xources_Step:
  "\<lbrakk> reachable s; (dom a s, u) \<notin> policy \<rbrakk> \<Longrightarrow> xources [a] s u = {u}" by (auto simp: xources_Cons xources_Nil enabled_Step dest: enabled_Step)

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

lemma xources_Step_2:
  "\<lbrakk> reachable s; (dom a s, u) \<in> policy \<rbrakk> \<Longrightarrow> xources [a] s u = {dom a s,u}" by (auto simp: xources_Cons xources_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> xources [a] s u = {dom a s, u}
theory Noninterference_Base_Alternatives

lemma xNoninfluence_strong_uwr_xources_ipurge_confidentiality_u_weak:
  "xNoninfluence_strong_uwr_xources_ipurge \<Longrightarrow> confidentiality_u_weak" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_ipurge_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: xources_Step_2 sameFor_dom_def uwr_equiv_def Step_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xNoninfluence_strong_uwr_xources_ipurge \<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>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; 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>xources [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>xources [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_Alternatives

lemma xNoninfluence_strong_uwr_sources_xpurge_confidentiality_u_weak:
  "xNoninfluence_strong_uwr_sources_xpurge \<Longrightarrow> confidentiality_u_weak" apply (clarsimp simp: xNoninfluence_strong_uwr_sources_xpurge_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. xNoninfluence_strong_uwr_sources_xpurge \<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> xpurge u as {s} = xpurge 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> xpurge u [a] {s} = xpurge 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> xpurge u [a] {s} = xpurge 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_Alternatives

lemma xNoninfluence_strong_uwr_xources_xpurge_confidentiality_u_weak:
  "xNoninfluence_strong_uwr_xources_xpurge \<Longrightarrow> confidentiality_u_weak" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_xpurge_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: xources_Step_2 sameFor_dom_def uwr_equiv_def Step_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xNoninfluence_strong_uwr_xources_xpurge \<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>xources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> xpurge u as {s} = xpurge 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>xources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> xpurge u [a] {s} = xpurge 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>xources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> xpurge u [a] {s} = xpurge 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_Alternatives

lemma xNoninfluence_strong_uwr_sources_ipurgx_confidentiality_u_weak:
  "xNoninfluence_strong_uwr_sources_ipurgx \<Longrightarrow> confidentiality_u_weak" apply (clarsimp simp: xNoninfluence_strong_uwr_sources_ipurgx_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. xNoninfluence_strong_uwr_sources_ipurgx \<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> ipurgx u as {s} = ipurgx 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> ipurgx u [a] {s} = ipurgx 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> ipurgx u [a] {s} = ipurgx 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_Alternatives

lemma xNoninfluence_strong_uwr_xources_ipurgx_confidentiality_u_weak:
  "xNoninfluence_strong_uwr_xources_ipurgx \<Longrightarrow> confidentiality_u_weak" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_ipurgx_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: xources_Step_2 sameFor_dom_def uwr_equiv_def Step_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xNoninfluence_strong_uwr_xources_ipurgx \<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>xources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurgx u as {s} = ipurgx 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>xources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurgx u [a] {s} = ipurgx 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>xources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurgx u [a] {s} = ipurgx 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_Alternatives

lemma ipurge_single_eq:
  "\<lbrakk> reachable s; reachable t; s \<sim>schedDomain\<sim> t \<rbrakk>
     \<Longrightarrow> ipurge u [a] {s} = ipurge u [a] {t}" apply (frule_tac e=a in schedIncludesCurrentDom) apply (simp add: ipurge_Cons ipurge_Nil sources_Cons sources_Nil) apply (auto dest: enabled_Step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t\<rbrakk> \<Longrightarrow> ipurge u [a] {s} = ipurge u [a] {t} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s = dom a t\<rbrakk> \<Longrightarrow> ipurge u [a] {s} = ipurge u [a] {t} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s = dom a t\<rbrakk> \<Longrightarrow> (dom a t = u \<longrightarrow> ((\<exists>s'. (s, s') \<in> local.Step a) \<longrightarrow> (\<exists>s'. (t, s') \<in> local.Step a) \<or> u \<leadsto> u \<and> (\<exists>s'. (t, s') \<in> local.Step a)) \<and> (u \<leadsto> u \<and> (\<exists>s'. (s, s') \<in> local.Step a) \<longrightarrow> (\<exists>s'. (t, s') \<in> local.Step a)) \<and> ((\<forall>s'. (s, s') \<notin> local.Step a) \<and> (u \<leadsto> u \<longrightarrow> (\<forall>s'. (s, s') \<notin> local.Step a)) \<longrightarrow> (\<forall>s'. (t, s') \<notin> local.Step a) \<and> (u \<leadsto> u \<longrightarrow> (\<forall>s'. (t, s') \<notin> local.Step a)))) \<and> (dom a t \<leadsto> u \<longrightarrow> ((\<exists>s'. (s, s') \<in> local.Step a) \<longrightarrow> (\<exists>s'. (t, s') \<in> local.Step a) \<and> dom a t = u \<or> (\<exists>s'. (t, s') \<in> local.Step a)) \<and> (u \<leadsto> u \<and> (\<exists>s'. (s, s') \<in> local.Step a) \<longrightarrow> (\<exists>s'. (t, s') \<in> local.Step a) \<and> dom a t = u \<or> (\<exists>s'. (t, s') \<in> local.Step a)) \<and> ((\<forall>s'. (s, s') \<notin> local.Step a) \<and> (u \<leadsto> u \<longrightarrow> (\<forall>s'. (s, s') \<notin> local.Step a)) \<longrightarrow> ((\<forall>s'. (t, s') \<notin> local.Step a) \<or> dom a t \<noteq> u) \<and> (\<forall>s'. (t, s') \<notin> local.Step a))) proof (prove)
goal:
No subgoals!