Theory Compositionality

section ‹Compasitionality of the during-execution security notions› 

theory Compositionality imports During_Execution begin


(*******************************************)
context PL_Indis 
begin 

(* The end-product compositionality results are listed as theorems 
(as opposed to lemmas). *)

subsection ‹Discreetness versus language constructs:›

theorem discr_Atm[simp]:
"discr (Atm atm) = presAtm atm"  
proof-    
  {fix c
   have 
   "(∃ atm. c = Atm atm ∧ presAtm atm) 
    ⟹ discr c"
   apply(erule discr_coind) 
   apply (metis Atm_transC_invert)
   by (metis PL.Atm_transT_invert presAtm_def)
  }
  moreover have "discr (Atm atm) ⟹ presAtm atm"
    by (metis Atm presAtm_def discr_transT)
  ultimately show ?thesis by blast
qed

theorem discr_If[simp]:
assumes "discr c1" and "discr c2"
shows "discr (If tst c1 c2)"
proof-    
  {fix c
   have 
   "(∃ tst c1 c2. c = If tst c1 c2 ∧ discr c1 ∧ discr c2) ⟹ discr c"
   apply(erule discr_coind) 
   apply (metis PL.If_transC_invert indis_refl)
   by (metis If_transT_invert)
  }
  thus ?thesis using assms by blast
qed

theorem discr_Seq[simp]:
assumes *: "discr c1" and **: "discr c2"
shows "discr (c1 ;; c2)"
proof-
  {fix c
   have 
   "(∃ c1 c2. c = c1 ;; c2 ∧ discr c1 ∧ discr c2) 
    ⟹ discr c"
   apply(erule discr_coind) 
   proof(tactic‹clarify_all_tac @{context}›)
     fix c s c' s' c1 c2
     assume c1: "discr c1" and c2: "discr c2" 
     assume "(c1 ;; c2, s) →c (c', s')"
     thus "s ≈ s' ∧ ((∃c1 c2. c' = c1 ;; c2 ∧ discr c1 ∧ discr c2) ∨ discr c')"
     apply - apply(erule Seq_transC_invert)
     apply (metis c1 c2 discr_transC discr_transC_indis)
     by (metis c1 c2 discr.cases)
   qed (insert Seq_transT_invert, blast)
  }
  thus ?thesis using assms by blast
qed

theorem discr_While[simp]:
assumes "discr c"
shows "discr (While tst c)"
proof-
  {fix c
   have 
   "(∃ tst d. c = While tst d ∧ discr d) ∨ 
    (∃ tst d1 d. c = d1 ;; (While tst d) ∧ discr d1 ∧ discr d)
    ⟹ discr c"
   apply(erule discr_coind)
   apply(tactic ‹mauto_no_simp_tac @{context}›)
   apply (metis While_transC_invert indis_refl)
   apply (metis Seq_transC_invert discr.cases)
   apply (metis While_transC_invert)
   apply (metis Seq_transC_invert discr.cases)
   apply (metis PL.While_transT_invert indis_refl)
   by (metis Seq_transT_invert)
  }
  thus ?thesis using assms by blast
qed

theorem discr_Par[simp]:
assumes *: "discr c1" and **: "discr c2"
shows "discr (Par c1 c2)"
proof-
  {fix c
   have 
   "(∃ c1 c2. c = Par c1 c2 ∧ discr c1 ∧ discr c2) 
    ⟹ discr c"
   apply(erule discr_coind) 
   proof(tactic‹clarify_all_tac @{context}›)
     fix c s c' s' c1 c2
     assume c1: "discr c1" and c2: "discr c2" 
     assume "(Par c1 c2, s) →c (c', s')"
     thus "s ≈ s' ∧ ((∃c1 c2. c' = Par c1 c2 ∧ discr c1 ∧ discr c2) ∨ discr c')"
     apply - apply(erule Par_transC_invert)
     by(metis c1 c2 discr.cases)+
   qed
  }
  thus ?thesis using assms by blast
qed


subsection ‹Discreetness versus language constructs:›

theorem discr0_Atm[simp]:
"discr0 (Atm atm) = presAtm atm"  
proof-    
  {fix c
   have 
   "(∃ atm. c = Atm atm ∧ presAtm atm) 
    ⟹ discr0 c"
   apply(erule discr0_coind) 
   apply (metis Atm_transC_invert)
   by (metis discr_Atm discr_transT)
  }
  moreover have "discr0 (Atm atm) ⟹ presAtm atm"
  by (metis Atm discr0_MtransT presAtm_def mustT_Atm transT_MtransT)
  ultimately show ?thesis by blast
qed

theorem discr0_If[simp]:
assumes "discr0 c1" and "discr0 c2"
shows "discr0 (If tst c1 c2)"
proof-    
  {fix c
   have 
   "(∃ tst c1 c2. c = If tst c1 c2 ∧ discr0 c1 ∧ discr0 c2) ⟹ discr0 c"
   apply(erule discr0_coind) 
   apply (metis If_transC_invert indis_refl)
   by (metis If_transT_invert)
  }
  thus ?thesis using assms by blast
qed

theorem discr0_Seq[simp]:
assumes *: "discr0 c1" and **: "discr0 c2"
shows "discr0 (c1 ;; c2)"
proof-
  {fix c
   have 
   "(∃ c1 c2. c = c1 ;; c2 ∧ discr0 c1 ∧ discr0 c2) 
    ⟹ discr0 c"
   apply(erule discr0_coind) 
   proof(tactic‹clarify_all_tac @{context}›)
     fix c s c' s' c1 c2
     assume mt: "mustT (c1 ;; c2) s" 
     and c1: "discr0 c1" and c2: "discr0 c2" 
     assume "(c1 ;; c2, s) →c (c', s')"
     thus "s ≈ s' ∧ ((∃c1 c2. c' = c1 ;; c2 ∧ discr0 c1 ∧ discr0 c2) ∨ discr0 c')"
     apply - apply(erule Seq_transC_invert)
     apply (metis mustT_Seq_L c1 c2 discr0_MtransC discr0_MtransC_indis mt 
                  transC_MtransC)
     by (metis c1 c2 discr0_transT mt mustT_Seq_L)
   qed (insert Seq_transT_invert, blast)
  }
  thus ?thesis using assms by blast
qed

theorem discr0_While[simp]:
assumes "discr0 c"
shows "discr0 (While tst c)"
proof-
  {fix c
   have 
   "(∃ tst d. c = While tst d ∧ discr0 d) ∨ 
    (∃ tst d1 d. c = d1 ;; (While tst d) ∧ discr0 d1 ∧ discr0 d)
    ⟹ discr0 c"
   proof (induct rule: discr0_coind)
     case (Term c s s')
     thus "s ≈ s'" 
     apply (elim exE disjE conjE)
     apply (metis While_transT_invert indis_refl)
     by (metis Seq_transT_invert)
   next
     case (Cont c s c' s')
     thus ?case
     apply(intro conjI)
     apply (elim exE disjE conjE)
     apply (metis While_transC_invert indis_refl)
     apply (metis Seq_transC_invert discr0_MtransC_indis discr0_transT 
                  mustT_Seq_L transC_MtransC)
     (*  *)
     apply (elim exE disjE conjE)
     apply (metis While_transC_invert)
     by (metis Cont(3) Seq_transC_invert discr0_transC mustT_Seq_L)
   qed   
  }
  thus ?thesis using assms by blast
qed

theorem discr0_Par[simp]:
assumes *: "discr0 c1" and **: "discr0 c2"
shows "discr0 (Par c1 c2)"
proof-
  {fix c
   have 
   "(∃ c1 c2. c = Par c1 c2 ∧ discr0 c1 ∧ discr0 c2) 
    ⟹ discr0 c"
   apply(induct rule: discr0_coind) 
   proof(tactic‹clarify_all_tac @{context}›)
     fix c s c' s' c1 c2
     assume mt: "mustT (Par c1 c2) s" and c1: "discr0 c1" and c2: "discr0 c2" 
     assume "(Par c1 c2, s) →c (c', s')"
     thus "s ≈ s' ∧ ((∃c1 c2. c' = Par c1 c2 ∧ discr0 c1 ∧ discr0 c2) ∨ discr0 c')"
     apply(elim Par_transC_invert)
     apply (metis c1 c2 discr0.simps mt mustT_Par_L)
     apply (metis c1 c2 discr0_transT mt mustT_Par_L)
     apply (metis c1 c2 discr0.simps indis_sym mt mustT_Par_R)
     by (metis PL.mustT_Par_R c1 c2 discr0_transT mt)
   qed
  }
  thus ?thesis using assms by blast
qed


subsection ‹Self-Isomorphism versus language constructs:›

theorem siso_Atm[simp]:
"siso (Atm atm) = compatAtm atm"  
proof-    
  {fix c
   have 
   "(∃ atm. c = Atm atm ∧ compatAtm atm) 
    ⟹ siso c"
   apply(erule siso_coind) 
   apply (metis Atm_transC_invert)
   apply (metis PL.Atm_transC_invert)
   by (metis Atm_transT_invert PL.Atm compatAtm_def)
  }
  moreover have "siso (Atm atm) ⟹ compatAtm atm" unfolding compatAtm_def
  by (metis Atm Atm_transT_invert siso_transT)
  ultimately show ?thesis by blast
qed 

theorem siso_If[simp]:
assumes  "compatTst tst" and "siso c1" and "siso c2"
shows "siso (If tst c1 c2)"
proof-    
  {fix c
   have 
   "(∃ tst c1 c2. c = If tst c1 c2 ∧ compatTst tst ∧ siso c1 ∧ siso c2) ⟹ siso c"
   apply(erule siso_coind) 
   apply (metis PL.If_transC_invert indis_refl)
   apply (metis IfTrue PL.IfFalse PL.If_transC_invert compatTst_def)
   by (metis If_transT_invert)
  }
  thus ?thesis using assms by blast
qed

theorem siso_Seq[simp]:
assumes *: "siso c1" and **: "siso c2"
shows "siso (c1 ;; c2)"
proof-
  {fix c
   have 
   "(∃ c1 c2. c = c1 ;; c2 ∧ siso c1 ∧ siso c2) 
    ⟹ siso c"
   apply(erule siso_coind) 
   proof(tactic‹clarify_all_tac @{context}›)
     fix c s t c' s' c1 c2
     assume "s ≈ t" and "(c1 ;; c2, s) →c (c', s')" and "siso c1" and "siso c2"
     thus "∃t'. s' ≈ t' ∧ (c1 ;; c2, t) →c (c', t')"
     apply - apply(erule Seq_transC_invert)
     apply (metis SeqC siso_transC_indis)
     by (metis PL.SeqT siso_transT)
   qed (insert Seq_transT_invert siso_transC, blast+)
  }
  thus ?thesis using assms by blast
qed

theorem siso_While[simp]:
assumes "compatTst tst" and "siso c"
shows "siso (While tst c)"
proof-
  {fix c
   have 
   "(∃ tst d. compatTst tst ∧ c = While tst d ∧ siso d) ∨ 
    (∃ tst d1 d. compatTst tst ∧ c = d1 ;; (While tst d) ∧ siso d1 ∧ siso d)
    ⟹ siso c"
   apply(erule siso_coind)
   apply auto
   apply (metis PL.Seq_transC_invert siso_transC)
   apply (metis WhileTrue While_transC_invert compatTst_def)
   apply (metis PL.SeqC siso_transC_indis)
   apply (metis PL.SeqT siso_transT)
   by (metis WhileFalse compatTst_def) 
  }
  thus ?thesis using assms by blast
qed

theorem siso_Par[simp]:
assumes *: "siso c1" and **: "siso c2"
shows "siso (Par c1 c2)"
proof-
  {fix c
   have 
   "(∃ c1 c2. c = Par c1 c2 ∧ siso c1 ∧ siso c2) 
    ⟹ siso c"
   apply(erule siso_coind)
   proof(tactic‹clarify_all_tac @{context}›)
     fix c s t c' s' c1 c2
     assume "s ≈ t" and "(Par c1 c2, s) →c (c', s')" and c1: "siso c1" and c2: "siso c2"
     thus "∃t'. s' ≈ t' ∧ (Par c1 c2, t) →c (c', t')"
     apply - apply(erule Par_transC_invert)
     by(metis ParCL ParTL ParCR ParTR c1 c2 siso_transT siso_transC_indis)+   
   qed (insert Par_transC_invert siso_transC Par_transT_invert, blast+)
  }
  thus ?thesis using assms by blast
qed


subsection ‹Self-Isomorphism versus language constructs:›

theorem siso0_Atm[simp]:
"siso0 (Atm atm) = compatAtm atm"  
proof-    
  {fix c
   have 
   "(∃ atm. c = Atm atm ∧ compatAtm atm) 
    ⟹ siso0 c"
   apply(erule siso0_coind) 
   apply (metis Atm_transC_invert)
   apply (metis PL.Atm_transC_invert)
   by (metis Atm_transT_invert PL.Atm compatAtm_def)
  }
  moreover have "siso0 (Atm atm) ⟹ compatAtm atm" unfolding compatAtm_def
  by (metis Atm Atm_transT_invert siso0_transT mustT_Atm)
  ultimately show ?thesis by blast
qed 

theorem siso0_If[simp]:
assumes  "compatTst tst" and "siso0 c1" and "siso0 c2"
shows "siso0 (If tst c1 c2)"
proof-    
  {fix c
   have 
   "(∃ tst c1 c2. c = If tst c1 c2 ∧ compatTst tst ∧ siso0 c1 ∧ siso0 c2) ⟹ siso0 c"
   apply(erule siso0_coind) 
   apply (metis PL.If_transC_invert indis_refl)
   apply (metis IfTrue PL.IfFalse PL.If_transC_invert compatTst_def)
   by (metis If_transT_invert)
  }
  thus ?thesis using assms by blast
qed

theorem siso0_Seq[simp]:
assumes *: "siso0 c1" and **: "siso0 c2"
shows "siso0 (c1 ;; c2)"
proof-
  {fix c
   have 
   "(∃ c1 c2. c = c1 ;; c2 ∧ siso0 c1 ∧ siso0 c2) 
    ⟹ siso0 c"
   proof (induct rule: siso0_coind)
     case (Indef c s c' s')
     thus ?case
     by (metis Seq_transC_invert mustT_Seq_L siso0_transC) 
   next
     case (Cont c s t c' s')
     then obtain c1 c2
     where c: "c = c1 ;; c2" and mt: "mustT (c1 ;; c2) s" "mustT (c1 ;; c2) t" 
     and st: "s ≈ t" and siso1: "siso0 c1" and siso2: "siso0 c2" by auto
     hence mt1: "mustT c1 s" "mustT c1 t"
     by (metis mustT_Seq_L)+
     have "(c1 ;; c2, s) →c (c', s')" using c Cont by auto
     thus ?case
     proof (elim Seq_transC_invert)
       fix c1' assume c1: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
       obtain t' where "(c1, t) →c (c1', t')" and "s' ≈ t'"
       using siso1 c1 st mt1 by (metis siso0_transC_indis) 
       thus ?thesis by (metis SeqC c c') 
     next
       assume "(c1, s) →t s'" and "c' = c2"
       thus ?thesis by (metis c SeqT mt1 siso0_transT siso1 st)
     qed
   qed auto
  }
  thus ?thesis using assms by blast
qed

theorem siso0_While[simp]:
assumes "compatTst tst" and "siso0 c"
shows "siso0 (While tst c)"
proof-
  {fix c
   have 
   "(∃ tst d. compatTst tst ∧ c = While tst d ∧ siso0 d) ∨ 
    (∃ tst d1 d. compatTst tst ∧ c = d1 ;; (While tst d) ∧ siso0 d1 ∧ siso0 d)
    ⟹ siso0 c"
   apply(erule siso0_coind)
   apply auto
   apply (metis mustT_Seq_L siso0_transC)
   apply (metis WhileTrue While_transC_invert compatTst_def)
   apply (metis SeqC mustT_Seq_L siso0_transC_indis)
   apply (metis SeqT mustT_Seq_L siso0_transT)
   by (metis WhileFalse compatTst_def)
  }
  thus ?thesis using assms by blast
qed

theorem siso0_Par[simp]:
assumes *: "siso0 c1" and **: "siso0 c2"
shows "siso0 (Par c1 c2)"
proof-
  {fix c
   have 
   "(∃ c1 c2. c = Par c1 c2 ∧ siso0 c1 ∧ siso0 c2) 
    ⟹ siso0 c"
   proof (induct rule: siso0_coind)
     case (Indef c s c' s')
     then obtain c1 c2 where c: "c = Par c1 c2" 
     and c1: "siso0 c1" and c2: "siso0 c2" by auto
     hence "(Par c1 c2, s) →c (c', s')" using c Indef by auto
     thus ?case
     apply(elim Par_transC_invert)
     by (metis Indef c c1 c2 mustT_Par_L mustT_Par_R siso0_transC)+ 
   next
     case (Cont c s t c' s')
     then obtain c1 c2 where c: "c = Par c1 c2" 
     and c1: "siso0 c1" and c2: "siso0 c2" by auto
     hence mt: "mustT c1 s" "mustT c1 t" "mustT c2 s" "mustT c2 t"
     by (metis Cont mustT_Par_L mustT_Par_R)+
     have "(Par c1 c2, s) →c (c', s')" using c Cont by auto
     thus ?case
     apply(elim Par_transC_invert)
     apply (metis Cont ParCL c c1 mt siso0_transC_indis)
     apply (metis Cont ParTL c c1 mt siso0_transT)
     apply (metis Cont ParCR c c2 mt siso0_transC_indis)
     by (metis Cont ParTR c c2 mt siso0_transT)
   qed auto 
  }
  thus ?thesis using assms by blast
qed


subsection‹Strong bisimilarity versus language constructs›

text ‹Atomic commands:›

definition thetaAtm where 
"thetaAtm atm ≡ {(Atm atm, Atm atm)}"

lemma thetaAtm_sym:
"sym (thetaAtm atm)"
unfolding thetaAtm_def sym_def by blast

lemma thetaAtm_Sretr:
assumes "compatAtm atm"
shows "thetaAtm atm ⊆ Sretr (thetaAtm atm)"
using assms 
unfolding compatAtm_def Sretr_def matchC_C_def matchT_T_def thetaAtm_def
apply simp by (metis Atm_transT_invert Atm) 

lemma thetaAtm_Sbis:
assumes "compatAtm atm"
shows "thetaAtm atm ⊆ Sbis"
apply(rule Sbis_raw_coind)
using assms thetaAtm_sym thetaAtm_Sretr by auto

theorem Atm_Sbis[simp]:
assumes "compatAtm atm" 
shows "Atm atm ≈s Atm atm"
using assms thetaAtm_Sbis unfolding thetaAtm_def by auto

text‹Sequential composition:› 

definition thetaSeq where 
"thetaSeq ≡ 
 {(c1 ;; c2, d1 ;; d2) | c1 c2 d1 d2. c1 ≈s d1 ∧ c2 ≈s d2}"

lemma thetaSeq_sym:
"sym thetaSeq"
unfolding thetaSeq_def sym_def using Sbis_Sym by blast

lemma thetaSeq_Sretr:
"thetaSeq ⊆ Sretr (thetaSeq Un Sbis)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈s d1" and c2d2: "c2 ≈s d2"
   hence matchC_C1: "matchC_C Sbis c1 d1" and matchC_C2: "matchC_C Sbis c2 d2"
     and matchT_T1: "matchT_T c1 d1" and matchT_T2: "matchT_T c2 d2"
   using Sbis_matchC_C Sbis_matchT_T by auto
   have "(c1 ;; c2, d1 ;; d2) ∈ Sretr (thetaSeq Un Sbis)"
   unfolding Sretr_def proof (clarify, intro conjI)
     show "matchC_C (thetaSeq Un Sbis) (c1 ;; c2) (d1 ;; d2)"
     unfolding matchC_C_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; c2, s) →c (c', s')"
       thus "∃d' t'. (d1 ;; d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaSeq Un Sbis"
       apply - proof(erule Seq_transC_invert) 
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
         hence "∃d1' t'. (d1, t) →c (d1', t') ∧ s' ≈ t' ∧ c1' ≈s d1'"
         using st matchC_C1 unfolding matchC_C_def by blast
         thus ?thesis unfolding c' thetaSeq_def
         apply simp by (metis SeqC c2d2 ) 
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →t t' ∧ s' ≈ t'"
         using st matchT_T1 unfolding matchT_T_def by auto
         thus ?thesis 
         unfolding c' thetaSeq_def
         apply simp by (metis PL.SeqT c2d2) 
       qed
     qed 
   qed (unfold matchT_T_def, auto)
  }
  thus ?thesis unfolding thetaSeq_def by auto
qed

lemma thetaSeq_Sbis:
"thetaSeq ⊆ Sbis"
apply(rule Sbis_coind)
using thetaSeq_sym thetaSeq_Sretr by auto

theorem Seq_Sbis[simp]:
assumes "c1 ≈s d1" and "c2 ≈s d2"
shows "c1 ;; c2 ≈s d1 ;; d2"
using assms thetaSeq_Sbis unfolding thetaSeq_def by blast 

text‹Conditional:›

definition thetaIf where 
"thetaIf ≡ 
 {(If tst c1 c2, If tst d1 d2) | tst c1 c2 d1 d2. compatTst tst ∧ c1 ≈s d1 ∧ c2 ≈s d2}"

lemma thetaIf_sym:
"sym thetaIf"
unfolding thetaIf_def sym_def using Sbis_Sym by blast

lemma thetaIf_Sretr:
"thetaIf ⊆ Sretr (thetaIf Un Sbis)"
proof-
  {fix tst c1 c2 d1 d2
   assume tst: "compatTst tst" and c1d1: "c1 ≈s d1" and c2d2: "c2 ≈s d2"
   hence matchC_C1: "matchC_C Sbis c1 d1" and matchC_C2: "matchC_C Sbis c2 d2"
     and matchT_T1: "matchT_T c1 d1" and matchT_T2: "matchT_T c2 d2"
   using Sbis_matchC_C Sbis_matchT_T by auto
   have "(If tst c1 c2, If tst d1 d2) ∈ Sretr (thetaIf Un Sbis)"
   unfolding Sretr_def proof (clarify, intro conjI)
     show "matchC_C (thetaIf Un Sbis) (If tst c1 c2) (If tst d1 d2)"
     unfolding matchC_C_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(If tst c1 c2, s) →c (c', s')"
       thus "∃d' t'. (If tst d1 d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaIf Un Sbis"
       apply - apply(erule If_transC_invert)
       unfolding thetaIf_def 
       apply simp apply (metis IfTrue c1d1 compatTst_def st tst)
       apply simp by (metis IfFalse c2d2 compatTst_def st tst)
     qed
   qed (unfold matchT_T_def, auto)
  }
  thus ?thesis unfolding thetaIf_def by auto
qed

lemma thetaIf_Sbis:
"thetaIf ⊆ Sbis"
apply(rule Sbis_coind)
using thetaIf_sym thetaIf_Sretr by auto

theorem If_Sbis[simp]:
assumes "compatTst tst" and "c1 ≈s d1" and "c2 ≈s d2"
shows "If tst c1 c2 ≈s If tst d1 d2"
using assms thetaIf_Sbis unfolding thetaIf_def by blast

text‹While loop:›

definition thetaWhile where 
"thetaWhile ≡ 
 {(While tst c, While tst d) | tst c d. compatTst tst ∧ c ≈s d} Un 
 {(c1 ;; (While tst c), d1 ;; (While tst d)) | tst c1 d1 c d. compatTst tst ∧ c1 ≈s d1 ∧ c ≈s d}"

lemma thetaWhile_sym:
"sym thetaWhile"
unfolding thetaWhile_def sym_def using Sbis_Sym by blast

lemma thetaWhile_Sretr:
"thetaWhile ⊆ Sretr (thetaWhile Un Sbis)"
proof-
  {fix tst c d 
   assume tst: "compatTst tst" and c_d: "c ≈s d"
   hence matchC_C: "matchC_C Sbis c d" 
     and matchT_T: "matchT_T c d" 
   using Sbis_matchC_C Sbis_matchT_T by auto
   have "(While tst c, While tst d) ∈ Sretr (thetaWhile Un Sbis)"
   unfolding Sretr_def proof (clarify, intro conjI)
     show "matchC_C (thetaWhile ∪ Sbis) (While tst c) (While tst d)"
     unfolding matchC_C_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(While tst c, s) →c (c', s')"
       thus "∃d' t'. (While tst d, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaWhile ∪ Sbis"
       apply - apply(erule While_transC_invert)
       unfolding thetaWhile_def apply simp
       by (metis WhileTrue c_d compatTst_def st tst)
     qed
   next
     show "matchT_T (While tst c) (While tst d)"
     unfolding matchT_T_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t s' assume st: "s ≈ t" assume "(While tst c, s) →t s'"
       thus "∃t'. (While tst d, t) →t t' ∧ s' ≈ t' "
       apply - apply(erule While_transT_invert)
       unfolding thetaWhile_def apply simp
       by (metis PL.WhileFalse compatTst_def st tst)    
     qed
   qed
  }
  moreover 
  {fix tst c1 d1  c d
   assume tst: "compatTst tst" and c1d1: "c1 ≈s d1" and c_d: "c ≈s d"
   hence matchC_C1: "matchC_C Sbis c1 d1" and matchC_C: "matchC_C Sbis c d" 
     and matchT_T1: "matchT_T c1 d1" and matchT_T: "matchT_T c d"
   using Sbis_matchC_C Sbis_matchT_T by auto
   have "(c1 ;; (While tst c), d1 ;; (While tst d)) ∈ Sretr (thetaWhile Un Sbis)"
   unfolding Sretr_def proof (clarify, intro conjI)
     show "matchC_C (thetaWhile ∪ Sbis) (c1 ;; (While tst c)) (d1 ;; (While tst d))"
     unfolding matchC_C_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; (While tst c), s) →c (c', s')"
       thus "∃d' t'. (d1 ;; (While tst d), t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaWhile ∪ Sbis"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume "(c1, s) →c (c1', s')" and c': "c' = c1' ;; (While tst c)"
         hence "∃d' t'. (d1, t) →c (d', t') ∧ s' ≈ t' ∧ c1' ≈s d'" 
         using st matchC_C1 unfolding matchC_C_def by blast
         thus ?thesis
         unfolding c' thetaWhile_def
         apply simp by (metis SeqC c_d tst) 
       next
         assume "(c1, s) →t s'" and c': "c' = While tst c"
         hence "∃t'. (d1, t) →t t' ∧ s' ≈ t'"
         using st matchT_T1 unfolding matchT_T_def by auto
         thus ?thesis
         unfolding c' thetaWhile_def 
         apply simp by (metis PL.SeqT c_d tst) 
       qed
     qed
   qed (unfold matchT_T_def, auto)
  }
  ultimately show ?thesis unfolding thetaWhile_def by auto
qed

lemma thetaWhile_Sbis:
"thetaWhile ⊆ Sbis"
apply(rule Sbis_coind)
using thetaWhile_sym thetaWhile_Sretr by auto

theorem While_Sbis[simp]:
assumes "compatTst tst" and "c ≈s d"
shows "While tst c ≈s While tst d"
using assms thetaWhile_Sbis unfolding thetaWhile_def by auto

text‹Parallel composition:›

definition thetaPar where 
"thetaPar ≡ 
 {(Par c1 c2, Par d1 d2) | c1 c2 d1 d2. c1 ≈s d1 ∧ c2 ≈s d2}"

lemma thetaPar_sym:
"sym thetaPar"
unfolding thetaPar_def sym_def using Sbis_Sym by blast

lemma thetaPar_Sretr:
"thetaPar ⊆ Sretr (thetaPar Un Sbis)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈s d1" and c2d2: "c2 ≈s d2"
   hence matchC_C1: "matchC_C Sbis c1 d1" and matchC_C2: "matchC_C Sbis c2 d2"
     and matchT_T1: "matchT_T c1 d1" and matchT_T2: "matchT_T c2 d2"
   using Sbis_matchC_C Sbis_matchT_T by auto
   have "(Par c1 c2, Par d1 d2) ∈ Sretr (thetaPar Un Sbis)"
   unfolding Sretr_def proof (clarify, intro conjI)
     show "matchC_C (thetaPar ∪ Sbis) (Par c1 c2) (Par d1 d2)"
     unfolding matchC_C_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus "∃d' t'. (Par d1 d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaPar ∪ Sbis"
       apply - proof(erule Par_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence "∃d' t'. (d1, t) →c (d', t') ∧ s' ≈ t' ∧ c1' ≈s d'"
         using st matchC_C1 unfolding matchC_C_def by blast
         thus ?thesis unfolding c' thetaPar_def
         apply simp by(metis ParCL c2d2)
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →t t' ∧ s' ≈ t'"
         using st matchT_T1 unfolding matchT_T_def by auto
         thus ?thesis 
         unfolding c' thetaPar_def
         apply simp by (metis PL.ParTL c2d2) 
       next
         fix c2' assume "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence "∃d' t'. (d2, t) →c (d', t') ∧ s' ≈ t' ∧ c2' ≈s d'"
         using st matchC_C2 unfolding matchC_C_def by blast
         thus ?thesis 
         unfolding c' thetaPar_def
         apply simp by (metis ParCR c1d1)
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence "∃t'. (d2, t) →t t' ∧ s' ≈ t'"
         using st matchT_T2 unfolding matchT_T_def by auto
         thus ?thesis 
         unfolding c' thetaPar_def
         apply simp by (metis PL.ParTR c1d1) 
       qed
     qed 
   qed (unfold matchT_T_def, auto)
  }
  thus ?thesis unfolding thetaPar_def by auto
qed

lemma thetaPar_Sbis:
"thetaPar ⊆ Sbis"
apply(rule Sbis_coind)
using thetaPar_sym thetaPar_Sretr by auto

theorem Par_Sbis[simp]:
assumes "c1 ≈s d1" and "c2 ≈s d2"
shows "Par c1 c2 ≈s Par d1 d2"
using assms thetaPar_Sbis unfolding thetaPar_def by blast


subsubsection‹01T-bisimilarity versus language constructs›

text ‹Atomic commands:›

theorem Atm_ZObisT:
assumes "compatAtm atm" 
shows "Atm atm ≈01T Atm atm"
by (metis Atm_Sbis assms bis_imp)

text‹Sequential composition:› 

definition thetaSeqZOT where 
"thetaSeqZOT ≡ 
 {(c1 ;; c2, d1 ;; d2) | c1 c2 d1 d2. c1 ≈01T d1 ∧ c2 ≈01T d2}"

lemma thetaSeqZOT_sym:
"sym thetaSeqZOT"
unfolding thetaSeqZOT_def sym_def using ZObisT_Sym by blast

lemma thetaSeqZOT_ZOretrT:
"thetaSeqZOT ⊆ ZOretrT (thetaSeqZOT Un ZObisT)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈01T d1" and c2d2: "c2 ≈01T d2"
   hence matchC_ZOC1: "matchC_ZOC ZObisT c1 d1" and matchC_ZOC2: "matchC_ZOC ZObisT c2 d2"
     and matchT_T1: "matchT_T c1 d1" and matchT_T2: "matchT_T c2 d2"
   using ZObisT_matchC_ZOC ZObisT_matchT_T by auto
   have "(c1 ;; c2, d1 ;; d2) ∈ ZOretrT (thetaSeqZOT Un ZObisT)"
   unfolding ZOretrT_def proof (clarify, intro conjI)
     show "matchC_ZOC (thetaSeqZOT Un ZObisT) (c1 ;; c2) (d1 ;; d2)"
     unfolding matchC_ZOC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; c2, s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', d1 ;; d2) ∈ thetaSeqZOT Un ZObisT) ∨
        (∃d' t'. (d1 ;; d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaSeqZOT Un ZObisT)"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
         hence
         "(s' ≈ t ∧ c1' ≈01T d1) ∨ 
          (∃d1' t'. (d1, t) →c (d1', t') ∧ s' ≈ t' ∧ c1' ≈01T d1')"
         using st matchC_ZOC1 unfolding matchC_ZOC_def by auto
         thus ?thesis unfolding c' thetaSeqZOT_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c2d2)
         apply simp by (metis SeqC c2d2 ) 
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →t t' ∧ s' ≈ t'"
         using st matchT_T1 unfolding matchT_T_def by auto
         thus ?thesis 
         unfolding c' thetaSeqZOT_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp by (metis PL.SeqT c2d2) 
       qed
     qed 
   qed (unfold matchT_T_def, auto)
  }
  thus ?thesis unfolding thetaSeqZOT_def by auto
qed

lemma thetaSeqZOT_ZObisT:
"thetaSeqZOT ⊆ ZObisT"
apply(rule ZObisT_coind)
using thetaSeqZOT_sym thetaSeqZOT_ZOretrT by auto

theorem Seq_ZObisT[simp]:
assumes "c1 ≈01T d1" and "c2 ≈01T d2"
shows "c1 ;; c2 ≈01T d1 ;; d2"
using assms thetaSeqZOT_ZObisT unfolding thetaSeqZOT_def by blast 

text‹Conditional:›

definition thetaIfZOT where 
"thetaIfZOT ≡ 
 {(If tst c1 c2, If tst d1 d2) | tst c1 c2 d1 d2. compatTst tst ∧ c1 ≈01T d1 ∧ c2 ≈01T d2}"

lemma thetaIfZOT_sym:
"sym thetaIfZOT"
unfolding thetaIfZOT_def sym_def using ZObisT_Sym by blast

lemma thetaIfZOT_ZOretrT:
"thetaIfZOT ⊆ ZOretrT (thetaIfZOT Un ZObisT)"
proof-
  {fix tst c1 c2 d1 d2
   assume tst: "compatTst tst" and c1d1: "c1 ≈01T d1" and c2d2: "c2 ≈01T d2"
   hence matchC_ZOC1: "matchC_ZOC ZObisT c1 d1" and matchC_ZOC2: "matchC_ZOC ZObisT c2 d2"
     and matchT_T1: "matchT_T c1 d1" and matchT_T2: "matchT_T c2 d2"
   using ZObisT_matchC_ZOC ZObisT_matchT_T by auto
   have "(If tst c1 c2, If tst d1 d2) ∈ ZOretrT (thetaIfZOT Un ZObisT)"
   unfolding ZOretrT_def proof (clarify, intro conjI)
     show "matchC_ZOC (thetaIfZOT Un ZObisT) (If tst c1 c2) (If tst d1 d2)"
     unfolding matchC_ZOC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(If tst c1 c2, s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', If tst d1 d2) ∈ thetaIfZOT Un ZObisT) ∨
        (∃d' t'. (If tst d1 d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaIfZOT Un ZObisT)"
       apply - apply(erule If_transC_invert)
       unfolding thetaIfZOT_def 
       apply simp apply (metis IfTrue c1d1 compatTst_def st tst)
       apply simp by (metis IfFalse c2d2 compatTst_def st tst)
     qed
   qed (unfold matchT_T_def, auto)
  }
  thus ?thesis unfolding thetaIfZOT_def by auto
qed

lemma thetaIfZOT_ZObisT:
"thetaIfZOT ⊆ ZObisT"
apply(rule ZObisT_coind)
using thetaIfZOT_sym thetaIfZOT_ZOretrT by auto

theorem If_ZObisT[simp]:
assumes "compatTst tst" and "c1 ≈01T d1" and "c2 ≈01T d2"
shows "If tst c1 c2 ≈01T If tst d1 d2"
using assms thetaIfZOT_ZObisT unfolding thetaIfZOT_def by blast

text‹While loop:›

definition thetaWhileZOT where 
"thetaWhileZOT ≡ 
 {(While tst c, While tst d) | tst c d. compatTst tst ∧ c ≈01T d} Un 
 {(c1 ;; (While tst c), d1 ;; (While tst d)) | tst c1 d1 c d. compatTst tst ∧ c1 ≈01T d1 ∧ c ≈01T d}"

lemma thetaWhileZOT_sym:
"sym thetaWhileZOT"
unfolding thetaWhileZOT_def sym_def using ZObisT_Sym by blast

lemma thetaWhileZOT_ZOretrT:
"thetaWhileZOT ⊆ ZOretrT (thetaWhileZOT Un ZObisT)"
proof-
  {fix tst c d 
   assume tst: "compatTst tst" and c_d: "c ≈01T d"
   hence matchC_ZOC: "matchC_ZOC ZObisT c d" 
     and matchT_T: "matchT_T c d" 
   using ZObisT_matchC_ZOC ZObisT_matchT_T by auto
   have "(While tst c, While tst d) ∈ ZOretrT (thetaWhileZOT Un ZObisT)"
   unfolding ZOretrT_def proof (clarify, intro conjI)
     show "matchC_ZOC (thetaWhileZOT ∪ ZObisT) (While tst c) (While tst d)"
     unfolding matchC_ZOC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(While tst c, s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', While tst d) ∈ thetaWhileZOT ∪ ZObisT) ∨ 
        (∃d' t'. (While tst d, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaWhileZOT ∪ ZObisT)"
       apply - apply(erule While_transC_invert)
       unfolding thetaWhileZOT_def apply simp
       by (metis WhileTrue c_d compatTst_def st tst)
     qed
   next
     show "matchT_T (While tst c) (While tst d)"
     unfolding matchT_T_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t s' assume st: "s ≈ t" assume "(While tst c, s) →t s'"
       thus "∃t'. (While tst d, t) →t t' ∧ s' ≈ t' "
       apply - apply(erule While_transT_invert)
       unfolding thetaWhileZOT_def apply simp
       by (metis PL.WhileFalse compatTst_def st tst)    
     qed
   qed
  }
  moreover 
  {fix tst c1 d1  c d
   assume tst: "compatTst tst" and c1d1: "c1 ≈01T d1" and c_d: "c ≈01T d"
   hence matchC_ZOC1: "matchC_ZOC ZObisT c1 d1" and matchC_ZOC: "matchC_ZOC ZObisT c d" 
     and matchT_T1: "matchT_T c1 d1" and matchT_T: "matchT_T c d"
   using ZObisT_matchC_ZOC ZObisT_matchT_T by auto
   have "(c1 ;; (While tst c), d1 ;; (While tst d)) ∈ ZOretrT (thetaWhileZOT Un ZObisT)"
   unfolding ZOretrT_def proof (clarify, intro conjI)
     show "matchC_ZOC (thetaWhileZOT ∪ ZObisT) (c1 ;; (While tst c)) (d1 ;; (While tst d))"
     unfolding matchC_ZOC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; (While tst c), s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', d1 ;; (While tst d)) ∈ thetaWhileZOT ∪ ZObisT) ∨ 
        (∃d' t'. (d1 ;; (While tst d), t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaWhileZOT ∪ ZObisT)"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume "(c1, s) →c (c1', s')" and c': "c' = c1' ;; (While tst c)"
         hence 
         "(s' ≈ t ∧ c1' ≈01T d1) ∨ 
          (∃d' t'. (d1, t) →c (d', t') ∧ s' ≈ t' ∧ c1' ≈01T d')" 
         using st matchC_ZOC1 unfolding matchC_ZOC_def by auto
         thus ?thesis
         unfolding c' thetaWhileZOT_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c_d tst)
         apply simp by (metis SeqC c_d tst) 
       next
         assume "(c1, s) →t s'" and c': "c' = While tst c"
         hence "∃t'. (d1, t) →t t' ∧ s' ≈ t'"
         using st matchT_T1 unfolding matchT_T_def by auto
         thus ?thesis
         unfolding c' thetaWhileZOT_def 
         apply simp by (metis PL.SeqT c_d tst) 
       qed
     qed
   qed (unfold matchT_T_def, auto)
  }
  ultimately show ?thesis unfolding thetaWhileZOT_def by auto
qed

lemma thetaWhileZOT_ZObisT:
"thetaWhileZOT ⊆ ZObisT"
apply(rule ZObisT_coind)
using thetaWhileZOT_sym thetaWhileZOT_ZOretrT by auto

theorem While_ZObisT[simp]:
assumes "compatTst tst" and "c ≈01T d"
shows "While tst c ≈01T While tst d"
using assms thetaWhileZOT_ZObisT unfolding thetaWhileZOT_def by auto

text‹Parallel composition:›

definition thetaParZOT where 
"thetaParZOT ≡ 
 {(Par c1 c2, Par d1 d2) | c1 c2 d1 d2. c1 ≈01T d1 ∧ c2 ≈01T d2}"

lemma thetaParZOT_sym:
"sym thetaParZOT"
unfolding thetaParZOT_def sym_def using ZObisT_Sym by blast

lemma thetaParZOT_ZOretrT:
"thetaParZOT ⊆ ZOretrT (thetaParZOT Un ZObisT)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈01T d1" and c2d2: "c2 ≈01T d2"
   hence matchC_ZOC1: "matchC_ZOC ZObisT c1 d1" and matchC_ZOC2: "matchC_ZOC ZObisT c2 d2"
     and matchT_T1: "matchT_T c1 d1" and matchT_T2: "matchT_T c2 d2"
   using ZObisT_matchC_ZOC ZObisT_matchT_T by auto
   have "(Par c1 c2, Par d1 d2) ∈ ZOretrT (thetaParZOT Un ZObisT)"
   unfolding ZOretrT_def proof (clarify, intro conjI)
     show "matchC_ZOC (thetaParZOT ∪ ZObisT) (Par c1 c2) (Par d1 d2)"
     unfolding matchC_ZOC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', Par d1 d2) ∈ thetaParZOT ∪ ZObisT) ∨
        (∃d' t'. (Par d1 d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParZOT ∪ ZObisT)"
       apply - proof(erule Par_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence
         "(s' ≈ t ∧ c1' ≈01T d1) ∨ 
          (∃d' t'. (d1, t) →c (d', t') ∧ s' ≈ t' ∧ c1' ≈01T d')"
         using st matchC_ZOC1 unfolding matchC_ZOC_def by auto
         thus ?thesis unfolding c' thetaParZOT_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c2d2)
         apply simp by(metis ParCL c2d2)
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →t t' ∧ s' ≈ t'"
         using st matchT_T1 unfolding matchT_T_def by auto
         thus ?thesis 
         unfolding c' thetaParZOT_def
         apply simp by (metis PL.ParTL c2d2) 
       next
         fix c2' assume "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence 
         "(s' ≈ t ∧ c2' ≈01T d2) ∨ 
          (∃d' t'. (d2, t) →c (d', t') ∧ s' ≈ t' ∧ c2' ≈01T d')"
         using st matchC_ZOC2 unfolding matchC_ZOC_def by auto
         thus ?thesis 
         unfolding c' thetaParZOT_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c1d1)
         apply simp by (metis ParCR c1d1)
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence "∃t'. (d2, t) →t t' ∧ s' ≈ t'"
         using st matchT_T2 unfolding matchT_T_def by auto
         thus ?thesis 
         unfolding c' thetaParZOT_def
         apply simp by (metis PL.ParTR c1d1) 
       qed
     qed 
   qed (unfold matchT_T_def, auto)
  }
  thus ?thesis unfolding thetaParZOT_def by auto
qed

lemma thetaParZOT_ZObisT:
"thetaParZOT ⊆ ZObisT"
apply(rule ZObisT_coind)
using thetaParZOT_sym thetaParZOT_ZOretrT by auto

theorem Par_ZObisT[simp]:
assumes "c1 ≈01T d1" and "c2 ≈01T d2"
shows "Par c1 c2 ≈01T Par d1 d2"
using assms thetaParZOT_ZObisT unfolding thetaParZOT_def by blast


subsubsection‹01-bisimilarity versus language constructs›

text‹Discreetness:›

theorem discr_ZObis[simp]:
assumes *: "discr c" and **: "discr d"
shows "c ≈01 d"
proof-
  let ?theta = "{(c,d) | c d. discr c ∧ discr d}"
  have "?theta ⊆ ZObis"
  proof(rule ZObis_raw_coind)
    show "sym ?theta" unfolding sym_def by blast
  next
    show "?theta ⊆ ZOretr ?theta"
    proof clarify
      fix c d assume c: "discr c" and d: "discr d"
      show "(c, d) ∈ ZOretr ?theta"
      unfolding ZOretr_def proof (clarify, intro conjI)
        show "matchC_ZO ?theta c d"
        unfolding matchC_ZO_def proof (tactic ‹mauto_no_simp_tac @{context}›)
          fix s t c' s'
          assume st: "s ≈ t" and cs: "(c, s) →c (c', s')"
          show 
          "(s' ≈ t ∧ (c', d) ∈ ?theta) ∨
           (∃d' t'. (d, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ ?theta) ∨
           (∃t'. (d, t) →t t' ∧ s' ≈ t' ∧ discr c')"
          proof-
            have "s ≈ s'" using c cs discr_transC_indis by blast
            hence s't: "s' ≈ t" using st indis_trans indis_sym by blast
            have "discr c'" using c cs discr_transC by blast
            hence "(c',d) ∈ ?theta" using d by blast
            thus ?thesis using s't by blast
          qed
        qed
      next
        show "matchT_ZO c d"
        unfolding matchT_ZO_def proof (tactic ‹mauto_no_simp_tac @{context}›)
          fix s t s'
          assume st: "s ≈ t" and cs: "(c, s) →t s'"
          show 
          "(s' ≈ t ∧ discr d) ∨
           (∃d' t'. (d, t) →c (d', t') ∧ s' ≈ t' ∧ discr d') ∨
           (∃t'. (d, t) →t t' ∧ s' ≈ t')"
          proof-
            have "s ≈ s'" using c cs discr_transT by blast
            hence s't: "s' ≈ t" using st indis_trans indis_sym by blast
            thus ?thesis using d by blast
          qed
        qed
      qed
    qed
  qed
  thus ?thesis using assms by blast
qed

text ‹Atomic commands:›

theorem Atm_ZObis[simp]:
assumes "compatAtm atm" 
shows "Atm atm ≈01 Atm atm"
by (metis Atm_Sbis assms bis_imp) 

text‹Sequential composition:›

definition thetaSeqZO where 
"thetaSeqZO ≡ 
 {(c1 ;; c2, d1 ;; d2) | c1 c2 d1 d2. c1 ≈01T d1 ∧ c2 ≈01 d2}"

lemma thetaSeqZO_sym:
"sym thetaSeqZO"
unfolding thetaSeqZO_def sym_def using ZObisT_Sym ZObis_Sym by blast

lemma thetaSeqZO_ZOretr:
"thetaSeqZO ⊆ ZOretr (thetaSeqZO Un ZObis)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈01T d1" and c2d2: "c2 ≈01 d2"
   hence matchC_ZOC1: "matchC_ZOC ZObisT c1 d1" and matchC_ZO2: "matchC_ZO ZObis c2 d2"
     and matchT_T1: "matchT_T c1 d1" and matchT_ZO2: "matchT_ZO c2 d2"
   using ZObisT_matchC_ZOC ZObisT_matchT_T ZObis_matchC_ZO ZObis_matchT_ZO by auto
   have "(c1 ;; c2, d1 ;; d2) ∈ ZOretr (thetaSeqZO Un ZObis)"
   unfolding ZOretr_def proof (clarify, intro conjI)
     show "matchC_ZO (thetaSeqZO Un ZObis) (c1 ;; c2) (d1 ;; d2)"
     unfolding matchC_ZO_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; c2, s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', d1 ;; d2) ∈ thetaSeqZO Un ZObis) ∨
        (∃d' t'. (d1 ;; d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaSeqZO Un ZObis) ∨ 
        (∃t'. (d1 ;; d2, t) →t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
         hence
         "(s' ≈ t ∧ c1' ≈01T d1) ∨ 
          (∃d1' t'. (d1, t) →c (d1', t') ∧ s' ≈ t' ∧ c1' ≈01T d1')"
         using st matchC_ZOC1 unfolding matchC_ZOC_def by auto
         thus ?thesis unfolding c' thetaSeqZO_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c2d2)
         apply simp by (metis SeqC c2d2 ) 
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →t t' ∧ s' ≈ t'"
         using st matchT_T1 unfolding matchT_T_def by auto
         thus ?thesis 
         unfolding c' thetaSeqZO_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp by (metis PL.SeqT c2d2) 
       qed
     qed 
   qed (unfold matchT_ZO_def, auto)
  }
  thus ?thesis unfolding thetaSeqZO_def by auto
qed

lemma thetaSeqZO_ZObis:
"thetaSeqZO ⊆ ZObis"
apply(rule ZObis_coind)
using thetaSeqZO_sym thetaSeqZO_ZOretr by auto

theorem Seq_ZObisT_ZObis[simp]:
assumes "c1 ≈01T d1" and "c2 ≈01 d2"
shows "c1 ;; c2 ≈01 d1 ;; d2"
using assms thetaSeqZO_ZObis unfolding thetaSeqZO_def by blast

theorem Seq_siso_ZObis[simp]:
assumes "siso e" and "c2 ≈01 d2"
shows "e ;; c2 ≈01 e ;; d2"
using assms by auto

(*  *)

definition thetaSeqZOD where 
"thetaSeqZOD ≡ 
 {(c1 ;; c2, d1 ;; d2) | c1 c2 d1 d2. c1 ≈01 d1 ∧ discr c2 ∧ discr d2}"

lemma thetaSeqZOD_sym:
"sym thetaSeqZOD"
unfolding thetaSeqZOD_def sym_def using ZObis_Sym by blast

lemma thetaSeqZOD_ZOretr:
"thetaSeqZOD ⊆ ZOretr (thetaSeqZOD Un ZObis)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈01 d1" and c2: "discr c2" and d2: "discr d2"
   hence matchC_ZO: "matchC_ZO ZObis c1 d1" 
     and matchT_ZO: "matchT_ZO c1 d1"
   using ZObis_matchC_ZO ZObis_matchT_ZO by auto
   have "(c1 ;; c2, d1 ;; d2) ∈ ZOretr (thetaSeqZOD Un ZObis)"
   unfolding ZOretr_def proof (clarify, intro conjI)
     show "matchC_ZO (thetaSeqZOD Un ZObis) (c1 ;; c2) (d1 ;; d2)"
     unfolding matchC_ZO_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; c2, s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', d1 ;; d2) ∈ thetaSeqZOD Un ZObis) ∨
        (∃d' t'. (d1 ;; d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaSeqZOD Un ZObis) ∨ 
        (∃t'. (d1 ;; d2, t) →t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
         hence
         "(s' ≈ t ∧ c1' ≈01 d1) ∨ 
          (∃d' t'. (d1, t) →c (d', t') ∧ s' ≈ t' ∧ c1' ≈01 d') ∨ 
          (∃t'. (d1, t) →t t' ∧ s' ≈ t' ∧ discr c1')"
         using st matchC_ZO unfolding matchC_ZO_def by auto
         thus ?thesis unfolding c' thetaSeqZOD_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c2 d2)
         apply simp apply (metis SeqC c2 d2)
         apply simp by (metis SeqT c2 d2 discr_Seq discr_ZObis) 
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence 
         "(s' ≈ t ∧ discr d1) ∨ 
          (∃d' t'. (d1, t) →c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d1, t) →t t' ∧ s' ≈ t')"
         using st matchT_ZO unfolding matchT_ZO_def by auto
         thus ?thesis 
         unfolding c' thetaSeqZOD_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c2 d2 discr_Seq discr_ZObis)
         apply simp apply (metis SeqC c2 d2 discr_Seq discr_ZObis)
         apply simp by (metis SeqT c2 d2 discr_ZObis) 
       qed
     qed 
   qed (unfold matchT_ZO_def, auto)
  }
  thus ?thesis unfolding thetaSeqZOD_def by auto
qed

lemma thetaSeqZOD_ZObis:
"thetaSeqZOD ⊆ ZObis"
apply(rule ZObis_coind)
using thetaSeqZOD_sym thetaSeqZOD_ZOretr by auto

theorem Seq_ZObis_discr[simp]:
assumes "c1 ≈01 d1" and "discr c2" and "discr d2"
shows "c1 ;; c2 ≈01 d1 ;; d2"
using assms thetaSeqZOD_ZObis unfolding thetaSeqZOD_def by blast

text‹Conditional:›

definition thetaIfZO where 
"thetaIfZO ≡ 
 {(If tst c1 c2, If tst d1 d2) | tst c1 c2 d1 d2. compatTst tst ∧ c1 ≈01 d1 ∧ c2 ≈01 d2}"

lemma thetaIfZO_sym:
"sym thetaIfZO"
unfolding thetaIfZO_def sym_def using ZObis_Sym by blast

lemma thetaIfZO_ZOretr:
"thetaIfZO ⊆ ZOretr (thetaIfZO Un ZObis)"
proof-
  {fix tst c1 c2 d1 d2
   assume tst: "compatTst tst" and c1d1: "c1 ≈01 d1" and c2d2: "c2 ≈01 d2"
   hence matchC_ZO1: "matchC_ZO ZObis c1 d1" and matchC_ZO2: "matchC_ZO ZObis c2 d2"
     and matchT_ZO1: "matchT_ZO c1 d1" and matchT_ZO2: "matchT_ZO c2 d2"
   using ZObis_matchC_ZO ZObis_matchT_ZO by auto
   have "(If tst c1 c2, If tst d1 d2) ∈ ZOretr (thetaIfZO Un ZObis)"
   unfolding ZOretr_def proof (clarify, intro conjI)
     show "matchC_ZO (thetaIfZO Un ZObis) (If tst c1 c2) (If tst d1 d2)"
     unfolding matchC_ZO_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(If tst c1 c2, s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', If tst d1 d2) ∈ thetaIfZO Un ZObis) ∨
        (∃d' t'. (If tst d1 d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaIfZO Un ZObis) ∨ 
        (∃t'. (If tst d1 d2, t) →t t' ∧ s' ≈ t' ∧ discr c')"
       apply - apply(erule If_transC_invert)
       unfolding thetaIfZO_def 
       apply simp apply (metis IfTrue c1d1 compatTst_def st tst)
       apply simp by (metis IfFalse c2d2 compatTst_def st tst)
     qed
   qed (unfold matchT_ZO_def, auto)
  }
  thus ?thesis unfolding thetaIfZO_def by auto
qed

lemma thetaIfZO_ZObis:
"thetaIfZO ⊆ ZObis"
apply(rule ZObis_coind)
using thetaIfZO_sym thetaIfZO_ZOretr by auto

theorem If_ZObis[simp]:
assumes "compatTst tst" and "c1 ≈01 d1" and "c2 ≈01 d2"
shows "If tst c1 c2 ≈01 If tst d1 d2"
using assms thetaIfZO_ZObis unfolding thetaIfZO_def by blast

text‹While loop:›

text‹01-bisimilarity does not interact with / preserve the While construct in 
any interesting way.›

(* Indeed, assume c ≈01 d and try to prove while tst c ≈01 while tst d.  
If tst is True in some state, we obtain the task of proving c ;; (while tst c) ≈01 d ;; (while tst d).  
Now, assume c takes a step to c' and d terminates, possibility allowed by ~01-bisimilarity, 
provided c' is discr.  So now we need to have, for discr c', the following: 
c' ;; (while tst c) ≈01 while tst d.  This is not true in general. *)

text‹Parallel composition:›

definition thetaParZOL1 where 
"thetaParZOL1 ≡ 
 {(Par c1 c2, d) | c1 c2 d. c1 ≈01 d ∧ discr c2}"

lemma thetaParZOL1_ZOretr:
"thetaParZOL1 ⊆ ZOretr (thetaParZOL1 Un ZObis)"
proof-
  {fix c1 c2 d
   assume c1d: "c1 ≈01 d" and c2: "discr c2"
   hence matchC_ZO: "matchC_ZO ZObis c1 d" 
     and matchT_ZO: "matchT_ZO c1 d" 
   using ZObis_matchC_ZO ZObis_matchT_ZO by auto
   have "(Par c1 c2, d) ∈ ZOretr (thetaParZOL1 Un ZObis)"
   unfolding ZOretr_def proof (clarify, intro conjI)
     show "matchC_ZO (thetaParZOL1 ∪ ZObis) (Par c1 c2) d"
     unfolding matchC_ZO_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus
       "(s' ≈ t ∧ (c', d) ∈ thetaParZOL1 ∪ ZObis) ∨
        (∃d' t'. (d, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParZOL1 ∪ ZObis) ∨
        (∃t'. (d, t) →t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Par_transC_invert)
         fix c1' assume "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence 
         "(s' ≈ t ∧ c1' ≈01 d) ∨ 
          (∃d' t'. (d, t) →c (d', t') ∧ s' ≈ t' ∧ c1' ≈01 d') ∨ 
          (∃t'. (d, t) →t t' ∧ s' ≈ t' ∧ discr c1')"
         using st matchC_ZO unfolding matchC_ZO_def by blast
         thus ?thesis unfolding thetaParZOL1_def
         apply - apply(elim disjE exE conjE) 
         apply simp apply (metis c2 c')
         apply simp apply (metis c2 c')
         apply simp by (metis c' c2 discr_Par) 
       next
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence 
         "(s' ≈ t ∧ discr d) ∨ 
          (∃d' t'. (d, t) →c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d, t) →t t' ∧ s' ≈ t')"
         using st matchT_ZO unfolding matchT_ZO_def by blast
         thus ?thesis unfolding thetaParZOL1_def
         apply - apply(elim disjE exE conjE)
         apply simp apply (metis c' c2 discr_ZObis)
         apply simp apply (metis c' c2 discr_ZObis)
         apply simp by (metis c' c2)  
       next
         fix c2' assume c2s: "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence "s ≈ s'" using c2 discr_transC_indis by blast
         hence s't: "s' ≈ t" using st indis_sym indis_trans by blast
         have "discr c2'" using c2 c2s discr_transC by blast
         thus ?thesis using s't c1d unfolding thetaParZOL1_def c' by simp
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence "s ≈ s'" using c2 discr_transT by blast
         hence s't: "s' ≈ t" using st indis_sym indis_trans by blast
         thus ?thesis using c1d unfolding thetaParZOL1_def c' by simp
       qed
     qed
   qed (unfold matchT_ZO_def, auto)
  }
  thus ?thesis unfolding thetaParZOL1_def by blast
qed

lemma thetaParZOL1_converse_ZOretr:
"thetaParZOL1 ^-1 ⊆ ZOretr (thetaParZOL1 ^-1 Un ZObis)"
proof-
  {fix c1 c2 d
   assume c1d: "c1 ≈01 d" and c2: "discr c2"
   hence matchC_ZO: "matchC_ZO ZObis d c1" 
     and matchT_ZO: "matchT_ZO d c1" 
   using ZObis_matchC_ZO_rev ZObis_matchT_ZO_rev by auto
   have "(d, Par c1 c2) ∈ ZOretr (thetaParZOL1¯ ∪ ZObis)"
   unfolding ZOretr_def proof (clarify, intro conjI)
     show "matchC_ZO (thetaParZOL1¯ ∪ ZObis) d (Par c1 c2)"
     unfolding matchC_ZO_def2 ZObis_converse proof (tactic ‹mauto_no_simp_tac @{context}›) 
       fix s t d' t'
       assume "s ≈ t" and "(d, t) →c (d', t')"
       hence 
       "(s ≈ t' ∧ d' ≈01 c1) ∨ 
        (∃c' s'. (c1, s) →c (c', s') ∧ s' ≈ t' ∧ d' ≈01 c') ∨ 
        (∃s'. (c1, s) →t s' ∧ s' ≈ t' ∧ discr d')"
       using matchC_ZO unfolding matchC_ZO_def2 by auto
       thus
       "(s ≈ t' ∧ (Par c1 c2, d') ∈ thetaParZOL1 ∪ ZObis) ∨
        (∃c' s'. (Par c1 c2, s) →c (c', s') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParZOL1 ∪ ZObis) ∨
        (∃s'. (Par c1 c2, s) →t s' ∧ s' ≈ t' ∧ discr d')"
       unfolding thetaParZOL1_def 
       apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
       apply simp apply (metis ZObis_Sym c2)
       apply simp apply (metis ParCL ZObis_sym c2 sym_def)
       apply simp by (metis ParTL c2 discr_ZObis) 
     qed
   next
     show "matchT_ZO d (Par c1 c2)"
     unfolding matchT_ZO_def2 ZObis_converse proof (tactic ‹mauto_no_simp_tac @{context}›) 
       fix s t t'
       assume "s ≈ t" and "(d, t) →t t'"
       hence 
       "(s ≈ t' ∧ discr c1) ∨ 
        (∃c' s'. (c1, s) →c (c', s') ∧ s' ≈ t' ∧ discr c') ∨ 
        (∃s'. (c1, s) →t s' ∧ s' ≈ t')"
       using matchT_ZO unfolding matchT_ZO_def2 by auto
       thus
       "(s ≈ t' ∧ discr (Par c1 c2)) ∨ 
        (∃c' s'. (Par c1 c2, s) →c (c', s') ∧ s' ≈ t' ∧ discr c') ∨ 
        (∃s'. (Par c1 c2, s) →t s' ∧ s' ≈ t')"
       apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
       apply simp apply (metis c2 discr_Par)
       apply simp apply (metis ParCL c2 discr_Par)
       apply simp by (metis ParTL c2)
     qed
   qed
  }
  thus ?thesis unfolding thetaParZOL1_def by blast
qed

lemma thetaParZOL1_ZObis:
"thetaParZOL1 ⊆ ZObis"
apply(rule ZObis_coind2)
using thetaParZOL1_ZOretr thetaParZOL1_converse_ZOretr by auto

theorem Par_ZObis_discrL1[simp]:
assumes "c1 ≈01 d" and "discr c2"
shows "Par c1 c2 ≈01 d"
using assms thetaParZOL1_ZObis unfolding thetaParZOL1_def by blast

theorem Par_ZObis_discrR1[simp]:
assumes "c ≈01 d1" and "discr d2"
shows "c ≈01 Par d1 d2"
using assms Par_ZObis_discrL1 ZObis_Sym by blast

(*  *)

definition thetaParZOL2 where 
"thetaParZOL2 ≡ 
 {(Par c1 c2, d) | c1 c2 d. discr c1 ∧ c2 ≈01 d}"

lemma thetaParZOL2_ZOretr:
"thetaParZOL2 ⊆ ZOretr (thetaParZOL2 Un ZObis)"
proof-
  {fix c1 c2 d
   assume c2d: "c2 ≈01 d" and c1: "discr c1" 
   hence matchC_ZO: "matchC_ZO ZObis c2 d" 
     and matchT_ZO: "matchT_ZO c2 d" 
   using ZObis_matchC_ZO ZObis_matchT_ZO by auto
   have "(Par c1 c2, d) ∈ ZOretr (thetaParZOL2 Un ZObis)"
   unfolding ZOretr_def proof (clarify, intro conjI)
     show "matchC_ZO (thetaParZOL2 ∪ ZObis) (Par c1 c2) d"
     unfolding matchC_ZO_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus
       "(s' ≈ t ∧ (c', d) ∈ thetaParZOL2 ∪ ZObis) ∨
        (∃d' t'. (d, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParZOL2 ∪ ZObis) ∨
        (∃t'. (d, t) →t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Par_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence "s ≈ s'" using c1 discr_transC_indis by blast
         hence s't: "s' ≈ t" using st indis_sym indis_trans by blast
         have "discr c1'" using c1 c1s discr_transC by blast
         thus ?thesis using s't c2d unfolding thetaParZOL2_def c' by simp
       next
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "s ≈ s'" using c1 discr_transT by blast
         hence s't: "s' ≈ t" using st indis_sym indis_trans by blast
         thus ?thesis using c2d unfolding thetaParZOL2_def c' by simp
       next
         fix c2' assume "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence 
         "(s' ≈ t ∧ c2' ≈01 d) ∨ 
          (∃d' t'. (d, t) →c (d', t') ∧ s' ≈ t' ∧ c2' ≈01 d') ∨ 
          (∃t'. (d, t) →t t' ∧ s' ≈ t' ∧ discr c2')"
         using st matchC_ZO unfolding matchC_ZO_def by blast
         thus ?thesis unfolding thetaParZOL2_def
         apply - apply(elim disjE exE conjE) 
         apply simp apply (metis c1 c')
         apply simp apply (metis c1 c')
         apply simp by (metis c' c1 discr_Par) 
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence 
         "(s' ≈ t ∧ discr d) ∨ 
          (∃d' t'. (d, t) →c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d, t) →t t' ∧ s' ≈ t')"
         using st matchT_ZO unfolding matchT_ZO_def by blast
         thus ?thesis unfolding thetaParZOL2_def
         apply - apply(elim disjE exE conjE)
         apply simp apply (metis c' c1 discr_ZObis)
         apply simp apply (metis c' c1 discr_ZObis)
         apply simp by (metis c' c1)          
       qed
     qed
   qed (unfold matchT_ZO_def, auto)
  }
  thus ?thesis unfolding thetaParZOL2_def by blast
qed

lemma thetaParZOL2_converse_ZOretr:
"thetaParZOL2 ^-1 ⊆ ZOretr (thetaParZOL2 ^-1 Un ZObis)"
proof-
  {fix c1 c2 d
   assume c2d: "c2 ≈01 d" and c1: "discr c1"
   hence matchC_ZO: "matchC_ZO ZObis d c2" 
     and matchT_ZO: "matchT_ZO d c2" 
   using ZObis_matchC_ZO_rev ZObis_matchT_ZO_rev by auto
   have "(d, Par c1 c2) ∈ ZOretr (thetaParZOL2¯ ∪ ZObis)"
   unfolding ZOretr_def proof (clarify, intro conjI)
     show "matchC_ZO (thetaParZOL2¯ ∪ ZObis) d (Par c1 c2)"
     unfolding matchC_ZO_def2 ZObis_converse proof (tactic ‹mauto_no_simp_tac @{context}›) 
       fix s t d' t'
       assume "s ≈ t" and "(d, t) →c (d', t')"
       hence 
       "(s ≈ t' ∧ d' ≈01 c2) ∨ 
        (∃c' s'. (c2, s) →c (c', s') ∧ s' ≈ t' ∧ d' ≈01 c') ∨ 
        (∃s'. (c2, s) →t s' ∧ s' ≈ t' ∧ discr d')"
       using matchC_ZO unfolding matchC_ZO_def2 by auto
       thus
       "(s ≈ t' ∧ (Par c1 c2, d') ∈ thetaParZOL2 ∪ ZObis) ∨
        (∃c' s'. (Par c1 c2, s) →c (c', s') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParZOL2 ∪ ZObis) ∨
        (∃s'. (Par c1 c2, s) →t s' ∧ s' ≈ t' ∧ discr d')"
       unfolding thetaParZOL2_def 
       apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
       apply simp apply (metis ZObis_Sym c1)
       apply simp apply (metis ParCR ZObis_sym c1 sym_def)
       apply simp by (metis ParTR c1 discr_ZObis) 
     qed
   next
     show "matchT_ZO d (Par c1 c2)"
     unfolding matchT_ZO_def2 ZObis_converse proof (tactic ‹mauto_no_simp_tac @{context}›) 
       fix s t t'
       assume "s ≈ t" and "(d, t) →t t'"
       hence 
       "(s ≈ t' ∧ discr c2) ∨ 
        (∃c' s'. (c2, s) →c (c', s') ∧ s' ≈ t' ∧ discr c') ∨ 
        (∃s'. (c2, s) →t s' ∧ s' ≈ t')"
       using matchT_ZO unfolding matchT_ZO_def2 by auto
       thus
       "(s ≈ t' ∧ discr (Par c1 c2)) ∨ 
        (∃c' s'. (Par c1 c2, s) →c (c', s') ∧ s' ≈ t' ∧ discr c') ∨ 
        (∃s'. (Par c1 c2, s) →t s' ∧ s' ≈ t')"
       apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
       apply simp apply (metis c1 discr_Par)
       apply simp apply (metis ParCR c1 discr_Par)
       apply simp by (metis ParTR c1)
     qed
   qed
  }
  thus ?thesis unfolding thetaParZOL2_def by blast
qed

lemma thetaParZOL2_ZObis:
"thetaParZOL2 ⊆ ZObis"
apply(rule ZObis_coind2)
using thetaParZOL2_ZOretr thetaParZOL2_converse_ZOretr by auto

theorem Par_ZObis_discrL2[simp]:
assumes "c2 ≈01 d" and "discr c1"
shows "Par c1 c2 ≈01 d"
using assms thetaParZOL2_ZObis unfolding thetaParZOL2_def by blast

theorem Par_ZObis_discrR2[simp]:
assumes "c ≈01 d2" and "discr d1"
shows "c ≈01 Par d1 d2"
using assms Par_ZObis_discrL2 ZObis_Sym by blast

(*  *)

definition thetaParZO where 
"thetaParZO ≡ 
 {(Par c1 c2, Par d1 d2) | c1 c2 d1 d2. c1 ≈01 d1 ∧ c2 ≈01 d2}"

lemma thetaParZO_sym:
"sym thetaParZO"
unfolding thetaParZO_def sym_def using ZObis_Sym by blast

lemma thetaParZO_ZOretr:
"thetaParZO ⊆ ZOretr (thetaParZO Un ZObis)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈01 d1" and c2d2: "c2 ≈01 d2"
   hence matchC_ZO1: "matchC_ZO ZObis c1 d1" and matchC_ZO2: "matchC_ZO ZObis c2 d2"
     and matchT_ZO1: "matchT_ZO c1 d1" and matchT_ZO2: "matchT_ZO c2 d2"
   using ZObis_matchC_ZO ZObis_matchT_ZO by auto
   have "(Par c1 c2, Par d1 d2) ∈ ZOretr (thetaParZO Un ZObis)"
   unfolding ZOretr_def proof (clarify, intro conjI)
     show "matchC_ZO (thetaParZO ∪ ZObis) (Par c1 c2) (Par d1 d2)"
     unfolding matchC_ZO_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus 
       "(s' ≈ t ∧ (c', Par d1 d2) ∈ thetaParZO ∪ ZObis) ∨
        (∃d' t'. (Par d1 d2, t) →c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParZO ∪ ZObis) ∨ 
        (∃t'. (Par d1 d2, t) →t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Par_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence
         "(s' ≈ t ∧ c1' ≈01 d1) ∨ 
          (∃d' t'. (d1, t) →c (d', t') ∧ s' ≈ t' ∧ c1' ≈01 d') ∨ 
          (∃t'. (d1, t) →t t' ∧ s' ≈ t' ∧ discr c1')"
         using st matchC_ZO1 unfolding matchC_ZO_def by auto
         thus ?thesis unfolding c' thetaParZO_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c2d2)
         apply simp apply (metis ParCL c2d2)
         apply simp by (metis ParTL Par_ZObis_discrL2 c2d2)   
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence 
         "(s' ≈ t ∧ discr d1) ∨ 
          (∃d' t'. (d1, t) →c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d1, t) →t t' ∧ s' ≈ t')"
         using st matchT_ZO1 unfolding matchT_ZO_def by auto
         thus ?thesis 
         unfolding c' thetaParZO_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis Par_ZObis_discrR2 c2d2)
         apply simp apply (metis PL.ParCL Par_ZObis_discrR2 c2d2)
         apply simp by (metis PL.ParTL c2d2) 
       next
         fix c2' assume "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence 
         "(s' ≈ t ∧ c2' ≈01 d2) ∨ 
          (∃d' t'. (d2, t) →c (d', t') ∧ s' ≈ t' ∧ c2' ≈01 d') ∨ 
          (∃t'. (d2, t) →t t' ∧ s' ≈ t' ∧ discr c2')"
         using st matchC_ZO2 unfolding matchC_ZO_def by auto
         thus ?thesis 
         unfolding c' thetaParZO_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis c1d1)
         apply simp apply (metis PL.ParCR c1d1)
         apply simp by (metis PL.ParTR Par_ZObis_discrL1 c1d1)
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence 
         "(s' ≈ t ∧ discr d2) ∨ 
          (∃d' t'. (d2, t) →c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d2, t) →t t' ∧ s' ≈ t')"
         using st matchT_ZO2 unfolding matchT_ZO_def by auto
         thus ?thesis 
         unfolding c' thetaParZO_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis Par_ZObis_discrR1 c1d1)
         apply simp apply (metis PL.ParCR Par_ZObis_discrR1 c1d1)
         apply simp by (metis PL.ParTR c1d1) 
       qed
     qed 
   qed (unfold matchT_ZO_def, auto)
  }
  thus ?thesis unfolding thetaParZO_def by auto
qed

lemma thetaParZO_ZObis:
"thetaParZO ⊆ ZObis"
apply(rule ZObis_coind)
using thetaParZO_sym thetaParZO_ZOretr by auto

theorem Par_ZObis[simp]:
assumes "c1 ≈01 d1" and "c2 ≈01 d2"
shows "Par c1 c2 ≈01 Par d1 d2"
using assms thetaParZO_ZObis unfolding thetaParZO_def by blast


subsubsection‹WT-bisimilarity versus language constructs›

text‹Discreetness:›

theorem noWhile_discr_WbisT[simp]:
  assumes "noWhile c1" and "noWhile c2" 
  and "discr c1" and "discr c2"
  shows "c1 ≈wT c2"
proof -
  from assms have "noWhile c1 ∧ noWhile c2 ∧ discr c1 ∧ discr c2" by auto
  then show ?thesis
  proof (induct rule: WbisT_coinduct)
    case cont then show ?case
      by (metis MtransC_Refl noWhile_transC discr_transC discr_transC_indis indis_sym indis_trans) 
  next
    case termi then show ?case
      by (metis discr_MtransT indis_sym indis_trans noWhile_MtransT transT_MtransT)
  qed simp
qed

text ‹Atomic commands:›

theorem Atm_WbisT:
assumes "compatAtm atm" 
shows "Atm atm ≈wT Atm atm"
by (metis Atm_Sbis assms bis_imp)

text‹Sequential composition:› 

definition thetaSeqWT where 
"thetaSeqWT ≡ 
 {(c1 ;; c2, d1 ;; d2) | c1 c2 d1 d2. c1 ≈wT d1 ∧ c2 ≈wT d2}"

lemma thetaSeqWT_sym:
"sym thetaSeqWT"
unfolding thetaSeqWT_def sym_def using WbisT_Sym by blast

lemma thetaSeqWT_WretrT:
"thetaSeqWT ⊆ WretrT (thetaSeqWT Un WbisT)"
proof- 
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈wT d1" and c2d2: "c2 ≈wT d2"
   hence matchC_MC1: "matchC_MC WbisT c1 d1" and matchC_MC2: "matchC_MC WbisT c2 d2"
     and matchT_MT1: "matchT_MT c1 d1" and matchT_T2: "matchT_MT c2 d2"
   using WbisT_matchC_MC WbisT_matchT_MT by auto
   have "(c1 ;; c2, d1 ;; d2) ∈ WretrT (thetaSeqWT Un WbisT)"
   unfolding WretrT_def proof (clarify, intro conjI)
     show "matchC_MC (thetaSeqWT Un WbisT) (c1 ;; c2) (d1 ;; d2)"
     unfolding matchC_MC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; c2, s) →c (c', s')"
       thus "(∃d' t'. (d1 ;; d2, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaSeqWT Un WbisT)"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
         hence "∃d1' t'. (d1, t) →*c (d1', t') ∧ s' ≈ t' ∧ c1' ≈wT d1'"
         using st matchC_MC1 unfolding matchC_MC_def by blast
         thus ?thesis unfolding c' thetaSeqWT_def
         apply simp by (metis PL.Seq_MtransC c2d2) 
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →*t t' ∧ s' ≈ t'"
         using st matchT_MT1 unfolding matchT_MT_def by auto
         thus ?thesis 
         unfolding c' thetaSeqWT_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp by (metis Seq_MtransT_MtransC c2d2) 
       qed
     qed 
   qed (unfold matchT_MT_def, auto)
  }
  thus ?thesis unfolding thetaSeqWT_def by auto
qed

lemma thetaSeqWT_WbisT:
"thetaSeqWT ⊆ WbisT"
apply(rule WbisT_coind)
using thetaSeqWT_sym thetaSeqWT_WretrT by auto

theorem Seq_WbisT[simp]:
assumes "c1 ≈wT d1" and "c2 ≈wT d2"
shows "c1 ;; c2 ≈wT d1 ;; d2"
using assms thetaSeqWT_WbisT unfolding thetaSeqWT_def by blast 

text‹Conditional:›

definition thetaIfWT where 
"thetaIfWT ≡ 
 {(If tst c1 c2, If tst d1 d2) | tst c1 c2 d1 d2. compatTst tst ∧ c1 ≈wT d1 ∧ c2 ≈wT d2}"

lemma thetaIfWT_sym:
"sym thetaIfWT"
unfolding thetaIfWT_def sym_def using WbisT_Sym by blast

lemma thetaIfWT_WretrT:
"thetaIfWT ⊆ WretrT (thetaIfWT Un WbisT)"
proof- 
  {fix tst c1 c2 d1 d2
   assume tst: "compatTst tst" and c1d1: "c1 ≈wT d1" and c2d2: "c2 ≈wT d2"
   hence matchC_MC1: "matchC_MC WbisT c1 d1" and matchC_MC2: "matchC_MC WbisT c2 d2"
     and matchT_MT1: "matchT_MT c1 d1" and matchT_MT2: "matchT_MT c2 d2"
   using WbisT_matchC_MC WbisT_matchT_MT by auto
   have "(If tst c1 c2, If tst d1 d2) ∈ WretrT (thetaIfWT Un WbisT)"
   unfolding WretrT_def proof (clarify, intro conjI)
     show "matchC_MC (thetaIfWT Un WbisT) (If tst c1 c2) (If tst d1 d2)"
     unfolding matchC_MC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(If tst c1 c2, s) →c (c', s')"
       thus "∃d' t'. (If tst d1 d2, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaIfWT Un WbisT"
       apply - apply(erule If_transC_invert)
       unfolding thetaIfWT_def 
       apply simp apply (metis IfTrue c1d1 compatTst_def st transC_MtransC tst) 
       apply simp by (metis IfFalse c2d2 compatTst_def st transC_MtransC tst) 
     qed
   qed (unfold matchT_MT_def, auto)
  }
  thus ?thesis unfolding thetaIfWT_def by auto
qed

lemma thetaIfWT_WbisT:
"thetaIfWT ⊆ WbisT"
apply(rule WbisT_coind)
using thetaIfWT_sym thetaIfWT_WretrT by auto

theorem If_WbisT[simp]:
assumes "compatTst tst" and "c1 ≈wT d1" and "c2 ≈wT d2"
shows "If tst c1 c2 ≈wT If tst d1 d2"
using assms thetaIfWT_WbisT unfolding thetaIfWT_def by blast

text‹While loop:›

definition thetaWhileW where 
"thetaWhileW ≡ 
 {(While tst c, While tst d) | tst c d. compatTst tst ∧ c ≈wT d} Un 
 {(c1 ;; (While tst c), d1 ;; (While tst d)) | tst c1 d1 c d. 
               compatTst tst ∧ c1 ≈wT d1 ∧ c ≈wT d}"

lemma thetaWhileW_sym:
"sym thetaWhileW"
unfolding thetaWhileW_def sym_def using WbisT_Sym by blast

lemma thetaWhileW_WretrT:
"thetaWhileW ⊆ WretrT (thetaWhileW Un WbisT)"
proof-
  {fix tst c d 
   assume tst: "compatTst tst" and c_d: "c ≈wT d"
   hence matchC_MC: "matchC_MC WbisT c d" 
     and matchT_MT: "matchT_MT c d" 
   using WbisT_matchC_MC WbisT_matchT_MT by auto
   have "(While tst c, While tst d) ∈ WretrT (thetaWhileW Un WbisT)"
   unfolding WretrT_def proof (clarify, intro conjI)
     show "matchC_MC (thetaWhileW ∪ WbisT) (While tst c) (While tst d)"
     unfolding matchC_MC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(While tst c, s) →c (c', s')"
       thus "∃d' t'. (While tst d, t) →*c (d', t') ∧ s' ≈ t' ∧ 
                     (c', d') ∈ thetaWhileW ∪ WbisT"
       apply - apply(erule While_transC_invert)
       unfolding thetaWhileW_def apply simp
       by (metis PL.WhileTrue PL.transC_MtransC c_d compatTst_def st tst)
     qed
   next
     show "matchT_MT (While tst c) (While tst d)"
     unfolding matchT_MT_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t s' assume st: "s ≈ t" assume "(While tst c, s) →t s'"
       thus "∃t'. (While tst d, t) →*t t' ∧ s' ≈ t' "
       apply - apply(erule While_transT_invert)
       unfolding thetaWhileW_def apply simp
       by (metis WhileFalse compatTst_def st transT_MtransT tst)       
     qed
   qed
  }
  moreover 
  {fix tst c1 d1  c d
   assume tst: "compatTst tst" and c1d1: "c1 ≈wT d1" and c_d: "c ≈wT d"
   hence matchC_MC1: "matchC_MC WbisT c1 d1" and matchC_MC: "matchC_MC WbisT c d" 
     and matchT_MT1: "matchT_MT c1 d1" and matchT_MT: "matchT_MT c d"
   using WbisT_matchC_MC WbisT_matchT_MT by auto
   have "(c1 ;; (While tst c), d1 ;; (While tst d)) ∈ WretrT (thetaWhileW Un WbisT)"
   unfolding WretrT_def proof (clarify, intro conjI)
     show "matchC_MC (thetaWhileW ∪ WbisT) (c1 ;; (While tst c)) (d1 ;; (While tst d))"
     unfolding matchC_MC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; (While tst c), s) →c (c', s')"
       thus "∃d' t'. (d1 ;; (While tst d), t) →*c (d', t') ∧ 
                     s' ≈ t' ∧ (c', d') ∈ thetaWhileW ∪ WbisT"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume "(c1, s) →c (c1', s')" and c': "c' = c1' ;; (While tst c)"
         hence "∃d' t'. (d1, t) →*c (d', t') ∧ s' ≈ t' ∧ c1' ≈wT d'" 
         using st matchC_MC1 unfolding matchC_MC_def by blast
         thus ?thesis
         unfolding c' thetaWhileW_def
         apply simp by (metis PL.Seq_MtransC c_d tst)
       next
         assume "(c1, s) →t s'" and c': "c' = While tst c"
         hence "∃t'. (d1, t) →*t t' ∧ s' ≈ t'"
         using st matchT_MT1 unfolding matchT_MT_def by auto
         thus ?thesis
         unfolding c' thetaWhileW_def 
         apply simp by (metis PL.Seq_MtransT_MtransC c_d tst)
       qed
     qed
   qed (unfold matchT_MT_def, auto)
  }
  ultimately show ?thesis unfolding thetaWhileW_def by auto
qed

lemma thetaWhileW_WbisT:
"thetaWhileW ⊆ WbisT"
apply(rule WbisT_coind)
using thetaWhileW_sym thetaWhileW_WretrT by auto

theorem While_WbisT[simp]:
assumes "compatTst tst" and "c ≈wT d"
shows "While tst c ≈wT While tst d"
using assms thetaWhileW_WbisT unfolding thetaWhileW_def by auto

text‹Parallel composition:›

definition thetaParWT where 
"thetaParWT ≡ 
 {(Par c1 c2, Par d1 d2) | c1 c2 d1 d2. c1 ≈wT d1 ∧ c2 ≈wT d2}"

lemma thetaParWT_sym:
"sym thetaParWT"
unfolding thetaParWT_def sym_def using WbisT_Sym by blast

lemma thetaParWT_WretrT:
"thetaParWT ⊆ WretrT (thetaParWT Un WbisT)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈wT d1" and c2d2: "c2 ≈wT d2"
   hence matchC_MC1: "matchC_MC WbisT c1 d1" and matchC_MC2: "matchC_MC WbisT c2 d2"
     and matchT_MT1: "matchT_MT c1 d1" and matchT_MT2: "matchT_MT c2 d2"
   using WbisT_matchC_MC WbisT_matchT_MT by auto
   have "(Par c1 c2, Par d1 d2) ∈ WretrT (thetaParWT Un WbisT)"
   unfolding WretrT_def proof (clarify, intro conjI)
     show "matchC_MC (thetaParWT ∪ WbisT) (Par c1 c2) (Par d1 d2)"
     unfolding matchC_MC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus "∃d' t'. (Par d1 d2, t) →*c (d', t') ∧ s' ≈ t' ∧ 
                     (c', d') ∈ thetaParWT ∪ WbisT"
       apply - proof(erule Par_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence "∃d' t'. (d1, t) →*c (d', t') ∧ s' ≈ t' ∧ c1' ≈wT d'"
         using st matchC_MC1 unfolding matchC_MC_def by blast
         thus ?thesis unfolding c' thetaParWT_def
         apply simp by (metis PL.ParCL_MtransC c2d2) 
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →*t t' ∧ s' ≈ t'"
         using st matchT_MT1 unfolding matchT_MT_def by blast
         thus ?thesis 
         unfolding c' thetaParWT_def
         apply simp by (metis PL.ParTL_MtransC c2d2)
       next
         fix c2' assume "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence "∃d' t'. (d2, t) →*c (d', t') ∧ s' ≈ t' ∧ c2' ≈wT d'"
         using st matchC_MC2 unfolding matchC_MC_def by blast
         thus ?thesis 
         unfolding c' thetaParWT_def
         apply simp by (metis PL.ParCR_MtransC c1d1)
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence "∃t'. (d2, t) →*t t' ∧ s' ≈ t'"
         using st matchT_MT2 unfolding matchT_MT_def by blast
         thus ?thesis 
         unfolding c' thetaParWT_def
         apply simp by (metis PL.ParTR_MtransC c1d1)
       qed
     qed 
   qed (unfold matchT_MT_def, auto)
  }
  thus ?thesis unfolding thetaParWT_def by auto
qed

lemma thetaParWT_WbisT:
"thetaParWT ⊆ WbisT"
apply(rule WbisT_coind)
using thetaParWT_sym thetaParWT_WretrT by auto

theorem Par_WbisT[simp]:
assumes "c1 ≈wT d1" and "c2 ≈wT d2"
shows "Par c1 c2 ≈wT Par d1 d2"
using assms thetaParWT_WbisT unfolding thetaParWT_def by blast


subsubsection‹T-bisimilarity versus language constructs›

text‹T-Discreetness:›

definition thetaFDW0 where 
"thetaFDW0 ≡ 
 {(c1,c2). discr0 c1 ∧ discr0 c2}"

lemma thetaFDW0_sym:
"sym thetaFDW0"
unfolding thetaFDW0_def sym_def using Sbis_Sym by blast

lemma thetaFDW0_RetrT:
"thetaFDW0 ⊆ RetrT thetaFDW0"
proof-
  {fix c d 
   assume c: "discr0 c" and d: "discr0 d"
   have "(c,d) ∈ RetrT thetaFDW0"
   unfolding RetrT_def proof (clarify, intro conjI)
     show "matchC_TMC thetaFDW0 c d"
     unfolding matchC_TMC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s' assume "mustT c s" "mustT d t" 
       "s ≈ t" and "(c, s) →c (c', s')"
       thus "∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaFDW0"
       unfolding thetaFDW0_def apply simp
       by (metis MtransC_Refl noWhile_transC c d discr0_transC discr0_transC_indis 
                 indis_sym indis_trans) 
     qed
   next
     show "matchT_TMT c d"
     unfolding matchT_TMT_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t s' assume mt: "mustT c s" "mustT d t"  
       and st: "s ≈ t" and cs: "(c, s) →t s'"
       obtain t' where dt: "(d, t) →*t t'" by (metis mt mustT_MtransT)
       hence "t ≈ t'" and "s ≈ s'" using mt cs c d discr0_transT discr0_MtransT by blast+
       hence "s' ≈ t'" using st indis_trans indis_sym by blast
       thus "∃t'. (d, t) →*t t' ∧ s' ≈ t'" using dt by blast     
     qed
   qed
  }
  thus ?thesis unfolding thetaFDW0_def by blast
qed

lemma thetaFDW0_BisT:
"thetaFDW0 ⊆ BisT"
apply(rule BisT_raw_coind)
using thetaFDW0_sym thetaFDW0_RetrT by auto

theorem discr0_BisT[simp]:
assumes "discr0 c1" and "discr0 c2"
shows "c1 ≈T c2"
using assms thetaFDW0_BisT unfolding thetaFDW0_def by blast   

text ‹Atomic commands:›

theorem Atm_BisT:
assumes "compatAtm atm" 
shows "Atm atm ≈T Atm atm"
by (metis assms siso0_Atm siso0_Sbis)

text‹Sequential composition:› 

definition thetaSeqTT where 
"thetaSeqTT ≡ 
 {(c1 ;; c2, d1 ;; d2) | c1 c2 d1 d2. c1 ≈T d1 ∧ c2 ≈T d2}"

lemma thetaSeqTT_sym:
"sym thetaSeqTT"
unfolding thetaSeqTT_def sym_def using BisT_Sym by blast

lemma thetaSeqTT_RetrT:
"thetaSeqTT ⊆ RetrT (thetaSeqTT ∪ BisT)"
proof- 
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈T d1" and c2d2: "c2 ≈T d2"
   hence matchC_TMC1: "matchC_TMC BisT c1 d1" and matchC_TMC2: "matchC_TMC BisT c2 d2"
     and matchT_TMT1: "matchT_TMT c1 d1" and matchT_T2: "matchT_TMT c2 d2"
   using BisT_matchC_TMC BisT_matchT_TMT by auto
   have "(c1 ;; c2, d1 ;; d2) ∈ RetrT (thetaSeqTT ∪ BisT)"
   unfolding RetrT_def proof (clarify, intro conjI)
     show "matchC_TMC (thetaSeqTT ∪ BisT) (c1 ;; c2) (d1 ;; d2)"
     unfolding matchC_TMC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume mt: "mustT (c1 ;; c2) s" "mustT (d1 ;; d2) t"
       and st: "s ≈ t" 
       hence mt1: "mustT c1 s" "mustT d1 t"
       by (metis mustT_Seq_L mustT_Seq_R)+
       assume 0: "(c1 ;; c2, s) →c (c', s')"
       thus "(∃d' t'. (d1 ;; d2, t) →*c (d', t') ∧ s' ≈ t' ∧ 
                      (c', d') ∈ thetaSeqTT ∪ BisT)"
       proof(elim Seq_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
         hence "∃d1' t'. (d1, t) →*c (d1', t') ∧ s' ≈ t' ∧ c1' ≈T d1'"
         using mt1 st matchC_TMC1 unfolding matchC_TMC_def by blast
         thus ?thesis unfolding c' thetaSeqTT_def
         apply simp by (metis Seq_MtransC c2d2) 
       next      
         assume c1: "(c1, s) →t s'" and c': "c' = c2"
         then obtain t' where d1: "(d1, t) →*t t'" and s't': "s' ≈ t'"
         using mt1 st matchT_TMT1 unfolding matchT_TMT_def by blast
         hence mt1: "mustT c2 s'" "mustT d2 t'"
         apply (metis 0 c' mt mustT_transC)
         by (metis mustT_Seq_R d1 mt(2))
         thus ?thesis 
         unfolding c' thetaSeqTT_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp by (metis Seq_MtransT_MtransC c2d2 d1 s't') 
       qed
     qed 
   qed (unfold matchT_TMT_def, auto)
  }
  thus ?thesis unfolding thetaSeqTT_def by auto
qed

lemma thetaSeqTT_BisT:
"thetaSeqTT ⊆ BisT"
apply(rule BisT_coind)
using thetaSeqTT_sym thetaSeqTT_RetrT by auto

theorem Seq_BisT[simp]:
assumes "c1 ≈T d1" and "c2 ≈T d2"
shows "c1 ;; c2 ≈T d1 ;; d2"
using assms thetaSeqTT_BisT unfolding thetaSeqTT_def by blast 

text‹Conditional:›

definition thetaIfTT where 
"thetaIfTT ≡ 
 {(If tst c1 c2, If tst d1 d2) | tst c1 c2 d1 d2. compatTst tst ∧ c1 ≈T d1 ∧ c2 ≈T d2}"

lemma thetaIfTT_sym:
"sym thetaIfTT"
unfolding thetaIfTT_def sym_def using BisT_Sym by blast

lemma thetaIfTT_RetrT:
"thetaIfTT ⊆ RetrT (thetaIfTT ∪ BisT)"
proof- 
  {fix tst c1 c2 d1 d2
   assume tst: "compatTst tst" and c1d1: "c1 ≈T d1" and c2d2: "c2 ≈T d2"
   hence matchC_TMC1: "matchC_TMC BisT c1 d1" and matchC_TMC2: "matchC_TMC BisT c2 d2"
     and matchT_TMT1: "matchT_TMT c1 d1" and matchT_TMT2: "matchT_TMT c2 d2"
   using BisT_matchC_TMC BisT_matchT_TMT by auto
   have "(If tst c1 c2, If tst d1 d2) ∈ RetrT (thetaIfTT ∪ BisT)"
   unfolding RetrT_def proof (clarify, intro conjI)
     show "matchC_TMC (thetaIfTT ∪ BisT) (If tst c1 c2) (If tst d1 d2)"
     unfolding matchC_TMC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(If tst c1 c2, s) →c (c', s')"
       thus "∃d' t'. (If tst d1 d2, t) →*c (d', t') ∧ s' ≈ t' ∧ 
                     (c', d') ∈ thetaIfTT ∪ BisT"
       apply - apply(erule If_transC_invert)
       unfolding thetaIfTT_def 
       apply simp apply (metis IfTrue c1d1 compatTst_def st transC_MtransC tst) 
       apply simp by (metis IfFalse c2d2 compatTst_def st transC_MtransC tst) 
     qed
   qed (unfold matchT_TMT_def, auto)
  }
  thus ?thesis unfolding thetaIfTT_def by auto
qed

lemma thetaIfTT_BisT:
"thetaIfTT ⊆ BisT"
apply(rule BisT_coind)
using thetaIfTT_sym thetaIfTT_RetrT by auto

theorem If_BisT[simp]:
assumes "compatTst tst" and "c1 ≈T d1" and "c2 ≈T d2"
shows "If tst c1 c2 ≈T If tst d1 d2"
using assms thetaIfTT_BisT unfolding thetaIfTT_def by blast

text‹While loop:›

definition thetaWhileW0 where 
"thetaWhileW0 ≡ 
 {(While tst c, While tst d) | tst c d. compatTst tst ∧ c ≈T d} ∪ 
 {(c1 ;; (While tst c), d1 ;; (While tst d)) | tst c1 d1 c d. 
               compatTst tst ∧ c1 ≈T d1 ∧ c ≈T d}"

lemma thetaWhileW0_sym:
"sym thetaWhileW0"
unfolding thetaWhileW0_def sym_def using BisT_Sym by blast

lemma thetaWhileW0_RetrT:
"thetaWhileW0 ⊆ RetrT (thetaWhileW0 ∪ BisT)"
proof-
  {fix tst c d 
   assume tst: "compatTst tst" and c_d: "c ≈T d"
   hence matchC_TMC: "matchC_TMC BisT c d" 
     and matchT_TMT: "matchT_TMT c d" 
   using BisT_matchC_TMC BisT_matchT_TMT by auto
   have "(While tst c, While tst d) ∈ RetrT (thetaWhileW0 ∪ BisT)"
   unfolding RetrT_def proof (clarify, intro conjI)
     show "matchC_TMC (thetaWhileW0 ∪ BisT) (While tst c) (While tst d)"
     unfolding matchC_TMC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(While tst c, s) →c (c', s')"
       thus "∃d' t'. (While tst d, t) →*c (d', t') ∧ s' ≈ t' ∧ 
                     (c', d') ∈ thetaWhileW0 ∪ BisT"
       apply - apply(erule While_transC_invert)
       unfolding thetaWhileW0_def apply simp
       by (metis WhileTrue transC_MtransC c_d compatTst_def st tst)
     qed
   next
     show "matchT_TMT (While tst c) (While tst d)"
     unfolding matchT_TMT_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t s' assume st: "s ≈ t" assume "(While tst c, s) →t s'"
       thus "∃t'. (While tst d, t) →*t t' ∧ s' ≈ t' "
       apply - apply(erule While_transT_invert)
       unfolding thetaWhileW0_def apply simp
       by (metis WhileFalse compatTst_def st transT_MtransT tst)       
     qed
   qed
  }
  moreover 
  {fix tst c1 d1  c d
   assume tst: "compatTst tst" and c1d1: "c1 ≈T d1" and c_d: "c ≈T d"
   hence matchC_TMC1: "matchC_TMC BisT c1 d1" and matchC_TMC: "matchC_TMC BisT c d" 
     and matchT_TMT1: "matchT_TMT c1 d1" and matchT_TMT: "matchT_TMT c d"
   using BisT_matchC_TMC BisT_matchT_TMT by auto
   have "(c1 ;; (While tst c), d1 ;; (While tst d)) ∈ RetrT (thetaWhileW0 ∪ BisT)"
   unfolding RetrT_def proof (clarify, intro conjI)
     show "matchC_TMC (thetaWhileW0 ∪ BisT) (c1 ;; (While tst c)) (d1 ;; (While tst d))"
     unfolding matchC_TMC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume mt: "mustT (c1 ;; While tst c) s" "mustT (d1 ;; While tst d) t"
       and st: "s ≈ t" 
       hence mt1: "mustT c1 s" "mustT d1 t"
       by (metis mustT_Seq_L mustT_Seq_R)+     
       assume 0: "(c1 ;; (While tst c), s) →c (c', s')"
       thus "∃d' t'. (d1 ;; (While tst d), t) →*c (d', t') ∧ 
                     s' ≈ t' ∧ (c', d') ∈ thetaWhileW0 ∪ BisT"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume "(c1, s) →c (c1', s')" and c': "c' = c1' ;; (While tst c)"
         hence "∃d' t'. (d1, t) →*c (d', t') ∧ s' ≈ t' ∧ c1' ≈T d'" 
         using mt1 st matchC_TMC1 unfolding matchC_TMC_def by blast
         thus ?thesis
         unfolding c' thetaWhileW0_def
         apply simp by (metis Seq_MtransC c_d tst)
       next
         assume "(c1, s) →t s'" and c': "c' = While tst c"
         then obtain t' where "(d1, t) →*t t' ∧ s' ≈ t'"
         using mt1 st matchT_TMT1 unfolding matchT_TMT_def by metis
         thus ?thesis
         unfolding c' thetaWhileW0_def 
         apply simp by (metis Seq_MtransT_MtransC c_d tst)
       qed
     qed
   qed (unfold matchT_TMT_def, auto)
  }
  ultimately show ?thesis unfolding thetaWhileW0_def by auto
qed

lemma thetaWhileW0_BisT:
"thetaWhileW0 ⊆ BisT"
apply(rule BisT_coind)
using thetaWhileW0_sym thetaWhileW0_RetrT by auto

theorem While_BisT[simp]:
assumes "compatTst tst" and "c ≈T d"
shows "While tst c ≈T While tst d"
using assms thetaWhileW0_BisT unfolding thetaWhileW0_def by auto

text‹Parallel composition:›

definition thetaParTT where 
"thetaParTT ≡ 
 {(Par c1 c2, Par d1 d2) | c1 c2 d1 d2. c1 ≈T d1 ∧ c2 ≈T d2}"

lemma thetaParTT_sym:
"sym thetaParTT"
unfolding thetaParTT_def sym_def using BisT_Sym by blast

lemma thetaParTT_RetrT:
"thetaParTT ⊆ RetrT (thetaParTT ∪ BisT)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈T d1" and c2d2: "c2 ≈T d2"
   hence matchC_TMC1: "matchC_TMC BisT c1 d1" and matchC_TMC2: "matchC_TMC BisT c2 d2"
     and matchT_TMT1: "matchT_TMT c1 d1" and matchT_TMT2: "matchT_TMT c2 d2"
   using BisT_matchC_TMC BisT_matchT_TMT by auto
   have "(Par c1 c2, Par d1 d2) ∈ RetrT (thetaParTT ∪ BisT)"
   unfolding RetrT_def proof (clarify, intro conjI)
     show "matchC_TMC (thetaParTT ∪ BisT) (Par c1 c2) (Par d1 d2)"
     unfolding matchC_TMC_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume "mustT (Par c1 c2) s" and "mustT (Par d1 d2) t"
       and st: "s ≈ t" 
       hence mt: "mustT c1 s" "mustT c2 s"
                 "mustT d1 t" "mustT d2 t"
       by (metis mustT_Par_L mustT_Par_R)+        
       assume "(Par c1 c2, s) →c (c', s')"
       thus "∃d' t'. (Par d1 d2, t) →*c (d', t') ∧ s' ≈ t' ∧ 
                     (c', d') ∈ thetaParTT ∪ BisT"
       proof(elim Par_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence "∃d' t'. (d1, t) →*c (d', t') ∧ s' ≈ t' ∧ c1' ≈T d'"
         using mt st matchC_TMC1 unfolding matchC_TMC_def by blast
         thus ?thesis unfolding c' thetaParTT_def
         apply simp by (metis ParCL_MtransC c2d2) 
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →*t t' ∧ s' ≈ t'"
         using mt st matchT_TMT1 unfolding matchT_TMT_def by blast
         thus ?thesis 
         unfolding c' thetaParTT_def
         apply simp by (metis PL.ParTL_MtransC c2d2)
       next
         fix c2' assume "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence "∃d' t'. (d2, t) →*c (d', t') ∧ s' ≈ t' ∧ c2' ≈T d'"
         using mt st matchC_TMC2 unfolding matchC_TMC_def by blast
         thus ?thesis 
         unfolding c' thetaParTT_def
         apply simp by (metis PL.ParCR_MtransC c1d1)
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence "∃t'. (d2, t) →*t t' ∧ s' ≈ t'"
         using mt st matchT_TMT2 unfolding matchT_TMT_def by blast
         thus ?thesis 
         unfolding c' thetaParTT_def
         apply simp by (metis PL.ParTR_MtransC c1d1)
       qed
     qed 
   qed (unfold matchT_TMT_def, auto)
  }
  thus ?thesis unfolding thetaParTT_def by auto
qed

lemma thetaParTT_BisT:
"thetaParTT ⊆ BisT"
apply(rule BisT_coind)
using thetaParTT_sym thetaParTT_RetrT by auto

theorem Par_BisT[simp]:
assumes "c1 ≈T d1" and "c2 ≈T d2"
shows "Par c1 c2 ≈T Par d1 d2"
using assms thetaParTT_BisT unfolding thetaParTT_def by blast


subsubsection‹W-bisimilarity versus language constructs›

text ‹Atomic commands:›

theorem Atm_Wbis[simp]:
assumes "compatAtm atm" 
shows "Atm atm ≈w Atm atm"
by (metis Atm_Sbis assms bis_imp)

text‹Discreetness:›

theorem discr_Wbis[simp]:
assumes *: "discr c" and **: "discr d"
shows "c ≈w d"
by (metis * ** bis_imp(4) discr_ZObis)

text‹Sequential composition:›

definition thetaSeqW where 
"thetaSeqW ≡ 
 {(c1 ;; c2, d1 ;; d2) | c1 c2 d1 d2. c1 ≈wT d1 ∧ c2 ≈w d2}"

lemma thetaSeqW_sym:
"sym thetaSeqW"
unfolding thetaSeqW_def sym_def using WbisT_Sym Wbis_Sym by blast

lemma thetaSeqW_Wretr:
"thetaSeqW ⊆ Wretr (thetaSeqW ∪ Wbis)"
proof- 
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈wT d1" and c2d2: "c2 ≈w d2"
   hence matchC_MC1: "matchC_MC WbisT c1 d1" and matchC_W2: "matchC_M Wbis c2 d2"
     and matchT_MT1: "matchT_MT c1 d1" and matchT_M2: "matchT_M c2 d2" 
   using WbisT_matchC_MC WbisT_matchT_MT Wbis_matchC_M Wbis_matchT_M by auto
   have "(c1 ;; c2, d1 ;; d2) ∈ Wretr (thetaSeqW ∪ Wbis)"
   unfolding Wretr_def proof (clarify, intro conjI)
     show "matchC_M (thetaSeqW ∪ Wbis) (c1 ;; c2) (d1 ;; d2)"
     unfolding matchC_M_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; c2, s) →c (c', s')"
       thus 
       "(∃d' t'. (d1 ;; d2, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaSeqW ∪ Wbis) ∨ 
        (∃t'. (d1 ;; d2, t) →*t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
         hence "∃d1' t'. (d1, t) →*c (d1', t') ∧ s' ≈ t' ∧ c1' ≈wT d1'"
         using st matchC_MC1 unfolding matchC_MC_def by blast
         thus ?thesis unfolding c' thetaSeqW_def
         apply simp by (metis PL.Seq_MtransC c2d2)
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "∃t'. (d1, t) →*t t' ∧ s' ≈ t'"
         using st matchT_MT1 unfolding matchT_MT_def by auto
         thus ?thesis 
         unfolding c' thetaSeqW_def
         apply simp by (metis PL.Seq_MtransT_MtransC c2d2) 
       qed
     qed 
   qed (unfold matchT_M_def, auto)
  }
  thus ?thesis unfolding thetaSeqW_def by auto
qed

lemma thetaSeqW_Wbis:
"thetaSeqW ⊆ Wbis"
apply(rule Wbis_coind)
using thetaSeqW_sym thetaSeqW_Wretr by auto

theorem Seq_WbisT_Wbis[simp]:
assumes "c1 ≈wT d1" and "c2 ≈w d2"
shows "c1 ;; c2 ≈w d1 ;; d2"
using assms thetaSeqW_Wbis unfolding thetaSeqW_def by blast

theorem Seq_siso_Wbis[simp]:
assumes "siso e" and "c2 ≈w d2"
shows "e ;; c2 ≈w e ;; d2"
using assms by auto

(*  *)

definition thetaSeqWD where 
"thetaSeqWD ≡ 
 {(c1 ;; c2, d1 ;; d2) | c1 c2 d1 d2. c1 ≈w d1 ∧ discr c2 ∧ discr d2}"

lemma thetaSeqWD_sym:
"sym thetaSeqWD"
unfolding thetaSeqWD_def sym_def using Wbis_Sym by blast

lemma thetaSeqWD_Wretr:
"thetaSeqWD ⊆ Wretr (thetaSeqWD ∪ Wbis)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈w d1" and c2: "discr c2" and d2: "discr d2"
   hence matchC_M: "matchC_M Wbis c1 d1" 
     and matchT_M: "matchT_M c1 d1"
   using Wbis_matchC_M Wbis_matchT_M by auto
   have "(c1 ;; c2, d1 ;; d2) ∈ Wretr (thetaSeqWD ∪ Wbis)"
   unfolding Wretr_def proof (clarify, intro conjI)
     show "matchC_M (thetaSeqWD ∪ Wbis) (c1 ;; c2) (d1 ;; d2)"
     unfolding matchC_M_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(c1 ;; c2, s) →c (c', s')"
       thus 
       "(∃d' t'. (d1 ;; d2, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaSeqWD ∪ Wbis) ∨ 
        (∃t'. (d1 ;; d2, t) →*t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Seq_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = c1' ;; c2"
         hence
         "(∃d' t'. (d1, t) →*c (d', t') ∧ s' ≈ t' ∧ c1' ≈w d') ∨ 
          (∃t'. (d1, t) →*t t' ∧ s' ≈ t' ∧ discr c1')"
         using st matchC_M unfolding matchC_M_def by blast
         thus ?thesis unfolding c' thetaSeqWD_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis PL.Seq_MtransC c2 d2)
         apply simp by (metis PL.Seq_MtransT_MtransC c2 d2 discr_Seq discr_Wbis)
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence 
         "(∃d' t'. (d1, t) →*c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d1, t) →*t t' ∧ s' ≈ t')"
         using st matchT_M unfolding matchT_M_def by blast
         thus ?thesis 
         unfolding c' thetaSeqWD_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis PL.Seq_MtransC c2 d2 discr_Seq discr_Wbis)
         apply simp by (metis PL.Seq_MtransT_MtransC c2 d2 discr_Wbis)
       qed
     qed 
   qed (unfold matchT_M_def, auto)
  }
  thus ?thesis unfolding thetaSeqWD_def by auto
qed

lemma thetaSeqWD_Wbis:
"thetaSeqWD ⊆ Wbis"
apply(rule Wbis_coind)
using thetaSeqWD_sym thetaSeqWD_Wretr by auto

theorem Seq_Wbis_discr[simp]:
assumes "c1 ≈w d1" and "discr c2" and "discr d2"
shows "c1 ;; c2 ≈w d1 ;; d2"
using assms thetaSeqWD_Wbis unfolding thetaSeqWD_def by blast

text‹Conditional:›

definition thetaIfW where 
"thetaIfW ≡ 
 {(If tst c1 c2, If tst d1 d2) | tst c1 c2 d1 d2. compatTst tst ∧ c1 ≈w d1 ∧ c2 ≈w d2}"

lemma thetaIfW_sym:
"sym thetaIfW"
unfolding thetaIfW_def sym_def using Wbis_Sym by blast

lemma thetaIfW_Wretr:
"thetaIfW ⊆ Wretr (thetaIfW ∪ Wbis)"
proof-
  {fix tst c1 c2 d1 d2
   assume tst: "compatTst tst" and c1d1: "c1 ≈w d1" and c2d2: "c2 ≈w d2"
   hence matchC_M1: "matchC_M Wbis c1 d1" and matchC_M2: "matchC_M Wbis c2 d2"
     and matchT_M1: "matchT_M c1 d1" and matchT_M2: "matchT_M c2 d2"
   using Wbis_matchC_M Wbis_matchT_M by auto
   have "(If tst c1 c2, If tst d1 d2) ∈ Wretr (thetaIfW ∪ Wbis)"
   unfolding Wretr_def proof (clarify, intro conjI)
     show "matchC_M (thetaIfW ∪ Wbis) (If tst c1 c2) (If tst d1 d2)"
     unfolding matchC_M_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(If tst c1 c2, s) →c (c', s')"
       thus 
       "(∃d' t'. (If tst d1 d2, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaIfW ∪ Wbis) ∨ 
        (∃t'. (If tst d1 d2, t) →*t t' ∧ s' ≈ t' ∧ discr c')"
       apply - apply(erule If_transC_invert)
       unfolding thetaIfW_def 
       apply simp apply (metis IfTrue c1d1 compatTst_def st transC_MtransC tst)
       apply simp by (metis IfFalse c2d2 compatTst_def st transC_MtransC tst)
     qed
   qed (unfold matchT_M_def, auto)
  }
  thus ?thesis unfolding thetaIfW_def by auto
qed

lemma thetaIfW_Wbis:
"thetaIfW ⊆ Wbis"
apply(rule Wbis_coind)
using thetaIfW_sym thetaIfW_Wretr by auto

theorem If_Wbis[simp]:
assumes "compatTst tst" and "c1 ≈w d1" and "c2 ≈w d2"
shows "If tst c1 c2 ≈w If tst d1 d2"
using assms thetaIfW_Wbis unfolding thetaIfW_def by blast

text‹While loop:›

text‹Again, w-bisimilarity does not interact with / preserve the While construct in 
any interesting way.›

text‹Parallel composition:›

definition thetaParWL1 where 
"thetaParWL1 ≡ 
 {(Par c1 c2, d) | c1 c2 d. c1 ≈w d ∧ discr c2}"

lemma thetaParWL1_Wretr:
"thetaParWL1 ⊆ Wretr (thetaParWL1 ∪ Wbis)"
proof-
  {fix c1 c2 d
   assume c1d: "c1 ≈w d" and c2: "discr c2"
   hence matchC_M: "matchC_M Wbis c1 d" 
     and matchT_M: "matchT_M c1 d" 
   using Wbis_matchC_M Wbis_matchT_M by auto
   have "(Par c1 c2, d) ∈ Wretr (thetaParWL1 ∪ Wbis)"
   unfolding Wretr_def proof (clarify, intro conjI)
     show "matchC_M (thetaParWL1 ∪ Wbis) (Par c1 c2) d"
     unfolding matchC_M_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus
       "(∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParWL1 ∪ Wbis) ∨
        (∃t'. (d, t) →*t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Par_transC_invert)
         fix c1' assume "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence 
         "(∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ c1' ≈w d') ∨ 
          (∃t'. (d, t) →*t t' ∧ s' ≈ t' ∧ discr c1')"
         using st matchC_M unfolding matchC_M_def by blast
         thus ?thesis unfolding thetaParWL1_def
         apply - apply(elim disjE exE conjE) 
         apply simp apply (metis c2 c')
         apply simp by (metis c' c2 discr_Par) 
       next
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence 
         "(∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d, t) →*t t' ∧ s' ≈ t')"
         using st matchT_M unfolding matchT_M_def by blast
         thus ?thesis unfolding thetaParWL1_def
         apply - apply(elim disjE exE conjE)
         apply simp apply (metis c' c2 discr_Wbis)
         apply simp by (metis c' c2)  
       next
         fix c2' assume c2s: "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence "s ≈ s'" using c2 discr_transC_indis by blast
         hence s't: "s' ≈ t" using st indis_sym indis_trans by blast
         have "discr c2'" using c2 c2s discr_transC by blast
         thus ?thesis using s't c1d unfolding thetaParWL1_def c' by auto
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence "s ≈ s'" using c2 discr_transT by blast
         hence s't: "s' ≈ t" using st indis_sym indis_trans by blast
         thus ?thesis using c1d unfolding thetaParWL1_def c' by auto
       qed
     qed
   qed (unfold matchT_M_def, auto)
  }
  thus ?thesis unfolding thetaParWL1_def by blast
qed

lemma thetaParWL1_converse_Wretr:
"thetaParWL1 ^-1 ⊆ Wretr (thetaParWL1 ^-1 ∪ Wbis)"
proof-
  {fix c1 c2 d
   assume c1d: "c1 ≈w d" and c2: "discr c2"
   hence matchC_M: "matchC_M Wbis d c1" 
     and matchT_M: "matchT_M d c1" 
   using Wbis_matchC_M_rev Wbis_matchT_M_rev by auto
   have "(d, Par c1 c2) ∈ Wretr (thetaParWL1¯ ∪ Wbis)"
   unfolding Wretr_def proof (clarify, intro conjI)
     show "matchC_M (thetaParWL1¯ ∪ Wbis) d (Par c1 c2)"
     unfolding matchC_M_def2 Wbis_converse proof (tactic ‹mauto_no_simp_tac @{context}›) 
       fix s t d' t'
       assume "s ≈ t" and "(d, t) →c (d', t')"
       hence 
       "(∃c' s'. (c1, s) →*c (c', s') ∧ s' ≈ t' ∧ d' ≈w c') ∨ 
        (∃s'. (c1, s) →*t s' ∧ s' ≈ t' ∧ discr d')"
       using matchC_M unfolding matchC_M_def2 by blast
       thus
       "(∃c' s'. (Par c1 c2, s) →*c (c', s') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParWL1 ∪ Wbis) ∨
        (∃s'. (Par c1 c2, s) →*t s' ∧ s' ≈ t' ∧ discr d')"
       unfolding thetaParWL1_def 
       apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
       apply simp apply (metis PL.ParCL_MtransC Wbis_Sym c2)
       apply simp by (metis PL.ParTL_MtransC c2 discr_Wbis)
     qed
   next
     show "matchT_M d (Par c1 c2)"
     unfolding matchT_M_def2 Wbis_converse proof (tactic ‹mauto_no_simp_tac @{context}›) 
       fix s t t'
       assume "s ≈ t" and "(d, t) →t t'"
       hence 
       "(∃c' s'. (c1, s) →*c (c', s') ∧ s' ≈ t' ∧ discr c') ∨ 
        (∃s'. (c1, s) →*t s' ∧ s' ≈ t')"
       using matchT_M unfolding matchT_M_def2 by blast
       thus
       "(∃c' s'. (Par c1 c2, s) →*c (c', s') ∧ s' ≈ t' ∧ discr c') ∨ 
        (∃s'. (Par c1 c2, s) →*t s' ∧ s' ≈ t')"
       apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
       apply (metis PL.ParCL_MtransC c2 discr_Par)
       by (metis PL.ParTL_MtransC c2)  
     qed
   qed
  }
  thus ?thesis unfolding thetaParWL1_def by blast
qed

lemma thetaParWL1_Wbis:
"thetaParWL1 ⊆ Wbis"
apply(rule Wbis_coind2)
using thetaParWL1_Wretr thetaParWL1_converse_Wretr by auto

theorem Par_Wbis_discrL1[simp]:
assumes "c1 ≈w d" and "discr c2"
shows "Par c1 c2 ≈w d"
using assms thetaParWL1_Wbis unfolding thetaParWL1_def by blast

theorem Par_Wbis_discrR1[simp]:
assumes "c ≈w d1" and "discr d2"
shows "c ≈w Par d1 d2"
using assms Par_Wbis_discrL1 Wbis_Sym by blast

(*  *)

definition thetaParWL2 where 
"thetaParWL2 ≡ 
 {(Par c1 c2, d) | c1 c2 d. discr c1 ∧ c2 ≈w d}"

lemma thetaParWL2_Wretr:
"thetaParWL2 ⊆ Wretr (thetaParWL2 ∪ Wbis)"
proof-
  {fix c1 c2 d
   assume c2d: "c2 ≈w d" and c1: "discr c1" 
   hence matchC_M: "matchC_M Wbis c2 d" 
     and matchT_M: "matchT_M c2 d" 
   using Wbis_matchC_M Wbis_matchT_M by auto
   have "(Par c1 c2, d) ∈ Wretr (thetaParWL2 ∪ Wbis)"
   unfolding Wretr_def proof (clarify, intro conjI)
     show "matchC_M (thetaParWL2 ∪ Wbis) (Par c1 c2) d"
     unfolding matchC_M_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus
       "(∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParWL2 ∪ Wbis) ∨
        (∃t'. (d, t) →*t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Par_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence "s ≈ s'" using c1 discr_transC_indis by blast
         hence s't: "s' ≈ t" using st indis_sym indis_trans by blast
         have "discr c1'" using c1 c1s discr_transC by blast
         thus ?thesis using s't c2d unfolding thetaParWL2_def c' by auto
       next
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence "s ≈ s'" using c1 discr_transT by blast
         hence s't: "s' ≈ t" using st indis_sym indis_trans by blast
         thus ?thesis using c2d unfolding thetaParWL2_def c' by auto
       next
         fix c2' assume "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence 
         "(∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ c2' ≈w d') ∨ 
          (∃t'. (d, t) →*t t' ∧ s' ≈ t' ∧ discr c2')"
         using st matchC_M unfolding matchC_M_def by blast
         thus ?thesis unfolding thetaParWL2_def
         apply - apply(elim disjE exE conjE) 
         apply simp apply (metis c1 c')
         apply simp by (metis c' c1 discr_Par) 
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence 
         "(∃d' t'. (d, t) →*c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d, t) →*t t' ∧ s' ≈ t')"
         using st matchT_M unfolding matchT_M_def by blast
         thus ?thesis unfolding thetaParWL2_def
         apply - apply(elim disjE exE conjE)
         apply simp apply (metis c' c1 discr_Wbis)
         apply simp by (metis c' c1)          
       qed
     qed
   qed (unfold matchT_M_def, auto)
  }
  thus ?thesis unfolding thetaParWL2_def by blast
qed

lemma thetaParWL2_converse_Wretr:
"thetaParWL2 ^-1 ⊆ Wretr (thetaParWL2 ^-1 ∪ Wbis)"
proof-
  {fix c1 c2 d
   assume c2d: "c2 ≈w d" and c1: "discr c1"
   hence matchC_M: "matchC_M Wbis d c2" 
     and matchT_M: "matchT_M d c2" 
   using Wbis_matchC_M_rev Wbis_matchT_M_rev by auto
   have "(d, Par c1 c2) ∈ Wretr (thetaParWL2¯ ∪ Wbis)"
   unfolding Wretr_def proof (clarify, intro conjI)
     show "matchC_M (thetaParWL2¯ ∪ Wbis) d (Par c1 c2)"
     unfolding matchC_M_def2 Wbis_converse proof (tactic ‹mauto_no_simp_tac @{context}›) 
       fix s t d' t'
       assume "s ≈ t" and "(d, t) →c (d', t')"
       hence 
       "(∃c' s'. (c2, s) →*c (c', s') ∧ s' ≈ t' ∧ d' ≈w c') ∨ 
        (∃s'. (c2, s) →*t s' ∧ s' ≈ t' ∧ discr d')"
       using matchC_M unfolding matchC_M_def2 by blast
       thus
       "(∃c' s'. (Par c1 c2, s) →*c (c', s') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParWL2 ∪ Wbis) ∨
        (∃s'. (Par c1 c2, s) →*t s' ∧ s' ≈ t' ∧ discr d')"
       unfolding thetaParWL2_def 
       apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
       apply simp apply (metis PL.ParCR_MtransC Wbis_Sym c1)
       apply simp by (metis PL.ParTR_MtransC c1 discr_Wbis) 
     qed
   next
     show "matchT_M d (Par c1 c2)"
     unfolding matchT_M_def2 Wbis_converse proof (tactic ‹mauto_no_simp_tac @{context}›) 
       fix s t t'
       assume "s ≈ t" and "(d, t) →t t'"
       hence 
       "(∃c' s'. (c2, s) →*c (c', s') ∧ s' ≈ t' ∧ discr c') ∨ 
        (∃s'. (c2, s) →*t s' ∧ s' ≈ t')"
       using matchT_M unfolding matchT_M_def2 by blast
       thus
       "(∃c' s'. (Par c1 c2, s) →*c (c', s') ∧ s' ≈ t' ∧ discr c') ∨ 
        (∃s'. (Par c1 c2, s) →*t s' ∧ s' ≈ t')"
       apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
       apply (metis PL.ParCR_MtransC c1 discr_Par)
       by (metis PL.ParTR_MtransC c1)
     qed
   qed
  }
  thus ?thesis unfolding thetaParWL2_def by blast
qed

lemma thetaParWL2_Wbis:
"thetaParWL2 ⊆ Wbis"
apply(rule Wbis_coind2)
using thetaParWL2_Wretr thetaParWL2_converse_Wretr by auto

theorem Par_Wbis_discrL2[simp]:
assumes "c2 ≈w d" and "discr c1"
shows "Par c1 c2 ≈w d"
using assms thetaParWL2_Wbis unfolding thetaParWL2_def by blast

theorem Par_Wbis_discrR2[simp]:
assumes "c ≈w d2" and "discr d1"
shows "c ≈w Par d1 d2"
using assms Par_Wbis_discrL2 Wbis_Sym by blast

(*  *)

definition thetaParW where 
"thetaParW ≡ 
 {(Par c1 c2, Par d1 d2) | c1 c2 d1 d2. c1 ≈w d1 ∧ c2 ≈w d2}"

lemma thetaParW_sym:
"sym thetaParW"
unfolding thetaParW_def sym_def using Wbis_Sym by blast

lemma thetaParW_Wretr:
"thetaParW ⊆ Wretr (thetaParW ∪ Wbis)"
proof-
  {fix c1 c2 d1 d2
   assume c1d1: "c1 ≈w d1" and c2d2: "c2 ≈w d2"
   hence matchC_M1: "matchC_M Wbis c1 d1" and matchC_M2: "matchC_M Wbis c2 d2"
     and matchT_M1: "matchT_M c1 d1" and matchT_M2: "matchT_M c2 d2"
   using Wbis_matchC_M Wbis_matchT_M by auto
   have "(Par c1 c2, Par d1 d2) ∈ Wretr (thetaParW ∪ Wbis)"
   unfolding Wretr_def proof (clarify, intro conjI)
     show "matchC_M (thetaParW ∪ Wbis) (Par c1 c2) (Par d1 d2)"
     unfolding matchC_M_def proof (tactic ‹mauto_no_simp_tac @{context}›)
       fix s t c' s'
       assume st: "s ≈ t" assume "(Par c1 c2, s) →c (c', s')"
       thus 
       "(∃d' t'. (Par d1 d2, t) →*c (d', t') ∧ s' ≈ t' ∧ (c', d') ∈ thetaParW ∪ Wbis) ∨ 
        (∃t'. (Par d1 d2, t) →*t t' ∧ s' ≈ t' ∧ discr c')"
       apply - proof(erule Par_transC_invert)
         fix c1' assume c1s: "(c1, s) →c (c1', s')" and c': "c' = Par c1' c2"
         hence
         "(∃d' t'. (d1, t) →*c (d', t') ∧ s' ≈ t' ∧ c1' ≈w d') ∨ 
          (∃t'. (d1, t) →*t t' ∧ s' ≈ t' ∧ discr c1')"
         using st matchC_M1 unfolding matchC_M_def by blast
         thus ?thesis unfolding c' thetaParW_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis PL.ParCL_MtransC c2d2) 
         apply simp by (metis PL.ParTL_MtransC Par_Wbis_discrL2 c2d2)
       next      
         assume "(c1, s) →t s'" and c': "c' = c2"
         hence 
         "(∃d' t'. (d1, t) →*c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d1, t) →*t t' ∧ s' ≈ t')"
         using st matchT_M1 unfolding matchT_M_def by blast
         thus ?thesis 
         unfolding c' thetaParW_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis PL.ParCL_MtransC Par_Wbis_discrR2 c2d2)
         apply simp by (metis PL.ParTL_MtransC c2d2) 
       next
         fix c2' assume "(c2, s) →c (c2', s')" and c': "c' = Par c1 c2'"
         hence 
         "(∃d' t'. (d2, t) →*c (d', t') ∧ s' ≈ t' ∧ c2' ≈w d') ∨ 
          (∃t'. (d2, t) →*t t' ∧ s' ≈ t' ∧ discr c2')"
         using st matchC_M2 unfolding matchC_M_def by blast
         thus ?thesis 
         unfolding c' thetaParW_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis PL.ParCR_MtransC c1d1)
         apply simp by (metis PL.ParTR_MtransC Par_Wbis_discrL1 c1d1) 
       next
         assume "(c2, s) →t s'" and c': "c' = c1"
         hence 
         "(∃d' t'. (d2, t) →*c (d', t') ∧ s' ≈ t' ∧ discr d') ∨ 
          (∃t'. (d2, t) →*t t' ∧ s' ≈ t')"
         using st matchT_M2 unfolding matchT_M_def by blast
         thus ?thesis 
         unfolding c' thetaParW_def
         apply - apply(tactic ‹mauto_no_simp_tac @{context}›)
         apply simp apply (metis PL.ParCR_MtransC Par_Wbis_discrR1 c1d1) 
         apply simp by (metis PL.ParTR_MtransC c1d1)
       qed
     qed 
   qed (unfold matchT_M_def, auto)
  }
  thus ?thesis unfolding thetaParW_def by auto
qed

lemma thetaParW_Wbis:
"thetaParW ⊆ Wbis"
apply(rule Wbis_coind)
using thetaParW_sym thetaParW_Wretr by auto

theorem Par_Wbis[simp]:
assumes "c1 ≈w d1" and "c2 ≈w d2"
shows "Par c1 c2 ≈w Par d1 d2"
using assms thetaParW_Wbis unfolding thetaParW_def by blast

end (* context PL_Indis *)
(*******************************************)


end