Theory Secrecy

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

section ‹Secrecy: Definitions and properties›

theory Secrecy
imports Secrecy_types inout ListExtras
begin

― ‹Encryption, decryption, signature creation and signature verification functions›
― ‹For these functions we define only their signatures and general axioms,›
― ‹because in order to reason effectively, we view them as abstract functions and›
― ‹abstract from their implementation details› 
consts 
  Enc  :: "Keys ⇒ Expression list ⇒ Expression list"
  Decr :: "Keys ⇒ Expression list ⇒ Expression list"
  Sign :: "Keys ⇒ Expression list ⇒ Expression list"
  Ext   :: "Keys ⇒ Expression list ⇒ Expression list"

― ‹Axioms on relations between encription and decription keys›
axiomatization
   EncrDecrKeys :: "Keys  ⇒ Keys ⇒ bool"
where
ExtSign: 
 "EncrDecrKeys K1 K2 ⟶ (Ext K1 (Sign K2 E)) = E"  and
DecrEnc:
 "EncrDecrKeys K1 K2 ⟶ (Decr K2 (Enc K1 E)) = E"

― ‹Set of private keys of a component›
consts
 specKeys :: "specID ⇒ Keys set"
― ‹Set of unguessable values used by a component›
consts 
 specSecrets :: "specID ⇒ Secrets set"

― ‹Join set of private keys and unguessable values used by a component›
definition
  specKeysSecrets :: "specID ⇒ KS set"
where
 "specKeysSecrets C ≡
  {y .  ∃ x. y = (kKS x)  ∧ (x ∈ (specKeys C))} ∪
  {z .  ∃ s. z = (sKS s)  ∧ (s ∈ (specSecrets C))}"

― ‹Predicate defining that a list of expression items does not contain›
― ‹any private key  or unguessable value used by a component›
definition
  notSpecKeysSecretsExpr :: "specID ⇒  Expression list ⇒ bool"
where
     "notSpecKeysSecretsExpr P e ≡
     (∀ x. (kE x) mem e ⟶ (kKS x) ∉ specKeysSecrets P) ∧
     (∀ y. (sE y) mem e ⟶ (sKS y) ∉ specKeysSecrets P)"

― ‹If a component is a composite one, the set of its private keys› 
― ‹is a union of the subcomponents' sets of the private keys›
definition
  correctCompositionKeys ::  "specID ⇒ bool"
where
  "correctCompositionKeys x ≡
    subcomponents x ≠ {} ⟶ 
    specKeys x =  ⋃ (specKeys ` (subcomponents x))" 

― ‹If a component is a composite one, the set of its unguessable values› 
― ‹is a union of the subcomponents' sets of the unguessable values›
definition
  correctCompositionSecrets ::  "specID ⇒ bool"
where
  "correctCompositionSecrets x ≡
    subcomponents x ≠ {} ⟶ 
    specSecrets x =  ⋃ (specSecrets ` (subcomponents x))" 

― ‹If a component is a composite one, the set of its private keys and› 
― ‹unguessable values is a union of the corresponding sets of its subcomponents›
definition
  correctCompositionKS ::  "specID ⇒ bool"
where
  "correctCompositionKS x ≡
    subcomponents x ≠ {} ⟶ 
    specKeysSecrets x =  ⋃ (specKeysSecrets ` (subcomponents x))" 

― ‹Predicate defining set of correctness properties of the component's›
― ‹interface  and relations on its private keys and unguessable values›
definition
  correctComponentSecrecy  ::  "specID ⇒ bool"
where 
  "correctComponentSecrecy x ≡ 
    correctCompositionKS x ∧ 
    correctCompositionSecrets x ∧ 
    correctCompositionKeys x ∧ 
    correctCompositionLoc x ∧
    correctCompositionIn x ∧
    correctCompositionOut x ∧ 
    correctInOutLoc x"

― ‹Predicate exprChannel I E defines whether the expression item E can be sent via the channel I›    
consts
 exprChannel :: "chanID ⇒ Expression ⇒ bool"

― ‹Predicate eoutM sP M E defines whether the component sP may eventually›
― ‹output an expression E if there exists a time interval t of› 
― ‹an output channel which contains this expression E›
definition
  eout :: "specID  ⇒ Expression ⇒ bool"
where
 "eout sP E ≡ 
  ∃ (ch :: chanID). ((ch ∈ (out sP)) ∧ (exprChannel ch E))"

― ‹Predicate eout sP E defines whether the component sP may eventually›
― ‹output an expression E via subset of channels M,›
― ‹which is a subset of output channels of sP,›
― ‹and if there exists a time interval t of› 
― ‹an output channel which contains this expression E›
definition
  eoutM :: "specID  ⇒ chanID set ⇒ Expression ⇒ bool"
where
 "eoutM sP M E ≡ 
  ∃ (ch :: chanID). ((ch ∈ (out sP)) ∧ (ch ∈ M) ∧ (exprChannel ch E))"

― ‹Predicate ineM sP M E defines whether a component sP may eventually›
― ‹get an expression E  if there exists a time interval t of› 
― ‹an input stream  which contains this expression E›
definition
  ine :: "specID  ⇒ Expression ⇒ bool"
where
 "ine sP E ≡ 
  ∃ (ch :: chanID). ((ch ∈ (ins sP)) ∧ (exprChannel ch E))"

― ‹Predicate ine sP E defines whether a component sP may eventually›
― ‹get an expression E via subset of channels M,›
― ‹which is a subset of input channels of sP,›
― ‹and if there exists a time interval t of› 
― ‹an input stream  which contains this expression E›
definition
  ineM :: "specID  ⇒ chanID set ⇒ Expression ⇒ bool"
where
 "ineM sP M E ≡ 
  ∃ (ch :: chanID). ((ch ∈ (ins sP)) ∧ (ch ∈ M) ∧ (exprChannel ch E))"

― ‹This predicate defines whether an input channel ch of a component sP›
― ‹is the only one input channel of this component›
― ‹via which it may eventually output an expression E›
definition
  out_exprChannelSingle :: "specID  ⇒ chanID ⇒ Expression ⇒ bool"
where
 "out_exprChannelSingle sP ch E ≡ 
  (ch ∈ (out sP)) ∧  
  (exprChannel ch E)  ∧
  (∀ (x :: chanID) (t :: nat). ((x ∈ (out sP)) ∧ (x ≠ ch) ⟶ ¬ exprChannel x E))"

― ‹This predicate  yields true if only the channels from the set chSet,›
― ‹which is a subset of input channels of the  component sP,›
― ‹may eventually output an expression E›
definition
 out_exprChannelSet :: "specID  ⇒ chanID set ⇒ Expression ⇒ bool"
where
 "out_exprChannelSet sP chSet E ≡ 
   ((∀ (x ::chanID). ((x ∈ chSet) ⟶ ((x ∈ (out sP)) ∧ (exprChannel x E))))
   ∧
   (∀ (x :: chanID). ((x ∉ chSet) ∧ (x ∈ (out sP)) ⟶ ¬ exprChannel x E)))"

― ‹This redicate defines whether›
― ‹an input channel ch of a component sP is the only one input channel›
― ‹of this component via which it may eventually get an expression E›
definition
 ine_exprChannelSingle :: "specID  ⇒ chanID ⇒ Expression ⇒ bool"
where
 "ine_exprChannelSingle sP ch E ≡ 
  (ch ∈ (ins sP)) ∧
  (exprChannel ch E)  ∧
  (∀ (x :: chanID) (t :: nat). (( x ∈ (ins sP)) ∧ (x ≠ ch) ⟶ ¬ exprChannel x E))"

― ‹This predicate yields true if the component sP may eventually›
― ‹get an expression E only via the channels from the set chSet,›
― ‹which is a subset of input channels of sP›
definition
 ine_exprChannelSet :: "specID  ⇒ chanID set ⇒ Expression ⇒ bool"
where
 "ine_exprChannelSet sP chSet E ≡ 
   ((∀ (x ::chanID). ((x ∈ chSet) ⟶ ((x ∈ (ins sP)) ∧ (exprChannel x E))))
   ∧
   (∀ (x :: chanID). ((x ∉ chSet) ∧ ( x ∈ (ins sP)) ⟶ ¬ exprChannel x E)))"

― ‹If a list of expression items does not contain any private key›
― ‹or unguessable value of a component P, then the first element› 
― ‹of the list is neither a private key nor unguessable value of P›
lemma notSpecKeysSecretsExpr_L1:
assumes "notSpecKeysSecretsExpr P (a # l)"
shows    "notSpecKeysSecretsExpr P [a]"
using assms by (simp add: notSpecKeysSecretsExpr_def)

― ‹If a list of expression items does not contain any private key›
― ‹or unguessable value of a component P, then this list without its first› 
― ‹element does not contain them too›
lemma notSpecKeysSecretsExpr_L2:
assumes "notSpecKeysSecretsExpr P (a # l)"
shows    "notSpecKeysSecretsExpr P l" 
using assms by (simp add: notSpecKeysSecretsExpr_def)

― ‹If a channel belongs to the set of input channels of a component P›
― ‹and does not belong to the set of local channels of the compositon of P and Q› 
― ‹then it belongs to the set of input channels of this composition›
lemma correctCompositionIn_L1:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionIn PQ" 
       and "ch ∉ loc PQ"
       and "ch ∈ ins P" 
shows    "ch ∈ ins PQ"
using assms by (simp add: correctCompositionIn_def)

― ‹If a channel belongs to the set of input channels of the compositon of P and Q›
― ‹then it belongs to the set of input channels either of P or of Q›
lemma correctCompositionIn_L2:
assumes "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ" 
       and "ch ∈ ins PQ" 
shows    "(ch ∈ ins P) ∨ (ch ∈ ins Q)" 
using assms by (simp add: correctCompositionIn_def)

lemma ineM_L1:
assumes "ch ∈ M" 
       and "ch ∈ ins P"
       and "exprChannel ch E"
shows    "ineM P M E"
using assms by (simp add: ineM_def, blast)

lemma ineM_ine:
assumes "ineM P M E"
shows    "ine P E"
using assms by (simp add: ineM_def ine_def, blast)

lemma not_ine_ineM:
assumes "¬ ine P E"
shows    "¬ ineM P M E"
using assms by (simp add: ineM_def ine_def)

lemma eoutM_eout:
assumes "eoutM P M E"
shows    "eout P E"
using assms by (simp add: eoutM_def eout_def, blast)

lemma not_eout_eoutM:
assumes "¬ eout P E"
shows    "¬ eoutM P M E"
using assms by (simp add: eoutM_def eout_def)

lemma correctCompositionKeys_subcomp1:
assumes "correctCompositionKeys C"
        and "x ∈ subcomponents C" 
        and "xb ∈ specKeys C"
shows "∃ x ∈ subcomponents C. (xb ∈ specKeys x)"
using assms by (simp add: correctCompositionKeys_def, auto)

lemma correctCompositionSecrets_subcomp1:
assumes "correctCompositionSecrets C" 
        and "x ∈ subcomponents C"
        and "s ∈ specSecrets C"
shows  "∃ x ∈ subcomponents C. (s ∈ specSecrets x)"
using assms by (simp add: correctCompositionSecrets_def, auto)

lemma correctCompositionKeys_subcomp2:
assumes "correctCompositionKeys C"
       and "xb ∈ subcomponents C"
       and "xc ∈ specKeys xb"
shows "xc ∈ specKeys C"
using assms by (simp add: correctCompositionKeys_def, auto)

lemma correctCompositionSecrets_subcomp2:
assumes "correctCompositionSecrets C"
        and "xb ∈ subcomponents C"
        and "xc ∈ specSecrets xb"
shows     "xc ∈ specSecrets C"
using assms by (simp add: correctCompositionSecrets_def, auto)

lemma correctCompKS_Keys:
assumes "correctCompositionKS C"
shows    "correctCompositionKeys C"
proof (cases "subcomponents C = {}")
  assume "subcomponents C = {}"
  from this and assms show ?thesis
  by (simp add: correctCompositionKeys_def)
next
  assume "subcomponents C ≠ {}"
  from this and assms show ?thesis 
  by (simp add: correctCompositionKS_def 
                correctCompositionKeys_def
                specKeysSecrets_def, blast)
qed

lemma correctCompKS_Secrets:
assumes "correctCompositionKS C"
shows    "correctCompositionSecrets C"
proof (cases "subcomponents C = {}")
  assume "subcomponents C = {}"
  from this and assms show ?thesis
  by (simp add: correctCompositionSecrets_def)
next
  assume "subcomponents C ≠ {}"
  from this and assms show ?thesis 
  by (simp add: correctCompositionKS_def 
                correctCompositionSecrets_def
                specKeysSecrets_def, blast)
qed

lemma correctCompKS_KeysSecrets:
assumes "correctCompositionKeys C"
        and "correctCompositionSecrets C"
shows    "correctCompositionKS C"
proof (cases "subcomponents C = {}")
  assume "subcomponents C = {}"
  from this and assms show ?thesis
  by (simp add: correctCompositionKS_def)
next
  assume "subcomponents C ≠ {}"
  from this and assms show ?thesis 
  by (simp add: correctCompositionKS_def 
                correctCompositionKeys_def 
                correctCompositionSecrets_def
                specKeysSecrets_def, blast)
qed 

lemma correctCompositionKS_subcomp1:
assumes "correctCompositionKS C"
       and h1:"x ∈ subcomponents C"
       and "xa ∈ specKeys C"
shows    "∃ y ∈ subcomponents C. (xa ∈ specKeys y)"
proof (cases "subcomponents C = {}")
  assume "subcomponents C = {}"
  from this and h1 show ?thesis by simp 
next
  assume "subcomponents C ≠ {}"
  from this and assms show ?thesis 
  by (simp add: correctCompositionKS_def specKeysSecrets_def, blast) 
qed

lemma correctCompositionKS_subcomp2:
assumes "correctCompositionKS C"
        and h1:"x ∈ subcomponents C"
        and "xa ∈ specSecrets C"
shows    "∃ y ∈ subcomponents C. xa ∈ specSecrets y"
proof (cases "subcomponents C = {}")
  assume "subcomponents C = {}"
  from this and h1 show ?thesis by simp 
next
  assume "subcomponents C ≠ {}"
  from this and assms show ?thesis 
  by (simp add: correctCompositionKS_def specKeysSecrets_def, blast)
qed

lemma correctCompositionKS_subcomp3:
assumes "correctCompositionKS C"
       and "x ∈ subcomponents C"
       and "xa ∈ specKeys x"
shows    "xa ∈ specKeys C"
using assms 
by (simp add: correctCompositionKS_def specKeysSecrets_def, auto)

lemma correctCompositionKS_subcomp4:
assumes "correctCompositionKS C"
        and "x ∈ subcomponents C"
        and "xa ∈ specSecrets x" 
shows     "xa ∈ specSecrets C"
using assms 
by (simp add: correctCompositionKS_def specKeysSecrets_def, auto)

lemma correctCompositionKS_PQ:
assumes "subcomponents PQ = {P, Q}"
       and "correctCompositionKS PQ" 
       and "ks ∈ specKeysSecrets PQ"
shows    "ks ∈ specKeysSecrets P ∨ ks ∈ specKeysSecrets Q"
using assms by (simp add: correctCompositionKS_def)

lemma correctCompositionKS_neg1:
assumes "subcomponents PQ = {P, Q}"
       and "correctCompositionKS PQ" 
       and "ks ∉ specKeysSecrets P"
       and "ks ∉ specKeysSecrets Q"
shows    "ks ∉ specKeysSecrets PQ"
using assms by (simp add: correctCompositionKS_def)

lemma correctCompositionKS_negP:
assumes "subcomponents PQ = {P, Q}"
        and "correctCompositionKS PQ" 
        and "ks ∉ specKeysSecrets PQ" 
shows     "ks ∉ specKeysSecrets P"
using assms by (simp add: correctCompositionKS_def)

lemma correctCompositionKS_negQ:
assumes "subcomponents PQ = {P, Q}"
        and "correctCompositionKS PQ" 
        and "ks ∉ specKeysSecrets PQ" 
shows     "ks ∉ specKeysSecrets Q"
using assms by (simp add: correctCompositionKS_def)

lemma out_exprChannelSingle_Set:
assumes "out_exprChannelSingle P ch E"
shows    "out_exprChannelSet P {ch} E"
using assms 
by (simp add: out_exprChannelSingle_def out_exprChannelSet_def)

lemma out_exprChannelSet_Single:
assumes "out_exprChannelSet P {ch} E"
shows    "out_exprChannelSingle P ch E"
using assms
by (simp add: out_exprChannelSingle_def out_exprChannelSet_def)

lemma ine_exprChannelSingle_Set:
assumes "ine_exprChannelSingle P ch E"
  shows "ine_exprChannelSet P {ch} E"
using assms 
by (simp add: ine_exprChannelSingle_def ine_exprChannelSet_def)

lemma ine_exprChannelSet_Single:
assumes "ine_exprChannelSet P {ch} E"
shows    "ine_exprChannelSingle P ch E"
using assms 
by (simp add: ine_exprChannelSingle_def ine_exprChannelSet_def)

lemma ine_ins_neg1:
assumes "¬ ine P m" 
       and "exprChannel x m"
shows    "x ∉ ins P"
using assms by (simp add: ine_def, auto)

theorem TBtheorem1a:
assumes "ine PQ E" 
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
shows "ine P E  ∨ ine Q E"
using assms 
by (simp add: ine_def correctCompositionIn_def, auto)

theorem TBtheorem1b:
assumes "ineM PQ M E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ" 
shows    "ineM P M E ∨ ineM Q M E"
using assms by (simp add: ineM_def correctCompositionIn_def, auto)

theorem TBtheorem2a:
assumes "eout PQ E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
shows    "eout P E ∨ eout Q E"
using assms by (simp add: eout_def correctCompositionOut_def, auto)

theorem TBtheorem2b:
assumes "eoutM PQ M E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
shows    "eoutM P M E ∨ eoutM Q M E"
using assms by (simp add: eoutM_def correctCompositionOut_def, auto)

lemma correctCompositionIn_prop1:
assumes "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
       and "x ∈ (ins PQ)"
shows   "(x ∈ (ins P)) ∨ (x ∈ (ins Q))" 
using assms by (simp add: correctCompositionIn_def)

lemma correctCompositionOut_prop1:
assumes "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "x ∈ (out PQ)"
shows    "(x ∈ (out P)) ∨ (x ∈ (out Q))" 
using assms by (simp add: correctCompositionOut_def)

theorem TBtheorem3a:
assumes "¬ (ine P E)"
       and "¬ (ine Q E)"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
shows    "¬ (ine PQ E)"
using assms by (simp add: ine_def correctCompositionIn_def, auto )

theorem TBlemma3b:
assumes h1:"¬ (ineM P M E)"
       and h2:"¬ (ineM Q M E)"
       and subPQ:"subcomponents PQ = {P,Q}"
       and cCompI:"correctCompositionIn PQ"
       and chM:"ch ∈ M" 
       and chPQ:"ch ∈ ins PQ"
       and eCh:"exprChannel ch E"
shows "False"
proof (cases "ch ∈ ins P")
  assume a1:"ch ∈ ins P"
  from a1 and chM and eCh have "ineM P M E" by (simp add: ineM_L1)
  from this and h1 show ?thesis by simp
next
  assume a2:"ch ∉ ins P" 
  from subPQ and cCompI and chPQ have "(ch ∈ ins P) ∨ (ch ∈ ins Q)"
    by (simp add: correctCompositionIn_L2)
  from this and a2 have "ch ∈ ins Q" by simp 
  from this and chM and eCh have "ineM Q M E" by (simp add: ineM_L1)
  from this and h2 show ?thesis by simp
qed

theorem TBtheorem3b:
assumes "¬ (ineM P M E)"
       and "¬ (ineM Q M E)"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
shows    "¬ (ineM PQ M E)"
using assms by (metis TBtheorem1b)    

theorem TBtheorem4a_empty:
assumes "(ine P E) ∨ (ine Q E)"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
       and "loc PQ = {}"
shows    "ine PQ E"
using assms by (simp add: ine_def correctCompositionIn_def, auto)

theorem TBtheorem4a_P:
assumes "ine P E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
       and "∃ ch. (ch ∈ (ins P) ∧ exprChannel ch E ∧ ch ∉ (loc PQ))"
shows    "ine PQ E"
using assms by (simp add: ine_def correctCompositionIn_def, auto) 

theorem TBtheorem4b_P:
assumes "ineM P M E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
       and "∃ ch. ((ch ∈ (ins Q)) ∧ (exprChannel ch E) ∧ 
                        (ch ∉ (loc PQ)) ∧ (ch ∈ M))"
shows    "ineM PQ M E"
using assms by (simp add: ineM_def correctCompositionIn_def, auto) 

theorem TBtheorem4a_PQ:
assumes "(ine P E) ∨ (ine Q E)"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
       and "∃ ch. (((ch ∈ (ins P)) ∨ (ch ∈ (ins Q) )) ∧ 
                         (exprChannel ch E) ∧  (ch ∉ (loc PQ)))"
shows    "ine PQ E"
using assms by (simp add: ine_def correctCompositionIn_def, auto) 

theorem TBtheorem4b_PQ:
assumes "(ineM P M E) ∨ (ineM Q M E)" 
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
       and "∃ ch. (((ch ∈ (ins P)) ∨ (ch ∈ (ins Q) )) ∧ 
                         (ch ∈ M) ∧ (exprChannel ch E) ∧  (ch ∉ (loc PQ)))"
shows     "ineM PQ M E"
using assms by (simp add: ineM_def correctCompositionIn_def, auto) 

theorem TBtheorem4a_notP1:
assumes "ine P E"
       and "¬ ine Q E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ" 
       and "∃ ch. ((ine_exprChannelSingle P ch E) ∧ (ch ∈ (loc PQ)))"
shows    "¬ ine PQ E"
using assms 
by (simp add: ine_def correctCompositionIn_def 
                     ine_exprChannelSingle_def, auto) 

theorem TBtheorem4b_notP1:
assumes "ineM P M E"
       and "¬ ineM Q M E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"  
       and "∃ ch. ((ine_exprChannelSingle P ch E) ∧ (ch ∈ M) 
                     ∧ (ch ∈ (loc PQ)))"
shows    "¬ ineM PQ M E"
using assms
by (simp add: ineM_def correctCompositionIn_def 
                     ine_exprChannelSingle_def, auto) 

theorem TBtheorem4a_notP2:
assumes "¬ ine Q E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ" 
       and "ine_exprChannelSet P ChSet E"
       and "∀ (x ::chanID). ((x ∈ ChSet) ⟶ (x ∈ (loc PQ)))" 
shows    "¬ ine PQ E"
using assms 
by (simp add: ine_def correctCompositionIn_def 
                     ine_exprChannelSet_def, auto) 

theorem TBtheorem4b_notP2:
assumes "¬ ineM Q M E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
       and "ine_exprChannelSet P ChSet E"
       and "∀ (x ::chanID). ((x ∈ ChSet) ⟶ (x ∈ (loc PQ)))"
shows    "¬ ineM PQ M E"
using assms 
by (simp add: ineM_def correctCompositionIn_def 
                     ine_exprChannelSet_def, auto) 

theorem TBtheorem4a_notPQ:
assumes "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ"
       and "ine_exprChannelSet P ChSetP E"
       and "ine_exprChannelSet Q ChSetQ E"
       and "∀ (x ::chanID). ((x ∈ ChSetP) ⟶ (x ∈ (loc PQ)))"
       and "∀ (x ::chanID). ((x ∈ ChSetQ) ⟶ (x ∈ (loc PQ)))"
shows    "¬ ine PQ E"
using assms 
by (simp add: ine_def correctCompositionIn_def 
                     ine_exprChannelSet_def, auto)

lemma ineM_Un1:
assumes "ineM P A E"
shows    "ineM P (A Un B) E"
using assms by (simp add: ineM_def, auto)

theorem TBtheorem4b_notPQ:
assumes "subcomponents PQ = {P,Q}"
       and "correctCompositionIn PQ" 
       and "ine_exprChannelSet P ChSetP E"
       and "ine_exprChannelSet Q ChSetQ E"
       and "∀ (x ::chanID). ((x ∈ ChSetP) ⟶ (x ∈ (loc PQ)))"
       and "∀ (x ::chanID). ((x ∈ ChSetQ) ⟶ (x ∈ (loc PQ)))"
shows    " ¬ ineM PQ M E"
using assms 
by (simp add: ineM_def correctCompositionIn_def 
                     ine_exprChannelSet_def, auto) 

lemma ine_nonempty_exprChannelSet:
assumes "ine_exprChannelSet P ChSet E"
       and "ChSet ≠ {}"
shows    "ine P E "
using assms by (simp add: ine_def ine_exprChannelSet_def, auto)

lemma ine_empty_exprChannelSet:
assumes "ine_exprChannelSet P ChSet E"
       and "ChSet = {}"
shows    "¬ ine P E"
using assms by (simp add: ine_def ine_exprChannelSet_def)

theorem TBtheorem5a_empty:
assumes "(eout P E) ∨ (eout Q E)"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "loc PQ = {}"
shows    "eout PQ E"
using assms by (simp add: eout_def correctCompositionOut_def, auto)

theorem TBtheorem45a_P:
assumes "eout P E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "∃ ch. ((ch ∈ (out P)) ∧ (exprChannel ch E) ∧ 
                        (ch ∉ (loc PQ)))"
shows    "eout PQ E"
using assms by (simp add: eout_def correctCompositionOut_def, auto)

theorem TBtheore54b_P:
assumes "eoutM P M E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ" 
       and "∃ ch. ((ch ∈ (out Q)) ∧ (exprChannel ch E) ∧ 
                        (ch ∉ (loc PQ)) ∧ (ch ∈ M) )"
shows    "eoutM PQ M E"
using assms by (simp add: eoutM_def correctCompositionOut_def, auto)

theorem TBtheorem5a_PQ:
assumes "(eout P E) ∨ (eout Q E)"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "∃ ch. (((ch ∈ (out P)) ∨ (ch ∈ (out Q) )) ∧ 
                        (exprChannel ch E) ∧  (ch ∉ (loc PQ)))"
shows    "eout PQ E"
using assms by (simp add: eout_def correctCompositionOut_def, auto)

theorem TBtheorem5b_PQ:
assumes "(eoutM P M E) ∨ (eoutM Q M E)" 
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "∃ ch. (((ch ∈ (out P)) ∨ (ch ∈ (out Q) )) ∧ (ch ∈ M) 
                      ∧ (exprChannel ch E) ∧  (ch ∉ (loc PQ)))"
shows    "eoutM PQ M E"
using assms by (simp add: eoutM_def correctCompositionOut_def, auto) 

theorem TBtheorem5a_notP1:
assumes "eout P E"
       and "¬ eout Q E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "∃ ch. ((out_exprChannelSingle P ch E) ∧ (ch ∈ (loc PQ)))"
shows    "¬ eout PQ E"
using assms 
by (simp add: eout_def correctCompositionOut_def 
                      out_exprChannelSingle_def, auto) 

theorem TBtheorem5b_notP1:
assumes "eoutM P M E"
       and "¬ eoutM Q M E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "∃ ch. ((out_exprChannelSingle P ch E) ∧ (ch ∈ M) 
                   ∧ (ch ∈ (loc PQ)))"
shows    "¬ eoutM PQ M E"
using assms 
by (simp add: eoutM_def correctCompositionOut_def 
                     out_exprChannelSingle_def, auto) 

theorem TBtheorem5a_notP2:
assumes "¬ eout Q E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ" 
       and "out_exprChannelSet P ChSet E"
       and "∀ (x ::chanID). ((x ∈ ChSet) ⟶ (x ∈ (loc PQ)))"
shows    "¬ eout PQ E"
using assms
by (simp add: eout_def correctCompositionOut_def 
                     out_exprChannelSet_def, auto)

theorem TBtheorem5b_notP2:
assumes "¬ eoutM Q M E"
       and "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "out_exprChannelSet P ChSet E"
       and "∀ (x ::chanID). ((x ∈ ChSet) ⟶ (x ∈ (loc PQ)))" 
shows    "¬ eoutM PQ M E"
using assms
by (simp add: eoutM_def correctCompositionOut_def 
                     out_exprChannelSet_def, auto)

theorem TBtheorem5a_notPQ:
assumes "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "out_exprChannelSet P ChSetP E"
       and "out_exprChannelSet Q ChSetQ E"
       and "∀ (x ::chanID). ((x ∈ ChSetP) ⟶ (x ∈ (loc PQ)))"
       and "∀ (x ::chanID). ((x ∈ ChSetQ) ⟶ (x ∈ (loc PQ)))"
shows    "¬ eout PQ E"
using assms
by (simp add: eout_def correctCompositionOut_def 
                     out_exprChannelSet_def, auto) 

theorem TBtheorem5b_notPQ:
assumes "subcomponents PQ = {P,Q}"
       and "correctCompositionOut PQ"
       and "out_exprChannelSet P ChSetP E"
       and "out_exprChannelSet Q ChSetQ E"
       and "M = ChSetP ∪ ChSetQ"
       and "∀ (x ::chanID). ((x ∈ ChSetP) ⟶ (x ∈ (loc PQ)))"
       and "∀ (x ::chanID). ((x ∈ ChSetQ) ⟶ (x ∈ (loc PQ)))"
shows    "¬ eoutM PQ M E"
using assms 
by (simp add: eoutM_def correctCompositionOut_def 
                     out_exprChannelSet_def, auto) 

end