theory Noninterference_Base

lemma confidentiality_u_weak:
  "\<lbrakk> confidentiality_u_weak; integrity_u \<rbrakk>
     \<Longrightarrow> confidentiality_u" apply (clarsimp simp: confidentiality_u_def) apply (erule impCE') apply (subst (asm) confidentiality_u_weak_def, blast) apply (frule integrity_uD, simp+) apply (drule_tac s=t and t="s'" in integrity_uD) apply assumption apply (drule_tac e=a in schedIncludesCurrentDom) apply simp apply (blast intro: uwr_sym) apply assumption apply (erule uwr_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u_weak; integrity_u\<rbrakk> \<Longrightarrow> confidentiality_u proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; integrity_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; dom a s \<leadsto> u \<longrightarrow> 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 (2 subgoals):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; integrity_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<leadsto> u; s \<sim>dom a s\<sim> t\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t'
 2. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; integrity_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; integrity_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; integrity_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (5 subgoals):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> reachable t
 2. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> (dom (?a48 a u s t s' t') t, ?u48 a u s t s' t') \<notin> policy
 3. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> t \<sim>?u48 a u s t s' t'\<sim> s'
 4. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> (t, ?s'48 a u s t s' t') \<in> local.Step (?a48 a u s t s' t')
 5. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t; ?s'48 a u s t s' t' \<sim>?u48 a u s t s' t'\<sim> s'\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (4 subgoals):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> (dom (?a48 a u s t s' t') t, ?u48 a u s t s' t') \<notin> policy
 2. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> t \<sim>?u48 a u s t s' t'\<sim> s'
 3. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> (t, ?s'48 a u s t s' t') \<in> local.Step (?a48 a u s t s' t')
 4. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t; ?s'48 a u s t s' t' \<sim>?u48 a u s t s' t'\<sim> s'\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (4 subgoals):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t; dom a s = dom a t\<rbrakk> \<Longrightarrow> (dom (?a48 a u s t s' t') t, ?u48 a u s t s' t') \<notin> policy
 2. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> t \<sim>?u48 a u s t s' t'\<sim> s'
 3. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> (t, ?s'48 a u s t s' t') \<in> local.Step (?a48 a u s t s' t')
 4. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t; ?s'48 a u s t s' t' \<sim>?u48 a u s t s' t'\<sim> s'\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (3 subgoals):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> t \<sim>u\<sim> s'
 2. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> (t, ?s'48 a u s t s' t') \<in> local.Step a
 3. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t; ?s'48 a u s t s' t' \<sim>u\<sim> s'\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (2 subgoals):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> (t, ?s'48 a u s t s' t') \<in> local.Step a
 2. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t; ?s'48 a u s t s' t' \<sim>u\<sim> s'\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<And>a u s t s' t'. \<lbrakk>confidentiality_u_weak; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<sim>u\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; (dom a s, u) \<notin> policy; s' \<sim>u\<sim> t; t' \<sim>u\<sim> s'\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal:
No subgoals!