Theory inout

(*
   Title: Theory  inout.thy
   Author:    Maria Spichkova <maria.spichkova at rmit.edu.au>, 2014
*)
 
section ‹Correctness of the relations between sets of Input/Output channels›
 
theory  inout 
imports Secrecy_types
begin

consts 
  subcomponents ::  "specID ⇒ specID set"

― ‹Mappings, defining sets of input, local, and output channels›
― ‹of a component›
consts
  ins :: "specID ⇒ chanID set"
  loc :: "specID ⇒ chanID set"
  out :: "specID ⇒ chanID set"

― ‹Predicate insuring the correct mapping from the component identifier›
― ‹to the set of input channels of a component›
definition
  inStream :: "specID ⇒ chanID set ⇒ bool"
where
  "inStream x y  ≡ (ins x = y)"

― ‹Predicate insuring the correct mapping from the component identifier›
― ‹to the set of local channels of a component›
definition
  locStream :: "specID ⇒ chanID set ⇒ bool"
where
  "locStream x y ≡ (loc x = y)"

― ‹Predicate insuring the correct mapping from the component identifier›
― ‹to the set of output channels of a component›
definition
  outStream :: "specID ⇒ chanID set ⇒ bool"
where
  "outStream x y ≡ (out x = y)"

― ‹Predicate insuring the correct relations between›
― ‹to the set of input, output and local channels of a component›
definition
  correctInOutLoc :: "specID ⇒ bool"
where
  "correctInOutLoc x ≡ 
   (ins x) ∩ (out x) = {} 
    ∧ (ins x) ∩ (loc x) = {} 
    ∧ (loc x) ∩ (out x) = {} " 

― ‹Predicate insuring the correct relations between›
― ‹sets of input channels within a composed component›
definition
  correctCompositionIn :: "specID ⇒ bool"
where
  "correctCompositionIn x ≡ 
  (ins x) = (⋃ (ins ` (subcomponents x)) - (loc x))
  ∧ (ins x) ∩ (⋃ (out ` (subcomponents x))) = {}" 

― ‹Predicate insuring the correct relations between›
― ‹sets of output channels within a composed component›
definition
  correctCompositionOut :: "specID ⇒ bool"
where
  "correctCompositionOut x ≡ 
  (out x) = (⋃ (out ` (subcomponents x))- (loc x))
  ∧ (out x) ∩ (⋃ (ins ` (subcomponents x))) = {} " 

― ‹Predicate insuring the correct relations between›
― ‹sets of local channels within a composed component›
definition
  correctCompositionLoc :: "specID ⇒ bool"
where
  "correctCompositionLoc x ≡ 
   (loc x) = ⋃ (ins ` (subcomponents x))
           ∩ ⋃ (out ` (subcomponents x))" 

― ‹If a component is an elementary one (has no subcomponents)›
― ‹its set of local channels should be empty›
lemma subcomponents_loc:
assumes "correctCompositionLoc x"
       and "subcomponents x = {}"
shows "loc x = {}"
using assms by (simp add: correctCompositionLoc_def)

end