theory Noninterference_Base

lemma non_sched_doms_cannot_schedule:
  "\<lbrakk> integrity_u; reachable s; dom a s \<noteq> schedDomain; (s,s') \<in> Step a \<rbrakk>
     \<Longrightarrow> s \<sim>schedDomain\<sim> s'" apply (drule_tac u=schedDomain in integrity_uD) apply assumption apply (erule contrapos_nn) apply (erule schedNotGlobalChannel) apply (rule uwr_refl) apply assumption apply (erule uwr_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable ?s
 2. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (dom ?a ?s, schedDomain) \<notin> policy
 3. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> ?s \<sim>schedDomain\<sim> ?t
 4. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (?s, ?s') \<in> local.Step ?a
 5. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a; ?s' \<sim>schedDomain\<sim> ?t\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (dom ?a s, schedDomain) \<notin> policy
 2. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> ?t
 3. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (s, ?s') \<in> local.Step ?a
 4. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a; ?s' \<sim>schedDomain\<sim> ?t\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>reachable s; (s, s') \<in> local.Step a; dom ?a s \<leadsto> schedDomain\<rbrakk> \<Longrightarrow> dom a s = schedDomain
 2. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> ?t
 3. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (s, ?s') \<in> local.Step ?a
 4. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a; ?s' \<sim>schedDomain\<sim> ?t\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> ?t
 2. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (s, ?s') \<in> local.Step a
 3. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a; ?s' \<sim>schedDomain\<sim> ?t\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (s, ?s') \<in> local.Step a
 2. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a; ?s' \<sim>schedDomain\<sim> s\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> local.Step a; s' \<sim>schedDomain\<sim> s\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> s' proof (prove)
goal:
No subgoals!