Theory DataDependencies

(*<*)
(*
   Title:  Theory  DataDependencies.thy
   Author: Maria Spichkova <maria.spichkova at rmit.edu.au>, 2014
*)
(*>*)

section "Inter-/Intracomponent dependencies"
 
theory DataDependencies
  imports DataDependenciesConcreteValues
begin

― ‹component and its subcomponents should be defined on different abstraction levels›
definition
correctCompositionDiffLevels :: "CSet  bool"
where 
  "correctCompositionDiffLevels S  
    C   subcomp S.  i. S  AbstrLevel i  C  AbstrLevel i"

― ‹General system's property: for all abstraction levels and all components should hold›
― ‹component and its subcomponents should be defined on different abstraction levels›
definition
correctCompositionDiffLevelsSYSTEM :: "bool"
where 
  "correctCompositionDiffLevelsSYSTEM  
   ( S::CSet. (correctCompositionDiffLevels S))"

― ‹if a local variable belongs to one of the subcomponents, it also belongs to the composed component›
definition
correctCompositionVAR ::  "CSet  bool"
where
  "correctCompositionVAR S  
    C   subcomp S.  v  VAR C.  v  VAR S"

― ‹General system's property: for all abstraction levels and all components should hold›
― ‹if a local variable belongs to one of the subcomponents, it also belongs to the composed component›
definition
correctCompositionVARSYSTEM ::  "bool"
where
  "correctCompositionVARSYSTEM  
   ( S::CSet. (correctCompositionVAR S))"

― ‹after correct decomposition of a component each of its local variable can belong only to one of its subcomponents›
definition
correctDeCompositionVAR ::  "CSet  bool"
where
  "correctDeCompositionVAR S  
    v  VAR S.   C1   subcomp S.  C2   subcomp S. v  VAR C1  v  VAR C2  C1 = C2"

― ‹General system's property: for all abstraction levels and all components should hold›
― ‹after correct decomposition of a component each of its local variable can belong only to one of its subcomponents›
definition
correctDeCompositionVARSYSTEM ::  "bool"
where
  "correctDeCompositionVARSYSTEM  
  ( S::CSet. (correctDeCompositionVAR S))"

― ‹if x is an output channel of a  component C on some anstraction level, 
it cannot be an output of another component on the same level›
definition
correctCompositionOUT ::  "chanID  bool"
where
  "correctCompositionOUT x  
    C i. x  OUT C  C  AbstrLevel i   ( S  AbstrLevel i. x  OUT S)"

― ‹General system's property: for all abstraction levels and all channels should hold›
definition
correctCompositionOUTSYSTEM ::  "bool"
where
  "correctCompositionOUTSYSTEM  ( x. correctCompositionOUT x)"

― ‹if X is a subcomponent of a  component C on some anstraction level, 
it cannot be a subcomponent of another component on the same level›
definition
correctCompositionSubcomp ::  "CSet  bool"
where
  "correctCompositionSubcomp X  
    C i. X  subcomp C  C  AbstrLevel i   ( S  AbstrLevel i. (S  C  X  subcomp S))"

― ‹General system's property: for all abstraction levels and all components should hold›
definition
correctCompositionSubcompSYSTEM ::  "bool"
where
  "correctCompositionSubcompSYSTEM  ( X. correctCompositionSubcomp X)"

― ‹If a component belongs is defined in the set CSet, 
it should belong to at least one abstraction level›
definition
allComponentsUsed ::  "bool"
where
  "allComponentsUsed    C.  i.  C  AbstrLevel i"

― ‹if a component does not have any local variables, none of its subcomponents has any local variables›
lemma correctDeCompositionVARempty:
  assumes "correctCompositionVAR S" 
          and "VAR S = {}"
  shows    " C   subcomp S. VAR C = {}"
using assms by (metis all_not_in_conv correctCompositionVAR_def)


― ‹function OUTfrom maps channel ID to the set of input channels it depends from,›
― ‹directly (OUTfromCh) or via local variables (VARfrom)› 
― ‹an empty set means that the channel is either input of the system or›
― ‹its values are generated within some component independently›
definition OUTfrom ::  "chanID  chanID set"
where
 "OUTfrom x  (OUTfromCh x)  {y.  v. v  (OUTfromV x)  y  (VARfrom v)}"
 
― ‹if x depends from some input channel(s) directly, then exists›
― ‹a component which has them as input channels and x as an output channel›
definition
  OUTfromChCorrect :: "chanID  bool"
where
  "OUTfromChCorrect x 
   (OUTfromCh x  {}  
      ( Z . (x  (OUT Z)  ( y  (OUTfromCh x). y  IN Z) )))"

― ‹General system's property: for channels in the system should hold:›
― ‹if x depends from some input channel(s) directly, then exists›
― ‹a component which has them as input channels and x as an output channel›
definition
  OUTfromChCorrectSYSTEM :: "bool"
where
  "OUTfromChCorrectSYSTEM  ( x::chanID. (OUTfromChCorrect x))"


― ‹if x depends from some local variables, then exists a component›
― ‹to which these variables belong and which has  x as an output channel›
definition
  OUTfromVCorrect1 :: "chanID  bool"
where
  "OUTfromVCorrect1 x 
   (OUTfromV x  {}  
      ( Z . (x  (OUT Z)  ( v  (OUTfromV x). v  VAR Z) )))"

― ‹General system's property: for channels in the system should hold the above property:›
definition
  OUTfromVCorrect1SYSTEM :: "bool"
where
  "OUTfromVCorrect1SYSTEM  ( x::chanID. (OUTfromVCorrect1 x))"

― ‹if x does not depend from any local variables, then it does not belong to any set VARfrom›
definition
  OUTfromVCorrect2 :: "chanID  bool"
where
  "OUTfromVCorrect2 x 
   (OUTfromV x = {}  ( v::varID. x  (VARto v)) )"

― ‹General system's property: for channels in the system should hold the above property:› 
definition
  OUTfromVCorrect2SYSTEM :: "bool"
where
  "OUTfromVCorrect2SYSTEM   ( x::chanID. (OUTfromVCorrect2 x))"

― ‹General system's property:›
― ‹definitions OUTfromV and VARto should give equivalent mappings›
definition
  OUTfromV_VARto :: "bool"
where
  "OUTfromV_VARto 
   ( x::chanID.  v::varID. (v  OUTfromV x  x  (VARto v)) )"

― ‹General system's property for abstraction levels 0 and 1›
― ‹if a variable v belongs to a component, then all the channels v›
― ‹depends from should be input channels of this component›
definition
  VARfromCorrectSYSTEM :: "bool"
where
  "VARfromCorrectSYSTEM 
   ( v::varID.  Z ((AbstrLevel level0)  (AbstrLevel level1)). 
     ( (v  VAR Z)   ( x  VARfrom v. x  IN Z) ))"

― ‹General system's property for abstraction levels 0 and 1›
― ‹if a variable v belongs to a component, then all the channels v›
― ‹provides value to should be input channels of this component›
definition
  VARtoCorrectSYSTEM :: "bool"
where
  "VARtoCorrectSYSTEM 
   ( v::varID.  Z  ((AbstrLevel level0)  (AbstrLevel level1)). 
     ( (v  VAR Z)    ( x  VARto v. x  OUT Z)))"

― ‹to detect local variables, unused for computation of any output› 
definition
  VARusefulSYSTEM :: "bool"
where
  "VARusefulSYSTEM  ( v::varID. (VARto v  {}))"

lemma
  OUTfromV_VARto_lemma: 
 assumes "OUTfromV x  {}"  and "OUTfromV_VARto"
 shows    " v::varID. x  (VARto v)" 
 using assms by (simp add: OUTfromV_VARto_def, auto)

(*<*)
(*>*)
subsection ‹Direct and indirect data dependencies between components›

― ‹The component C should be defined on the same abstraction›
― ‹level we are seaching for its direct or indirect sources,›
― ‹otherwise we get an empty set as result›
definition
  DSources :: "AbstrLevelsID  CSet  CSet set"
where
 "DSources i C  {Z.   x. x  (IN C)  x  (OUT Z)  Z  (AbstrLevel i)  C  (AbstrLevel i)}"

lemma DSourcesLevelX:
"(DSources i X)   (AbstrLevel i)" 
by (simp add: DSources_def, auto)

― ‹The component C should be defined on the same abstraction level we are› 
― ‹seaching for its direct or indirect acceptors (coponents, for which C is a source),›
― ‹otherwise we get an empty set as result›
definition
  DAcc :: "AbstrLevelsID  CSet  CSet set"
where
 "DAcc i C  {Z.   x. x  (OUT C)  x  (IN Z)  Z  (AbstrLevel i)  C  (AbstrLevel i)}"

axiomatization
  Sources :: "AbstrLevelsID  CSet  CSet set"
where 
SourcesDef:
"(Sources i C) = (DSources i C)  ( S  (DSources i C). (Sources i S))" 
and
SourceExistsDSource:
"S  (Sources i C)  ( Z. S  (DSources i Z))"
and
NDSourceExistsDSource:
"S  (Sources i C)  S  (DSources i C)  
 ( Z. S  (DSources i Z)  Z  (Sources i C))"
and
SourcesTrans:
"(C  Sources i S  S  Sources i Z)  C  Sources i Z"
and 
SourcesLevelX:
"(Sources i X)   (AbstrLevel i)" 
and
SourcesLoop:
"(Sources i C) = (XS  (Sources i S))  (Sources i S) = (ZS  (Sources i C)) 
 (Sources i C) = XS   ZS  { C, S}" 
― ‹if we have a loop in the dependencies we need to cut it for counting the sources›

axiomatization
  Acc :: "AbstrLevelsID  CSet  CSet set"
where 
AccDef:
"(Acc i C) = (DAcc i C)  ( S  (DAcc i C). (Acc i S))" 
and
Acc_Sources:
"(X  Acc i C) = (C  Sources i X)"
and
AccSigleLoop:
"DAcc i C = {S}  DAcc i S = {C}  Acc i C = {C, S}" 
and
AccLoop:
"(Acc i C) = (XS  (Acc i S))  (Acc i S) = (ZS  (Acc i C)) 
 (Acc i C) = XS   ZS  { C, S}" 
― ‹if we have a loop in the dependencies we need to cut it for counting the accessors›

lemma Acc_SourcesNOT: "(X  Acc i C) = (C  Sources i X)"
by (metis Acc_Sources)

― ‹component S is not a source for any component on the abstraction level i›
definition
  isNotDSource :: "AbstrLevelsID  CSet  bool"
where
 "isNotDSource i S  ( x  (OUT S). ( Z  (AbstrLevel i). (x  (IN Z))))"

― ‹component S is not a source for a component Z on the abstraction level i›
definition
  isNotDSourceX :: "AbstrLevelsID  CSet  CSet  bool"
where
 "isNotDSourceX i S C  ( x  (OUT S). (C  (AbstrLevel i)  (x  (IN C))))"

lemma isNotSource_isNotSourceX:
"isNotDSource i S = ( C. isNotDSourceX i S C)" 
by (auto, (simp add: isNotDSource_def isNotDSourceX_def)+)

lemma DAcc_DSources:
"(X  DAcc i C) = (C  DSources i X)"
by (auto, (simp add: DAcc_def DSources_def, auto)+)
 
lemma DAcc_DSourcesNOT:
"(X  DAcc i C) = (C  DSources i X)"
by (auto, (simp add: DAcc_def DSources_def, auto)+)

lemma DSource_level:
  assumes "S  (DSources i C)"
  shows    "C   (AbstrLevel i)"
using assms by (simp add: DSources_def, auto)

lemma SourceExistsDSource_level:
  assumes "S  (Sources i C)"
  shows    " Z   (AbstrLevel i). (S  (DSources i Z))"
using assms by (metis DSource_level SourceExistsDSource) 
  
lemma Sources_DSources:
 "(DSources i C)  (Sources i C)"   
proof -  
  have "(Sources i C) = (DSources i C)  ( S  (DSources i C). (Sources i S))" 
    by (rule SourcesDef)
  thus ?thesis by auto
qed

lemma NoDSourceNoSource:
  assumes "S  (Sources i C)"
  shows     "S  (DSources i C)"
using assms by (metis (full_types) Sources_DSources rev_subsetD)

lemma DSourcesEmptySources:
  assumes "DSources i C = {}"
  shows    "Sources i C = {}" 
proof - 
  have "(Sources i C) = (DSources i C)  ( S  (DSources i C). (Sources i S))"  
    by (rule SourcesDef) 
  with assms show ?thesis by auto
qed

lemma DSource_Sources:
  assumes  "S  (DSources i C)"
  shows     "(Sources i S)   (Sources i C)"
proof - 
 have  "(Sources i C) = (DSources i C)  ( S  (DSources i C). (Sources i S))"
  by (rule SourcesDef)
  with assms show ?thesis by auto
qed

lemma SourcesOnlyDSources:
  assumes " X. (X  (DSources i C)  (DSources i X) = {})"
  shows    "Sources i C = DSources i C"
proof - 
 have sDef:  "(Sources i C) = (DSources i C)  ( S  (DSources i C). (Sources i S))"
  by (rule SourcesDef)
 from assms have  " X. (X  (DSources i C)  (Sources i X) = {})"
   by (simp add: DSourcesEmptySources)
 hence "( S  (DSources i C). (Sources i S)) = {}"  by auto
 with sDef  show ?thesis by simp
qed

lemma SourcesEmptyDSources:
 assumes "Sources i C = {}"
 shows "DSources i C = {}"
using assms  by (metis Sources_DSources bot.extremum_uniqueI)

lemma NotDSource:
 assumes " x  (OUT S). ( Z  (AbstrLevel i). (x  (IN Z)))"
 shows    " C  (AbstrLevel i) . S  (DSources i C)" 
using assms  by (simp add: AbstrLevel0 DSources_def) 

lemma allNotDSource_NotSource:
 assumes " C . S  (DSources i C)" 
 shows    " Z. S  (Sources i Z)" 
using assms  by (metis SourceExistsDSource) 

lemma NotDSource_NotSource:
 assumes " C  (AbstrLevel i). S  (DSources i C)" 
 shows    " Z  (AbstrLevel i). S  (Sources i Z)" 
using assms by (metis SourceExistsDSource_level)  

lemma isNotSource_Sources: 
 assumes "isNotDSource i S"
 shows " C   (AbstrLevel i). S  (Sources i C)" 
using assms  
by (simp add: isNotDSource_def, metis (full_types) NotDSource NotDSource_NotSource)

lemma SourcesAbstrLevel:
assumes "x  Sources i S"
shows "x  AbstrLevel i"
using assms
by (metis SourcesLevelX in_mono)

lemma DSourceIsSource:
  assumes  "C  DSources i S" 
     shows  "C  Sources i S" 
proof -
  have "(Sources i S) = (DSources i S)  ( Z  (DSources i S). (Sources i Z))" 
    by (rule SourcesDef)
  with assms show ?thesis  by simp
qed

lemma DSourceOfDSource:
  assumes  "Z  DSources i S" 
         and  "S  DSources i C"
  shows     "Z  Sources i C"
using assms
proof -
  from assms have src:"Sources i S  Sources i C" by (simp add: DSource_Sources)
  from assms have  "Z  Sources i S"  by (simp add: DSourceIsSource)
  with src   show ?thesis  by auto
qed

lemma SourceOfDSource:
  assumes  "Z  Sources i S" 
         and  "S  DSources i C"
  shows     "Z  Sources i C"
using assms
proof -
  from assms have "Sources i S  Sources i C" by (simp add: DSource_Sources) 
  thus ?thesis by (metis (full_types) assms(1) rev_subsetD)  
qed

lemma DSourceOfSource:
  assumes  cDS:"C  DSources i S" 
         and  sS:"S  Sources i Z"  
  shows     "C  Sources i Z"
proof -
  from cDS have  "C  Sources i S"  by (simp add: DSourceIsSource)
  from this and sS show ?thesis by (metis (full_types) SourcesTrans)  
qed

lemma Sources_singleDSource:
  assumes "DSources i S = {C}" 
  shows    "Sources i S = {C}  Sources i C"
proof - 
 have sDef:  "(Sources i S) = (DSources i S)  ( Z  (DSources i S). (Sources i Z))"
     by (rule SourcesDef)
  from assms have "( Z  (DSources i S). (Sources i Z)) = Sources i C"
     by auto
  with sDef assms show ?thesis by simp
qed

lemma Sources_2DSources:
  assumes "DSources i S = {C1, C2}" 
  shows    "Sources i S = {C1, C2}  Sources i C1   Sources i C2"
proof - 
  have sDef:  "(Sources i S) = (DSources i S)  ( Z  (DSources i S). (Sources i Z))"
     by (rule SourcesDef)
  from assms have "( Z  (DSources i S). (Sources i Z)) = Sources i C1   Sources i C2"
     by auto
  with sDef and assms show ?thesis by simp
qed

lemma Sources_3DSources:
  assumes "DSources i S = {C1, C2, C3}" 
  shows    "Sources i S = {C1, C2, C3}  Sources i C1   Sources i C2   Sources i C3"
proof - 
  have sDef: "(Sources i S) = (DSources i S)  ( Z  (DSources i S). (Sources i Z))" 
     by (rule SourcesDef)
  from assms have "( Z  (DSources i S). (Sources i Z)) = Sources i C1   Sources i C2   Sources i C3"
     by auto
  with sDef and assms show ?thesis by simp
qed

lemma singleDSourceEmpty4isNotDSource:
  assumes "DAcc i C = {S}" 
         and "Z  S"
  shows "C  (DSources i Z)" 
proof -
  from assms have "(Z  DAcc i C)"  by simp
  thus ?thesis by (simp add: DAcc_DSourcesNOT)
qed

lemma singleDSourceEmpty4isNotDSourceLevel:
  assumes "DAcc i C = {S}"
  shows " Z  (AbstrLevel i). Z  S  C  (DSources i Z)" 
using assms  by (metis singleDSourceEmpty4isNotDSource)


lemma "isNotDSource_EmptyDAcc":
  assumes "isNotDSource i S" 
  shows    "DAcc i S ={}"
using assms  by (simp add: DAcc_def isNotDSource_def, auto)

lemma "isNotDSource_EmptyAcc":
  assumes "isNotDSource i S" 
  shows    "Acc i S = {}"
proof -
  have "(Acc i S) = (DAcc i S)  ( X  (DAcc i S). (Acc i X))"  
     by (rule AccDef)
  thus ?thesis by (metis SUP_empty Un_absorb assms isNotDSource_EmptyDAcc) 
qed

lemma singleDSourceEmpty_Acc:
  assumes "DAcc i C = {S}" 
         and "isNotDSource i S" 
  shows  "Acc i C = {S}"  
proof - 
  have AccC:"(Acc i C) = (DAcc i C)  ( S  (DAcc i C). (Acc i S))"  
     by (rule AccDef)
  from assms have "Acc i S = {}" by (simp add: isNotDSource_EmptyAcc)
  with AccC show ?thesis
     by (metis SUP_empty UN_insert Un_commute Un_empty_left assms(1)) 
qed

lemma singleDSourceEmpty4isNotSource:
  assumes "DAcc i C = {S}"
         and nSourcS:"isNotDSource i S"
         and "Z  S"
  shows "C  (Sources i Z)" 
proof - 
  from assms have  "Acc i C = {S}"  by (simp add: singleDSourceEmpty_Acc)
  with assms have "Z  Acc i C" by simp
  thus ?thesis by (simp add: Acc_SourcesNOT)
qed

lemma singleDSourceEmpty4isNotSourceLevel:
  assumes "DAcc i C = {S}"
         and nSourcS:"isNotDSource i S" 
  shows " Z  (AbstrLevel i). Z  S  C  (Sources i Z)" 
using assms
by (metis singleDSourceEmpty4isNotSource)


lemma singleDSourceLoop:
  assumes "DAcc i C = {S}"
         and "DAcc i S = {C}"
  shows " Z  (AbstrLevel i). (Z  S  Z  C  C  (Sources i Z))" 
using assms
by (metis AccSigleLoop Acc_SourcesNOT empty_iff insert_iff)


(*<*)
(*>*)
subsection ‹Components that are elementary wrt. data dependencies›

― ‹two output channels of a component C are corelated, if they mutually depend on the same local variable(s)›
definition
   outPairCorelated :: "CSet  chanID  chanID  bool"
where
  "outPairCorelated C x y 
  (x  OUT C)    (y  OUT C)  
  (OUTfromV x)  (OUTfromV y)  {}"

― ‹We call a set of output channels of a conponent correlated to it output channel x,›
― ‹if they mutually depend on the same local variable(s)›
definition
   outSetCorelated :: "chanID  chanID set"
where
  "outSetCorelated x   
  { y::chanID .  v::varID. (v  (OUTfromV x)  (y  VARto v)) }"

― ‹Elementary component according to the data dependencies.›
― ‹This constraint should hold for all components on the abstraction level 1›
definition
elementaryCompDD :: "CSet  bool"
where
  "elementaryCompDD C  
  (( x. (OUT C) = {x} )  
   ( x  (OUT C).  y  (OUT C). ((outSetCorelated x)  (outSetCorelated y)  {}) ))"

― ‹the set (outSetCorelated x) is empty if x does not depend from any variable›
lemma outSetCorelatedEmpty1:
 assumes "OUTfromV x = {}"
 shows "outSetCorelated x = {}"
using assms by (simp add: outSetCorelated_def)

― ‹if x depends from at least one variable and the predicates OUTfromV and VARto are defined correctly,›
― ‹the set (outSetCorelated x) contains x itself›
lemma outSetCorelatedNonemptyX:
 assumes "OUTfromV x   {}" and correct3:"OUTfromV_VARto"
 shows "x  outSetCorelated x"
proof -
  from assms have " v::varID. x  (VARto v)" 
    by (rule OUTfromV_VARto_lemma)
  from this and assms show ?thesis
    by (simp add:  outSetCorelated_def OUTfromV_VARto_def)
qed

― ‹if the set (outSetCorelated x) is empty, this means that x does not depend from any variable›
lemma outSetCorelatedEmpty2:
 assumes "outSetCorelated x = {}"   and correct3:"OUTfromV_VARto"
 shows  "OUTfromV x = {}"
proof (rule ccontr)
  assume OUTfromVNonempty:"OUTfromV x  {}"
  from this and correct3 have "x  outSetCorelated x" 
    by (rule outSetCorelatedNonemptyX)
  from this and assms show False by simp
qed

(*<*)
(*>*)
subsection ‹Set of components needed to check a specific property›

― ‹set of components specified on abstreaction level i, which input channels belong to the set chSet›
definition
  inSetOfComponents :: "AbstrLevelsID  chanID set  CSet set"
where
 "inSetOfComponents i chSet 
  {X. (((IN X)  chSet  {})   X  (AbstrLevel i))}"

― ‹Set of components from the abstraction level i, which output channels belong to the set chSet›
definition
  outSetOfComponents :: "AbstrLevelsID  chanID set  CSet set"
where
 "outSetOfComponents i chSet 
  {Y. (((OUT Y)  chSet  {})  Y  (AbstrLevel i))}"

― ‹Set of components from the abstraction level i,›
― ‹which have output channels from the set chSet or are sources for such components›
definition
  minSetOfComponents ::  "AbstrLevelsID  chanID set  CSet set"
where
 "minSetOfComponents i chSet 
  (outSetOfComponents i chSet) 
  ( S  (outSetOfComponents i chSet). (Sources i S))"

― ‹Please note that a system output cannot beat the same time a local chanel.›

― ‹channel x is a system input on an abstraction level i›
definition systemIN ::"chanID  AbstrLevelsID  bool"
where
  "systemIN x i  ( C1  (AbstrLevel i). x  (IN C1))  ( C2  (AbstrLevel i). x  (OUT C2))"

― ‹channel x is a system input on an abstraction level i›
definition systemOUT ::"chanID  AbstrLevelsID  bool"
where
  "systemOUT x i  ( C1  (AbstrLevel i). x  (IN C1))  ( C2  (AbstrLevel i). x  (OUT C2))"

― ‹channel x is a system local channel on an abstraction level i›
definition systemLOC ::"chanID  AbstrLevelsID  bool"
where
  "systemLOC x i  ( C1  (AbstrLevel i). x  (IN C1))  ( C2  (AbstrLevel i). x  (OUT C2))"

lemma systemIN_noOUT:
  assumes "systemIN x i"
  shows    "¬ systemOUT x i"
using assms by (simp add: systemIN_def systemOUT_def)

lemma systemOUT_noIN:
  assumes "systemOUT x i"
  shows    "¬ systemIN x i"
using assms by (simp add: systemIN_def systemOUT_def)

lemma systemIN_noLOC:
  assumes "systemIN x i"
  shows    "¬ systemLOC x i"
using assms by (simp add: systemIN_def systemLOC_def)

lemma systemLOC_noIN:
  assumes "systemLOC x i"
  shows    "¬ systemIN x i"
using assms by (simp add: systemIN_def systemLOC_def)

lemma systemOUT_noLOC:
  assumes "systemOUT x i"
  shows    "¬ systemLOC x i"
using assms by (simp add: systemOUT_def systemLOC_def)

lemma systemLOC_noOUT:
  assumes "systemLOC x i"
  shows    "¬ systemOUT x i"
using assms by (simp add: systemLOC_def systemOUT_def)

definition
  noIrrelevantChannels ::  "AbstrLevelsID  chanID set  bool"
where
 "noIrrelevantChannels i chSet 
   x  chSet. ((systemIN x i) 
   ( Z  (minSetOfComponents i chSet). x  (IN Z)))"


definition
  allNeededINChannels ::  "AbstrLevelsID  chanID set  bool"
where
 "allNeededINChannels i chSet 
  ( Z  (minSetOfComponents i chSet).  x  (IN Z). ((systemIN x i)  (x  chSet)))"

― ‹the set (outSetOfComponents i chSet) should be a subset of all components specified on the abstraction level i›
lemma outSetOfComponentsLimit:
"outSetOfComponents i chSet  AbstrLevel i"
by (metis (lifting) mem_Collect_eq outSetOfComponents_def subsetI)

― ‹the set (inSetOfComponents i chSet) should be a subset of all components specified on the abstraction level i›
lemma inSetOfComponentsLimit:
"inSetOfComponents i chSet  AbstrLevel i"
by (metis (lifting) inSetOfComponents_def mem_Collect_eq subsetI)

― ‹the set of components, which are sources for the components›
― ‹out of (inSetOfComponents i chSet), should be a subset of› 
― ‹all components specified on the abstraction level i›
lemma SourcesLevelLimit:
"( S  (outSetOfComponents i chSet). (Sources i S))  AbstrLevel i"
proof -
  have sg1:"outSetOfComponents i chSet  AbstrLevel i"
    by (simp add: outSetOfComponentsLimit)
  have " S. S  (outSetOfComponents i chSet)  Sources i S  AbstrLevel i"
    by (metis SourcesLevelX)
  from this and sg1 show ?thesis by auto
qed

lemma minSetOfComponentsLimit:
"minSetOfComponents i chSet  AbstrLevel i"
proof -
  have sg1: "outSetOfComponents i chSet  AbstrLevel i"
    by (simp add: outSetOfComponentsLimit)
  have "( S  (outSetOfComponents i chSet). (Sources i S))  AbstrLevel i"
    by (simp add:  SourcesLevelLimit)
  with sg1 show ?thesis  by (simp add: minSetOfComponents_def)
qed 

(*<*)
(*>*)
subsection ‹Additional properties: Remote Computation›

― ‹The value of  $UplSizeHighLoad$ $x$ is True if its $UplSize$ measure is greather that a predifined value›
definition UplSizeHighLoadCh ::  "chanID  bool"
where
   "UplSizeHighLoadCh x  (x  UplSizeHighLoad)"

― ‹if the $Perf$ measure of at least one subcomponent is greather than a predifined value,›
― ‹the $Perf$ measure of this component is greather than $HighPerf$ too›
axiomatization HighPerfComp ::  "CSet  bool"
where
HighPerfComDef:
   "HighPerfComp C =
   ((C  HighPerfSet)  ( Z  subcomp C. (HighPerfComp Z)))"

end