(*  Title:      NI/Noninfluence.thy
    Id:         $Id: Noninfluence.thy,v 1.6 2004/01/29 17:36:47 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2003 Siemens AG; any non-commercial use is granted

*)
header {* Noninfluence *}

(*<*)
theory Noninfluence imports Noninterference Nonleakage begin

(*>*)
subsection "the deterministic case"

constdefs
  noninfluence :: "bool" 
 "noninfluence \<equiv> \<forall>as u s t. s \<approx>sources as u\<approx> t \<longrightarrow> s \<simeq>as,u,ipurge u as\<simeq> t"

lemma noninfluence_implies_noninterference: "noninfluence \<Longrightarrow> noninterference"
(*<*)
apply (unfold noninfluence_def noninterference_def)
apply (blast intro: gen_uwr_s0)
done
(*>*)

theorem noninfluence:
  "\<lbrakk>weakly_step_consistent; local_respect; output_consistent\<rbrakk> \<Longrightarrow> noninfluence"
(*<*)
apply (drule (1) gen_noninterference_sources)
apply (unfold gen_noninterference_def noninfluence_def obs_equiv_def)
apply (blast dest: output_consistentD)
done
(*>*)

subsection "the nondeterministic case"

constdefs
  Noninfluence :: "bool" 
 "Noninfluence \<equiv> 
  \<forall>as bs u s t. s \<approx>sources as u\<approx> t \<longrightarrow> ipurge u as = ipurge u bs \<longrightarrow> s \<lesssim>as,u,bs\<lesssim> t"

lemma Noninfluence_implies_Noninterference: "Noninfluence \<Longrightarrow> Noninterference"
(*<*)
apply (unfold Noninfluence_def Noninterference_def)
apply (blast intro: gen_uwr_s0)
done
(*>*)

theorem Noninfluence:
  "\<lbrakk>uni_Step_consistent; uni_Local_respect; output_consistent\<rbrakk> \<Longrightarrow> Noninfluence"
(*<*)
apply (drule (1) gen_Noninterference_sources)
apply (unfold gen_Noninterference_def Noninfluence_def obs_PO_def)
apply (blast dest: output_consistentD)
done

end
(*>*)