Session ComponentDependencies

Theory DataDependenciesConcreteValues

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

section "Case Study: Definitions"
 
theory DataDependenciesConcreteValues
  imports Main
begin

datatype CSet = sA1| sA2| sA3| sA4| sA5| sA6| sA7| sA8| sA9|
               sA11| sA12| sA21| sA22| sA23|  sA31| sA32| sA41| sA42|
               sA71| sA72| sA81| sA82| sA91| sA92| sA93|
               sS1| sS2| sS3| sS4| sS5| sS6| sS7| sS8| sS9| sS10| sS11|
               sS12 |sS13| sS14| sS15| sS1opt | sS4opt | sS7opt | sS11opt

datatype chanID = data1| data2| data3| data4| data5| data6| data7| 
data8| data9| data10| data11| data12| data13| data14| data15| 
data16| data17| data18| data19| data20| data21| data22| data23| data24

datatype varID = stA1 | stA2 | stA4 | stA6

datatype AbstrLevelsID = level0 | level1 | level2 | level3

― ‹function IN maps component ID to the set of its input channels›
fun IN ::  "CSet  chanID set"
where 
   "IN sA1 = { data1 }" 
| "IN sA2 = { data2, data3 }"
| "IN sA3 = { data4, data5 }"
| "IN sA4 = { data6, data7, data13 }"
| "IN sA5 = { data8 }"
| "IN sA6 = { data14 }"
| "IN sA7 = { data15, data16 }"
| "IN sA8 = { data17, data18, data19, data22 }"
| "IN sA9 = { data20, data21 }"
| "IN sA11 = { data1 }"
| "IN sA12 = { data1 }"
| "IN sA21 = { data2 }"
| "IN sA22 = { data2, data3 }"
| "IN sA23 = { data2 }"
| "IN sA31 = { data4 }"
| "IN sA32 = { data5 }"
| "IN sA41 = { data6, data7 }"
| "IN sA42 = { data13 }"
| "IN sA71 = { data15 }"
| "IN sA72 = { data16 }"
| "IN sA81 = { data17, data22 }"
| "IN sA82 = { data18, data19 }"
| "IN sA91 = { data20 }"
| "IN sA92 = { data20 }"
| "IN sA93 = { data21 }"
| "IN sS1 = { data1 }"
| "IN sS2 = { data1 }"
| "IN sS3 = { data2 }"
| "IN sS4 = { data2 }"
| "IN sS5 = { data5 }"
| "IN sS6 = { data2, data7 }"
| "IN sS7 = { data13 }"
| "IN sS8 = { data8 }"
| "IN sS9 = { data14 }"
| "IN sS10 = { data15 }"
| "IN sS11 = { data16 }"
| "IN sS12 = { data17}"
| "IN sS13= { data20 }" 
| "IN sS14 = { data18, data19 }"
| "IN sS15 = { data21 }"
| "IN sS1opt = { data1 }"
| "IN sS4opt = { data2 }"
| "IN sS7opt = { data13 }" 
| "IN sS11opt = { data16, data19 }" 

― ‹function OUT maps component ID to the set of its output channels›
fun OUT ::  "CSet  chanID set"
where 
   "OUT sA1 = { data2, data10 }" 
| "OUT sA2 = { data4, data5, data11, data12 }"
| "OUT sA3 = { data6, data7 }"
| "OUT sA4 = { data3, data8 }"
| "OUT sA5 = { data9 }"
| "OUT sA6 = { data15, data16 }"
| "OUT sA7 = { data17, data18 }"
| "OUT sA8 = { data20, data21 }"
| "OUT sA9 = { data22, data23, data24 }"
| "OUT sA11 = { data2 }"
| "OUT sA12= { data10 }"
| "OUT sA21 = { data11 }"
| "OUT sA22 = { data4, data12 }"
| "OUT sA23 = { data5 }"
| "OUT sA31= { data6 }"
| "OUT sA32 = { data7 }"
| "OUT sA41 = { data3 }"
| "OUT sA42 = { data8 }"
| "OUT sA71 = { data17 }"
| "OUT sA72 = { data18 }"
| "OUT sA81 = { data20 }"
| "OUT sA82 = { data21 }"
| "OUT sA91 = { data22 }"
| "OUT sA92 = { data23 }"
| "OUT sA93 = { data24 }"
| "OUT sS1 = { data10 }"
| "OUT sS2 = { data2 }"
| "OUT sS3 = { data11 }"
| "OUT sS4 = { data5 }"
| "OUT sS5 = { data7 }"
| "OUT sS6 = { data12 }"
| "OUT sS7 = { data8 }"
| "OUT sS8 = { data9 }"
| "OUT sS9 = { data15, data16 }"
| "OUT sS10 = { data17 }"
| "OUT sS11 = { data18 }"
| "OUT sS12 = { data20}"
| "OUT sS13= { data23 }" 
| "OUT sS14 = { data21 }"
| "OUT sS15 = { data24 }"
| "OUT sS1opt = { data2, data10 }"
| "OUT sS4opt = { data12 }"
| "OUT sS7opt = { data9 }"
| "OUT sS11opt = { data24 }"


― ‹function VAR maps component IDs to the set of its local variables›
fun VAR ::  "CSet  varID set"
where 
   "VAR sA1 = { stA1 }" 
| "VAR sA2 = { stA2 }"
| "VAR sA3 = {}"
| "VAR sA4 = { stA4 }"
| "VAR sA5 = {}"
| "VAR sA6 = { stA6 }"
| "VAR sA7 = {}"
| "VAR sA8 = {}"
| "VAR sA9 = {}"
| "VAR sA11 = {}"
| "VAR sA12 = { stA1 }"
| "VAR sA21 = {}"
| "VAR sA22 = { stA2 }"
| "VAR sA23 = {}"
| "VAR sA31 = {}"
| "VAR sA32 = {}"
| "VAR sA41 = {stA4 }"
| "VAR sA42 = {}"
| "VAR sA71 = {}"
| "VAR sA72 = {}"
| "VAR sA81 = {}"
| "VAR sA82 = {}"
| "VAR sA91 = {}"
| "VAR sA92 = {}"
| "VAR sA93 = {}"
| "VAR sS1 = { stA1 }"
| "VAR sS2 = {}"
| "VAR sS3 = {}"
| "VAR sS4 = {}"
| "VAR sS5 = {}"
| "VAR sS6 = {stA2, stA4}"
| "VAR sS7 = {}"
| "VAR sS8 = {}"
| "VAR sS9 = {stA6}"
| "VAR sS10 = {}"
| "VAR sS11 = {}"
| "VAR sS12 = {}"
| "VAR sS13 = {}"
| "VAR sS14 = {}"
| "VAR sS15 = {}"
| "VAR sS1opt = { stA1 }"
| "VAR sS4opt = { stA2, stA4 }"
| "VAR sS7opt = {}"
| "VAR sS11opt = {}"


― ‹function subcomp maps component ID to the set of its subcomponents›
fun subcomp ::  "CSet  CSet set"
where 
   "subcomp sA1 = { sA11, sA12 }" 
| "subcomp sA2 = { sA21, sA22, sA23 }"
| "subcomp sA3 = { sA31, sA32 }"
| "subcomp sA4 = { sA41, sA42 }"
| "subcomp sA5 = {}"
| "subcomp sA6 = {}"
| "subcomp sA7 = { sA71, sA72 }"
| "subcomp sA8 = { sA81, sA82 }"
| "subcomp sA9 = { sA91, sA92, sA93 }" 
| "subcomp sA11 = {}"
| "subcomp sA12 = {}"
| "subcomp sA21 = {}"
| "subcomp sA22 = {}"
| "subcomp sA23 = {}"
| "subcomp sA31 = {}"
| "subcomp sA32 = {}"
| "subcomp sA41 = {}"
| "subcomp sA42 = {}"
| "subcomp sA71 = {}"
| "subcomp sA72 = {}"
| "subcomp sA81 = {}"
| "subcomp sA82 = {}"
| "subcomp sA91 = {}"
| "subcomp sA92 = {}"
| "subcomp sA93 = {}"
| "subcomp sS1 = { sA12 }"
| "subcomp sS2 = { sA11 }"
| "subcomp sS3 = { sA21 }"
| "subcomp sS4 = { sA23 }"
| "subcomp sS5 = { sA32 }"
| "subcomp sS6 = { sA22, sA31, sA41 }"
| "subcomp sS7 = { sA42}"
| "subcomp sS8 = { sA5 }"
| "subcomp sS9 = { sA6 }"
| "subcomp sS10 = { sA71 }"
| "subcomp sS11 = { sA72 }"
| "subcomp sS12 = { sA81, sA91 }"
| "subcomp sS13 = { sA92 }"
| "subcomp sS14 = { sA82 }"
| "subcomp sS15 = { sA93 }"
| "subcomp sS1opt = { sA11, sA12 }"
| "subcomp sS4opt = { sA22, sA23, sA31, sA32, sA41 }"
| "subcomp sS7opt = { sA42, sA5 }"
| "subcomp sS11opt = { sA72, sA82, sA93 }"

― ‹function AbstrLevel maps abstraction level ID to the corresponding set of components›
axiomatization
  AbstrLevel ::  "AbstrLevelsID  CSet set"
where
AbstrLevel0:
"AbstrLevel level0 = {sA1, sA2, sA3, sA4, sA5, sA6, sA7, sA8, sA9}"
and
AbstrLevel1:
"AbstrLevel level1 = {sA11, sA12, sA21, sA22, sA23, sA31, sA32, 
 sA41, sA42, sA5, sA6, sA71, sA72, sA81, sA82, sA91, sA92, sA93}"
and
AbstrLevel2:
"AbstrLevel level2 = {sS1, sS2, sS3, sS4, sS5, sS6, sS7, sS8, 
                               sS9, sS10, sS11, sS12, sS13, sS14, sS15}"
and
AbstrLevel3:
"AbstrLevel level3 = {sS1opt, sS3, sS4opt, sS7opt, sS9, sS10, sS11opt, sS12, sS13 }"

― ‹function VARfrom maps variable ID to the set of input channels it depends from›
fun VARfrom :: "varID  chanID set"
where
   "VARfrom stA1 = {data1}"
| "VARfrom stA2 = {data3}"
| "VARfrom stA4 = {data6, data7}" 
| "VARfrom stA6 = {data14}" 

― ‹function VARto maps variable ID to the set of output channels depending from this variable›
fun VARto :: "varID  chanID set"
where
   "VARto stA1 = {data10}"
| "VARto stA2 = {data4, data12}"
| "VARto stA4 = {data3}" 
| "VARto stA6 = {data15, data16}" 

― ‹function OUTfromCh maps channel ID to the set of input channels›
― ‹from which it depends derectly;›
― ‹an empty set means that the channel is either input of the system or›
― ‹its values are computed from local variables or are generated›
― ‹within some component independently›
fun OUTfromCh ::  "chanID  chanID set"
where
   "OUTfromCh data1 = {}"
| "OUTfromCh data2 = {data1}"
| "OUTfromCh data3 = {}"
| "OUTfromCh data4 = {data2}"
| "OUTfromCh data5 = {data2}"
| "OUTfromCh data6 = {data4}"
| "OUTfromCh data7 = {data5}"
| "OUTfromCh data8 = {data13}"
| "OUTfromCh data9 = {data8}"
| "OUTfromCh data10 = {}"
| "OUTfromCh data11 = {data2}"
| "OUTfromCh data12 = {}"
| "OUTfromCh data13 = {}"
| "OUTfromCh data14 = {}"
| "OUTfromCh data15 = {}"
| "OUTfromCh data16 = {}"
| "OUTfromCh data17 = {data15}"
| "OUTfromCh data18 = {data16}"
| "OUTfromCh data19 = {}"
| "OUTfromCh data20 = {data17, data22}"
| "OUTfromCh data21 = {data18, data19}"
| "OUTfromCh data22 = {data20}"
| "OUTfromCh data23 = {data21}"
| "OUTfromCh data24 = {data20}"

― ‹function OUTfromV maps channel ID to the set of local variables it depends from›
fun OUTfromV ::  "chanID  varID set" 
where
   "OUTfromV data1 = {}"
| "OUTfromV data2 = {}"
| "OUTfromV data3 = {stA4}"
| "OUTfromV data4 = {stA2}"
| "OUTfromV data5 = {}"
| "OUTfromV data6 = {}"
| "OUTfromV data7 = {}"
| "OUTfromV data8 = {}"
| "OUTfromV data9 = {}"
| "OUTfromV data10 = {stA1}"
| "OUTfromV data11 = {}"
| "OUTfromV data12 = {stA2}"
| "OUTfromV data13 = {}"
| "OUTfromV data14 = {}"
| "OUTfromV data15 = {stA6}"
| "OUTfromV data16 = {stA6}"
| "OUTfromV data17 = {}"
| "OUTfromV data18 = {}"
| "OUTfromV data19 = {}"
| "OUTfromV data20 = {}"
| "OUTfromV data21 = {}"
| "OUTfromV data22 = {}"
| "OUTfromV data23 = {}"
| "OUTfromV data24 = {}"

― ‹Set of channels channels which have  UplSize measure greather that the predifined value $HighLoad$›
definition
   UplSizeHighLoad ::  "chanID set"
where
  "UplSizeHighLoad  {data1, data4, data5, data6, data7, data8, data18, data21}"

― ‹Set of components from the abstraction level 1 for which the Perf measure is greather that the predifined value $HighPerf$›
definition
   HighPerfSet ::  "CSet set"
where
  "HighPerfSet  {sA22, sA23, sA41, sA42, sA72, sA93}"

end

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

Theory DataDependenciesCaseStudy

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

section "Case Study: Verification of Properties"
 
theory DataDependenciesCaseStudy
  imports DataDependencies
begin


subsection ‹Correct composition of components›

― ‹the lemmas  AbstrLevels X Y with corresponding proofs can be composend›
― ‹and proven automatically, their proofs are identical›
lemma AbstrLevels_A1_A11:
  assumes "sA1  AbstrLevel i"
  shows "sA11  AbstrLevel i"
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)

lemma AbstrLevels_A1_A12:
  assumes "sA1  AbstrLevel i"
  shows "sA12  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A2_A21:
  assumes "sA2  AbstrLevel i"
  shows "sA21  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A2_A22:
  assumes "sA2  AbstrLevel i"
  shows "sA22  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A2_A23:
  assumes "sA2  AbstrLevel i"
  shows "sA23  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A3_A31:
  assumes "sA3  AbstrLevel i"
  shows "sA31  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A3_A32:
  assumes "sA3  AbstrLevel i"
  shows "sA32  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A4_A41:
  assumes "sA4  AbstrLevel i"
  shows "sA41  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A4_A42:
  assumes "sA4  AbstrLevel i"
  shows "sA42  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A7_A71:
  assumes "sA7  AbstrLevel i"
  shows "sA71  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A7_A72:
  assumes "sA7  AbstrLevel i"
  shows "sA72  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)

lemma AbstrLevels_A8_A81:
  assumes "sA8  AbstrLevel i"
  shows "sA81  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)

lemma AbstrLevels_A8_A82:
  assumes "sA8  AbstrLevel i"
  shows "sA82  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A9_A91:
  assumes "sA9  AbstrLevel i"
  shows "sA91  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A9_A92:
  assumes "sA9  AbstrLevel i"
  shows "sA92  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_A9_A93:
  assumes "sA9  AbstrLevel i"
  shows "sA93  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S1_A12:
  assumes "sS1  AbstrLevel i"
  shows "sA12  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S2_A11:
  assumes "sS2  AbstrLevel i"
  shows "sA11  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S3_A21:
  assumes "sS3  AbstrLevel i"
  shows "sA21  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S4_A23:
  assumes "sS4  AbstrLevel i"
  shows "sA23  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S5_A32:
  assumes "sS5  AbstrLevel i"
  shows "sA32  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S6_A22:
  assumes "sS6  AbstrLevel i"
  shows "sA22  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S6_A31:
  assumes "sS6  AbstrLevel i"
  shows "sA31  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S6_A41:
  assumes "sS6  AbstrLevel i"
  shows "sA41  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S7_A42:
  assumes "sS7  AbstrLevel i"
  shows "sA42  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S8_A5:
  assumes "sS8  AbstrLevel i"
  shows "sA5  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S9_A6:
  assumes "sS9  AbstrLevel i"
  shows "sA6  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S10_A71:
  assumes "sS10  AbstrLevel i"
  shows "sA71  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S11_A72:
  assumes "sS11  AbstrLevel i"
  shows "sA72  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S12_A81:
  assumes "sS12  AbstrLevel i"
  shows "sA81  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S12_A91:
  assumes "sS12  AbstrLevel i"
  shows "sA91  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S13_A92:
  assumes "sS13  AbstrLevel i"
  shows "sA92  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S14_A82:
  assumes "sS14  AbstrLevel i"
  shows "sA82  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S15_A93:
  assumes "sS15  AbstrLevel i"
  shows "sA93  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S1opt_A11:
  assumes "sS1opt  AbstrLevel i"
  shows "sA11  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S1opt_A12:
  assumes "sS1opt  AbstrLevel i"
  shows "sA12  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S4opt_A23:
  assumes "sS4opt  AbstrLevel i"
  shows "sA23  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S4opt_A32:
  assumes "sS4opt  AbstrLevel i"
  shows "sA32  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S4opt_A22:
  assumes "sS4opt  AbstrLevel i"
  shows "sA22  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S4opt_A31:
  assumes "sS4opt  AbstrLevel i"
  shows "sA31  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S4opt_A41:
  assumes "sS4opt  AbstrLevel i"
  shows "sA41  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S7opt_A42:
  assumes "sS7opt  AbstrLevel i"
  shows "sA42  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S7opt_A5:
  assumes "sS7opt  AbstrLevel i"
  shows "sA5  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S11opt_A72:
  assumes "sS11opt  AbstrLevel i"
  shows "sA72  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S11opt_A82:
  assumes "sS11opt  AbstrLevel i"
  shows "sA82  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma AbstrLevels_S11opt_A93:
  assumes "sS11opt  AbstrLevel i"
  shows "sA93  AbstrLevel i"
(*<*)
using assms 
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)
(*>*)


lemma correctCompositionDiffLevelsA1: "correctCompositionDiffLevels sA1"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_A1_A11 AbstrLevels_A1_A12)(*>*)


lemma correctCompositionDiffLevelsA2: "correctCompositionDiffLevels sA2"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_A2_A21 AbstrLevels_A2_A22 AbstrLevels_A2_A23)(*>*)


lemma correctCompositionDiffLevelsA3: "correctCompositionDiffLevels sA3"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_A3_A31 AbstrLevels_A3_A32)(*>*)


lemma correctCompositionDiffLevelsA4: "correctCompositionDiffLevels sA4"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_A4_A41 AbstrLevels_A4_A42)(*>*)


― ‹lemmas  correctCompositionDiffLevelsX and corresponding proofs›
― ‹are identical for all elementary components, they can be constructed automatically› 
lemma correctCompositionDiffLevelsA5: "correctCompositionDiffLevels sA5"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA6: "correctCompositionDiffLevels sA6"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA7: "correctCompositionDiffLevels sA7"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_A7_A71 AbstrLevels_A7_A72)(*>*)

lemma correctCompositionDiffLevelsA8: "correctCompositionDiffLevels sA8"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_A8_A81 AbstrLevels_A8_A82)(*>*)

lemma correctCompositionDiffLevelsA9: "correctCompositionDiffLevels sA9"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_A9_A91 AbstrLevels_A9_A92 AbstrLevels_A9_A93)(*>*)

lemma correctCompositionDiffLevelsA11: "correctCompositionDiffLevels sA11"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA12: "correctCompositionDiffLevels sA12"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA21: "correctCompositionDiffLevels sA21"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA22: "correctCompositionDiffLevels sA22"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA23: "correctCompositionDiffLevels sA23"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA31: "correctCompositionDiffLevels sA31"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA32: "correctCompositionDiffLevels sA32"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA41: "correctCompositionDiffLevels sA41"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA42: "correctCompositionDiffLevels sA42"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA71: "correctCompositionDiffLevels sA71"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA72: "correctCompositionDiffLevels sA72"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA81: "correctCompositionDiffLevels sA81"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA82: "correctCompositionDiffLevels sA82"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA91: "correctCompositionDiffLevels sA91"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA92: "correctCompositionDiffLevels sA92"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsA93: "correctCompositionDiffLevels sA93"
(*<*)by (simp add: correctCompositionDiffLevels_def) (*>*)

lemma correctCompositionDiffLevelsS1: "correctCompositionDiffLevels sS1"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S1_A12) (*>*)

lemma correctCompositionDiffLevelsS2: "correctCompositionDiffLevels sS2"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S2_A11) (*>*)

lemma correctCompositionDiffLevelsS3: "correctCompositionDiffLevels sS3"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S3_A21) (*>*)

lemma correctCompositionDiffLevelsS4: "correctCompositionDiffLevels sS4"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S4_A23) (*>*)

lemma correctCompositionDiffLevelsS5: "correctCompositionDiffLevels sS5"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S5_A32) (*>*)

lemma correctCompositionDiffLevelsS6: "correctCompositionDiffLevels sS6"
(*<*)by (simp add: correctCompositionDiffLevels_def  AbstrLevels_S6_A22 AbstrLevels_S6_A31 AbstrLevels_S6_A41) (*>*)

lemma correctCompositionDiffLevelsS7: "correctCompositionDiffLevels sS7"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S7_A42) (*>*)

lemma correctCompositionDiffLevelsS8: "correctCompositionDiffLevels sS8"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S8_A5) (*>*)

lemma correctCompositionDiffLevelsS9: "correctCompositionDiffLevels sS9"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S9_A6) (*>*)

lemma correctCompositionDiffLevelsS10: "correctCompositionDiffLevels sS10"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S10_A71) (*>*)

lemma correctCompositionDiffLevelsS11: "correctCompositionDiffLevels sS11"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S11_A72) (*>*)

lemma correctCompositionDiffLevelsS12: "correctCompositionDiffLevels sS12"
(*<*)by (simp add: correctCompositionDiffLevels_def  AbstrLevels_S12_A81 AbstrLevels_S12_A91) (*>*)

lemma correctCompositionDiffLevelsS13: "correctCompositionDiffLevels sS13"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S13_A92) (*>*)

lemma correctCompositionDiffLevelsS14: "correctCompositionDiffLevels sS14"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S14_A82) (*>*)

lemma correctCompositionDiffLevelsS15: "correctCompositionDiffLevels sS15"
(*<*)by (simp add: correctCompositionDiffLevels_def AbstrLevels_S15_A93) (*>*)

lemma correctCompositionDiffLevelsS1opt: "correctCompositionDiffLevels sS1opt"
(*<*)by (simp add: correctCompositionDiffLevels_def  AbstrLevels_S1opt_A11 AbstrLevels_S1opt_A12) (*>*)

lemma correctCompositionDiffLevelsS4opt: "correctCompositionDiffLevels sS4opt"
(*<*)by (simp add: correctCompositionDiffLevels_def  AbstrLevels_S4opt_A22 
      AbstrLevels_S4opt_A23  AbstrLevels_S4opt_A31  
      AbstrLevels_S4opt_A32  AbstrLevels_S4opt_A41) (*>*)

lemma correctCompositionDiffLevelsS7opt: "correctCompositionDiffLevels sS7opt"
(*<*)by (simp add: correctCompositionDiffLevels_def  AbstrLevels_S7opt_A42 AbstrLevels_S7opt_A5) (*>*)

lemma correctCompositionDiffLevelsS11opt: "correctCompositionDiffLevels sS11opt"
(*<*)by (simp add: correctCompositionDiffLevels_def  AbstrLevels_S11opt_A72 
        AbstrLevels_S11opt_A82 AbstrLevels_S11opt_A93) (*>*)

lemma correctCompositionDiffLevelsSYSTEM_holds:
"correctCompositionDiffLevelsSYSTEM"
(*<*)by (simp add: correctCompositionDiffLevelsSYSTEM_def, clarify, case_tac S, 
simp add: correctCompositionDiffLevelsA1, 
simp add: correctCompositionDiffLevelsA2,
simp add: correctCompositionDiffLevelsA3,
simp add: correctCompositionDiffLevelsA4,
simp add: correctCompositionDiffLevelsA5,
simp add: correctCompositionDiffLevelsA6,
simp add: correctCompositionDiffLevelsA7,
simp add: correctCompositionDiffLevelsA8,
simp add: correctCompositionDiffLevelsA9,
simp add: correctCompositionDiffLevelsA11,
simp add: correctCompositionDiffLevelsA12,
simp add: correctCompositionDiffLevelsA21,
simp add: correctCompositionDiffLevelsA22,
simp add: correctCompositionDiffLevelsA23,
simp add: correctCompositionDiffLevelsA31,
simp add: correctCompositionDiffLevelsA32,
simp add: correctCompositionDiffLevelsA41,
simp add: correctCompositionDiffLevelsA42,
simp add: correctCompositionDiffLevelsA71,
simp add: correctCompositionDiffLevelsA72,
simp add: correctCompositionDiffLevelsA81,
simp add: correctCompositionDiffLevelsA82,
simp add: correctCompositionDiffLevelsA91,
simp add: correctCompositionDiffLevelsA92,
simp add: correctCompositionDiffLevelsA93,
simp add: correctCompositionDiffLevelsS1,
simp add: correctCompositionDiffLevelsS2,
simp add: correctCompositionDiffLevelsS3,
simp add: correctCompositionDiffLevelsS4,
simp add: correctCompositionDiffLevelsS5,
simp add: correctCompositionDiffLevelsS6,
simp add: correctCompositionDiffLevelsS7,
simp add: correctCompositionDiffLevelsS8,
simp add: correctCompositionDiffLevelsS9,
simp add: correctCompositionDiffLevelsS10,
simp add: correctCompositionDiffLevelsS11,
simp add: correctCompositionDiffLevelsS12,
simp add: correctCompositionDiffLevelsS13,
simp add: correctCompositionDiffLevelsS14,
simp add: correctCompositionDiffLevelsS15,
simp add: correctCompositionDiffLevelsS1opt,
simp add: correctCompositionDiffLevelsS4opt,
simp add: correctCompositionDiffLevelsS7opt, 
simp add: correctCompositionDiffLevelsS11opt)(*>*)

lemma correctCompositionVARSYSTEM_holds:
"correctCompositionVARSYSTEM"
by (simp add: correctCompositionVARSYSTEM_def, clarify, case_tac S, (simp add: correctCompositionVAR_def)+)

lemma correctDeCompositionVARSYSTEM_holds:
"correctDeCompositionVARSYSTEM"
by (simp add: correctDeCompositionVARSYSTEM_def, clarify, case_tac S, (simp add: correctDeCompositionVAR_def)+)


subsection ‹Correct specification of the relations between channels›

lemma OUTfromChCorrect_data1: "OUTfromChCorrect data1"
by (simp add: OUTfromChCorrect_def)

lemma OUTfromChCorrect_data2: "OUTfromChCorrect data2"
by (metis IN.simps(27) OUT.simps(27) OUTfromCh.simps(2) OUTfromChCorrect_def insertI1)

lemma OUTfromChCorrect_data3: "OUTfromChCorrect data3"
by (metis OUTfromCh.simps(3) OUTfromChCorrect_def)

lemma OUTfromChCorrect_data4: "OUTfromChCorrect data4"
by (metis IN.simps(2) OUT.simps(2) OUTfromCh.simps(4) OUTfromChCorrect_def insertI1 singleton_iff)

lemma OUTfromChCorrect_data5: "OUTfromChCorrect data5"
by  (simp add: OUTfromChCorrect_def, metis IN.simps(14) OUT.simps(14) insertI1)

lemma OUTfromChCorrect_data6: "OUTfromChCorrect data6"
by  (simp add: OUTfromChCorrect_def, metis IN.simps(15) OUT.simps(15) insertI1)

lemma OUTfromChCorrect_data7: "OUTfromChCorrect data7"
by (simp add: OUTfromChCorrect_def, metis IN.simps(16) OUT.simps(16) insertI1)

lemma OUTfromChCorrect_data8: "OUTfromChCorrect data8"
by (simp add: OUTfromChCorrect_def, metis IN.simps(18) OUT.simps(18) insertI1) 

 
lemma OUTfromChCorrect_data9: "OUTfromChCorrect data9"
by (simp add: OUTfromChCorrect_def , metis IN.simps(33) OUT.simps(33) singleton_iff)

lemma OUTfromChCorrect_data10: "OUTfromChCorrect data10"
by (simp add: OUTfromChCorrect_def)

lemma OUTfromChCorrect_data11: "OUTfromChCorrect data11"
by (simp add: OUTfromChCorrect_def, metis (full_types) IN.simps(2) 
OUT.simps(2) OUT.simps(31) Un_empty_right Un_insert_left Un_insert_right insertI1)

lemma OUTfromChCorrect_data12: "OUTfromChCorrect data12"
by (simp add: OUTfromChCorrect_def)

lemma OUTfromChCorrect_data13: "OUTfromChCorrect data13"
by (simp add: OUTfromChCorrect_def)

lemma OUTfromChCorrect_data14: "OUTfromChCorrect data14"
by (metis OUTfromCh.simps(14) OUTfromChCorrect_def)

lemma OUTfromChCorrect_data15: "OUTfromChCorrect data15"
by (metis OUTfromCh.simps(15) OUTfromChCorrect_def)

lemma OUTfromChCorrect_data16: "OUTfromChCorrect data16"
by (metis OUTfromCh.simps(16) OUTfromChCorrect_def)

lemma OUTfromChCorrect_data17: "OUTfromChCorrect data17"
proof - 
  have "data17  OUT sA71  data15  IN sA71"
    by (metis IN.simps(19) OUT.simps(19) insertI1)  
  thus ?thesis by (metis IN.simps(19) OUTfromCh.simps(17) OUTfromChCorrect_def) 
qed

lemma OUTfromChCorrect_data18: "OUTfromChCorrect data18"
by (simp add: OUTfromChCorrect_def, metis IN.simps(20) OUT.simps(20) insertI1)

lemma OUTfromChCorrect_data19: "OUTfromChCorrect data19"
by (metis OUTfromCh.simps(19) OUTfromChCorrect_def)

lemma OUTfromChCorrect_data20: "OUTfromChCorrect data20"
by  (simp add: OUTfromChCorrect_def, metis IN.simps(21) OUT.simps(21) insertI1 insert_subset subset_insertI)

lemma OUTfromChCorrect_data21: "OUTfromChCorrect data21"
by (simp add: OUTfromChCorrect_def, metis (full_types) 
IN.simps(22) OUT.simps(22) insertI1 insert_subset subset_insertI)

lemma OUTfromChCorrect_data22: "OUTfromChCorrect data22"
by (simp add: OUTfromChCorrect_def, metis (full_types) IN.simps(23) OUT.simps(23) insertI1)

lemma OUTfromChCorrect_data23: "OUTfromChCorrect data23"
by (simp add: OUTfromChCorrect_def, metis (full_types) IN.simps(9) OUT.simps(9) insert_subset subset_insertI)

lemma OUTfromChCorrect_data24: "OUTfromChCorrect data24"
by (simp add: OUTfromChCorrect_def, metis IN.simps(9) OUT.simps(9) insertI1 insert_subset subset_insertI)

lemma OUTfromChCorrectSYSTEM_holds: "OUTfromChCorrectSYSTEM"
by (simp add: OUTfromChCorrectSYSTEM_def,  clarify, case_tac x,
simp add: OUTfromChCorrect_data1, simp add: OUTfromChCorrect_data2, 
simp add: OUTfromChCorrect_data3, simp add: OUTfromChCorrect_data4,  
simp add: OUTfromChCorrect_data5, simp add: OUTfromChCorrect_data6, 
simp add: OUTfromChCorrect_data7, simp add: OUTfromChCorrect_data8,
simp add: OUTfromChCorrect_data9, simp add: OUTfromChCorrect_data10,
simp add: OUTfromChCorrect_data11, simp add: OUTfromChCorrect_data12,
simp add: OUTfromChCorrect_data13, simp add: OUTfromChCorrect_data14, 
simp add: OUTfromChCorrect_data15, simp add: OUTfromChCorrect_data16,
simp add: OUTfromChCorrect_data17, simp add: OUTfromChCorrect_data18,
simp add: OUTfromChCorrect_data19, simp add: OUTfromChCorrect_data20,
simp add: OUTfromChCorrect_data21, simp add: OUTfromChCorrect_data22, 
simp add: OUTfromChCorrect_data23, simp add: OUTfromChCorrect_data24)

lemma OUTfromVCorrect1_data1: "OUTfromVCorrect1 data1"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data2: "OUTfromVCorrect1 data2"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data3: "OUTfromVCorrect1 data3"
proof - 
  have "data3  OUT sA41  stA4  VAR sA41"
    by (metis OUT.simps(17) VAR.simps(17) insertI1) 
  thus ?thesis by (metis OUTfromV.simps(3) OUTfromVCorrect1_def VAR.simps(17)) 
qed

lemma OUTfromVCorrect1_data4: "OUTfromVCorrect1 data4"
by (simp add: OUTfromVCorrect1_def, metis (full_types) OUT.simps(2) VAR.simps(2) insertI1) 

lemma OUTfromVCorrect1_data5: "OUTfromVCorrect1 data5"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data6: "OUTfromVCorrect1 data6"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data7: "OUTfromVCorrect1 data7"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data8: "OUTfromVCorrect1 data8"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data9: "OUTfromVCorrect1 data9"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data10: "OUTfromVCorrect1 data10"
proof -
  have "data10  OUT sA12  stA1  VAR sA12"
    by (metis OUT.simps(11) VAR.simps(11) insertI1) 
  thus ?thesis by (metis OUT.simps(26) OUTfromV.simps(10) OUTfromVCorrect1_def VAR.simps(26) insertI1) 
qed 

lemma OUTfromVCorrect1_data11: "OUTfromVCorrect1 data11"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data12: "OUTfromVCorrect1 data12"
proof - 
  have "data12  OUT sA22  stA2  VAR sA22"
    by (metis (full_types) OUT.simps(13) VAR.simps(13) insertCI) 
  thus ?thesis by (metis OUTfromV.simps(12) OUTfromVCorrect1_def VAR.simps(13)) 
qed

lemma OUTfromVCorrect1_data13: "OUTfromVCorrect1 data13"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data14: "OUTfromVCorrect1 data14"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data15: "OUTfromVCorrect1 data15"
proof -
  have A6ch:"data15  OUT sA6  stA6  VAR sA6"
    by (metis OUT.simps(6) VAR.simps(6) insertI1) 
  thus ?thesis by (simp add: OUTfromVCorrect1_def, metis A6ch) 
qed

lemma OUTfromVCorrect1_data16: "OUTfromVCorrect1 data16"
proof -
  have A6ch:"data16  OUT sA6  stA6  VAR sA6"
    by (metis (full_types) OUT.simps(6) VAR.simps(6) insertCI)
  thus ?thesis by (simp add: OUTfromVCorrect1_def, metis A6ch) 
qed

lemma OUTfromVCorrect1_data17: "OUTfromVCorrect1 data17"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data18: "OUTfromVCorrect1 data18"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data19: "OUTfromVCorrect1 data19"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data20: "OUTfromVCorrect1 data20"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data21: "OUTfromVCorrect1 data21"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data22: "OUTfromVCorrect1 data22"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data23: "OUTfromVCorrect1 data23"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1_data24: "OUTfromVCorrect1 data24"
by (simp add: OUTfromVCorrect1_def)

lemma OUTfromVCorrect1SYSTEM_holds: "OUTfromVCorrect1SYSTEM"
by (simp add: OUTfromVCorrect1SYSTEM_def, clarify, case_tac x, 
simp add: OUTfromVCorrect1_data1, simp add: OUTfromVCorrect1_data2,
simp add: OUTfromVCorrect1_data3, simp add: OUTfromVCorrect1_data4, 
simp add: OUTfromVCorrect1_data5, simp add: OUTfromVCorrect1_data6, 
simp add: OUTfromVCorrect1_data7, simp add: OUTfromVCorrect1_data8, 
simp add: OUTfromVCorrect1_data9, simp add: OUTfromVCorrect1_data10, 
simp add: OUTfromVCorrect1_data11, simp add: OUTfromVCorrect1_data12, 
simp add: OUTfromVCorrect1_data13, simp add: OUTfromVCorrect1_data14, 
simp add: OUTfromVCorrect1_data15, simp add: OUTfromVCorrect1_data16, 
simp add: OUTfromVCorrect1_data17, simp add: OUTfromVCorrect1_data18,
simp add: OUTfromVCorrect1_data19, simp add: OUTfromVCorrect1_data20,
simp add: OUTfromVCorrect1_data21, simp add: OUTfromVCorrect1_data22,
simp add: OUTfromVCorrect1_data23, simp add: OUTfromVCorrect1_data24)

lemma OUTfromVCorrect2SYSTEM: "OUTfromVCorrect2SYSTEM"
by (simp add: OUTfromVCorrect2SYSTEM_def, auto, case_tac x,
      ((simp add: OUTfromVCorrect2_def, auto, case_tac v, auto) | 
       (simp add: OUTfromVCorrect2_def) )+)

lemma OUTfromV_VARto_holds:
"OUTfromV_VARto"
by (simp add: OUTfromV_VARto_def, auto, (case_tac x, auto), (case_tac v, auto))

lemma VARfromCorrectSYSTEM_holds:
"VARfromCorrectSYSTEM"
by (simp add: VARfromCorrectSYSTEM_def AbstrLevel0 AbstrLevel1)

lemma VARtoCorrectSYSTEM_holds:
"VARtoCorrectSYSTEM"
by (simp add: VARtoCorrectSYSTEM_def AbstrLevel0 AbstrLevel1)

lemma VARusefulSYSTEM_holds:
"VARusefulSYSTEM"
by (simp add: VARusefulSYSTEM_def, auto, case_tac v, auto)


subsection ‹Elementary components›

― ‹On the abstraction level 0 only the components sA5 and sA6 are elementary›

lemma NOT_elementaryCompDD_sA1:  "¬ elementaryCompDD sA1" 
proof -
  have "outSetCorelated data2  outSetCorelated data10 = {}"
  by (metis OUTfromV.simps(2) inf_bot_left outSetCorelatedEmpty1) 
  thus ?thesis by (simp add: elementaryCompDD_def)
qed

lemma NOT_elementaryCompDD_sA2: "¬ elementaryCompDD sA2" 
proof -
  have "outSetCorelated data5  outSetCorelated data11 = {}"
  by (metis OUTfromV.simps(5) inf_bot_right inf_commute outSetCorelatedEmpty1)
  thus ?thesis by (simp add: elementaryCompDD_def)
qed 

lemma NOT_elementaryCompDD_sA3:  "¬ elementaryCompDD sA3" 
proof -
  have "outSetCorelated data6  outSetCorelated data7 = {}"
  by (metis OUTfromV.simps(7) inf_bot_right outSetCorelatedEmpty1) 
  thus ?thesis by (simp add: elementaryCompDD_def)
qed

lemma NOT_elementaryCompDD_sA4:  "¬ elementaryCompDD sA4" 
proof -
  have "outSetCorelated data3  outSetCorelated data8 = {}"
  by (metis OUTfromV.simps(8) inf_bot_left inf_commute outSetCorelatedEmpty1)
  thus ?thesis by (simp add: elementaryCompDD_def)  
qed

lemma elementaryCompDD_sA5:  "elementaryCompDD sA5" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA6:  "elementaryCompDD sA6" 
proof -
  have oSet15:"outSetCorelated data15  {}" 
    by (simp add: outSetCorelated_def, auto)
  have oSet16:"outSetCorelated data16  {}"
    by (simp add: outSetCorelated_def, auto)
  have "outSetCorelated data15  outSetCorelated data16  {}"
    by (simp add: outSetCorelated_def, auto)
  with oSet15 oSet16 show ?thesis by (simp add: elementaryCompDD_def, auto) 
qed

lemma NOT_elementaryCompDD_sA7:  "¬ elementaryCompDD sA7" 
proof - 
  have "outSetCorelated data17  outSetCorelated data18 = {}"
  by (metis (full_types) OUTfromV.simps(17) disjoint_iff_not_equal empty_iff outSetCorelatedEmpty1) 
  thus ?thesis by  (simp add: elementaryCompDD_def)
qed

lemma NOT_elementaryCompDD_sA8:  "¬ elementaryCompDD sA8" 
proof - 
  have "outSetCorelated data20  outSetCorelated data21 = {}"
  by (metis OUTfromV.simps(21) inf_bot_right outSetCorelatedEmpty1)
  thus ?thesis by  (simp add: elementaryCompDD_def)
qed

lemma NOT_elementaryCompDD_sA9:  "¬ elementaryCompDD sA9" 
proof - 
  have "outSetCorelated data23  outSetCorelated data24 = {}"
  by (metis (full_types) OUTfromV.simps(23) disjoint_iff_not_equal empty_iff outSetCorelatedEmpty1)
  thus ?thesis by  (simp add: elementaryCompDD_def)  
qed

― ‹On the abstraction level 1 all components are elementary›

lemma elementaryCompDD_sA11:  "elementaryCompDD sA11" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA12:  "elementaryCompDD sA12" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA21: "elementaryCompDD sA21" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA22: "elementaryCompDD sA22" 
proof - 
  have oSet4:"outSetCorelated data4  {}"  
    by (simp add: outSetCorelated_def, auto)
  have oSet12:"outSetCorelated data12  {}"  
    by (simp add: outSetCorelated_def, auto)
  have "outSetCorelated data4  outSetCorelated data12  {}"
    by (simp add: outSetCorelated_def, auto)
  with oSet4 oSet12 show ?thesis 
    by  (simp add: elementaryCompDD_def, auto)
qed 

lemma elementaryCompDD_sA23: "elementaryCompDD sA23" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA31: "elementaryCompDD sA31" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA32: "elementaryCompDD sA32" 
by  (simp add: elementaryCompDD_def)


lemma elementaryCompDD_sA41: "elementaryCompDD sA41" 
by  (simp add: elementaryCompDD_def) 

lemma elementaryCompDD_sA42: "elementaryCompDD sA42" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA71: "elementaryCompDD sA71" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA72: "elementaryCompDD sA72" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA81: "elementaryCompDD sA81" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA82: "elementaryCompDD sA82" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA91: "elementaryCompDD sA91" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA92: "elementaryCompDD sA92" 
by  (simp add: elementaryCompDD_def)

lemma elementaryCompDD_sA93: "elementaryCompDD sA93" 
by  (simp add: elementaryCompDD_def)

subsection ‹Source components›

― ‹Abstraction level 0›

lemma A5_NotDSource_level0: "isNotDSource level0 sA5"
by (simp add: isNotDSource_def, auto,  case_tac "Z", auto)

lemma DSourcesA1_L0: "DSources level0 sA1 = {}"
by (simp add: DSources_def, auto, case_tac "x", auto) 

lemma DSourcesA2_L0: "DSources level0 sA2 = { sA1, sA4}"
by (simp add: DSources_def AbstrLevel0, auto) 

lemma DSourcesA3_L0: "DSources level0 sA3 = { sA2 }"
by (simp add: DSources_def AbstrLevel0, auto) 

lemma DSourcesA4_L0: "DSources level0 sA4 = { sA3 }"
by (simp add: DSources_def AbstrLevel0, auto) 

lemma DSourcesA5_L0: "DSources level0 sA5 = { sA4 }"
by (simp add: DSources_def AbstrLevel0, auto)  

lemma DSourcesA6_L0: "DSources level0 sA6 = {}"
by (simp add: DSources_def, auto, case_tac "x", auto) 

lemma DSourcesA7_L0: "DSources level0 sA7 = {sA6}"
by (simp add: DSources_def AbstrLevel0, auto) 

lemma DSourcesA8_L0: "DSources level0 sA8 = {sA7, sA9}"
by (simp add: DSources_def AbstrLevel0, force)

lemma DSourcesA9_L0: "DSources level0 sA9 = {sA8}"
by (simp add: DSources_def AbstrLevel0, auto) 

lemma A1_DAcc_level0: "DAcc level0 sA1 = { sA2 }" 
by (simp add: DAcc_def  AbstrLevel0, auto)

lemma A2_DAcc_level0: "DAcc level0 sA2 = { sA3 }" 
by (simp add: DAcc_def  AbstrLevel0, force)

lemma A3_DAcc_level0: "DAcc level0 sA3 = { sA4 }" 
by (simp add: DAcc_def  AbstrLevel0, auto)

lemma A4_DAcc_level0: "DAcc level0 sA4 = { sA2, sA5 }" 
by (simp add: DAcc_def  AbstrLevel0, auto)

lemma A5_DAcc_level0: "DAcc level0 sA5 = {}" 
by (simp add: DAcc_def  AbstrLevel0, auto)

lemma A6_DAcc_level0: "DAcc level0 sA6 = { sA7 }" 
by (simp add: DAcc_def  AbstrLevel0, auto)

lemma A7_DAcc_level0: "DAcc level0 sA7 = { sA8 }" 
by (simp add: DAcc_def  AbstrLevel0, auto)

lemma A8_DAcc_level0: "DAcc level0 sA8 = { sA9 }" 
by (simp add: DAcc_def  AbstrLevel0, auto)

lemma A9_DAcc_level0: "DAcc level0 sA9 = { sA8 }" 
by (simp add: DAcc_def  AbstrLevel0, force)

lemma A8_NSources:
" C  (AbstrLevel level0). (C  sA9  C  sA8  sA8  (Sources level0 C))"
by (metis A8_DAcc_level0 A9_DAcc_level0 singleDSourceLoop)

lemma A9_NSources:
" C  (AbstrLevel level0). (C  sA9  C  sA8  sA9  (Sources level0 C))"
by (metis A8_DAcc_level0 A9_DAcc_level0 singleDSourceLoop)

lemma A7_Acc:
"(Acc level0 sA7) = {sA8, sA9}"
  by (metis A7_DAcc_level0 A8_DAcc_level0 A9_DAcc_level0 AccDef AccSigleLoop insert_commute) 

lemma A7_NSources:
" C  (AbstrLevel level0). (C  sA9  C  sA8  sA7  (Sources level0 C))"
by (metis A7_Acc Acc_Sources insert_iff singleton_iff)

lemma A5_Acc: "(Acc level0 sA5) = {}"
by (metis A5_NotDSource_level0 isNotDSource_EmptyAcc)

lemma A6_Acc:
"(Acc level0 sA6) = {sA7, sA8, sA9}"
proof -
  have daA6:  "DAcc level0 sA6 = { sA7 }"  by (rule A6_DAcc_level0)
  hence "( S  (DAcc level0 sA6). (Acc level0 S)) = (Acc level0 sA7)"  by simp
  hence aA6:"( S  (DAcc level0 sA6). (Acc level0 S)) = { sA8, sA9 }" by (simp add: A7_Acc)
  have "(Acc level0 sA6) = (DAcc level0 sA6)  ( S  (DAcc level0 sA6). (Acc level0 S))"  
    by (rule AccDef)
  with daA6 aA6 show ?thesis by auto
qed

lemma A6_NSources:
" C  (AbstrLevel level0). (C  sA9  C  sA8  C  sA7  sA6  (Sources level0 C))"
by (metis (full_types) A6_Acc A7_Acc Acc_SourcesNOT insert_iff singleton_iff)

lemma SourcesA1_L0: "Sources level0 sA1 = {}"  
by (simp add: DSourcesA1_L0 DSourcesEmptySources) 
     
lemma SourcesA2_L0: "Sources level0 sA2 = { sA1, sA2, sA3, sA4 }"
proof 
  show "Sources level0 sA2  {sA1, sA2, sA3, sA4}"
  proof -
    have A2level0:"sA2  (AbstrLevel level0)" by (simp add: AbstrLevel0)
    have sgA5:"sA5  Sources level0 sA2" 
      by (metis A5_NotDSource_level0 DSource_level NoDSourceNoSource 
            allNotDSource_NotSource isNotSource_Sources)
     from A2level0 have sgA6:"sA6  Sources level0 sA2" by (simp add: A6_NSources)
     from A2level0 have sgA7:"sA7  Sources level0 sA2" by (simp add: A7_NSources)
     from A2level0 have sgA8:"sA8  Sources level0 sA2" by (simp add: A8_NSources)
     from A2level0 have sgA9:"sA9  Sources level0 sA2" by (simp add: A9_NSources)
     have "Sources level0 sA2  {sA1, sA2, sA3, sA4, sA5, sA6, sA7, sA8, sA9}"
        by (metis AbstrLevel0 SourcesLevelX) 
     with sgA5 sgA6 sgA7 sgA8 sgA9 show "Sources level0 sA2  {sA1, sA2, sA3, sA4}"
        by blast   
  qed
next
  show "{sA1, sA2, sA3, sA4}  Sources level0 sA2"
  proof -
    have dsA4:"{ sA3 }  Sources level0 sA2"
       by (metis DSource_Sources DSourcesA2_L0 DSourcesA4_L0 
             Sources_DSources insertI1 insert_commute subset_trans)
    have "{ sA2 }  Sources level0 sA2"
      by (metis DSource_Sources DSourcesA2_L0 DSourcesA3_L0 
             DSourcesA4_L0 Sources_DSources insertI1 
             insert_commute subset_trans)
    with dsA4 show "{sA1, sA2, sA3, sA4}  Sources level0 sA2"
       by (metis DSourcesA2_L0 Sources_DSources insert_subset)
   qed
qed
        
lemma SourcesA3_L0: "Sources level0 sA3 = { sA1, sA2, sA3, sA4 }"
proof 
  show "Sources level0 sA3  {sA1, sA2, sA3, sA4}"
  proof -
    have a2:"Sources level0 sA2 = { sA1, sA2, sA3, sA4}" by (simp add: SourcesA2_L0)
    have "{ sA2 }  DSources level0 sA3" by (simp add: DSourcesA3_L0)
    with a2 show "Sources level0 sA3  {sA1, sA2, sA3, sA4}"
       by (metis DSource_Sources DSourcesA2_L0 DSourcesA4_L0 insertI1 insert_commute subset_trans)
  qed
next
   show "{sA1, sA2, sA3, sA4}  Sources level0 sA3"
   by (metis (full_types) DSource_Sources DSourcesA3_L0  SourcesA2_L0 insertI1)
qed    
             
lemma SourcesA4_L0: "Sources level0 sA4 = { sA1, sA2, sA3, sA4 }"
proof -
  have  A3s:"Sources level0 sA3 = { sA1, sA2, sA3, sA4 }" by (rule  SourcesA3_L0)
  have  "Sources level0 sA4 = {sA3}  Sources level0 sA3"
    by (metis DSourcesA4_L0 Sources_singleDSource) 
  with A3s show ?thesis by auto
qed  

lemma SourcesA5_L0: "Sources level0 sA5 = { sA1, sA2, sA3, sA4 }"
proof -  
  have  A4s:"Sources level0 sA4 = { sA1, sA2, sA3, sA4 }" by (rule  SourcesA4_L0)
  have  "Sources level0 sA5 = {sA4}  Sources level0 sA4"
    by (metis DSourcesA5_L0 Sources_singleDSource) 
  with A4s show ?thesis by auto
qed  

lemma SourcesA6_L0: "Sources level0 sA6 = {}"  
by (simp add: DSourcesA6_L0 DSourcesEmptySources) 

lemma SourcesA7_L0: "Sources level0 sA7 = { sA6 }"  
by (metis DSourcesA7_L0 SourcesA6_L0 SourcesEmptyDSources SourcesOnlyDSources singleton_iff)

 
lemma SourcesA8_L0: "Sources level0 sA8 = { sA6, sA7, sA8, sA9 }"  
proof - 
  have  dA8:"DSources level0 sA8 = {sA7, sA9}" by (rule DSourcesA8_L0)
  have  dA9:"DSources level0 sA9 = {sA8}" by (rule DSourcesA9_L0)
  have "(Sources level0 sA8) = (DSources level0 sA8)  ( S  (DSources level0 sA8). (Sources level0 S))" 
    by (rule SourcesDef)
  hence sourcesA8:"(Sources level0 sA8) = ({sA7, sA9, sA6}  (Sources level0 sA9))" 
    by (simp add:  DSourcesA8_L0 SourcesA7_L0, auto)
  have "(Sources level0 sA9) = (DSources level0 sA9)  ( S  (DSources level0 sA9). (Sources level0 S))" 
    by (rule SourcesDef)
  hence "(Sources level0 sA9) = ({sA8}  (Sources level0 sA8))" 
    by (simp add:  DSourcesA9_L0)
  with sourcesA8 have "(Sources level0 sA8) = {sA7, sA9, sA6}  {sA8}  {sA8, sA9}"
    by (metis SourcesLoop)  
  thus  ?thesis by auto
qed

lemma SourcesA9_L0: "Sources level0 sA9 = { sA6, sA7, sA8, sA9 }"  
proof - 
  have "(Sources level0 sA9) = (DSources level0 sA9)  ( S  (DSources level0 sA9). (Sources level0 S))" 
    by (rule SourcesDef)
  hence sourcesA9:"(Sources level0 sA9) = ({sA8}  (Sources level0 sA8))" 
    by (simp add:  DSourcesA9_L0)
   thus ?thesis  by (metis SourcesA8_L0 Un_insert_right insert_absorb2 insert_is_Un) 
qed
 

― ‹Abstraction level 1›

lemma A12_NotSource_level1: "isNotDSource level1 sA12"
by (simp add: isNotDSource_def, auto,  case_tac "Z", auto)

lemma A21_NotSource_level1: "isNotDSource level1 sA21"
by (simp add: isNotDSource_def, auto,  case_tac "Z", auto)

lemma A5_NotSource_level1: "isNotDSource level1 sA5"
by (simp add: isNotDSource_def, auto,  case_tac "Z", auto)

lemma A92_NotSource_level1: "isNotDSource level1 sA92"
by (simp add: isNotDSource_def, auto,  case_tac "Z", auto)

lemma A93_NotSource_level1: "isNotDSource level1 sA93"
by (simp add: isNotDSource_def, auto,  case_tac "Z", auto)


lemma A11_DAcc_level1: "DAcc level1 sA11 = { sA21, sA22, sA23 }" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A12_DAcc_level1: "DAcc level1 sA12 = {}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A21_DAcc_level1: "DAcc level1 sA21 = {}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A22_DAcc_level1: "DAcc level1 sA22 = {sA31}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A23_DAcc_level1: "DAcc level1 sA23 = {sA32}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A31_DAcc_level1: "DAcc level1 sA31 = {sA41}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A32_DAcc_level1: "DAcc level1 sA32 = {sA41}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A41_DAcc_level1: "DAcc level1 sA41 = {sA22}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A42_DAcc_level1: "DAcc level1 sA42 = {sA5}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A5_DAcc_level1: "DAcc level1 sA5 = {}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A6_DAcc_level1: "DAcc level1 sA6 = {sA71, sA72}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A71_DAcc_level1: "DAcc level1 sA71 = {sA81}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A72_DAcc_level1: "DAcc level1 sA72 = {sA82}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A81_DAcc_level1: "DAcc level1 sA81 = {sA91, sA92}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A82_DAcc_level1: "DAcc level1 sA82 = {sA93}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A91_DAcc_level1: "DAcc level1 sA91 = {sA81}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A92_DAcc_level1: "DAcc level1 sA92 = {}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A93_DAcc_level1: "DAcc level1 sA93 = {}" 
by (simp add: DAcc_def  AbstrLevel1, auto)

lemma A42_NSources_L1:
" C  (AbstrLevel level1). C  sA5  sA42  (Sources level1 C)"
by (metis A42_DAcc_level1 A5_NotSource_level1 singleDSourceEmpty4isNotSource)

lemma A5_NotSourceSet_level1 :
" C   (AbstrLevel level1). sA5  (Sources level1 C)"
by (metis A5_NotSource_level1 isNotSource_Sources)

lemma A92_NotSourceSet_level1 :
" C   (AbstrLevel level1). sA92  (Sources level1 C)" 
by (metis A92_NotSource_level1 isNotSource_Sources)

lemma A93_NotSourceSet_level1 :
" C   (AbstrLevel level1). sA93  (Sources level1 C)" 
by (metis A93_NotSource_level1 isNotSource_Sources)


lemma DSourcesA11_L1: "DSources level1 sA11 = {}"
by (simp add: DSources_def, auto, case_tac "x", auto) 

lemma DSourcesA12_L1: "DSources level1 sA12 = {}"
by (simp add: DSources_def AbstrLevel1, auto) 

lemma DSourcesA21_L1: "DSources level1 sA21 = {sA11}"
by (simp add: DSources_def AbstrLevel1, auto) 

lemma DSourcesA22_L1: "DSources level1 sA22 = {sA11, sA41}"
by (simp add: DSources_def AbstrLevel1, auto) 

lemma DSourcesA23_L1: "DSources level1 sA23 = {sA11}"
by (simp add: DSources_def AbstrLevel1, auto) 

lemma DSourcesA31_L1: "DSources level1 sA31 = { sA22 }"
by (simp add: DSources_def AbstrLevel1, auto) 

lemma DSourcesA32_L1: "DSources level1 sA32 = { sA23 }"
by (simp add: DSources_def AbstrLevel1, auto) 

lemma DSourcesA41_L1: "DSources level1 sA41 = { sA31, sA32 }"
by (simp add: DSources_def AbstrLevel1, auto) 

lemma DSourcesA42_L1: "DSources level1 sA42 = {}"
by (simp add: DSources_def AbstrLevel1, auto) 

lemma DSourcesA5_L1: "DSources level1 sA5 = { sA42 }"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma DSourcesA6_L1: "DSources level1 sA6 = {}"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma DSourcesA71_L1: "DSources level1 sA71 = { sA6 }"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma DSourcesA72_L1: "DSources level1 sA72 = { sA6 }"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma DSourcesA81_L1: "DSources level1 sA81 = { sA71, sA91 }"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma DSourcesA82_L1: "DSources level1 sA82 = { sA72 }"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma DSourcesA91_L1: "DSources level1 sA91 = { sA81 }"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma DSourcesA92_L1: "DSources level1 sA92 = { sA81 }"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma DSourcesA93_L1: "DSources level1 sA93 = { sA82 }"
by (simp add: DSources_def AbstrLevel1, auto)  

lemma A82_Acc: "(Acc level1 sA82) = {sA93}"
by (metis A82_DAcc_level1 A93_NotSource_level1 singleDSourceEmpty_Acc) 

lemma A82_NSources_L1:
" C  (AbstrLevel level1). (C  sA93  sA82  (Sources level1 C))"
by (metis A82_Acc Acc_Sources singleton_iff) 

lemma A72_Acc: "(Acc level1 sA72) = {sA82, sA93}"
proof -
  have daA72:  "DAcc level1 sA72 = { sA82 }"  by (rule A72_DAcc_level1)
  hence "( S  (DAcc level1 sA72). (Acc level1 S)) = (Acc level1 sA82)"  by simp
  hence aA72:"( S  (DAcc level1 sA72). (Acc level1 S)) = { sA93 }" by (simp add: A82_Acc)
  have "(Acc level1 sA72) = (DAcc level1 sA72)  ( S  (DAcc level1 sA72). (Acc level1 S))"  
    by (rule AccDef)
  with daA72 aA72 show ?thesis by auto
qed

lemma A72_NSources_L1:
" C  (AbstrLevel level1). (C  sA93  C  sA82  sA72  (Sources level1 C))"
by (metis A72_Acc Acc_Sources insert_iff singleton_iff) 

lemma A92_Acc: "(Acc level1 sA92) = {}"
by (metis A92_NotSource_level1 isNotDSource_EmptyAcc)

lemma A92_NSources_L1:
" C  (AbstrLevel level1). (sA92  (Sources level1 C))"
by (metis A92_NotSourceSet_level1)
 
lemma A91_Acc: "(Acc level1 sA91) = {sA81, sA91, sA92}"
proof -
  have da91:  "DAcc level1 sA91 = { sA81 }"  by (rule A91_DAcc_level1)
  hence a91:"( S  (DAcc level1 sA91). (Acc level1 S)) = (Acc level1 sA81)"  by simp
  have "(Acc level1 sA91) = (DAcc level1 sA91)  ( S  (DAcc level1 sA91). (Acc level1 S))"  by (rule AccDef)
  with da91 a91 have acc91:"(Acc level1 sA91) = { sA81 }  (Acc level1 sA81)" by simp
  have da81:  "DAcc level1 sA81 = { sA91, sA92 }"  by (rule A81_DAcc_level1)
  hence a81:"( S  (DAcc level1 sA81). (Acc level1 S)) = (Acc level1 sA92)  (Acc level1 sA91)"  by auto
  have "(Acc level1 sA81) = (DAcc level1 sA81)  ( S  (DAcc level1 sA81). (Acc level1 S))"  by (rule AccDef)
  with da81 a81 have acc81: "(Acc level1 sA81) = { sA91, sA92 }   (Acc level1 sA91)"
    by (metis A92_Acc sup_bot.left_neutral)
  from acc91 acc81 have "(Acc level1 sA91) = { sA81 }  { sA91, sA92 }   {sA91, sA81}"
   by (metis AccLoop)
  thus ?thesis by auto
qed

lemma A91_NSources_L1:
" C  (AbstrLevel level1). (C  sA92  C  sA91  C  sA81  sA91  (Sources level1 C))"
proof -
  have " C  (AbstrLevel level1). (C  sA92  C  sA91  C  sA81   (C  (Acc level1 sA91)))"
    by (metis A91_Acc insert_iff singleton_iff)
  thus ?thesis  by (metis Acc_SourcesNOT) 
qed

lemma A81_Acc: "(Acc level1 sA81) = {sA81, sA91, sA92}"
proof -
  have da91:  "DAcc level1 sA91 = { sA81 }"  by (rule A91_DAcc_level1)
  hence a91:"( S  (DAcc level1 sA91). (Acc level1 S)) = (Acc level1 sA81)"  by simp
  have "(Acc level1 sA91) = (DAcc level1 sA91)  ( S  (DAcc level1 sA91). (Acc level1 S))"  by (rule AccDef)
  with da91 a91 have acc91:"(Acc level1 sA91) = { sA81 }  (Acc level1 sA81)" by simp
  have da81:  "DAcc level1 sA81 = { sA91, sA92 }"  by (rule A81_DAcc_level1)
  hence a81:"( S  (DAcc level1 sA81). (Acc level1 S)) = (Acc level1 sA92)  (Acc level1 sA91)"  by auto
  have "(Acc level1 sA81) = (DAcc level1 sA81)  ( S  (DAcc level1 sA81). (Acc level1 S))"  by (rule AccDef)
  with da81 a81 have acc81: "(Acc level1 sA81) = { sA91, sA92 }   (Acc level1 sA91)"
    by (metis A92_Acc sup_bot.left_neutral)
  from acc81 acc91 have "(Acc level1 sA81) =  { sA91, sA92 }   { sA81 }  {sA81, sA91}"
   by (metis AccLoop)
  thus ?thesis by auto
qed

lemma A81_NSources_L1:
" C  (AbstrLevel level1). (C  sA92  C  sA91  C  sA81  sA81  (Sources level1 C))"
proof -
  have " C  (AbstrLevel level1). (C  sA92  C  sA91  C  sA81   (C  (Acc level1 sA81)))"
    by (metis A81_Acc insert_iff singleton_iff)
  thus ?thesis  by (metis Acc_SourcesNOT) 
qed

lemma A71_Acc: "(Acc level1 sA71) = {sA81, sA91, sA92}"
proof -
  have da71:  "DAcc level1 sA71 = { sA81 }"  by (rule A71_DAcc_level1)
  hence a71:"( S  (DAcc level1 sA71). (Acc level1 S)) = (Acc level1 sA81)"  by simp
  have "(Acc level1 sA71) = (DAcc level1 sA71)  ( S  (DAcc level1 sA71). (Acc level1 S))"  by (rule AccDef)
  with da71 a71 show ?thesis by (metis A91_Acc A91_DAcc_level1 AccDef) 
qed

lemma A71_NSources_L1:
" C  (AbstrLevel level1). (C  sA92  C  sA91  C  sA81  sA71  (Sources level1 C))"
proof -
  have " C  (AbstrLevel level1). (C  sA92  C  sA91  C  sA81   (C  (Acc level1 sA71)))"
    by (metis A71_Acc insert_iff singleton_iff)
  thus ?thesis  by (metis Acc_SourcesNOT) 
qed

lemma A6_Acc_L1:
"(Acc level1 sA6) = {sA71, sA72, sA81, sA82, sA91, sA92, sA93}"
proof -
  have daA6:  "DAcc level1 sA6 = { sA71, sA72 }"  by (rule A6_DAcc_level1)
  hence "( S  (DAcc level1 sA6). (Acc level1 S)) = (Acc level1 sA71)  (Acc level1 sA72)"  by simp
  hence aA6:"( S  (DAcc level1 sA6). (Acc level1 S)) = {sA81, sA91, sA92}  {sA82, sA93}" 
    by (simp add: A71_Acc A72_Acc)
  have "(Acc level1 sA6) = (DAcc level1 sA6)  ( S  (DAcc level1 sA6). (Acc level1 S))"  
    by (rule AccDef)
  with daA6 aA6 show ?thesis by auto
qed

lemma A6_NSources_L1Acc:
" C  (AbstrLevel level1). (C  (Acc level1 sA6)  sA6  (Sources level1 C))"
by (metis Acc_SourcesNOT)


lemma A6_NSources_L1:
" C  (AbstrLevel level1). (C  sA93  C  sA92  C  sA91  C  sA82   C  sA81  C  sA72  C  sA71 
 sA6  (Sources level1 C))"
proof -
  have " C  (AbstrLevel level1). 
  (C  sA93  C  sA92  C  sA91  C  sA82   C  sA81  C  sA72  C  sA71 
   (C  (Acc level1 sA6)))"
     by (metis A6_Acc_L1 empty_iff insert_iff)
  thus ?thesis  by (metis Acc_SourcesNOT) 
qed

lemma A5_Acc_L1: "(Acc level1 sA5) = {}"
by (metis A5_NotSource_level1 isNotDSource_EmptyAcc)


lemma SourcesA11_L1: "Sources level1 sA11 = {}"  
by (simp add: DSourcesA11_L1 DSourcesEmptySources) 

lemma SourcesA12_L1: "Sources level1 sA12 = {}"  
by (simp add: DSourcesA12_L1  DSourcesEmptySources) 

lemma SourcesA21_L1: "Sources level1 sA21 = {sA11}"
by (simp add: DSourcesA21_L1 SourcesA11_L1  Sources_singleDSource) 

lemma SourcesA22_L1: "Sources level1 sA22 = {sA11, sA22,  sA23, sA31, sA32, sA41}"
proof
  show "Sources level1 sA22  {sA11, sA22, sA23, sA31, sA32, sA41}"
  proof -
     have A2level1:"sA22  (AbstrLevel level1)" by (simp add: AbstrLevel1)
     from A2level1 have sgA42:"sA42  Sources level1 sA22" by (metis A42_NSources_L1 CSet.distinct(347)) 
     have sgA5:"sA5  Sources level1 sA22"
     by (metis A5_NotSource_level1 Acc_Sources all_not_in_conv isNotDSource_EmptyAcc)  
     have sgA12:"sA12  Sources level1 sA22" by (metis A12_NotSource_level1 A2level1 isNotSource_Sources)   
     have sgA21:"sA21  Sources level1 sA22"
     by (metis A21_NotSource_level1 DAcc_DSourcesNOT NDSourceExistsDSource empty_iff isNotDSource_EmptyDAcc)
     from A2level1 have sgA6:"sA6  Sources level1 sA22" by (simp add: A6_NSources_L1)
     from A2level1 have sgA71:"sA71  Sources level1 sA22" by (simp add: A71_NSources_L1)
     from A2level1 have sgA72:"sA72  Sources level1 sA22" by (simp add: A72_NSources_L1)
     from A2level1 have sgA81:"sA81  Sources level1 sA22" by (simp add: A81_NSources_L1)
     from A2level1 have sgA82:"sA82  Sources level1 sA22" by (simp add: A82_NSources_L1)
     from A2level1 have sgA91:"sA91  Sources level1 sA22" by (simp add: A91_NSources_L1)
     from A2level1 have sgA92:"sA92  Sources level1 sA22" by (simp add: A92_NSources_L1) 
     from A2level1 have sgA93:"sA93  Sources level1 sA22" by (metis A93_NotSourceSet_level1)  
     have "Sources level1 sA22  {sA11, sA12, sA21, sA22, sA23, sA31, sA32, 
        sA41, sA42, sA5, sA6, sA71, sA72, sA81, sA82, sA91, sA92, sA93}"
        by (metis AbstrLevel1 SourcesLevelX) 
     with sgA5 sgA12 sgA21 sgA42 sgA6 sgA71 sgA72 sgA81 sgA82 sgA91 sgA92 sgA93 show 
     "Sources level1 sA22  {sA11, sA22, sA23, sA31, sA32, sA41}"
         by auto 
    qed
next 
  show "{sA11, sA22, sA23, sA31, sA32, sA41}  Sources level1 sA22" 
  proof - 
    have sDef:"(Sources level1 sA22) = (DSources level1 sA22)  ( S  (DSources level1 sA22). (Sources level1 S))" 
       by (rule SourcesDef) 
    have A11s: "sA11  Sources level1 sA22" by (metis DSourceIsSource DSourcesA22_L1 insertI1)  
    have A41s: "sA41  Sources level1 sA22" by (metis (full_types) DSourceIsSource DSourcesA22_L1 insertCI)
    have A31s: "sA31  Sources level1 sA22" 
      by (metis (full_types) A41s DSourceIsSource DSourcesA41_L1 SourcesTrans insertCI)
    have A32s: "sA32  Sources level1 sA22"
      by (metis A32_DAcc_level1 A41s DAcc_DSourcesNOT DSourceOfSource insertI1)
    have A23s: "sA23  Sources level1 sA22"  by (metis A32s DSourceOfSource DSourcesA32_L1 insertI1)
    have A22s: "sA22  Sources level1 sA22"  by (metis A31s DSourceOfSource DSourcesA31_L1 insertI1)
    with A11s A22s A23s A31s A32s A41s show ?thesis by auto
    qed
qed 

lemma SourcesA23_L1: "Sources level1 sA23 = {sA11}"
by (simp add: DSourcesA23_L1 SourcesA11_L1  Sources_singleDSource)  

lemma SourcesA31_L1: "Sources level1 sA31 = {sA11, sA22, sA23, sA31, sA32, sA41}"
by (metis DSourcesA31_L1 SourcesA22_L1 Sources_singleDSource Un_insert_right insert_absorb2 insert_is_Un)

lemma SourcesA32_L1: "Sources level1 sA32 = {sA11, sA23}"
by (metis DSourcesA32_L1 SourcesA23_L1 Sources_singleDSource Un_insert_right insert_is_Un)
 
lemma SourcesA41_L1: "Sources level1 sA41 = {sA11, sA22, sA23, sA31, sA32, sA41}"
by (metis DSourcesA41_L1 SourcesA31_L1 SourcesA32_L1 Sources_2DSources Un_absorb Un_commute Un_insert_left)

lemma SourcesA42_L1: "Sources level1 sA42 = {}"  
by (simp add: DSourcesA42_L1  DSourcesEmptySources) 

lemma SourcesA5_L1: "Sources level1 sA5 = {sA42}"
by (simp add: DSourcesA5_L1 SourcesA42_L1  Sources_singleDSource) 

lemma SourcesA6_L1: "Sources level1 sA6 = {}"  
by (simp add: DSourcesA6_L1 DSourcesEmptySources) 

lemma SourcesA71_L1: "Sources level1 sA71 = {sA6}"
by (metis DSourcesA71_L1 SourcesA6_L1 SourcesEmptyDSources SourcesOnlyDSources singleton_iff)   

lemma SourcesA81_L1: "Sources level1 sA81 = {sA6, sA71, sA81, sA91}"  
proof - 
  have  dA81:"DSources level1 sA81 = {sA71, sA91}" by (rule DSourcesA81_L1)
  have  dA91:"DSources level1 sA91 = {sA81}" by (rule DSourcesA91_L1)
  have "(Sources level1 sA81) = (DSources level1 sA81)  ( S  (DSources level1 sA81). (Sources level1 S))" 
    by (rule SourcesDef)
  with dA81 have  "(Sources level1 sA81) = ({sA71, sA91}  (Sources level1 sA71)  (Sources level1 sA91))"
    by (metis (hide_lams, no_types) SUP_empty UN_insert Un_insert_left sup_bot.left_neutral sup_commute)
  hence sourcesA81:"(Sources level1 sA81) = ({sA71, sA91, sA6}  (Sources level1 sA91))"
    by (metis SourcesA71_L1 insert_is_Un sup_assoc)
  have "(Sources level1 sA91) = (DSources level1 sA91)  ( S  (DSources level1 sA91). (Sources level1 S))" 
    by (rule SourcesDef)
  with dA91 have "(Sources level1 sA91) = ({sA81}  (Sources level1 sA81))"  by simp
  with sourcesA81 have "(Sources level1 sA81) = {sA71, sA91, sA6}  {sA81}  {sA81, sA91}"
    by (metis SourcesLoop)  
  thus  ?thesis by auto
qed

(*lemma Sources_singleDSource:
  assumes "DSources i S = {C}" 
  shows    "Sources i S = {C} ∪ Sources i C" *)
lemma SourcesA91_L1: "Sources level1 sA91 = {sA6, sA71, sA81, sA91}"
proof -
  have  "DSources level1 sA91 = {sA81}" by (rule DSourcesA91_L1)
  thus ?thesis by (metis SourcesA81_L1 Sources_singleDSource 
          Un_empty_left Un_insert_left insert_absorb2 insert_commute) 
qed

lemma SourcesA92_L1: "Sources level1 sA92 = {sA6, sA71, sA81, sA91}"
by (metis DSourcesA91_L1 DSourcesA92_L1 SourcesA91_L1 Sources_singleDSource) 

lemma SourcesA72_L1: "Sources level1 sA72 = {sA6}"
by (metis DSourcesA6_L1 DSourcesA72_L1 SourcesOnlyDSources singleton_iff)   

lemma SourcesA82_L1: "Sources level1 sA82 = {sA6, sA72}"  
proof - 
  have  dA82:"DSources level1 sA82 = {sA72}" by (rule DSourcesA82_L1)
  have "(Sources level1 sA82) = (DSources level1 sA82)  ( S  (DSources level1 sA82). (Sources level1 S))" 
    by (rule SourcesDef)
  with dA82 have "(Sources level1 sA82) =  {sA72}  (Sources level1 sA72)"  by simp
  thus ?thesis by (metis SourcesA72_L1 Un_commute insert_is_Un) 
qed

lemma SourcesA93_L1: "Sources level1 sA93 = {sA6, sA72, sA82}"
by (metis DSourcesA93_L1 SourcesA82_L1 Sources_singleDSource Un_insert_right insert_is_Un)   


― ‹Abstraction level 2›

lemma SourcesS1_L2: "Sources level2 sS1 = {}"
proof -
  have "DSources level2 sS1 = {}"  by (simp add: DSources_def AbstrLevel2, auto)
  thus ?thesis  by (simp add: DSourcesEmptySources)
qed

lemma SourcesS2_L2: "Sources level2 sS2 = {}"
proof -
  have "DSources level2 sS2 = {}"  by (simp add: DSources_def AbstrLevel2, auto)
  thus ?thesis  by (simp add: DSourcesEmptySources)
qed

lemma SourcesS3_L2: "Sources level2 sS3 = {sS2}"
proof -
  have DSourcesS3:"DSources level2 sS3 = {sS2}"  by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS2 = {}"  by (rule SourcesS2_L2)
  with DSourcesS3 show ?thesis  by  (simp add: Sources_singleDSource)
qed

lemma SourcesS4_L2:  "Sources level2 sS4 = {sS2}"
proof -
  have DSourcesS4:"DSources level2 sS4 = {sS2}" by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS2 = {}"  by (rule SourcesS2_L2)
  with DSourcesS4 show ?thesis  by  (simp add: Sources_singleDSource)
qed

lemma SourcesS5_L2:  "Sources level2 sS5 = {sS2, sS4}"
proof -
  have DSourcesS5:"DSources level2 sS5 = {sS4}"  by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS4 = {sS2}" by (rule SourcesS4_L2)
  with DSourcesS5 show ?thesis  by  (simp add: Sources_singleDSource)
qed

lemma SourcesS6_L2:  "Sources level2 sS6 = {sS2, sS4, sS5}"
proof -
  have DSourcesS6:"DSources level2 sS6 = {sS2, sS5}"  by (simp add: DSources_def AbstrLevel2, auto)
  have SourcesS2:"Sources level2 sS2 = {}"  by (rule SourcesS2_L2)
  have "Sources level2 sS5 = {sS2, sS4}"  by (rule SourcesS5_L2)
  with  SourcesS2 DSourcesS6 show ?thesis  by (simp add: Sources_2DSources, auto)
qed

lemma SourcesS7_L2:  "Sources level2 sS7 = {}"
proof -
  have "DSources level2 sS7 = {}"  by (simp add: DSources_def AbstrLevel2, auto)
  thus ?thesis  by (simp add: DSourcesEmptySources)
qed

lemma SourcesS8_L2:
 "Sources level2 sS8 = {sS7}"
proof -
  have DSourcesS8:"DSources level2 sS8 = {sS7}"  by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS7 = {}"  by (rule SourcesS7_L2)
  with DSourcesS8 show ?thesis  by  (simp add: Sources_singleDSource)
qed

lemma SourcesS9_L2:
 "Sources level2 sS9 = {}"
proof -
  have "DSources level2 sS9 = {}"  by (simp add: DSources_def AbstrLevel2, auto)
  thus ?thesis  by (simp add: DSourcesEmptySources)
qed

lemma SourcesS10_L2: "Sources level2 sS10 = {sS9}"
proof -
  have DSourcesS10:"DSources level2 sS10 = {sS9}" by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS9 = {}" by (rule SourcesS9_L2)
  with DSourcesS10 show ?thesis  by  (simp add: Sources_singleDSource)
qed

lemma SourcesS11_L2: "Sources level2 sS11 = {sS9}"
proof -
  have DSourcesS11:"DSources level2 sS11 = {sS9}"  by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS9 = {}"  by (rule SourcesS9_L2)
  with DSourcesS11 show ?thesis  by  (simp add: Sources_singleDSource)
qed

lemma SourcesS12_L2: "Sources level2 sS12 = {sS9, sS10}"
proof -
  have DSourcesS12:"DSources level2 sS12 = {sS10}" by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS10 = {sS9}"  by (rule SourcesS10_L2)
  with DSourcesS12 show ?thesis  by  (simp add: Sources_singleDSource)
qed

lemma SourcesS13_L2: "Sources level2 sS13 = {sS9, sS10, sS12}"
proof -
  have DSourcesS13:"DSources level2 sS13 = {sS12}"  by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS12 = {sS9, sS10}" by (rule SourcesS12_L2)
  with DSourcesS13 show ?thesis by  (simp add: Sources_singleDSource)
qed

lemma SourcesS14_L2: "Sources level2 sS14 = {sS9, sS11}"
proof -
  have DSourcesS14:"DSources level2 sS14 = {sS11}"  by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS11 = {sS9}"  by (rule SourcesS11_L2)
  with DSourcesS14 show ?thesis  by  (simp add: Sources_singleDSource)
qed

lemma SourcesS15_L2: "Sources level2 sS15 = {sS9, sS11, sS14}"
proof -
  have DSourcesS15:"DSources level2 sS15= {sS14}"  by (simp add: DSources_def AbstrLevel2, auto)
  have "Sources level2 sS14 = {sS9, sS11}"  by (rule SourcesS14_L2)
  with DSourcesS15 show ?thesis by  (simp add: Sources_singleDSource)
qed


subsection ‹Minimal sets of components to prove certain properties›

lemma minSetOfComponentsTestL2p1:
"minSetOfComponents level2 {data10, data13} = {sS1}"
proof - 
  have outL2:"outSetOfComponents level2 {data10, data13} = {sS1}"
    by (simp add: outSetOfComponents_def  AbstrLevel2, auto) 
  have "Sources level2 sS1 = {}" by (simp add: SourcesS1_L2)
  with outL2 show ?thesis by (simp add:  minSetOfComponents_def)
qed

lemma NOT_noIrrelevantChannelsTestL2p1:
" ¬ noIrrelevantChannels level2 {data10, data13}"
by (simp add: noIrrelevantChannels_def systemIN_def minSetOfComponentsTestL2p1 AbstrLevel2)

lemma NOT_allNeededINChannelsTestL2p1:
"¬ allNeededINChannels  level2 {data10, data13}"
by (simp add: allNeededINChannels_def minSetOfComponentsTestL2p1  systemIN_def AbstrLevel2)

lemma minSetOfComponentsTestL2p2:
"minSetOfComponents level2 {data1, data12} = {sS2, sS4, sS5, sS6}"
proof - 
  have outL2:"outSetOfComponents level2 {data1, data12} = {sS6}"
    by (simp add: outSetOfComponents_def  AbstrLevel2, auto) 
  have "Sources level2 sS6 = {sS2, sS4, sS5}"
    by  (simp add: SourcesS6_L2) 
  with outL2 show ?thesis 
    by (simp add:  minSetOfComponents_def) 
qed
 
lemma noIrrelevantChannelsTestL2p2:
"noIrrelevantChannels level2  {data1, data12}"
by (simp add: noIrrelevantChannels_def systemIN_def minSetOfComponentsTestL2p2 AbstrLevel2)

lemma allNeededINChannelsTestL2p2:
"allNeededINChannels  level2 {data1, data12}"
by (simp add: allNeededINChannels_def minSetOfComponentsTestL2p2  systemIN_def AbstrLevel2)

lemma minSetOfComponentsTestL1p3:
"minSetOfComponents level1 {data1, data10, data11} = {sA12, sA11, sA21}"
proof - 
  have sg1:"outSetOfComponents level1 {data1, data10, data11} = {sA12, sA21}"
    by (simp add: outSetOfComponents_def  AbstrLevel1, auto)  
  have "DSources level1 sA12 = {}"
    by (simp add: DSources_def AbstrLevel1, auto) 
  hence sg2:"Sources level1 sA12 = {}"
    by (simp add: DSourcesEmptySources)  
  have sg3:"DSources level1 sA21 = {sA11}"
    by (simp add: DSources_def AbstrLevel1, auto) 
  have sg4:"DSources level1 sA11 = {}"
    by (simp add: DSources_def AbstrLevel1, auto)  
  hence "Sources level1 sA21 = {sA11}"
    by (metis SourcesOnlyDSources sg3 singleton_iff)
  from this and sg1 and sg2 show ?thesis
     by (simp add:  minSetOfComponents_def, blast) 
qed

lemma noIrrelevantChannelsTestL1p3:
"noIrrelevantChannels level1  {data1, data10, data11}"
by (simp add: noIrrelevantChannels_def systemIN_def minSetOfComponentsTestL1p3 AbstrLevel1)

lemma allNeededINChannelsTestL1p3:
"allNeededINChannels  level1 {data1, data10, data11}"
by (simp add: allNeededINChannels_def minSetOfComponentsTestL1p3  systemIN_def AbstrLevel1)

lemma minSetOfComponentsTestL2p3:
"minSetOfComponents level2 {data1, data10, data11} = {sS1, sS2, sS3}"
proof - 
  have sg1:"outSetOfComponents level2 {data1, data10, data11} = {sS1, sS3}"
    by (simp add: outSetOfComponents_def  AbstrLevel2, auto)  
  have sS1:"Sources level2 sS1 = {}" by (simp add: SourcesS1_L2)
  have "Sources level2 sS3 = {sS2}" by (simp add: SourcesS3_L2)
   with sg1 sS1 show ?thesis
     by (simp add:  minSetOfComponents_def, blast) 
qed
 
lemma noIrrelevantChannelsTestL2p3:
"noIrrelevantChannels level2  {data1, data10, data11}"
by (simp add: noIrrelevantChannels_def systemIN_def minSetOfComponentsTestL2p3 AbstrLevel2)

lemma allNeededINChannelsTestL2p3:
"allNeededINChannels  level2 {data1, data10, data11}"
by (simp add: allNeededINChannels_def minSetOfComponentsTestL2p3  systemIN_def AbstrLevel2)

end