kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference_Base_Alternatives

lemma Noninfluence_strong_uwr_pg_confidentiality_u_weak:
  "Noninfluence_strong_uwr_pg \<Longrightarrow> confidentiality_u_weak" apply (clarsimp simp: Noninfluence_strong_uwr_pg_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 ipurge_single_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Noninfluence_strong_uwr_pg \<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 {t} \<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] {t} \<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] {t} \<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 Nonleakage_gen_xNonleakage_gen:
  "confidentiality_u \<Longrightarrow> Nonleakage_gen = xNonleakage_gen" apply (simp add: Nonleakage_gen_def xNonleakage_gen_def) apply (fastforce simp: xources_sources) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> Nonleakage_gen = xNonleakage_gen proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> (\<forall>as s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> uwr_equiv s as t as u) = (\<forall>as s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>xources as s u\<approx> t \<longrightarrow> uwr_equiv s as t as u) proof (prove)
goal:
No subgoals!
theory Noninterference_Base_Alternatives

lemma xNoninfluence_strong_uwr_xources_ipurge_integrity_u:
  "xNoninfluence_strong_uwr_xources_ipurge \<Longrightarrow> integrity_u" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_ipurge_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. xNoninfluence_strong_uwr_xources_ipurge \<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>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; (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>xources [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>xources [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_Alternatives

lemma xNoninfluence_strong_uwr_sources_xpurge_integrity_u:
  "xNoninfluence_strong_uwr_sources_xpurge \<Longrightarrow> integrity_u" apply (clarsimp simp: xNoninfluence_strong_uwr_sources_xpurge_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: xources_Step sameFor_dom_def uwr_refl
                   uwr_equiv_def Step_def xpurge_Cons xpurge_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. xNoninfluence_strong_uwr_sources_xpurge \<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> xpurge u as {s} = xpurge 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> xpurge u [a] {s} = xpurge 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> xpurge u [a] {s} = xpurge 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_Alternatives

lemma xNoninfluence_strong_uwr_xources_xpurge_integrity_u:
  "xNoninfluence_strong_uwr_xources_xpurge \<Longrightarrow> integrity_u" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_xpurge_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: xources_Step sameFor_dom_def uwr_refl
                   uwr_equiv_def Step_def xpurge_Cons xpurge_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. xNoninfluence_strong_uwr_xources_xpurge \<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>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; (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>xources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> xpurge u [a] {s} = xpurge 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>xources [a] s u\<approx> s \<longrightarrow> s \<sim>schedDomain\<sim> s \<longrightarrow> xpurge u [a] {s} = xpurge 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_Alternatives

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

lemma xNoninfluence_strong_uwr_xources_ipurgx_integrity_u:
  "xNoninfluence_strong_uwr_xources_ipurgx \<Longrightarrow> integrity_u" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_ipurgx_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 ipurgx_Cons ipurgx_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. xNoninfluence_strong_uwr_xources_ipurgx \<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>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; (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>xources [a] s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> ipurgx u [a] {s} = ipurgx 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>xources [a] s u\<approx> s \<longrightarrow> s \<sim>schedDomain\<sim> s \<longrightarrow> ipurgx u [a] {s} = ipurgx 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_Alternatives

lemma xNoninfluence_strong_uwr_sources_xpurgx_integrity_u:
  "xNoninfluence_strong_uwr_sources_xpurgx \<Longrightarrow> integrity_u" apply (clarsimp simp: xNoninfluence_strong_uwr_sources_xpurgx_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: xources_Step sameFor_dom_def uwr_refl
                   uwr_equiv_def Step_def xpurgx_Cons xpurgx_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. xNoninfluence_strong_uwr_sources_xpurgx \<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> xpurgx u as {s} = xpurgx 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> xpurgx u [a] {s} = xpurgx 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> xpurgx u [a] {s} = xpurgx 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!