(*<*) (* 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