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