(*  Title:      NI/Noninterference.thy
    Id:         $Id: Noninterference.thy,v 1.15 2004/03/03 16:22:59 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Noninterference *}
(*<*)
theory Noninterference imports Generics begin

(*>*)
subsection "purging"

consts gen_purge :: "sourcef => domain => action list => action list" 
primrec 
  Nil : "gen_purge sf u []     = []"
  Cons: "gen_purge sf u (a#as) = (if dom a \<in> sf (a#as) u then [a] else []) 
                                 @ gen_purge sf u as"

constdefs --{* also for transitive policies *}
  ipurge :: "domain => action list => action list" 
 "ipurge \<equiv> gen_purge sources"
lemma sources_ipurge(*<*) [simp](*>*): "sources (ipurge u as) u = sources as u"
(*<*)
by (unfold sources_def, induct "as", auto simp add: sources_def ipurge_def gen_chain.Cons)

lemma sources_Cons_ipurge: "sources (a # ipurge u as) u = sources (a#as) u"
by (simp add: sources_Cons)

lemma sources_ipurgeD: 
  "v \<in> sources (ipurge u as) u \<Longrightarrow> v \<in> sources as u"
by (simp)

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

lemma ipurge_Cons [simp]: "ipurge u (a#as) = (if dom a \<in> sources (a#as) u
                          then [a] else []) @ ipurge u as"
by (simp add: ipurge_def)

lemma Nil_ipurge_sourcesD [rule_format]: 
  "[] = ipurge u bs \<longrightarrow> x \<in> sources bs u \<longrightarrow> x = u"
apply (induct "bs")
apply  (auto simp add: ipurge_def sources_Cons)
done

lemma Cons_ipurge_sourcesD: 
 "\<forall>bs. ipurge u as = ipurge u bs \<longrightarrow> sources as u = sources bs u \<Longrightarrow>
  a # ipurge u as = ipurge u bs \<longrightarrow> sources (a # as) u = sources bs u"
apply (induct "bs")
apply  (auto elim!: sources_subset_Cons [THEN subsetD])
apply    (drule spec, erule impE, rule refl, 
          simp add: sources_Cons split add: split_if_asm)+
done

lemma ipurge_sources_cong_lemma [rule_format]: 
 "\<forall>bs. ipurge u as = ipurge u bs \<longrightarrow> sources as u = sources bs u"
apply (induct "as")
apply  (auto simp add: intro: sources_refl dest: Nil_ipurge_sourcesD)
apply     (blast dest: Cons_ipurge_sourcesD)
apply    (blast dest: Cons_ipurge_sourcesD)
apply  (auto simp add: sources_Cons split add: split_if_asm)
done
(*>*)
lemma ipurge_sources_cong: 
  "ipurge u as = ipurge u bs \<Longrightarrow> sources as u = sources bs u"
(*<*)
by (erule ipurge_sources_cong_lemma)
(*>*)
lemma ipurge_idempotent(*<*) [simp](*>*): "ipurge u (ipurge u as) = ipurge u as"
(*<*)
apply (induct "as")
apply (simp_all)
apply clarify
apply (erule swap)
apply (simp add: dom_in_sources_Cons_eq_lemma)
done
(*>*)

constdefs --{* specical case of @{term ipurge} for transitive policies *}
  tpurge   :: "domain => action list => action list"
 "tpurge \<equiv> gen_purge tsources"
lemma tpurge_idempotent(*<*) [simp](*>*): "tpurge u (tpurge u as) = tpurge u as"
(*<*)
by (induct "as", simp_all add: tpurge_def tsources_def)
(*>*)
lemma "tpurge u = filter (\<lambda>a. (dom a \<leadsto> u))" 
(*<*)
by (rule ext, induct_tac "x", auto simp add: tpurge_def tsources_def)
(*>*)
lemma (in policy_trans) tpurge_conincides: "tpurge = ipurge"
(*<*)
apply (unfold ipurge_def tpurge_def)
apply (rule ext)+
apply (induct_tac "xa")
apply  (simp_all only: gen_purge.Nil gen_purge.Cons 
                 tsources_def dom_in_sources_Cons_eq mem_Collect_eq)
done
(*>*)
subsection "the deterministic case"

subsubsection "general version"

constdefs 
  noninterference :: "bool"
 "noninterference \<equiv> \<forall>as u. s0 \<simeq>as,u,ipurge u as\<simeq> s0"

constdefs --{* common structure of @{term "noninterference"} and @{text "noninfluence"} *}
  gen_noninterference :: "sourcef => bool"
 "gen_noninterference sf \<equiv>  
  \<forall>u as s t. s \<approx>sf as u\<approx> t \<longrightarrow> run as s \<sim>u\<sim> run (ipurge u as) t"

lemma output_consistent_and_gen_noninterference_implies_noninterference:
  "output_consistent \<Longrightarrow> gen_noninterference sf \<Longrightarrow> noninterference"
(*<*)
apply (simp add: gen_noninterference_def noninterference_def)
apply (blast intro: gen_uwr_s0 dest: output_consistentD obs_equivI)
done
(*>*)

constdefs 
  local_respect_left :: "bool"
 "local_respect_left \<equiv> \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> t"

  local_respect_right :: "bool"
 "local_respect_right \<equiv> \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> s \<sim>u\<sim> step a t"

  local_respect :: "bool"
 "local_respect \<equiv> local_respect_left \<and> local_respect_right"
(*<*)
lemma local_respect_leftD: 
  "\<lbrakk>local_respect_left; dom a \<notleadsto> u; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> step a s \<sim>u\<sim> t"
by (unfold local_respect_left_def, blast)

lemma local_respect_rightD: 
  "\<lbrakk>local_respect_right; dom a \<notleadsto> u; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> s \<sim>u\<sim> step a t"
by (unfold local_respect_right_def, blast)

lemma local_respectD: 
  "local_respect \<Longrightarrow> local_respect_left \<and> local_respect_right"
by (unfold local_respect_def, blast)

(*>*)

lemma (in uwr_refl) local_respect_classical: 
  "local_respect \<Longrightarrow> \<forall>a u s. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> step a s"
(*<*)
by (blast dest: local_respectD local_respect_rightD intro: uwr_refl)
(*>*)
lemma (in uwr_trans) classical_local_respect: 
  "\<forall>s u t. s \<sim>u\<sim> t \<longrightarrow> t \<sim>u\<sim> s \<Longrightarrow>
   \<forall>a u s. dom a \<notleadsto> u \<longrightarrow> s \<sim>u\<sim> step a s \<Longrightarrow> local_respect"
(*<*)
by (unfold local_respect_def local_respect_left_def local_respect_right_def,
    blast dest: uwr_trans)
(*>*)

lemma local_respect_implies_step_respect: "local_respect \<Longrightarrow> step_respect"
(*<*)
apply (unfold step_respect_def)
apply (clarify dest!: local_respectD)
apply (frule (2) local_respect_leftD)
apply (erule (2) local_respect_rightD)
done
(*>*)

lemma gen_noninterference_sources: --{* Rushby's Lemma 5 *}
 "weakly_step_consistent \<Longrightarrow> local_respect \<Longrightarrow> gen_noninterference sources"
(*<*)
apply (unfold gen_noninterference_def, rule, rule)
apply (induct_tac "as")
apply  (auto split del: split_if)
apply (drule spec, drule spec, erule mp)
apply (auto)
apply  (drule local_respect_implies_step_respect)
apply  (erule (2) sources_unwinding_step)
apply (rule gen_uwr_uwr)
apply  (erule sources_uwr_ConsD [THEN conjunct2])
apply (blast dest: local_respectD local_respect_leftD sources_trans)
done
(*>*)

theorem noninterference: --{* Rushby's Theorem 7 *}
"\<lbrakk>weakly_step_consistent; local_respect; output_consistent\<rbrakk> \<Longrightarrow> noninterference"
(*<*)
by (blast intro: gen_noninterference_sources
    output_consistent_and_gen_noninterference_implies_noninterference)

(*>*)
subsubsection "simple version"

constdefs
 step_consistent :: "bool" --{* new premise @{term "dom a \<leadsto> u"} *}
"step_consistent \<equiv> \<forall>a u s t. dom a \<leadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> step a s \<sim>u\<sim> step a t"

theorem simple_noninterference: --{* Rushby's Theorem 1 *}
 "step_consistent \<Longrightarrow> local_respect \<Longrightarrow> gen_noninterference singleton"
(*<*)
apply (simp add: gen_noninterference_def, rule, rule)
apply (induct_tac "as")
apply  (auto split del: split_if)
apply (drule spec, drule spec, erule mp)
apply (auto)
apply  (case_tac "dom a \<leadsto> u")
apply   (simp add: step_consistent_def)
apply  (blast 
         dest: local_respect_implies_step_respect [THEN step_respectD])
apply (blast dest: rev_sources_direct local_respectD local_respect_leftD)
done

lemma simple_noninterference_implies_gen_noninterference_sources:
  "gen_noninterference singleton \<Longrightarrow> gen_noninterference sources"
by (unfold gen_noninterference_def, 
    blast intro: gen_uwr_mono [OF _ singleton_subset_sources])

(*>*)
subsubsection "strong version"
(*
constdefs
  strong_gen_noninterference :: "sourcef => bool"
 "strong_gen_noninterference sf \<equiv> \<forall>u as s t bs. s \<approx>sf as u\<approx> t \<longrightarrow> 
   gen_purge sf u as = gen_purge sf u bs \<longrightarrow> run as s \<sim>u\<sim> run bs t"

lemma gen_purge_nilD [rule_format]: "local_respect_right \<Longrightarrow> 
  [] = gen_purge sf u bs \<longrightarrow> (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> s \<sim>u\<sim> run bs t)"
apply (induct "bs")
apply  (simp_all)
apply (clarify)
apply (drule sym, erule (1) impE)
apply (drule spec, erule mp)
#
apply (blast dest: local_respect_rightD rev_sources_direct)
done

lemma gen_purge_consD [rule_format]: 
 "local_respect_right \<Longrightarrow> a # as = ipurge u bs  \<longrightarrow>
  (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> (\<forall>t. s \<approx>sources (a#as) u\<approx> t \<longrightarrow> s \<approx>sources (a#as) u\<approx> run bsa t) \<and> as = ipurge u bsc)"
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (clarsimp)
apply (drule spec, erule mp)
apply (blast dest: local_respect_rightD rev_sources_trans gen_unwindingD
       intro!: gen_unwindingI)
done

lemma strong_noninterference:
 "weakly_step_consistent \<Longrightarrow> local_respect \<Longrightarrow> strong_noninterference"
apply (subgoal_tac "\<forall>u as bs s t. ipurge u as = ipurge u bs \<longrightarrow> 
                    s \<approx>sources as u\<approx> t \<longrightarrow> run as s \<sim>u\<sim> run bs t")
apply  (unfold strong_noninterference_def, blast)
apply (rule, rule, simp)
apply (frule local_respectD, erule conjE)
apply (induct_tac "as")
apply  (auto)
apply   (erule (2) ipurge_nilD)
apply  (frule (1) ipurge_consD, clarify)
apply  (drule spec, erule (1) impE)
apply  (thin_tac "a # ?as = ipurge u ?bs")
apply  (thin_tac "ipurge u list = ipurge u bsc")
apply  (simp add: sources_Cons_ipurge)
apply  (drule spec, drule spec, erule mp)
apply  (drule spec, erule (1) impE)
apply  (drule local_respect_implies_step_respect)
apply  (blast dest: sources_unwinding_step) 
apply (drule spec, erule impE, rule refl)
apply (drule spec, drule spec, erule mp)
apply (drule sources_unwinding_ConsD [THEN conjunct2])
apply (rule gen_unwindingI)
apply (blast dest: local_respect_leftD gen_unwindingD rev_sources_trans)
done
*)
constdefs
  strong_noninterference :: "bool"
 "strong_noninterference \<equiv> \<forall>as u bs. ipurge u as = ipurge u bs \<longrightarrow> s0 \<simeq>as,u,bs\<simeq> s0"

lemma strong_noninterference_implies_noninterference:
 "strong_noninterference \<Longrightarrow> noninterference"
(*<*)
apply (unfold strong_noninterference_def noninterference_def obs_equiv_def)
apply (clarify)
apply (drule spec)+
apply (erule mp)
apply (simp only: ipurge_idempotent)
done

lemma gen_noninterference_sources_left [rule_format]:
"weakly_step_consistent \<Longrightarrow> local_respect \<Longrightarrow> 
\<forall>u as s t. s \<approx>sources as u\<approx> t \<longrightarrow> run (ipurge u as) s \<sim>u\<sim> run as t"
apply (rule, rule)
apply (induct_tac "as")
apply  (auto split del: split_if)
apply (drule spec, drule spec, erule mp)
apply (auto)
apply  (drule local_respect_implies_step_respect)
apply  (erule (2) sources_unwinding_step)
apply (rule gen_uwr_uwr)
apply  (erule sources_uwr_ConsD [THEN conjunct2])
apply (blast dest: local_respectD local_respect_rightD 
             intro: sources_trans)
done

lemma strong_noninterference00:
"\<lbrakk>weakly_step_consistent; local_respect; output_consistent\<rbrakk> \<Longrightarrow> strong_noninterference"
apply (unfold strong_noninterference_def obs_equiv_def, clarify)
apply (rule trans)
defer 1
apply  (erule output_consistentD)
apply  (erule (1) gen_noninterference_sources_left)
apply  (rule gen_uwr_s0)
apply (erule output_consistentD)
apply (drule (1) gen_noninterference_sources)
apply (drule sym)
apply (simp add: gen_noninterference_def gen_uwr_s0)
done

lemma strong_noninterference0:
"output_consistent \<Longrightarrow> gen_noninterference sources \<Longrightarrow> strong_noninterference"
apply (unfold strong_noninterference_def obs_equiv_def gen_noninterference_def)
apply (clarify)
apply (rule trans)
apply  (erule output_consistentD)
apply  (blast intro: gen_uwr_s0)
apply (rule sym)
apply (erule output_consistentD)
apply (simp add: gen_uwr_s0)
done
(*>*)

lemma ipurge_nilD [rule_format]: "local_respect_right \<Longrightarrow> 
  [] = ipurge u bs \<longrightarrow> (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> s \<sim>u\<sim> run bs t)"
(*<*)
apply (induct "bs")
apply  (simp_all)
apply (blast intro: sym 
       dest: local_respect_rightD rev_sources_direct)
done

lemma ipurge_consD0 [rule_format]: --{* unused *}
 "local_respect_right \<Longrightarrow> a # as = ipurge u bs \<longrightarrow> 
   (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> as = ipurge u bsc \<and> 
   (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> s \<sim>u\<sim> run bsa t))"
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (simp)
apply (blast dest: local_respect_rightD rev_sources_direct)
done
(*>*)

lemma ipurge_consD [rule_format]: 
 "local_respect_right \<Longrightarrow> a # as = ipurge u bs  \<longrightarrow>
  (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> as = ipurge u bsc \<and> 
(\<forall>t. s \<approx>sources (a#as) u\<approx> t \<longrightarrow> s \<approx>sources (a#as) u\<approx> run bsa t))"
(*<*)
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (clarsimp)
apply (drule spec, erule mp)
apply (drule rev_sources_trans)
apply (blast dest: local_respect_rightD gen_uwrD intro!: gen_uwrI)
done
(*>*)

theorem strong_noninterference:
 "\<lbrakk>weakly_step_consistent; local_respect; output_consistent\<rbrakk> \<Longrightarrow> strong_noninterference"
(*<*)
apply (subgoal_tac "\<forall>u as bs s t. ipurge u as = ipurge u bs \<longrightarrow> 
                    s \<approx>sources as u\<approx> t \<longrightarrow> run as s \<sim>u\<sim> run bs t")
apply  (unfold strong_noninterference_def obs_equiv_def)
apply  (fast elim!: output_consistentD intro: gen_uwr_s0)
apply (rule, rule, simp)
apply (frule local_respectD)
apply (induct_tac "as")
apply  (auto)
apply   (erule (2) ipurge_nilD)
apply  (frule (1) ipurge_consD, clarify)
apply  (drule spec, erule (1) impE)
apply  (thin_tac "a # ?as = ipurge u ?bs")
apply  (thin_tac "ipurge u list = ipurge u bsc")
apply  (simp add: sources_Cons_ipurge)
apply  (drule spec, drule spec, erule mp)
apply  (drule spec, erule (1) impE)
apply  (drule local_respect_implies_step_respect)
apply  (blast dest: sources_unwinding_step) 
apply (drule spec, erule impE, rule refl)
apply (drule spec, drule spec, erule mp)
apply (drule sources_uwr_ConsD [THEN conjunct2])
apply (rule gen_uwrI)
apply (blast dest: local_respect_leftD gen_uwrD rev_sources_trans)
done
(*>*)
(*
subsubsection "access control interpretation"

typedecl "name"
typedecl "value"
consts contents :: "state => name => value"

consts observe :: "domain => name set"
       alter   :: "domain => name set"

defs uwr_def: "s \<sim>u\<sim> t \<equiv> \<forall>n\<in>observe u. contents s n = contents t n"

locale canonical_output = --{* special case: all observable values are output *}
  fixes value2output :: "value => output" --{* type coercion *}
  assumes output_def: 
     "output u s \<equiv> {value2output (contents s n) |n. n \<in> observe u}"
lemma (in canonical_output) canonical_output_consistent: "output_consistent"
*)(*<*)
(*apply (auto simp add: output_consistent_def uwr_def output_def)
apply (rule_tac x = "n" in exI)
apply (simp)
done
*)(*>*)
(*
constdefs --{* Reference Monitor Assumptions *}
  RMA1 :: "bool"
 "RMA1 \<equiv> output_consistent"

  RMA2 :: "bool" --{* new premises @{term "dom a \<leadsto> u"}, @{term "s \<sim>u\<sim> t"}, and @{term "n \<in> observe u"} *}
 "RMA2 \<equiv> \<forall>a u s t n. s \<sim>dom a\<sim> t \<longrightarrow> dom a \<leadsto> u \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> n \<in> observe u \<longrightarrow> 
                      (contents (step a s) n \<noteq> contents s n \<or> 
                       contents (step a t) n \<noteq> contents t n) \<longrightarrow> 
                       contents (step a s) n = contents (step a t) n"

  RMA3 :: "bool"
 "RMA3 \<equiv> \<forall>a s n. contents (step a s) n \<noteq> contents s n \<longrightarrow> n \<in> alter (dom a)"

  AC_policy_consistent :: "bool"
 "AC_policy_consistent \<equiv> \<forall>u v. alter u \<inter> observe v \<noteq> {} \<longrightarrow> u \<leadsto> v"
*)(*<*)
(*lemma AC_policy_consistent_revD: 
  "AC_policy_consistent \<Longrightarrow> n \<in> observe v \<Longrightarrow> u \<notleadsto> v \<Longrightarrow> n \<notin> alter u"
by (unfold AC_policy_consistent_def, blast)

lemma AC_unwinding_weakly_step_consistentI:
  "(!!a u s t n. \<lbrakk>dom a \<leadsto> u; s \<sim>dom a\<sim> t; s \<sim>u\<sim> t; n \<in> observe u; 
                  contents (step a s) n \<noteq> contents s n \<or> 
                  contents (step a t) n \<noteq> contents t n\<rbrakk> \<Longrightarrow> 
                  contents (step a s) n = contents (step a t) n)
 \<Longrightarrow> weakly_step_consistent"
apply (clarsimp simp add: weakly_step_consistent_def uwr_def)
apply (case_tac "contents (step a s) n = contents s n \<and> 
                 contents (step a t) n = contents t n")
apply  (auto)
done
(*>*)

lemma RMA2_implies_weakly_step_consistent: "RMA2 \<Longrightarrow> weakly_step_consistent"
(*<*)
by (rule AC_unwinding_weakly_step_consistentI, simp add: RMA2_def)
(*>*)

lemma RMA3_AC_policy_consistent_implies_local_respect: 
  "RMA3 \<Longrightarrow> AC_policy_consistent \<Longrightarrow> local_respect"
(*<*)
apply (unfold RMA3_def uwr_def
       local_respect_def local_respect_left_def local_respect_right_def)
apply (safe)
apply  (drule (1) bspec, drule sym, simp, blast dest: AC_policy_consistent_revD)
apply (drule (1) bspec, simp, blast dest: sym AC_policy_consistent_revD)
done
(*>*)

theorem access_control_secure: 
  "\<lbrakk>RMA1; RMA2; RMA3; AC_policy_consistent\<rbrakk> \<Longrightarrow> noninterference"
(*<*)
by (auto simp: RMA1_def 
 intro!: noninterference RMA2_implies_weakly_step_consistent
 elim: RMA3_AC_policy_consistent_implies_local_respect)

(*>*)
*)
subsection "the nondeterministic case"

constdefs 
  Noninterference :: "bool"
 "Noninterference \<equiv> \<forall>as u bs. ipurge u as = ipurge u bs \<longrightarrow> s0 \<lesssim>as,u,bs\<lesssim> s0"

  gen_Noninterference :: "sourcef => bool"
 "gen_Noninterference sf \<equiv> \<forall>as bs s s' u t. ipurge u as = ipurge u bs \<longrightarrow> 
         (s, s') \<in> Run as \<longrightarrow> s \<approx>sf as u\<approx> t \<longrightarrow> 
   (\<exists>t'. (t, t') \<in> Run bs \<and> s' \<sim>u\<sim> t')"
lemma 
  output_consistent_and_gen_Noninterference_implies_Noninterference:
  "output_consistent \<Longrightarrow> gen_Noninterference sf \<Longrightarrow> Noninterference"
(*<*)
apply (unfold Noninterference_def gen_Noninterference_def)
apply (blast intro: gen_uwr_s0 dest: output_consistentD obs_POI)
done
(*>*)
subsubsection "simple version"

constdefs 
  Local_respect_left :: "bool"
 "Local_respect_left \<equiv> \<forall>a u s t s'. dom a \<notleadsto> u \<longrightarrow> 
  s \<sim>u\<sim> t \<longrightarrow> (s, s') \<in> Step a \<longrightarrow> s' \<sim>u\<sim> t"

  Local_respect_right :: "bool"
 "Local_respect_right \<equiv> \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> 
  s \<sim>u\<sim> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> s \<sim>u\<sim> t')"
(*<*)
lemma Local_respect_leftD: 
 "\<lbrakk>Local_respect_left; dom a \<notleadsto> u; (s, s') \<in> Step a; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t" 
by (unfold Local_respect_left_def, blast)

lemma Local_respect_rightD: 
  "\<lbrakk>Local_respect_right; dom a \<notleadsto> u; s \<sim>u\<sim> t\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> Step a \<and> s \<sim>u\<sim> t'"
by (unfold Local_respect_right_def, blast)
(*>*)

lemma Local_respect_implies_Step_respect:
 "\<lbrakk>Local_respect_left; Local_respect_right\<rbrakk> \<Longrightarrow> Step_respect"
(*<*)
by (unfold Step_respect_def, blast dest: Local_respect_leftD Local_respect_rightD)
(*>*)

lemma (in uwr_refl) Local_respect_left_Mantel: 
  "Local_respect_left \<Longrightarrow> 
   \<forall>a u s t s'. dom a \<notleadsto> u \<longrightarrow> (s, s') \<in> Step a \<longrightarrow> s' \<sim>u\<sim> s"
(*<*)
by (blast dest: Local_respect_leftD intro: uwr_refl)
(*>*)

lemma (in uwr_refl) Local_respect_right_Mantel: 
  "Local_respect_right \<Longrightarrow> 
   \<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> t \<sim>u\<sim> t')"
(*<*)
by (blast dest: Local_respect_rightD intro: uwr_refl)
(*>*)

lemma (in uwr_trans) Mantel_Local_respect_left: 
  "\<forall>a u s t s'. dom a \<notleadsto> u \<longrightarrow> (s, s') \<in> Step a \<longrightarrow> s' \<sim>u\<sim> s \<Longrightarrow> 
   Local_respect_left"
(*<*)
by (unfold Local_respect_left_def, blast dest: uwr_trans)
(*>*)

lemma (in uwr_trans) Mantel_Local_respect_right: 
  "\<forall>a u s t. dom a \<notleadsto> u \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> t \<sim>u\<sim> t') \<Longrightarrow> 
   Local_respect_right"
(*<*)
by (unfold Local_respect_right_def, blast dest: uwr_trans)
(*>*)

lemma ipurge_NilD [rule_format]: "Local_respect_right \<Longrightarrow> 
  [] = ipurge u bs \<longrightarrow> (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Run bs \<and> s \<sim>u\<sim> t'))"
(*<*)
apply (induct "bs")
apply  (simp_all)
apply (blast intro: sym 
       dest: Local_respect_rightD rev_sources_direct)
done
(*>*)

lemma ipurge_ConsD [rule_format]: "Local_respect_right \<Longrightarrow> 
  a # as = ipurge u bs \<longrightarrow> (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> as = ipurge u bsc \<and>
  (\<forall>t. s \<sim>u\<sim> t \<longrightarrow> (\<exists>ta. (t, ta) \<in> Run bsa \<and> s \<sim>u\<sim> ta)))"
(*<*)
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (simp)
apply (blast dest: Local_respect_rightD rev_sources_direct)
done

theorem simple_Noninterference_lemma: 
 "Step_consistent \<Longrightarrow> Local_respect_left \<Longrightarrow> Local_respect_right \<Longrightarrow> 
  gen_Noninterference singleton"
apply (subgoal_tac "\<forall>u as s' s bs t. (s, s')\<in>Run as \<longrightarrow> 
                    ipurge u as = ipurge u bs \<longrightarrow> s \<sim>u\<sim> t \<longrightarrow> 
                  (\<exists>t'. (t, t')\<in>Run bs \<and> s' \<sim>u\<sim> t')")
apply  (simp add: gen_Noninterference_def)
apply (rule, rule, rule, simp)
apply (induct_tac "as")
apply (auto split del: split_if)
apply  (fast elim!: ipurge_NilD)
apply (rename_tac sa sb sc bs t)
apply (drule spec, erule (1) impE)
apply (simp split add: split_if_asm)
apply  (frule (1) ipurge_ConsD, clarify)
apply  (drule spec, erule (1) impE)
apply  (thin_tac "a # ?as = ipurge u ?bs")
apply  (thin_tac "ipurge u list = ipurge u bsc")
apply  (simp)
apply  (drule spec, erule (1) impE, clarify)
apply  (drule (1) Local_respect_implies_Step_respect) 
apply  (thin_tac "sa \<sim>u\<sim> t")
apply  (drule (3) simple_unwinding_Step, blast)
apply (blast dest: rev_sources_direct Local_respect_leftD)
done
(*>*)

theorem simple_Noninterference: 
 "Step_consistent \<Longrightarrow> Local_respect_left \<Longrightarrow> Local_respect_right \<Longrightarrow> 
  output_consistent \<Longrightarrow> Noninterference"
(*<*)
apply (drule (2) simple_Noninterference_lemma)
apply (simp add: Noninterference_def gen_Noninterference_def)
apply (blast intro: uwr_s0 dest: output_consistentD obs_POI)
done
(*>*)

subsubsection "uniform version"

constdefs
  uni_Local_respect_right :: "bool"
 "uni_Local_respect_right \<equiv> \<forall>a us s t. \<not>(\<exists>u\<in>us. dom a \<leadsto> u) \<longrightarrow> (\<exists>u. u\<in>us) \<longrightarrow>
  s \<approx>us\<approx> t \<longrightarrow> (\<exists>t'. (t, t') \<in> Step a \<and> s \<approx>us\<approx> t')"
 
  uni_Local_respect :: "bool"
 "uni_Local_respect \<equiv> Local_respect_left \<and> uni_Local_respect_right"

lemma uni_Local_respect_leftD: "\<lbrakk>Local_respect_left; 
  (s, s') \<in> Step a; \<not>(\<exists>u\<in>us. dom a \<leadsto> u); s \<approx>us\<approx> t\<rbrakk> \<Longrightarrow> s' \<approx>us\<approx> t" 
(*<*)
apply (rule gen_uwrI)
apply (drule (1) gen_uwrD)
apply (blast dest: Local_respect_leftD)
done

lemma uni_Local_respect_rightD: 
  "\<lbrakk>uni_Local_respect_right; \<not>(\<exists>u\<in>us. dom a \<leadsto> u); u\<in>us; s \<approx>us\<approx> t\<rbrakk> \<Longrightarrow> 
    \<exists>t'. (t, t') \<in> Step a \<and> s \<approx>us\<approx> t'"
by (unfold uni_Local_respect_right_def, blast)

lemma uni_Local_respectD: 
  "uni_Local_respect \<Longrightarrow> Local_respect_left \<and> uni_Local_respect_right"
by (unfold uni_Local_respect_def, blast)
(*>*)

lemma uni_Local_respect_right_implies_Local_respect_right: 
  "uni_Local_respect_right \<Longrightarrow> Local_respect_right"
(*<*)
apply (unfold Local_respect_right_def uni_Local_respect_right_def, clarify)
apply (drule spec, drule_tac x = "{u}" in spec, auto)
done
(*>*)

lemma uni_Local_respect_implies_uni_Step_respect: 
  "uni_Local_respect \<Longrightarrow> uni_Step_respect"
(*<*)
by (unfold uni_Step_respect_def, blast dest: uni_Local_respectD 
    uni_Local_respect_leftD uni_Local_respect_rightD)
(*>*)

lemma uni_ipurge_ConsD [rule_format]: "uni_Local_respect_right \<Longrightarrow> 
  a # as = ipurge u bs \<longrightarrow> (\<exists>bsa bsc. bs = bsa @ a # bsc \<and> as = ipurge u bsc \<and> 
  (\<forall>t. s \<approx>sources (a#as) u\<approx> t \<longrightarrow> (\<exists>ta. (t, ta) \<in> Run bsa \<and> s \<approx>sources (a#as) u\<approx> ta)))"
(*<*)
apply (induct "bs") 
apply  (simp_all)
apply (rule conjI)
apply  (clarify, rule_tac x = "[]" in exI, simp)
apply (clarsimp)
apply (rule exI)+
apply (rule conjI)
apply  (rule append_Cons [symmetric])
apply (clarsimp)
apply (drule rev_sources_trans)
apply (drule (1) uni_Local_respect_rightD, rule sources_refl, erule asm_rl)
apply (blast)
done
(*>*)

lemma gen_Noninterference_sources: 
 "uni_Step_consistent \<Longrightarrow> uni_Local_respect \<Longrightarrow> gen_Noninterference sources"
(*<*)
apply (subgoal_tac "\<forall>u as s' s bs t. (s, s')\<in>Run as \<longrightarrow> 
                    ipurge u as = ipurge u bs \<longrightarrow> s \<approx>sources as u\<approx> t \<longrightarrow> 
                  (\<exists>t'. (t, t')\<in>Run bs \<and> s' \<sim>u\<sim> t')")
apply  (unfold gen_Noninterference_def, blast)
apply (rule, rule, rule, simp)
apply (frule uni_Local_respectD, erule conjE)
apply (induct_tac "as")
apply  (auto split del: split_if)
apply  (drule uni_Local_respect_right_implies_Local_respect_right)
apply  (fast elim!: ipurge_NilD)
apply (rename_tac sa sb sc bs t)
apply (drule spec, erule (1) impE)
apply (simp split add: split_if_asm)
apply  (frule (1) uni_ipurge_ConsD, clarify)
apply  (drule spec, erule (1) impE)
apply  (thin_tac "a # ?as = ipurge u ?bs")
apply  (thin_tac "ipurge u list = ipurge u bsc")
apply  (simp add: sources_Cons_ipurge)
apply  (drule spec, erule (1) impE, clarify)
apply  (drule uni_Local_respect_implies_uni_Step_respect)
apply  (thin_tac "sa \<approx>sources (a # list) u\<approx> t")
apply  (drule (3) sources_unwinding_Step) 
apply  (blast)
apply (drule spec, erule impE, rule refl) 
apply (drule sources_uwr_ConsD [THEN conjunct2])
apply (blast dest: uni_Local_respect_leftD rev_sources_trans)
done
(*>*)

theorem Noninterference: "uni_Step_consistent \<Longrightarrow> 
 uni_Local_respect \<Longrightarrow> output_consistent \<Longrightarrow> Noninterference"
(*<*)
by (blast intro: gen_Noninterference_sources 
    output_consistent_and_gen_Noninterference_implies_Noninterference)

end
(*>*)