kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference_Base_Alternatives

lemma xNoninfluence_strong_uwr_xources_xpurgx_integrity_u:
  "xNoninfluence_strong_uwr_xources_xpurgx \<Longrightarrow> integrity_u" apply (clarsimp simp: xNoninfluence_strong_uwr_xources_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_xources_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>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; 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> 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>xources [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!
theory Noninterference_Base_Alternatives

lemma Noninfluence_strong_uwr_pg_integrity_u:
  "Noninfluence_strong_uwr_pg \<Longrightarrow> integrity_u" apply (clarsimp simp: Noninfluence_strong_uwr_pg_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_pg \<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 {t} \<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 [] {t} \<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_Alternatives

lemma Noninfluence_strong_uwr_equiv_xNoninfluence_strong_uwr_xources_ipurge:
  "Noninfluence_strong_uwr = xNoninfluence_strong_uwr_xources_ipurge" apply (rule iffI) apply (subst xNoninfluence_strong_uwr_xources_ipurge_Noninfluence_strong_uwr) apply (erule Noninfluence_strong_uwr_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_integrity_u) apply assumption apply (rule Noninfluence_strong_uwr) apply (erule xNoninfluence_strong_uwr_xources_ipurge_confidentiality_u_weak) apply (erule xNoninfluence_strong_uwr_xources_ipurge_integrity_u) done

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

lemma Noninfluence_strong_uwr_equiv_xNoninfluence_strong_uwr_sources_xpurge:
  "Noninfluence_strong_uwr = xNoninfluence_strong_uwr_sources_xpurge" apply (rule iffI) apply (subst xNoninfluence_strong_uwr_sources_xpurge_Noninfluence_strong_uwr) apply (erule Noninfluence_strong_uwr_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_integrity_u) apply assumption apply (rule Noninfluence_strong_uwr) apply (erule xNoninfluence_strong_uwr_sources_xpurge_confidentiality_u_weak) apply (erule xNoninfluence_strong_uwr_sources_xpurge_integrity_u) done

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

lemma Noninfluence_strong_uwr_equiv_xNoninfluence_strong_uwr_xources_xpurge:
  "Noninfluence_strong_uwr = xNoninfluence_strong_uwr_xources_xpurge" apply (rule iffI) apply (subst xNoninfluence_strong_uwr_xources_xpurge_Noninfluence_strong_uwr) apply (erule Noninfluence_strong_uwr_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_integrity_u) apply assumption apply (rule Noninfluence_strong_uwr) apply (erule xNoninfluence_strong_uwr_xources_xpurge_confidentiality_u_weak) apply (erule xNoninfluence_strong_uwr_xources_xpurge_integrity_u) done

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

lemma Noninfluence_strong_uwr_equiv_xNoninfluence_strong_uwr_sources_ipurgx:
  "Noninfluence_strong_uwr = xNoninfluence_strong_uwr_sources_ipurgx" apply (rule iffI) apply (subst xNoninfluence_strong_uwr_sources_ipurgx_Noninfluence_strong_uwr) apply (erule Noninfluence_strong_uwr_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_integrity_u) apply assumption apply (rule Noninfluence_strong_uwr) apply (erule xNoninfluence_strong_uwr_sources_ipurgx_confidentiality_u_weak) apply (erule xNoninfluence_strong_uwr_sources_ipurgx_integrity_u) done

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

lemma Noninfluence_strong_uwr_equiv_xNoninfluence_strong_uwr_sources_xpurgx:
  "Noninfluence_strong_uwr = xNoninfluence_strong_uwr_sources_xpurgx" apply (rule iffI) apply (subst xNoninfluence_strong_uwr_sources_xpurgx_Noninfluence_strong_uwr) apply (erule Noninfluence_strong_uwr_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_integrity_u) apply assumption apply (rule Noninfluence_strong_uwr) apply (erule xNoninfluence_strong_uwr_sources_xpurgx_confidentiality_u_weak) apply (erule xNoninfluence_strong_uwr_sources_xpurgx_integrity_u) done

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

lemma Noninfluence_strong_uwr_equiv_xNoninfluence_strong_uwr_xources_xpurgx:
  "Noninfluence_strong_uwr = xNoninfluence_strong_uwr_xources_xpurgx" apply (rule iffI) apply (subst xNoninfluence_strong_uwr_xources_xpurgx_Noninfluence_strong_uwr) apply (erule Noninfluence_strong_uwr_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_integrity_u) apply assumption apply (rule Noninfluence_strong_uwr) apply (erule xNoninfluence_strong_uwr_xources_xpurgx_confidentiality_u_weak) apply (erule xNoninfluence_strong_uwr_xources_xpurgx_integrity_u) done

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

lemma Noninfluence_strong_uwr_equiv_Noninfluence_strong_uwr_pg:
  "Noninfluence_strong_uwr = Noninfluence_strong_uwr_pg" apply (rule iffI) apply (subst Noninfluence_strong_uwr_pg_Noninfluence_strong_uwr) apply (erule Noninfluence_strong_uwr_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_integrity_u) apply assumption apply (rule Noninfluence_strong_uwr) apply (erule Noninfluence_strong_uwr_pg_confidentiality_u_weak) apply (erule Noninfluence_strong_uwr_pg_integrity_u) done

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

lemma equiv_valid_2_bind_general:
  assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D B C R (Q rv) (Q' rv') (g rv) (g' rv')"
  assumes r1: "equiv_valid_2 D A B R' P P' f f'"
  assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
  assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
  shows "equiv_valid_2 D A C R (\<lambda> s. P s \<and> S s) (\<lambda> s. P' s \<and> S' s) (f >>= g) (f' >>= g')" using assms unfolding bind_def equiv_valid_2_def valid_def apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A C R (\<lambda>s. P s \<and> S s) (\<lambda>s. P' s \<and> S' s) (f >>= g) (f' >>= g') proof (prove)
using this:
R' ?rv ?rv' \<Longrightarrow> equiv_valid_2 D B C R (Q ?rv) (Q' ?rv') (g ?rv) (g' ?rv')
equiv_valid_2 D A B R' P P' f f'
\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>
\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>

goal (1 subgoal):
 1. equiv_valid_2 D A C R (\<lambda>s. P s \<and> S s) (\<lambda>s. P' s \<and> S' s) (f >>= g) (f' >>= g') proof (prove)
using this:
R' ?rv ?rv' \<Longrightarrow> \<forall>s t. Q ?rv s \<and> Q' ?rv' t \<and> D s t \<and> B s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (g ?rv s). \<forall>(rvb, t')\<in>fst (g' ?rv' t). R rva rvb \<and> D s' t' \<and> C s' t')
\<forall>s t. P s \<and> P' t \<and> D s t \<and> A s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f' t). R' rva rvb \<and> D s' t' \<and> B s' t')
\<forall>s. S s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). Q r s')
\<forall>s. S' s \<longrightarrow> (\<forall>(r, s')\<in>fst (f' s). Q' r s')

goal (1 subgoal):
 1. \<forall>s t. (P s \<and> S s) \<and> (P' t \<and> S' t) \<and> D s t \<and> A s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (\<Union> (fst ` (\<lambda>(x, y). g x y) ` fst (f s)), True \<in> snd ` (\<lambda>(x, y). g x y) ` fst (f s) \<or> snd (f s)). \<forall>(rvb, t')\<in>fst (\<Union> (fst ` (\<lambda>(x, y). g' x y) ` fst (f' t)), True \<in> snd ` (\<lambda>(x, y). g' x y) ` fst (f' t) \<or> snd (f' t)). R rva rvb \<and> D s' t' \<and> C s' t') proof (prove)
goal:
No subgoals!
theory EquivValid

lemma equiv_valid_2_bind:
  assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D A A R (Q rv) (Q' rv') (g rv) (g' rv')"
  assumes r1: "equiv_valid_2 D A A R' P P' f f'"
  assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
  assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
  shows "equiv_valid_2 D A A R (\<lambda> s. P s \<and> S s) (\<lambda> s. P' s \<and> S' s) (f >>= g) (f' >>= g')" using assms by (blast intro: equiv_valid_2_bind_general)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A A R (\<lambda>s. P s \<and> S s) (\<lambda>s. P' s \<and> S' s) (f >>= g) (f' >>= g') proof (prove)
using this:
R' ?rv ?rv' \<Longrightarrow> equiv_valid_2 D A A R (Q ?rv) (Q' ?rv') (g ?rv) (g' ?rv')
equiv_valid_2 D A A R' P P' f f'
\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>
\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>

goal (1 subgoal):
 1. equiv_valid_2 D A A R (\<lambda>s. P s \<and> S s) (\<lambda>s. P' s \<and> S' s) (f >>= g) (f' >>= g')