kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference_Base

lemma reachable_Step:
  "\<lbrakk> reachable s; (s,s') \<in> Step a \<rbrakk> \<Longrightarrow> reachable s'" apply (erule reachable_execution) apply (simp add: Step_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable s' proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> local.Step a \<Longrightarrow> s' \<in> execution A s ?js proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma reachable_induct_helper:
  assumes a: "\<And>s s' a. \<lbrakk> reachable s; P s; (s, s') \<in> Step a \<rbrakk> \<Longrightarrow> P s'"
  shows "\<lbrakk> (s0, s1) \<in> Run Step as; P s0 \<rbrakk> \<Longrightarrow> P s1" apply (induct as arbitrary: s1 rule: rev_induct) apply simp apply (fastforce dest: Run_mid intro: a Run_reachable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s0, s1) \<in> Run local.Step as; P s0\<rbrakk> \<Longrightarrow> P s1 proof (prove)
goal (2 subgoals):
 1. \<And>s1. \<lbrakk>(s0, s1) \<in> Run local.Step []; P s0\<rbrakk> \<Longrightarrow> P s1
 2. \<And>x xs s1. \<lbrakk>\<And>s1. \<lbrakk>(s0, s1) \<in> Run local.Step xs; P s0\<rbrakk> \<Longrightarrow> P s1; (s0, s1) \<in> Run local.Step (xs @ [x]); P s0\<rbrakk> \<Longrightarrow> P s1 proof (prove)
goal (1 subgoal):
 1. \<And>x xs s1. \<lbrakk>\<And>s1. \<lbrakk>(s0, s1) \<in> Run local.Step xs; P s0\<rbrakk> \<Longrightarrow> P s1; (s0, s1) \<in> Run local.Step (xs @ [x]); P s0\<rbrakk> \<Longrightarrow> P s1 proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma reachable_induct:
  "\<lbrakk> \<And>s s' a. reachable s \<Longrightarrow> (s,s') \<in> (Step a) \<Longrightarrow> P s \<Longrightarrow> P s'; reachable s1; P s0 \<rbrakk>
     \<Longrightarrow> P s1" apply (drule reachable_Run) apply (elim exE) apply (rule reachable_induct_helper) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; (s, s') \<in> local.Step a; P s\<rbrakk> \<Longrightarrow> P s'; reachable s1; P s0\<rbrakk> \<Longrightarrow> P s1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; (s, s') \<in> local.Step a; P s\<rbrakk> \<Longrightarrow> P s'; P s0; \<exists>as. (s0, s1) \<in> Run local.Step as\<rbrakk> \<Longrightarrow> P s1 proof (prove)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; (s, s') \<in> local.Step a; P s\<rbrakk> \<Longrightarrow> P s'; P s0; (s0, s1) \<in> Run local.Step as\<rbrakk> \<Longrightarrow> P s1 proof (prove)
goal (3 subgoals):
 1. \<And>as s s' a. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; (s, s') \<in> local.Step a; P s\<rbrakk> \<Longrightarrow> P s'; P s0; (s0, s1) \<in> Run local.Step as; reachable s; P s; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> P s'
 2. \<And>as. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; (s, s') \<in> local.Step a; P s\<rbrakk> \<Longrightarrow> P s'; P s0; (s0, s1) \<in> Run local.Step as\<rbrakk> \<Longrightarrow> (s0, s1) \<in> Run local.Step (?as3 as)
 3. \<And>as. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; (s, s') \<in> local.Step a; P s\<rbrakk> \<Longrightarrow> P s'; P s0; (s0, s1) \<in> Run local.Step as\<rbrakk> \<Longrightarrow> P s0 proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Run_det:
  "obs_det \<Longrightarrow> \<exists>s'. {s'. (s,s') \<in> Run Step as} = {s'}" apply (induct as arbitrary: s rule: rev_induct) apply simp apply (simp add: Run_app relcomp_def) apply (drule_tac x=s in meta_spec) apply clarsimp apply (drule_tac s=s' and js="[x]" in obs_detD) apply (clarsimp simp: Step_def) apply (rule_tac x="s'a" in exI) apply (auto dest: equalityD1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obs_det \<Longrightarrow> \<exists>s'. {s'. (s, s') \<in> Run local.Step as} = {s'} proof (prove)
goal (2 subgoals):
 1. \<And>s. obs_det \<Longrightarrow> \<exists>s'. {s'. (s, s') \<in> Run local.Step []} = {s'}
 2. \<And>x xs s. \<lbrakk>\<And>s. obs_det \<Longrightarrow> \<exists>s'. {s'. (s, s') \<in> Run local.Step xs} = {s'}; obs_det\<rbrakk> \<Longrightarrow> \<exists>s'. {s'. (s, s') \<in> Run local.Step (xs @ [x])} = {s'} proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. obs_det \<Longrightarrow> \<exists>s'. {s'. (s, s') \<in> Run local.Step xs} = {s'}; obs_det\<rbrakk> \<Longrightarrow> \<exists>s'. {s'. (s, s') \<in> Run local.Step (xs @ [x])} = {s'} proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. \<exists>s'. {s'. (s, s') \<in> Run local.Step xs} = {s'}; obs_det\<rbrakk> \<Longrightarrow> \<exists>s'. {s'. ((\<lambda>x xa. (x, xa) \<in> Run local.Step xs) OO (\<lambda>xa xb. (xa, xb) \<in> local.Step x) OO (=)) s s'} = {s'} proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>obs_det; \<exists>s'. {s'. (s, s') \<in> Run local.Step xs} = {s'}\<rbrakk> \<Longrightarrow> \<exists>s'. {s'. ((\<lambda>x xa. (x, xa) \<in> Run local.Step xs) OO (\<lambda>xa xb. (xa, xb) \<in> local.Step x) OO (=)) s s'} = {s'} proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s'. \<lbrakk>obs_det; {s'. (s, s') \<in> Run local.Step xs} = {s'}\<rbrakk> \<Longrightarrow> \<exists>s'. {s'. ((\<lambda>x xa. (x, xa) \<in> Run local.Step xs) OO (\<lambda>xa xb. (xa, xb) \<in> local.Step x) OO (=)) s s'} = {s'} proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s'. \<lbrakk>{s'. (s, s') \<in> Run local.Step xs} = {s'}; \<exists>s'a. execution A s' [x] = {s'a}\<rbrakk> \<Longrightarrow> \<exists>s'. {s'. ((\<lambda>x xa. (x, xa) \<in> Run local.Step xs) OO (\<lambda>xa xb. (xa, xb) \<in> local.Step x) OO (=)) s s'} = {s'} proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' s'a. \<lbrakk>{s'. (s, s') \<in> Run local.Step xs} = {s'}; execution A s' [x] = {s'a}\<rbrakk> \<Longrightarrow> \<exists>s'. {s'. ((\<lambda>x xa. (x, xa) \<in> Run local.Step xs) OO (\<lambda>xa xb. xb \<in> execution A xa [x]) OO (=)) s s'} = {s'} proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' s'a. \<lbrakk>{s'. (s, s') \<in> Run local.Step xs} = {s'}; execution A s' [x] = {s'a}\<rbrakk> \<Longrightarrow> {s'. ((\<lambda>x xa. (x, xa) \<in> Run local.Step xs) OO (\<lambda>xa xb. xb \<in> execution A xa [x]) OO (=)) s s'} = {s'a} proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma eq:
  "\<lbrakk> S \<subseteq> T; \<exists>x. S = {x}; \<exists>y. T = {y} \<rbrakk> \<Longrightarrow> S = T" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> T; \<exists>x. S = {x}; \<exists>y. T = {y}\<rbrakk> \<Longrightarrow> S = T
theory Noninterference_Base

lemma execution_Run:
  "reachable s \<Longrightarrow> execution A s as = {s'. (s,s') \<in> Run Step as}" apply (rule disjE[OF obs_det_or_no_abs]) apply (rule eq) apply (erule execution_subset_Run) apply (erule obs_detD) apply (erule Run_det) apply (rule equalityI) apply (erule execution_subset_Run) apply (erule (1) Run_subset_execution) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> execution A s as = {s'. (s, s') \<in> Run local.Step as} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; obs_det\<rbrakk> \<Longrightarrow> execution A s as = {s'. (s, s') \<in> Run local.Step as}
 2. \<lbrakk>reachable s; no_abs\<rbrakk> \<Longrightarrow> execution A s as = {s'. (s, s') \<in> Run local.Step as} proof (prove)
goal (4 subgoals):
 1. \<lbrakk>reachable s; obs_det\<rbrakk> \<Longrightarrow> execution A s as \<subseteq> {s'. (s, s') \<in> Run local.Step as}
 2. \<lbrakk>reachable s; obs_det\<rbrakk> \<Longrightarrow> \<exists>x. execution A s as = {x}
 3. \<lbrakk>reachable s; obs_det\<rbrakk> \<Longrightarrow> \<exists>y. {s'. (s, s') \<in> Run local.Step as} = {y}
 4. \<lbrakk>reachable s; no_abs\<rbrakk> \<Longrightarrow> execution A s as = {s'. (s, s') \<in> Run local.Step as} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>reachable s; obs_det\<rbrakk> \<Longrightarrow> \<exists>x. execution A s as = {x}
 2. \<lbrakk>reachable s; obs_det\<rbrakk> \<Longrightarrow> \<exists>y. {s'. (s, s') \<in> Run local.Step as} = {y}
 3. \<lbrakk>reachable s; no_abs\<rbrakk> \<Longrightarrow> execution A s as = {s'. (s, s') \<in> Run local.Step as} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; obs_det\<rbrakk> \<Longrightarrow> \<exists>y. {s'. (s, s') \<in> Run local.Step as} = {y}
 2. \<lbrakk>reachable s; no_abs\<rbrakk> \<Longrightarrow> execution A s as = {s'. (s, s') \<in> Run local.Step as} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; no_abs\<rbrakk> \<Longrightarrow> execution A s as = {s'. (s, s') \<in> Run local.Step as} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; no_abs\<rbrakk> \<Longrightarrow> execution A s as \<subseteq> {s'. (s, s') \<in> Run local.Step as}
 2. \<lbrakk>reachable s; no_abs\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step as} \<subseteq> execution A s as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; no_abs\<rbrakk> \<Longrightarrow> {s'. (s, s') \<in> Run local.Step as} \<subseteq> execution A s as proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma inv_and_inj: "reachable s \<Longrightarrow> Fin A i = s \<Longrightarrow> Init A s = {i}" using Fin_inj Init_inv_Fin by (blast dest: injD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; Fin A i = s\<rbrakk> \<Longrightarrow> Init A s = {i} proof (prove)
using this:
inj (Fin A)
reachable ?s \<Longrightarrow> Init A ?s = {s'. Fin A s' = ?s}

goal (1 subgoal):
 1. \<lbrakk>reachable s; Fin A i = s\<rbrakk> \<Longrightarrow> Init A s = {i}
theory Noninterference_Base

lemma s0_reachable:
  "reachable s0" apply (simp add: reachable_def) apply (rule_tac x="[]" in exI) apply (simp add: execution_def steps_def) using Fin_Init_s0 .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s0 proof (prove)
goal (1 subgoal):
 1. \<exists>js. s0 \<in> execution A s0 js proof (prove)
goal (1 subgoal):
 1. s0 \<in> execution A s0 [] proof (prove)
goal (1 subgoal):
 1. s0 \<in> Fin A ` Init A s0 proof (prove)
using this:
s0 \<in> Fin A ` Init A s0

goal (1 subgoal):
 1. s0 \<in> Fin A ` Init A s0
theory Noninterference_Base

lemma uwr_sym:
  "x \<sim>(u::'d)\<sim> y \<Longrightarrow> y \<sim>u\<sim> x" apply (cut_tac u=u in uwr_equiv_rel) apply (clarsimp simp: equiv_def) apply (blast dest: symD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<sim>u\<sim> y \<Longrightarrow> y \<sim>u\<sim> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim>u\<sim> y; equiv UNIV (uwr u)\<rbrakk> \<Longrightarrow> y \<sim>u\<sim> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim>u\<sim> y; refl (uwr u); sym (uwr u); trans (uwr u)\<rbrakk> \<Longrightarrow> y \<sim>u\<sim> x proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma uwr_trans:
  "\<lbrakk> x \<sim>(u::'d)\<sim> y; y \<sim>u\<sim> z \<rbrakk> \<Longrightarrow> x \<sim>u\<sim> z" apply (cut_tac u=u in uwr_equiv_rel) apply (clarsimp simp: equiv_def) apply (blast dest: transD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim>u\<sim> y; y \<sim>u\<sim> z\<rbrakk> \<Longrightarrow> x \<sim>u\<sim> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim>u\<sim> y; y \<sim>u\<sim> z; equiv UNIV (uwr u)\<rbrakk> \<Longrightarrow> x \<sim>u\<sim> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim>u\<sim> y; y \<sim>u\<sim> z; refl (uwr u); sym (uwr u); trans (uwr u)\<rbrakk> \<Longrightarrow> x \<sim>u\<sim> z proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma sameFor_subset_dom: "\<lbrakk>s \<approx>(x::'d set)\<approx> t; y \<subseteq> x\<rbrakk> \<Longrightarrow> s \<approx>y\<approx> t" by (fastforce simp: sameFor_dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<approx>x\<approx> t; y \<subseteq> x\<rbrakk> \<Longrightarrow> s \<approx>y\<approx> t
theory Noninterference_Base

lemma sameFor_inter_domI: "s \<approx>(S::'d set)\<approx> t \<Longrightarrow> s \<approx>(S \<inter> B)\<approx> t" by (auto simp: sameFor_dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<approx>S\<approx> t \<Longrightarrow> s \<approx>(S \<inter> B)\<approx> t
theory Noninterference_Base

lemma sameFor_sym_dom:
  "s \<approx>(S::'d set)\<approx> t \<Longrightarrow> t \<approx>S\<approx> s" by (auto simp: sameFor_dom_def uwr_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<approx>S\<approx> t \<Longrightarrow> t \<approx>S\<approx> s
theory Noninterference_Base

lemma uwr_equiv_sym:
  "uwr_equiv s as t bs u \<Longrightarrow> uwr_equiv t bs s as u" by (fastforce simp: uwr_equiv_def uwr_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uwr_equiv s as t bs u \<Longrightarrow> uwr_equiv t bs s as u
theory Noninterference_Base

lemma uwr_equiv_trans:
  "\<lbrakk> reachable t; uwr_equiv s as t bs x; uwr_equiv t bs u cs x \<rbrakk>
     \<Longrightarrow> uwr_equiv s as u cs x" apply (clarsimp simp: uwr_equiv_def) apply (cut_tac s=t and js=bs in reachable_enabled) apply assumption apply (blast intro: uwr_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable t; uwr_equiv s as t bs x; uwr_equiv t bs u cs x\<rbrakk> \<Longrightarrow> uwr_equiv s as u cs x proof (prove)
goal (1 subgoal):
 1. \<And>s' t'. \<lbrakk>reachable t; \<forall>s' t'. s' \<in> execution A s as \<and> t' \<in> execution A t bs \<longrightarrow> s' \<sim>x\<sim> t'; \<forall>s' t'. s' \<in> execution A t bs \<and> t' \<in> execution A u cs \<longrightarrow> s' \<sim>x\<sim> t'; s' \<in> execution A s as; t' \<in> execution A u cs\<rbrakk> \<Longrightarrow> s' \<sim>x\<sim> t' proof (prove)
goal (2 subgoals):
 1. \<And>s' t'. \<lbrakk>reachable t; \<forall>s' t'. s' \<in> execution A s as \<and> t' \<in> execution A t bs \<longrightarrow> s' \<sim>x\<sim> t'; \<forall>s' t'. s' \<in> execution A t bs \<and> t' \<in> execution A u cs \<longrightarrow> s' \<sim>x\<sim> t'; s' \<in> execution A s as; t' \<in> execution A u cs\<rbrakk> \<Longrightarrow> reachable t
 2. \<And>s' t'. \<lbrakk>reachable t; \<forall>s' t'. s' \<in> execution A s as \<and> t' \<in> execution A t bs \<longrightarrow> s' \<sim>x\<sim> t'; \<forall>s' t'. s' \<in> execution A t bs \<and> t' \<in> execution A u cs \<longrightarrow> s' \<sim>x\<sim> t'; s' \<in> execution A s as; t' \<in> execution A u cs; \<exists>s'. s' \<in> execution A t bs\<rbrakk> \<Longrightarrow> s' \<sim>x\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>s' t'. \<lbrakk>reachable t; \<forall>s' t'. s' \<in> execution A s as \<and> t' \<in> execution A t bs \<longrightarrow> s' \<sim>x\<sim> t'; \<forall>s' t'. s' \<in> execution A t bs \<and> t' \<in> execution A u cs \<longrightarrow> s' \<sim>x\<sim> t'; s' \<in> execution A s as; t' \<in> execution A u cs; \<exists>s'. s' \<in> execution A t bs\<rbrakk> \<Longrightarrow> s' \<sim>x\<sim> t' proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma ipurge_Nil:
  "ipurge u [] ss = []" by (auto simp: ipurge_def)

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

lemma ipurge_Cons:
  "ipurge u (a#as) ss = (if (\<exists>s\<in>ss. dom a s \<in> sources (a#as) s u)
                         then a#ipurge u as (\<Union>s\<in>ss. {s'. (s,s') \<in> Step a})
                         else ipurge u as ss)" by (auto simp: ipurge_def)

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

lemma INT_cong':
  assumes a: "\<And>x. Q x \<Longrightarrow> P x = P' x"
  shows "\<Inter>{P x|x. Q x} = \<Inter>{P' x|x. Q x}" by (auto simp: a)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Inter> {P x |x. Q x} = \<Inter> {P' x |x. Q x}
theory Noninterference_Base

lemma obs_equiv_sym:
  "obs_equiv s as t bs u \<Longrightarrow> obs_equiv t bs s as u" by (clarsimp simp: obs_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obs_equiv s as t bs u \<Longrightarrow> obs_equiv t bs s as u
theory Noninterference_Base

lemma obs_equiv_trans:
  "\<lbrakk> reachable t; obs_equiv s as t bs u; obs_equiv t bs x cs u \<rbrakk>
     \<Longrightarrow> obs_equiv s as x cs u" apply (clarsimp simp: obs_equiv_def) apply (cut_tac s=t and js=bs in reachable_enabled, assumption, blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable t; obs_equiv s as t bs u; obs_equiv t bs x cs u\<rbrakk> \<Longrightarrow> obs_equiv s as x cs u proof (prove)
goal (1 subgoal):
 1. \<And>s' t'. \<lbrakk>reachable t; \<forall>s'. s' \<in> execution A s as \<and> (\<exists>t'. t' \<in> execution A t bs) \<longrightarrow> out u s' = out u t'; \<forall>s' t'. s' \<in> execution A t bs \<and> t' \<in> execution A x cs \<longrightarrow> out u s' = out u t'; s' \<in> execution A s as; t' \<in> execution A x cs\<rbrakk> \<Longrightarrow> out u s' = out u t' proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma notin_policyI:
  "\<lbrakk> dom a s \<notin> sources (a # list) s u; \<exists>s'. (s,s') \<in> Step a \<and> ua \<in> sources list s' u \<rbrakk>
     \<Longrightarrow> (dom a s,ua) \<notin> policy" by (clarsimp simp: sources_Cons)

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

lemma Noninfluence_strong_Noninterference_strong:
  "Noninfluence_strong \<Longrightarrow> Noninterference_strong" apply (clarsimp simp: Noninfluence_strong_def Noninterference_strong_def) apply (drule_tac x=u in spec, drule_tac x=as in spec, drule_tac x=bs in spec) apply (fastforce simp: sameFor_dom_def uwr_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Noninfluence_strong \<Longrightarrow> Noninterference_strong proof (prove)
goal (1 subgoal):
 1. \<And>u as bs 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> obs_equiv s as t bs u; reachable s; ipurge u as {s} = ipurge u bs {s}\<rbrakk> \<Longrightarrow> obs_equiv s as s bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; \<forall>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> obs_equiv s as t bs u\<rbrakk> \<Longrightarrow> obs_equiv s as s bs u proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Noninfluence_strong_Nonleakage:
  "Noninfluence_strong \<Longrightarrow> Nonleakage" by (clarsimp simp: Noninfluence_strong_def Nonleakage_def)

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

lemma no_domain_visible_nondeterminism:
  "\<lbrakk> confidentiality_u; reachable s; (s,s') \<in> Step a; (s,s'') \<in> Step a \<rbrakk>
     \<Longrightarrow> s' \<sim>d\<sim> s''" apply (clarsimp simp: confidentiality_u_def) apply (fastforce intro: uwr_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>d\<sim> s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a u s t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>u\<sim> t'); reachable s; (s, s') \<in> local.Step a; (s, s'') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>d\<sim> s'' proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma integrity_u_more:
  "integrity_u \<Longrightarrow> integrity_u_more" apply (clarsimp simp: integrity_u_more_def integrity_u_def) apply (blast dest: uwr_sym uwr_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_u \<Longrightarrow> integrity_u_more proof (prove)
goal (1 subgoal):
 1. \<And>a u s s' t. \<lbrakk>\<forall>a u s. reachable s \<longrightarrow> (dom a s, u) \<notin> policy \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> s \<sim>u\<sim> s'); reachable s; (dom a s, u) \<notin> policy; s \<sim>u\<sim> t; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma integrity_uD:
  "\<lbrakk> integrity_u; reachable s; (dom a s,u) \<notin> policy; s \<sim>u\<sim> t; (s,s') \<in> Step a \<rbrakk>
     \<Longrightarrow> s' \<sim>u\<sim> t" apply (drule integrity_u_more) apply (simp add: integrity_u_more_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; reachable s; (dom a s, u) \<notin> policy; s \<sim>u\<sim> t; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (dom a s, u) \<notin> policy; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; integrity_u_more\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma confidentiality_u_confidentiality_u_weak:
  "confidentiality_u \<Longrightarrow> confidentiality_u_weak" apply (simp add: confidentiality_u_def confidentiality_u_weak_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> confidentiality_u_weak proof (prove)
goal (1 subgoal):
 1. \<forall>a u s t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>u\<sim> t') \<Longrightarrow> \<forall>a u s t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> dom a s \<leadsto> u \<longrightarrow> s \<sim>dom a s\<sim> t \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>u\<sim> t') proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma impCE':
  "\<lbrakk> P \<longrightarrow> Q; \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R; \<not> P \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<longrightarrow> Q; \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R; \<not> P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Noninterference_Base

lemma obs_equivI:
  "\<lbrakk> output_consistent; uwr_equiv s as t bs ob \<rbrakk> \<Longrightarrow> obs_equiv s as t bs ob" apply (clarsimp simp: obs_equiv_def) apply (auto simp: uwr_equiv_def output_consistent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>output_consistent; uwr_equiv s as t bs ob\<rbrakk> \<Longrightarrow> obs_equiv s as t bs ob proof (prove)
goal (1 subgoal):
 1. \<And>s' t'. \<lbrakk>output_consistent; uwr_equiv s as t bs ob; s' \<in> execution A s as; t' \<in> execution A t bs\<rbrakk> \<Longrightarrow> out ob s' = out ob t' proof (prove)
goal:
No subgoals!