theory Noninterference_Base

lemma sched_equiv_preserved:
  "\<lbrakk> confidentiality_u; reachable s; reachable t;
     s \<sim>schedDomain\<sim> t; (s,s') \<in> Step a; (t,t') \<in> Step a \<rbrakk>
     \<Longrightarrow> s' \<sim>schedDomain\<sim> t'" apply (case_tac "dom a s = schedDomain") apply (subst (asm) confidentiality_u_def) apply (drule_tac x=a in spec) apply (drule_tac x=schedDomain in spec) apply (drule_tac x=s in spec) apply (drule_tac x=t in spec) apply simp apply (subst (asm) confidentiality_u_def) apply (blast intro: schedNotGlobalChannel) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s = schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' proof (prove)
goal (2 subgoals):
 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; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s = schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s = schedDomain; \<forall>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')\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s = schedDomain; \<forall>s t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> schedDomain \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>schedDomain\<sim> t')\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s = schedDomain; \<forall>t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> schedDomain \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>schedDomain\<sim> t')\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s = schedDomain; reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (dom a s \<leadsto> schedDomain \<longrightarrow> s \<sim>dom a s\<sim> t) \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> (\<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> s' \<sim>schedDomain\<sim> t')\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' 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; reachable t; s \<sim>schedDomain\<sim> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t' proof (prove)
goal:
No subgoals!