# 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 ```