theory Noninterference_Base

lemma Nonleakage_gen:
  "confidentiality_u \<Longrightarrow> Nonleakage_gen" apply (subst Nonleakage_gen_def) apply (rule allI) apply (induct_tac as) apply (simp add: sources_Nil uwr_equiv_def execution_Run sameFor_dom_def) apply (clarsimp) apply (rule uwr_equiv_Cons_bothI) apply assumption apply assumption apply clarsimp apply (drule_tac x=s' in spec, drule_tac x=u in spec, drule_tac x=t' in spec) apply (clarsimp simp: reachable_Step) apply (erule impE) apply (blast intro: sched_equiv_preserved) apply (erule mp) apply (blast intro: sources_unwinding_step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> Nonleakage_gen proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> \<forall>as s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> uwr_equiv s as t as u proof (prove)
goal (1 subgoal):
 1. \<And>as. confidentiality_u \<Longrightarrow> \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> uwr_equiv s as t as u proof (prove)
goal (2 subgoals):
 1. \<And>as. confidentiality_u \<Longrightarrow> \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources [] s u\<approx> t \<longrightarrow> uwr_equiv s [] t [] u
 2. \<And>as a list. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u\<rbrakk> \<Longrightarrow> \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources (a # list) s u\<approx> t \<longrightarrow> uwr_equiv s (a # list) t (a # list) u proof (prove)
goal (1 subgoal):
 1. \<And>as a list. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u\<rbrakk> \<Longrightarrow> \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources (a # list) s u\<approx> t \<longrightarrow> uwr_equiv s (a # list) t (a # list) u proof (prove)
goal (1 subgoal):
 1. \<And>a list s u t. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t\<rbrakk> \<Longrightarrow> uwr_equiv s (a # list) t (a # list) u proof (prove)
goal (3 subgoals):
 1. \<And>a list s u t. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t\<rbrakk> \<Longrightarrow> reachable s
 2. \<And>a list s u t. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t\<rbrakk> \<Longrightarrow> reachable t
 3. \<And>a list s u t. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t\<rbrakk> \<Longrightarrow> \<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> uwr_equiv s' list t' list u proof (prove)
goal (2 subgoals):
 1. \<And>a list s u t. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t\<rbrakk> \<Longrightarrow> reachable t
 2. \<And>a list s u t. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t\<rbrakk> \<Longrightarrow> \<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> uwr_equiv s' list t' list u proof (prove)
goal (1 subgoal):
 1. \<And>a list s u t. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t\<rbrakk> \<Longrightarrow> \<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> uwr_equiv s' list t' list u proof (prove)
goal (1 subgoal):
 1. \<And>a list s u t s' t'. \<lbrakk>confidentiality_u; \<forall>s u t. reachable s \<and> reachable t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> s \<approx>sources list s u\<approx> t \<longrightarrow> uwr_equiv s list t list u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> uwr_equiv s' list t' list u proof (prove)
goal (1 subgoal):
 1. \<And>a list s u t s' t'. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; reachable s' \<and> reachable t' \<longrightarrow> s' \<sim>schedDomain\<sim> t' \<longrightarrow> s' \<approx>sources list s' u\<approx> t' \<longrightarrow> uwr_equiv s' list t' list u\<rbrakk> \<Longrightarrow> uwr_equiv s' list t' list u proof (prove)
goal (1 subgoal):
 1. \<And>a list s u t s' t'. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; s' \<sim>schedDomain\<sim> t' \<longrightarrow> s' \<approx>sources list s' u\<approx> t' \<longrightarrow> uwr_equiv s' list t' list u\<rbrakk> \<Longrightarrow> uwr_equiv s' list t' list u proof (prove)
goal (2 subgoals):
 1. \<And>a list s u t s' t'. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<And>a list s u t s' t'. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; s' \<approx>sources list s' u\<approx> t' \<longrightarrow> uwr_equiv s' list t' list u\<rbrakk> \<Longrightarrow> uwr_equiv s' list t' list u proof (prove)
goal (1 subgoal):
 1. \<And>a list s u t s' t'. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a; s' \<approx>sources list s' u\<approx> t' \<longrightarrow> uwr_equiv s' list t' list u\<rbrakk> \<Longrightarrow> uwr_equiv s' list t' list u proof (prove)
goal (1 subgoal):
 1. \<And>a list s u t s' t'. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<sim>schedDomain\<sim> t; s \<approx>sources (a # list) s u\<approx> t; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<approx>sources list s' u\<approx> t' proof (prove)
goal:
No subgoals!