# Theory Compositionality

```section ‹Compositionality of Resumption-Based Noninterference›

theory Compositionality
imports Resumption_Based
begin

(* The results corresponding to the paper's Prop. 2 are marked below with "theorem". *)

context PL_Indis
begin

subsection‹Compatibility and discreetness of atoms, tests and choices›

definition compatAtm where
"compatAtm atm ≡
ALL s t. s ≈ t ⟶ aval atm s ≈ aval atm t"

definition presAtm where
"presAtm atm ≡
ALL s. s ≈ aval atm s"

definition compatTst where
"compatTst tst ≡
ALL s t. s ≈ t ⟶ tval tst s = tval tst t"

lemma discrAt_compatAt[simp]:
assumes "presAtm atm"
shows "compatAtm atm"
using assms unfolding compatAtm_def
by (metis presAtm_def indis_sym indis_trans)

definition compatCh where
"compatCh ch ≡ ∀ s t. s ≈ t ⟶ cval ch s = cval ch t"

lemma compatCh_cval[simp]:
assumes "compatCh ch" and "s ≈ t"
shows " cval ch s = cval ch t"
using assms unfolding compatCh_def by auto

subsection‹Compositionality of self-isomorphism›

text‹Self-Isomorphism versus language constructs:›

lemma siso_Done[simp]:
"siso Done"
proof-
{fix c :: "('test, 'atom, 'choice) cmd"
assume "c = Done" hence "siso c"
apply induct by auto
}
thus ?thesis by blast
qed

lemma siso_Atm[simp]:
"siso (Atm atm) = compatAtm atm"
proof-
{fix c :: "('test, 'atom, 'choice) cmd"
assume "∃ atm. c = Atm atm ∧ compatAtm atm"
hence "siso c"
apply induct
apply (metis compatAtm_def eff_Atm cont_Atm wt_Atm)
by (metis cont_Atm siso_Done)
}
moreover have "siso (Atm atm) ⟹ compatAtm atm" unfolding compatAtm_def
by (metis brn.simps eff_Atm less_Suc_eq mult_less_cancel1 nat_mult_1 siso_cont_indis)
ultimately show ?thesis by blast
qed

lemma siso_Seq[simp]:
assumes *: "siso c1" and **: "siso c2"
shows "siso (c1 ;; c2)"
proof-
{fix c :: "('test, 'atom, 'choice) cmd"
assume "∃ c1 c2. c = c1 ;; c2 ∧ siso c1 ∧ siso c2"
hence "siso c"
proof induct
case (Obs c s t i)
then obtain c1 c2 where "i < brn c1"
and "c = c1 ;; c2" and "siso c1 ∧ siso c2"
and "s ≈ t" by auto
thus ?case by (cases "finished (cont c1 s i)") auto
next
case (Cont c s i)
then obtain c1 c2 where "i < brn c1" and
"c = c1 ;; c2 ∧ siso c1 ∧ siso c2" by fastforce
thus ?case by(cases "finished (cont c1 s i)", auto)
qed
}
thus ?thesis using assms by blast
qed

lemma siso_While[simp]:
assumes "compatTst tst" and "siso c"
shows "siso (While tst c)"
proof-
{fix c :: "('test, 'atom, 'choice) cmd"
assume
"(∃ tst d. compatTst tst ∧ c = While tst d ∧ siso d) ∨
(∃ tst d1 d. compatTst tst ∧ c = d1 ;; (While tst d) ∧ siso d1 ∧ siso d)"
hence "siso c"
proof induct
case (Obs c s t i)
hence i: " i < brn c" and st: "s ≈ t" by auto
from Obs show ?case
proof(elim disjE exE conjE)
fix tst d
assume "compatTst tst" and "c = While tst d" and "siso d"
thus ?thesis using i st unfolding compatTst_def
by (cases "tval tst s", simp_all)
next
fix tst d1 d
assume "compatTst tst" and "c = d1 ;; While tst d"
and "siso d1" and "siso d"
thus ?thesis
using i st unfolding compatTst_def
apply(cases "tval tst s", simp_all)
by (cases "finished (cont d1 s i)", simp_all)+
qed
next
case (Cont c s i)
hence i: " i < brn c" by simp
from Cont show ?case
proof(elim disjE exE conjE)
fix tst d
assume "compatTst tst" and "c = While tst d" and "siso d"
thus ?thesis by (cases "tval tst s", simp_all)
next
fix tst d1 d
assume "compatTst tst" and "c = d1 ;; While tst d" and "siso d1" and "siso d"
thus ?thesis using i unfolding compatTst_def
apply (cases "tval tst s", simp_all)
by (cases "finished (cont d1 s i)", simp_all)+
qed
qed
}
thus ?thesis using assms by blast
qed

lemma siso_Ch[simp]:
assumes "compatCh ch"
and *: "siso c1" and **: "siso c2"
shows "siso (Ch ch c1 c2)"
proof-
{fix c :: "('test, 'atom, 'choice) cmd"
assume "∃ ch c1 c2. compatCh ch ∧ c = Ch ch c1 c2 ∧ siso c1 ∧ siso c2"
hence "siso c"
proof induct
case (Obs c s t i)
then obtain ch c1 c2 where "i < 2"
and "compatCh ch" and "c = Ch ch c1 c2" and "siso c1 ∧ siso c2"
and "s ≈ t" by fastforce
thus ?case by (cases i) auto
next
case (Cont c s i)
then obtain ch c1 c2 where "i < 2" and
"compatCh ch ∧ c = Ch ch c1 c2 ∧ siso c1 ∧ siso c2" by fastforce
thus ?case by (cases i) auto
qed
}
thus ?thesis using assms by blast
qed

lemma siso_Par[simp]:
assumes "properL cl" and "sisoL cl"
shows "siso (Par cl)"
proof-
{fix c :: "('test, 'atom, 'choice) cmd"
assume "∃ cl. c = Par cl ∧ properL cl ∧ sisoL cl"
hence "siso c"
proof induct
case (Obs c s t ii)
then obtain cl where ii: "ii < brnL cl (length cl)"
and cl: "properL cl"
and c: "c = Par cl" and siso: "sisoL cl"
and st: "s ≈ t" by auto
let ?N = "length cl"
from cl ii show ?case
apply(cases rule: brnL_cases)
using siso st cl unfolding c by fastforce
next
case (Cont c s ii)
then obtain cl where ii: "ii < brnL cl (length cl)"
and cl: "properL cl"
and c: "c = Par cl" and sisoL: "sisoL cl"
by auto
from cl ii show ?case
apply (cases rule: brnL_cases)
using cl sisoL unfolding c by auto
qed
}
thus ?thesis using assms by blast
qed

lemma siso_ParT[simp]:
assumes "properL cl" and "sisoL cl"
shows "siso (ParT cl)"
proof-
{fix c :: "('test, 'atom, 'choice) cmd"
assume "∃ cl. c = ParT cl ∧ properL cl ∧ sisoL cl"
hence "siso c"
proof induct
case (Obs c s t ii)
then obtain cl where ii: "ii < brnL cl (length cl)"
and cl: "properL cl"
and c: "c = ParT cl" and siso: "sisoL cl"
and st: "s ≈ t" by auto
let ?N = "length cl"
from cl ii show ?case proof (cases rule: brnL_cases)
case (Local n i)
show ?thesis (is "?eff ∧ ?wt ∧ ?mv")
proof-
have eff_mv: "?eff ∧ ?mv" using Local siso cl st unfolding c by force
have wt: ?wt
proof(cases "WtFT cl = 1")
case True
thus ?thesis unfolding c using Local cl st siso True
by (cases "n = pickFT cl ∧ i = 0") auto
next
case False
thus ?thesis unfolding c using Local cl st siso False
by (cases "finished (cl!n)") auto
qed
from eff_mv wt show ?thesis by simp
qed
qed
next
case (Cont c s ii)
then obtain cl where ii: "ii < brnL cl (length cl)"
and cl: "properL cl"
and c: "c = ParT cl" and siso: "sisoL cl"
by auto
from cl ii show ?case apply (cases rule: brnL_cases)
using siso cl unfolding c by force
qed
}
thus ?thesis using assms by blast
qed

text‹Self-isomorphism implies strong bisimilarity:›

lemma bij_betw_emp[simp]:
"bij_betw f {} {}"
unfolding bij_betw_def by auto

lemma part_full[simp]:
"part I {I}"
unfolding part_def by auto

definition singlPart where
"singlPart I ≡ {{i} | i . i ∈ I}"

lemma part_singlPart[simp]:
"part I (singlPart I)"
unfolding part_def singlPart_def by auto

lemma singlPart_inj_on[simp]:
"inj_on (image f) (singlPart I) = inj_on f I"
unfolding inj_on_def singlPart_def
apply auto
by (metis image_insert insertI1 insert_absorb insert_code singleton_inject)

lemma singlPart_surj[simp]:
"(image f) ` (singlPart I) = (singlPart J) ⟷ f ` I = J"
unfolding inj_on_def singlPart_def apply auto by blast

lemma singlPart_bij_betw[simp]:
"bij_betw (image f) (singlPart I) (singlPart J) = bij_betw f I J"
unfolding bij_betw_def by auto

lemma singlPart_finite1:
assumes "finite (singlPart I)"
shows "finite (I::'a set)"
proof-
define u where "u i = {i}" for i :: 'a
have "u ` I ⊆ singlPart I" unfolding u_def singlPart_def by auto
moreover have "inj_on u I" unfolding u_def inj_on_def by auto
ultimately show ?thesis using assms
by (metis ‹inj_on u I› finite_imageD infinite_super)
qed

lemma singlPart_finite[simp]:
"finite (singlPart I) = finite I"
using singlPart_finite1[of I] unfolding singlPart_def by auto

lemma emp_notIn_singlPart[simp]:
"{} ∉ singlPart I"
unfolding singlPart_def by auto

lemma Sbis_coinduct[consumes 1, case_names step, coinduct set]:
"R c d ⟹
(⋀c d s t. R c d ⟹ s ≈ t ⟹
∃P F. mC_C_part c d P F ∧ inj_on F P ∧ mC_C_wt c d s t P F ∧
(∀I∈P. ∀i∈I. ∀j∈F I.
eff c s i ≈ eff d t j ∧ (R (cont c s i) (cont d t j) ∨ (cont c s i, cont d t j) ∈ Sbis)))
⟹ (c, d) ∈ Sbis"
using Sbis_coind[of "{(x, y). R x y}"]
unfolding Sretr_def matchC_C_def mC_C_def mC_C_eff_cont_def
apply (simp add: subset_eq Ball_def )
apply metis
done

lemma siso_Sbis[simp]: "siso c ⟹ c ≈s c"
proof (coinduction arbitrary: c)
case (step s t c) with siso_cont_indis[of c s t] part_singlPart[of "{..<brn c}"] show ?case
by (intro exI[of _ "singlPart {..< brn c}"] exI[of _ id])
(auto simp add: mC_C_part_def mC_C_wt_def singlPart_def)
qed

subsection ‹Discreetness versus language constructs:›

lemma discr_Done[simp]: "discr Done"
by coinduction auto

lemma discr_Atm_presAtm[simp]: "discr (Atm atm) = presAtm atm"
proof-
have "presAtm atm ⟹ discr (Atm atm)"
by (coinduction arbitrary: atm) (auto simp: presAtm_def)
moreover have "discr (Atm atm) ⟹ presAtm atm"
unfolding presAtm_def
by (metis One_nat_def brn.simps(2) discr.simps eff_Atm lessI)
ultimately show ?thesis by blast
qed

lemma discr_Seq[simp]:
"discr c1 ⟹ discr c2 ⟹ discr (c1 ;; c2)"
by (coinduction arbitrary: c1 c2)
(simp, metis cont_Seq_finished discr_cont cont_Seq_notFinished)

lemma discr_While[simp]: assumes "discr c" shows "discr (While tst c)"
proof-
{fix c :: "('test, 'atom, 'choice) cmd"
assume
"(∃ tst d. c = While tst d ∧ discr d) ∨
(∃ tst d1 d. c = d1 ;; (While tst d) ∧ discr d1 ∧ discr d)"
hence "discr c"
apply induct apply safe
apply (metis eff_While indis_refl)
apply (metis cont_While_False discr_Done cont_While_True)
apply (metis eff_Seq discr.simps brn.simps)
by (metis cont_Seq_finished discr.simps cont_Seq_notFinished brn.simps)
}
thus ?thesis using assms by blast
qed

lemma discr_Ch[simp]: "discr c1 ⟹ discr c2 ⟹ discr (Ch ch c1 c2)"
by coinduction (simp, metis indis_refl less_2_cases cont_Ch_L cont_Ch_R)

lemma discr_Par[simp]: "properL cl ⟹ discrL cl ⟹ discr (Par cl)"
proof (coinduction arbitrary: cl, clarsimp)
fix cl ii s
assume *: "properL cl" "ii < brnL cl (length cl)" and "discrL cl"
from * show "s ≈ eff (Par cl) s ii ∧
((∃cl'. cont (Par cl) s ii = Par cl' ∧ properL cl' ∧ discrL cl') ∨ discr (cont (Par cl) s ii))"
proof (cases rule: brnL_cases)
case (Local n i)
with ‹discrL cl› have "s ≈ eff (cl ! n) s i" by simp
thus ?thesis
using Local ‹discrL cl› ‹properL cl› by auto
qed
qed

lemma discr_ParT[simp]: "properL cl ⟹ discrL cl ⟹ discr (ParT cl)"
proof (coinduction arbitrary: cl, clarsimp)
fix p cl s ii assume "properL cl" "ii < brnL cl (length cl)" "discrL cl"
then show "s ≈ eff (ParT cl) s ii ∧
((∃cl'. cont (ParT cl) s ii = ParT cl' ∧ properL cl' ∧ discrL cl') ∨ discr (cont (ParT cl) s ii))"
proof (cases rule: brnL_cases)
case (Local n i)
have "s ≈ eff (cl ! n) s i" using Local ‹discrL cl› by simp
thus ?thesis using Local ‹discrL cl› ‹properL cl› by simp
qed
qed

lemma discr_finished[simp]: "proper c ⟹ finished c ⟹ discr c"
by (induct c rule: proper_induct) (auto simp: discrL_intro)

subsection‹Strong bisimilarity versus language constructs›

lemma Sbis_pres_discr_L:
"c ≈s d ⟹ discr d ⟹ discr c"
proof (coinduction arbitrary: d c, clarsimp)
fix c d s i
assume d: "c ≈s d" "discr d" and i: "i < brn c"
then obtain P F where
match: "mC_C Sbis c d s s P F"
using Sbis_mC_C[of c d s s] by blast
hence "⋃P = {..<brn c}"
using i unfolding mC_C_def mC_C_part_def part_def by simp
then obtain I where I: "I ∈ P" and i: "i ∈ I" using i by auto
obtain j where j: "j ∈ F I"
using match I unfolding mC_C_def mC_C_part_def by blast
hence "j < brn d" using I match
unfolding mC_C_def mC_C_part_def part_def apply simp by blast
hence md: "discr (cont d s j)" and s: "s ≈ eff d s j"
using d discr_cont[of d j s] discr_eff_indis[of d j s] by auto
have "eff c s i ≈ eff d s j" and md2: "cont c s i ≈s cont d s j"
using I i j match unfolding mC_C_def mC_C_eff_cont_def by auto
hence "s ≈ eff c s i" using s indis_sym indis_trans by blast
thus "s ≈ eff c s i ∧ ((∃d. cont c s i ≈s d ∧ discr d) ∨ discr (cont c s i))"
using md md2 by blast
qed

lemma Sbis_pres_discr_R:
assumes "discr c" and "c ≈s d"
shows "discr d"
using assms Sbis_pres_discr_L Sbis_sym by blast

lemma Sbis_finished_discr_L:
assumes "c ≈s d" and "proper d" and "finished d"
shows "discr c"
using assms Sbis_pres_discr_L by auto

lemma Sbis_finished_discr_R:
assumes "proper c" and "finished c" and "c ≈s d"
shows "discr d"
using assms Sbis_pres_discr_R[of c d] by auto

(*  *)

definition thetaSD where
"thetaSD ≡ {(c, d) | c d . proper c ∧ proper d ∧ discr c ∧ discr d}"

lemma thetaSD_Sretr:
"thetaSD ⊆ Sretr thetaSD"
unfolding Sretr_def matchC_C_def proof safe
fix c d s t
assume c_d: "(c, d) ∈ thetaSD" and st: "s ≈ t"
hence p: "proper c ∧ proper d" unfolding thetaSD_def by auto
let ?P = "{{..<brn c}}"
let ?F = "% I. {..< brn d}"
have 0: "{..<brn c} ≠ {}"  "{..<brn d} ≠ {}"
using p int_emp brn_gt_0 by blast+
show "∃P F. mC_C thetaSD c d s t P F"
apply -
apply(rule exI[of _ ?P]) apply(rule exI[of _ ?F])
unfolding mC_C_def proof(intro conjI)
show "mC_C_part c d ?P ?F"
unfolding mC_C_part_def using 0 unfolding part_def by auto
next
show "inj_on ?F ?P" unfolding inj_on_def by simp
next
show "mC_C_wt c d s t ?P ?F" unfolding mC_C_wt_def using p by auto
next
show "mC_C_eff_cont thetaSD c d s t ?P ?F"
unfolding mC_C_eff_cont_def proof clarify
fix I i j
assume i: "i < brn c" and j: "j < brn d"
hence "s ≈ eff c s i" using c_d unfolding thetaSD_def by simp
moreover have "t ≈ eff d t j" using i j c_d unfolding thetaSD_def by simp
ultimately have "eff c s i ≈ eff d t j" using st indis_sym indis_trans by blast
thus "eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ thetaSD"
using c_d i j unfolding thetaSD_def by auto
qed
qed
qed

lemma thetaSD_Sbis:
"thetaSD ⊆ Sbis"
using Sbis_raw_coind thetaSD_Sretr by blast

theorem discr_Sbis[simp]:
assumes "proper c" and "proper d" and "discr c" and "discr d"
shows "c ≈s d"
using assms thetaSD_Sbis unfolding thetaSD_def by auto

(* Done: *)

definition thetaSDone where
"thetaSDone ≡ {(Done, Done)}"

lemma thetaSDone_Sretr:
"thetaSDone ⊆ Sretr thetaSDone"
unfolding Sretr_def matchC_C_def thetaSDone_def proof safe
fix s t assume st: "s ≈ t"
let ?P = "{{0}}" let ?F = id
show "∃P F. mC_C {(Done, Done)} Done Done s t P F"
apply(intro exI[of _ ?P]) apply(intro exI[of _ ?F])
unfolding m_defsAll part_def using st by auto
qed

lemma thetaSDone_Sbis:
"thetaSDone ⊆ Sbis"
using Sbis_raw_coind thetaSDone_Sretr by blast

theorem Done_Sbis[simp]:
"Done ≈s Done"
using thetaSDone_Sbis unfolding thetaSDone_def by auto

(* Atm: *)
definition thetaSAtm where
"thetaSAtm atm ≡
{(Atm atm, Atm atm), (Done, Done)}"

lemma thetaSAtm_Sretr:
assumes "compatAtm atm"
shows "thetaSAtm atm ⊆ Sretr (thetaSAtm atm)"
unfolding Sretr_def matchC_C_def thetaSAtm_def proof safe
fix s t assume st: "s ≈ t"
let ?P = "{{0}}" let ?F = id
show "∃P F. mC_C {(Atm atm, Atm atm), (Done, Done)} Done Done s t P F"
apply(intro exI[of _ ?P]) apply(intro exI[of _ ?F])
unfolding m_defsAll part_def using st by auto
next
fix s t assume st: "s ≈ t"
let ?P = "{{0}}" let ?F = id
show "∃P F. mC_C {(Atm atm, Atm atm), (Done, Done)} (Atm atm) (Atm atm) s t P F"
apply(intro exI[of _ ?P]) apply(intro exI[of _ ?F])
unfolding m_defsAll part_def using st assms unfolding compatAtm_def by auto
qed

lemma thetaSAtm_Sbis:
assumes "compatAtm atm"
shows "thetaSAtm atm ⊆ Sbis"
using assms Sbis_raw_coind thetaSAtm_Sretr by blast

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

(* Seq *)
definition thetaSSeqI where
"thetaSSeqI ≡
{(e ;; c, e ;; d) | e c d . siso e ∧ c ≈s d}"

lemma thetaSSeqI_Sretr:
"thetaSSeqI ⊆ Sretr (thetaSSeqI Un Sbis)"
unfolding Sretr_def matchC_C_def proof safe
fix c d s t
assume c_d: "(c, d) ∈ thetaSSeqI" and st: "s ≈ t"
then obtain e c1 d1 where e: "siso e" and c1d1: "c1 ≈s d1"
and c: "c = e ;; c1" and d: "d = e ;; d1"
unfolding thetaSSeqI_def by auto
let ?P = "{{i} | i . i < brn e}"
let ?F = "%I. I"
show "∃P F. mC_C (thetaSSeqI Un Sbis) c d s t P F"
apply(rule exI[of _ ?P]) apply(rule exI[of _ ?F])
unfolding mC_C_def proof (intro conjI)
show "mC_C_part c d ?P ?F"
unfolding mC_C_part_def proof (intro conjI)
show "part {..<brn c} ?P"
unfolding part_def proof safe
fix i assume "i < brn c"
thus "i ∈ ⋃ ?P" using c e st siso_cont_indis[of e s t] by auto
qed (unfold c, simp)
(*  *)
thus "part {..<brn d} (?F ` ?P)" unfolding c d by auto
qed auto
next
show "mC_C_eff_cont (thetaSSeqI Un Sbis) c d s t ?P ?F"
unfolding mC_C_eff_cont_def proof (intro impI allI, elim conjE)
fix I i j
assume I: "I ∈ ?P" and i: "i ∈ I" and j: "j ∈ I"
show "eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ thetaSSeqI ∪ Sbis"
proof(cases "I = {}")
case True thus ?thesis using i by simp
next
case False
then obtain i' where "j ∈ ?F {i'}" and "i' < brn e"
using I j by auto
thus ?thesis
using st c_d e i j I unfolding c d thetaSSeqI_def
by (cases "finished (cont e s i')") auto
qed
qed
qed (insert st c_d c, unfold m_defsAll thetaSSeqI_def part_def, auto)
qed

lemma thetaSSeqI_Sbis:
"thetaSSeqI ⊆ Sbis"
using Sbis_coind thetaSSeqI_Sretr by blast

theorem Seq_siso_Sbis[simp]:
assumes "siso e" and "c2 ≈s d2"
shows "e ;; c2 ≈s e ;; d2"
using assms thetaSSeqI_Sbis unfolding thetaSSeqI_def by auto

(*  *)
definition thetaSSeqD where
"thetaSSeqD ≡
{(c1 ;; c2, d1 ;; d2) |
c1 c2 d1 d2.
proper c1 ∧ proper d1 ∧ proper c2 ∧ proper d2 ∧
discr c2 ∧ discr d2 ∧
c1 ≈s d1}"

lemma thetaSSeqD_Sretr:
"thetaSSeqD ⊆ Sretr (thetaSSeqD Un Sbis)"
unfolding Sretr_def matchC_C_def proof safe
fix c d s t
assume c_d: "(c, d) ∈ thetaSSeqD" and st: "s ≈ t"
then obtain c1 c2 d1 d2 where
c1d1: "proper c1" "proper d1" "c1 ≈s d1" and
c2d2: "proper c2" "proper d2" "discr c2" "discr d2"
and c: "c = c1 ;; c2" and d: "d = d1 ;; d2"
unfolding thetaSSeqD_def by auto
from c1d1 st obtain P F
where match: "mC_C Sbis c1 d1 s t P F"
using Sbis_mC_C by blast
have P: "⋃P = {..<brn c1}" and FP: "⋃ (F ` P) = {..<brn d1}"
using match unfolding mC_C_def mC_C_part_def part_def by metis+
show "∃P F. mC_C (thetaSSeqD Un Sbis) c d s t P F"
apply(rule exI[of _ P]) apply(rule exI[of _ F])
unfolding mC_C_def proof (intro conjI)
show "mC_C_eff_cont (thetaSSeqD ∪ Sbis) c d s t P F"
unfolding mC_C_eff_cont_def proof(intro allI impI, elim conjE)
fix i j I assume I : "I ∈ P" and i: "i ∈ I" and j: "j ∈ F I"
let ?c1' = "cont c1 s i"  let ?d1' = "cont d1 t j"
let ?s' = "eff c1 s i"  let ?t' = "eff d1 t j"
have "i < brn c1" using i I P by blast note i = this i
have "j < brn d1" using j I FP by blast note j = this j
have c1'd1': "?c1' ≈s ?d1'"
"proper ?c1'" "proper ?d1'"
using c1d1 i j I match unfolding c mC_C_def mC_C_eff_cont_def by auto
show "eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ thetaSSeqD ∪ Sbis"
(is "?eff ∧ ?cont") proof
show ?eff using match I i j unfolding c d m_defsAll by simp
next
show ?cont
proof(cases "finished ?c1'")
case True note c1' = True
hence csi: "cont c s i = c2" using i match unfolding c m_defsAll by simp
show ?thesis
proof(cases "finished ?d1'")
case True
hence "cont d t j = d2" using j match unfolding d m_defsAll by simp
thus ?thesis using csi c2d2 by simp
next
case False
hence dtj: "cont d t j = ?d1' ;; d2"
using j match unfolding d m_defsAll by simp
have "discr ?d1'" using c1'd1'  c1' Sbis_finished_discr_R by blast
thus ?thesis using c1'd1' c2d2 unfolding csi dtj by simp
qed
next
case False note Done_c = False
hence csi: "cont c s i = ?c1' ;; c2"
using i match unfolding c m_defsAll by simp
show ?thesis
proof(cases "finished (cont d1 t j)")
case True note d1' = True
hence dtj: "cont d t j = d2" using j match unfolding d m_defsAll by simp
have "discr ?c1'" using c1'd1'  d1' Sbis_finished_discr_L by blast
thus ?thesis using c1'd1' c2d2 unfolding csi dtj by simp
next
case False
hence dtj: "cont d t j = ?d1' ;; d2" using j match unfolding d m_defsAll by simp
thus ?thesis unfolding csi dtj thetaSSeqD_def
using c1'd1' c2d2 by blast
qed
qed
qed
qed
qed(insert match, unfold m_defsAll c d, auto)
qed

lemma thetaSSeqD_Sbis:
"thetaSSeqD ⊆ Sbis"
using Sbis_coind thetaSSeqD_Sretr by blast

theorem Seq_Sbis[simp]:
assumes "proper c1" and "proper d1" and "proper c2" and "proper d2"
and "c1 ≈s d1" and "discr c2" and "discr d2"
shows "c1 ;; c2 ≈s d1 ;; d2"
using assms thetaSSeqD_Sbis unfolding thetaSSeqD_def by auto

(* Note: no compositionality w.r.t. while loop. *)

(* Ch *)
definition thetaSCh where
"thetaSCh ch c1 c2 d1 d2 ≡ {(Ch ch c1 c2, Ch ch d1 d2)}"

lemma thetaSCh_Sretr:
assumes "compatCh ch" and "c1 ≈s d1" and "c2 ≈s d2"
shows "thetaSCh ch c1 c2 d1 d2 ⊆
Sretr (thetaSCh ch c1 c2 d1 d2 ∪ Sbis)"
(is "?th ⊆ Sretr (?th ∪ Sbis)")
unfolding Sretr_def matchC_C_def proof safe
fix c d s t
assume c_d: "(c, d) ∈ ?th" and st: "s ≈ t"
hence c: "c = Ch ch c1 c2" "brn c = 2"
and d: "d = Ch ch d1 d2" "brn d = 2"
unfolding thetaSCh_def by auto
let ?P = "{{0}, {1}}"
let ?F = "%I. I"
show "∃P F. mC_C (?th Un Sbis) c d s t P F"
apply(rule exI[of _ ?P]) apply(rule exI[of _ ?F])
using assms st c_d c unfolding m_defsAll thetaSCh_def part_def by auto
qed

lemma thetaSCh_Sbis:
assumes "compatCh ch" and "c1 ≈s d1" and "c2 ≈s d2"
shows "thetaSCh ch c1 c2 d1 d2 ⊆ Sbis"
using Sbis_coind thetaSCh_Sretr[OF assms] by blast

theorem Ch_siso_Sbis[simp]:
assumes "compatCh ch" and "c1 ≈s d1" and "c2 ≈s d2"
shows "Ch ch c1 c2 ≈s Ch ch d1 d2"
using thetaSCh_Sbis[OF assms] unfolding thetaSCh_def by auto

(* Par: *)

definition shift where
"shift cl n ≡ image (%i. brnL cl n + i)"

definition "back" where
"back cl n ≡ image (% ii. ii - brnL cl n)"

lemma emp_shift[simp]:
"shift cl n I = {} ⟷ I = {}"
unfolding shift_def by auto

lemma emp_shift_rev[simp]:
"{} = shift cl n I ⟷ I = {}"
unfolding shift_def by auto

lemma emp_back[simp]:
"back cl n II = {} ⟷ II = {}"
unfolding back_def by force

lemma emp_back_rev[simp]:
"{} = back cl n II ⟷ II = {}"
unfolding back_def by force

lemma in_shift[simp]:
"brnL cl n + i ∈ shift cl n I ⟷ i ∈ I"
unfolding shift_def by auto

lemma in_back[simp]:
"ii ∈ II ⟹ ii - brnL cl n ∈ back cl n II"
unfolding back_def by auto

lemma in_back2[simp]:
assumes "ii > brnL cl n" and "II ⊆ {brnL cl n ..<+ brn (cl!n)}"
shows "ii - brnL cl n ∈ back cl n II ⟷ ii ∈ II" (is "?L ⟷ ?R")
using assms unfolding back_def by force

lemma shift[simp]:
assumes "I ⊆ {..< brn (cl!n)}"
shows "shift cl n I ⊆ {brnL cl n ..<+ brn (cl!n)}"
using assms unfolding shift_def by auto

lemma shift2[simp]:
assumes "I ⊆ {..< brn (cl!n)}"
and "ii ∈ shift cl n I"
shows "brnL cl n ≤ ii ∧ ii < brnL cl n + brn (cl!n)"
using assms unfolding shift_def by auto

lemma shift3[simp]:
assumes n: "n < length cl" and I: "I ⊆ {..< brn (cl!n)}"
and ii: "ii ∈ shift cl n I"
shows "ii < brnL cl (length cl)"
proof-
have "ii < brnL cl n + brn (cl!n)" using I ii by simp
also have "... ≤ brnL cl (length cl)" using n
by (metis brnL_Suc brnL_mono Suc_leI)
finally show ?thesis .
qed

lemma "back"[simp]:
assumes "II ⊆ {brnL cl n ..<+ brn (cl!n)}"
shows "back cl n II ⊆ {..< brn (cl!n)}"
using assms unfolding back_def by force

lemma back2[simp]:
assumes "II ⊆ {brnL cl n ..<+ brn (cl!n)}"
and "i ∈ back cl n II"
shows "i < brn (cl!n)"
using assms unfolding back_def by force

lemma shift_inj[simp]:
"shift cl n I1 = shift cl n I2 ⟷ I1 = I2"
unfolding shift_def by force

lemma shift_mono[simp]:
"shift cl n I1 ⊆ shift cl n I2 ⟷ I1 ⊆ I2"
unfolding shift_def by auto

lemma shift_Int[simp]:
"shift cl n I1 ∩ shift cl n I2 = {} ⟷ I1 ∩ I2 = {}"
unfolding shift_def by force

lemma inj_shift: "inj (shift cl n)"
unfolding inj_on_def by simp

lemma inj_on_shift: "inj_on (shift cl n) K"
using inj_shift unfolding inj_on_def by simp

lemma back_shift[simp]:
"back cl n (shift cl n I) = I"
unfolding back_def shift_def by force

lemma shift_back[simp]:
assumes "II ⊆ {brnL cl n ..<+ brn (cl!n)}"
shows "shift cl n (back cl n II) = II"
using assms unfolding shift_def back_def atLeastLessThan_def by force

lemma back_inj[simp]:
assumes II1: "II1 ⊆ {brnL cl n ..<+ brn (cl!n)}"
and II2: "II2 ⊆ {brnL cl n ..<+ brn (cl!n)}"
shows "back cl n II1 = back cl n II2 ⟷ II1 = II2" (is "?L = ?R ⟷ II1 = II2")
proof
have "II1 = shift cl n ?L" using II1 by simp
also assume "?L = ?R"
also have "shift cl n ?R = II2" using II2 by simp
finally show "II1 = II2" .
qed auto

lemma back_mono[simp]:
assumes "II1 ⊆ {brnL cl n ..<+ brn (cl!n)}"
and "II2 ⊆ {brnL cl n ..< brnL cl n + brn (cl!n)}"
shows "back cl n II1 ⊆ back cl n II2 ⟷ II1 ⊆ II2"
(is "?L ⊆ ?R ⟷ II1 ⊆ II2")
proof-
have "?L ⊆ ?R ⟷ shift cl n ?L ⊆ shift cl n ?R" by simp
also have "... ⟷ II1 ⊆ II2" using assms by simp
finally show ?thesis .
qed

lemma back_Int[simp]:
assumes "II1 ⊆ {brnL cl n ..<+ brn (cl!n)}"
and "II2 ⊆ {brnL cl n ..< brnL cl n + brn (cl!n)}"
shows "back cl n II1 ∩ back cl n II2 = {} ⟷ II1 ∩ II2 = {}"
(is "?L ∩ ?R = {} ⟷ II1 ∩ II2 = {}")
proof-
have "?L ∩ ?R = {} ⟷ shift cl n ?L ∩ shift cl n ?R = {}" by simp
also have "... ⟷ II1 ∩ II2 = {}" using assms by simp
finally show ?thesis .
qed

lemma inj_on_back:
"inj_on (back cl n) (Pow {brnL cl n ..<+ brn (cl!n)})"
unfolding inj_on_def by simp

lemma shift_surj:
assumes "II ⊆ {brnL cl n ..<+ brn (cl!n)}"
shows "∃ I. I ⊆ {..< brn (cl!n)} ∧ shift cl n I = II"
apply(intro exI[of _ "back cl n II"]) using assms by simp

lemma back_surj:
assumes "I ⊆ {..< brn (cl!n)}"
shows "∃ II. II ⊆ {brnL cl n ..<+ brn (cl!n)} ∧ back cl n II = I"
apply(intro exI[of _ "shift cl n I"]) using assms by simp

lemma shift_part[simp]:
assumes "part {..< brn (cl!n)} P"
shows "part {brnL cl n ..<+ brn (cl!n)} (shift cl n ` P)"
unfolding part_def proof(intro conjI allI impI)
show "⋃ (shift cl n ` P) = {brnL cl n ..<+ brn (cl!n)}"
proof safe
fix ii I assume ii: "ii ∈ shift cl n I" and "I ∈ P"
hence "I ⊆ {..< brn (cl!n)}" using assms unfolding part_def by blast
thus "ii ∈ {brnL cl n ..<+ brn (cl!n)}" using ii by simp
next
fix ii assume ii_in: "ii ∈ {brnL cl n..<+brn (cl ! n)}"
define i where "i = ii - brnL cl n"
have ii: "ii = brnL cl n + i" unfolding i_def using ii_in by force
have "i ∈ {..< brn (cl!n)}" unfolding i_def using ii_in by auto
then obtain I where i: "i ∈ I" and I: "I ∈ P"
using assms unfolding part_def by blast
thus "ii ∈ ⋃ (shift cl n ` P)" unfolding ii by force
qed
qed(insert assms, unfold part_def, force)

lemma part_brn_disj1:
assumes P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n)"
and n1: "n1 < length cl" and n2: "n2 < length cl"
and II1: "II1 ∈ shift cl n1 ` (P n1)" and II2: "II2 ∈ shift cl n2 ` (P n2)" and d: "n1 ≠ n2"
shows "II1 ∩ II2 = {}"
proof-
let ?N = "length cl"
obtain I1 I2 where I1: "I1 ∈ P n1" and I2: "I2 ∈ P n2"
and II1: "II1 = shift cl n1 I1" and II2: "II2 = shift cl n2 I2"
using II1 II2 by auto
have "I1 ⊆ {..< brn (cl!n1)}" and "I2 ⊆ {..< brn (cl!n2)}"
using n1 I1 n2 I2 P unfolding part_def by blast+
hence "II1 ⊆ {brnL cl n1 ..<+ brn (cl!n1)}" and "II2 ⊆ {brnL cl n2 ..<+ brn (cl!n2)}"
unfolding II1 II2 by auto
thus ?thesis using n1 n2 d brnL_Int by blast
qed

lemma part_brn_disj2:
assumes P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and n1: "n1 < length cl" and n2: "n2 < length cl" and d: "n1 ≠ n2"
shows "shift cl n1 ` (P n1) ∩ shift cl n2 ` (P n2) = {}" (is "?L ∩ ?R = {}")
proof-
{fix II assume II: "II ∈ ?L ∩ ?R"
hence "II = {}" using part_brn_disj1[of cl P n1 n2 II II] assms by blast
hence "{} ∈ ?L" using II by blast
then obtain I where I: "I ∈ P n1" and II: "{} = shift cl n1 I" by blast
hence "I = {}" by simp
hence False using n1 P I by blast
}
thus ?thesis by blast
qed

lemma part_brn_disj3:
assumes P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n)"
and n1: "n1 < length cl" and n2: "n2 < length cl"
and I1: "I1 ∈ P n1" and I2: "I2 ∈ P n2" and d: "n1 ≠ n2"
shows "shift cl n1 I1 ∩ shift cl n2 I2 = {}"
apply(rule part_brn_disj1)
using assms by auto

lemma sum_wt_Par_sub_shift[simp]:
assumes cl: "properL cl" and n: "n < length cl" and
I: "I ⊆ {..< brn (cl ! n)}"
shows
"sum (wt (Par cl) s) (shift cl n I) =
1 / (length cl) * sum (wt (cl ! n) s) I"
using assms sum_wt_Par_sub unfolding shift_def by simp

lemma sum_wt_ParT_sub_WtFT_pickFT_0_shift[simp]:
assumes cl: "properL cl" and nf: "WtFT cl = 1"
and I: "I ⊆ {..< brn (cl ! (pickFT cl))}" "0 ∈ I"
shows
"sum (wt (ParT cl) s) (shift cl (pickFT cl) I) = 1"
using assms sum_wt_ParT_sub_WtFT_pickFT_0
unfolding shift_def by simp

lemma sum_wt_ParT_sub_WtFT_notPickFT_0_shift[simp]:
assumes cl: "properL cl" and nf: "WtFT cl = 1" and n: "n < length cl"
and I: "I ⊆ {..< brn (cl ! n)}" and nI: "n = pickFT cl ⟶ 0 ∉ I"
shows "sum (wt (ParT cl) s) (shift cl n I) = 0"
using assms sum_wt_ParT_sub_WtFT_notPickFT_0 unfolding shift_def by simp

lemma sum_wt_ParT_sub_notWtFT_finished_shift[simp]:
assumes cl: "properL cl" and nf: "WtFT cl ≠ 1" and n: "n < length cl" and cln: "finished (cl!n)"
and I: "I ⊆ {..< brn (cl ! n)}"
shows "sum (wt (ParT cl) s) (shift cl n I) = 0"
using assms sum_wt_ParT_sub_notWtFT_finished
unfolding shift_def by simp

lemma sum_wt_ParT_sub_notWtFT_notFinished_shift[simp]:
assumes cl: "properL cl" and nf: "WtFT cl ≠ 1"
and n: "n < length cl" and cln: "¬ finished (cl!n)"
and I: "I ⊆ {..< brn (cl ! n)}"
shows
"sum (wt (ParT cl) s) (shift cl n I) =
(1 / (length cl)) / (1 - WtFT cl) * sum (wt (cl ! n) s) I"
using assms sum_wt_ParT_sub_notWtFT_notFinished
unfolding shift_def by simp

(*  *)

definition UNpart where
"UNpart cl P ≡ ⋃ n < length cl. shift cl n ` (P n)"

lemma UNpart_cases[elim, consumes 1, case_names Local]:
assumes "II ∈ UNpart cl P" and
"⋀ n I. ⟦n < length cl; I ∈ P n; II = shift cl n I⟧ ⟹ phi"
shows phi
using assms unfolding UNpart_def by auto

lemma emp_UNpart:
assumes "⋀ n. n < length cl ⟹ {} ∉ P n"
shows "{} ∉ UNpart cl P"
using assms unfolding UNpart_def by auto

lemma part_UNpart:
assumes cl: "properL cl" and
P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n)"
shows "part {..< brnL cl (length cl)} (UNpart cl P)"
(is "part ?J ?Q")
proof-
let ?N = "length cl"
have J: "?J = (⋃ n ∈ {..< ?N}. {brnL cl n ..<+ brn (cl!n)})"
using cl brnL_UN by auto
have Q: "?Q = (⋃ n ∈ {..< ?N}. shift cl n ` (P n))"
unfolding UNpart_def by auto
show ?thesis unfolding J Q apply(rule part_UN)
using P brnL_Int by auto
qed

(*  *)

definition pickT_pred where
"pickT_pred cl P II n ≡ n < length cl ∧ II ∈ shift cl n ` (P n)"

definition pickT where
"pickT cl P II ≡ SOME n. pickT_pred cl P II n"

lemma pickT_pred:
assumes "II ∈ UNpart cl P"
shows "∃ n. pickT_pred cl P II n"
using assms unfolding UNpart_def pickT_pred_def by auto

lemma pickT_pred_unique:
assumes P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n)  ∧ {} ∉ P n"
and 1: "pickT_pred cl P II n1" and 2: "pickT_pred cl P II n2"
shows "n1 = n2"
proof-
{assume "n1 ≠ n2"
hence "shift cl n1 ` (P n1) ∩ shift cl n2 ` (P n2) = {}"
using assms part_brn_disj2 unfolding pickT_pred_def by blast
hence False using 1 2 unfolding pickT_pred_def by blast
}
thus ?thesis by auto
qed

lemma pickT_pred_pickT:
assumes "II ∈ UNpart cl P"
shows "pickT_pred cl P II (pickT cl P II)"
unfolding pickT_def apply(rule someI_ex)
using assms pickT_pred by auto

lemma pickT_pred_pickT_unique:
assumes P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and "pickT_pred cl P II n"
shows "n = pickT cl P II"
unfolding pickT_def apply(rule sym, rule some_equality)
using assms pickT_pred_unique[of cl P II] by auto

lemma pickT_length[simp]:
assumes "II ∈ UNpart cl P"
shows "pickT cl P II < length cl"
using assms pickT_pred_pickT unfolding pickT_pred_def by auto

lemma pickT_shift[simp]:
assumes "II ∈ UNpart cl P"
shows "II ∈ shift cl (pickT cl P II) ` (P (pickT cl P II))"
using assms pickT_pred_pickT unfolding pickT_pred_def by auto

lemma pickT_unique:
assumes P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and "n < length cl" and "II ∈ shift cl n ` (P n)"
shows "n = pickT cl P II"
using assms pickT_pred_pickT_unique unfolding pickT_pred_def by auto

definition UNlift where
"UNlift cl dl P F II ≡
shift dl (pickT cl P II) (F (pickT cl P II) (back cl (pickT cl P II) II))"

lemma UNlift_shift[simp]:
assumes P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and n: "n < length cl" and I: "I ∈ P n"
shows "UNlift cl dl P F (shift cl n I) = shift dl n (F n I)"
proof-
let ?N = "length cl"
define II where "II = shift cl n I"
have II: "shift cl n I = II" using II_def by simp
have n: "n = pickT cl P II" apply(rule pickT_unique)
using assms unfolding II_def by auto
have "back cl n II = I" unfolding II_def by simp
hence "shift dl n (F n (back cl n II)) = shift dl n (F n I)" by simp
thus ?thesis unfolding UNlift_def II n[THEN sym] .
qed

lemma UNlift_inj_on:
assumes l: "length cl = length dl"
and P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and FP: "⋀ n. n < length dl ⟹ part {..< brn (dl!n)} (F n ` (P n)) ∧ {} ∉ F n ` (P n)"
and F: "⋀ n. n < length cl ⟹ inj_on (F n) (P n)"
shows "inj_on (UNlift cl dl P F) (UNpart cl P)" (is "inj_on ?G ?Q")
unfolding inj_on_def proof clarify
fix II1 II2
assume II1: "II1 ∈ ?Q" and II2: "II2 ∈ ?Q" and G: "?G II1 = ?G II2"
from II1 show "II1 = II2"
proof(cases rule: UNpart_cases)
case (Local n1 I1)
hence n1: "n1 < length cl" "n1 < length dl" and I1: "I1 ∈ P n1"
and II1: "II1 = shift cl n1 I1" using l by auto
hence G1_def: "?G II1 = shift dl n1 (F n1 I1)" using P by simp
have Pn1: "part {..< brn (dl!n1)} (F n1 ` (P n1))" "{} ∉ F n1 ` (P n1)"
using n1 FP by auto
have F1_in: "F n1 I1 ∈ F n1 ` (P n1)" using I1 by simp
hence Fn1I1: "F n1 I1 ≠ {}" "F n1 I1 ⊆ {..< brn (dl!n1)}"
using Pn1 by (blast, unfold part_def, blast)
hence G1: "?G II1 ≠ {}" "?G II1 ⊆ {brnL dl n1 ..<+ brn (dl!n1)}"
unfolding G1_def by simp_all
from II2 show ?thesis
proof(cases rule: UNpart_cases)
case (Local n2 I2)
hence n2: "n2 < length cl" "n2 < length dl" and I2: "I2 ∈ P n2"
and II2: "II2 = shift cl n2 I2" using l by auto
hence G2_def: "?G II2 = shift dl n2 (F n2 I2)" using P by simp
have Pn2: "part {..< brn (dl!n2)} (F n2 ` (P n2))" "{} ∉ F n2 ` (P n2)"
using n2 FP by auto
have F2_in: "F n2 I2 ∈ F n2 ` (P n2)" using I2 by simp
hence Fn2I2: "F n2 I2 ≠ {}" "F n2 I2 ⊆ {..< brn (dl!n2)}"
using Pn2 by (blast, unfold part_def, blast)
hence G2: "?G II2 ≠ {}" "?G II2 ⊆ {brnL dl n2 ..<+ brn (dl!n2)}"
unfolding G2_def by simp_all
(*  *)
have n12: "n1 = n2" using n1 n2 G1 G2 G brnL_Int by blast
have "F n1 I1 = F n2 I2" using G unfolding G1_def G2_def n12 by simp
hence "I1 = I2" using I1 I2 n1 F unfolding n12 inj_on_def by simp
thus ?thesis unfolding II1 II2 n12 by simp
qed
qed
qed

lemma UNlift_UNpart:
assumes l: "length cl = length dl"
and P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
shows "(UNlift cl dl P F) ` (UNpart cl P) = UNpart dl (%n. F n ` (P n))" (is "?G ` ?Q = ?R")
proof safe
fix II assume II: "II ∈ ?Q"
thus "?G II ∈ ?R"
proof(cases rule: UNpart_cases)
case (Local n I)
hence n: "n < length cl" "n < length dl" and I: "I ∈ P n"
and II: "II = shift cl n I" using l by auto
hence G: "?G II = shift dl n (F n I)" using P by simp
show ?thesis using n I unfolding G UNpart_def by auto
qed
next
fix JJ assume JJ: "JJ ∈ ?R"
thus "JJ ∈ ?G ` ?Q"
proof(cases rule: UNpart_cases)
case (Local n J)
hence n: "n < length cl" "n < length dl" and J: "J ∈ F n ` (P n)"
and JJ: "JJ = shift dl n J" using l by auto
then obtain I where I: "I ∈ P n" and "J = F n I" by auto
hence "JJ = shift dl n (F n I)" using JJ by simp
also have "... = UNlift cl dl P F (shift cl n I)" using n I P by simp
finally have JJ: "JJ = UNlift cl dl P F (shift cl n I)" .
show ?thesis using n I unfolding JJ UNpart_def by auto
qed
qed

lemma emp_UNlift_UNpart:
assumes l: "length cl = length dl"
and P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and FP: "⋀ n. n < length dl ⟹ {} ∉ F n ` (P n)"
shows "{} ∉ (UNlift cl dl P F) ` (UNpart cl P)" (is "{} ∉ ?R")
proof-
have R: "?R = UNpart dl (%n. F n ` (P n))"
apply(rule UNlift_UNpart) using assms by auto
show ?thesis unfolding R apply(rule emp_UNpart) using FP by simp
qed

lemma part_UNlift_UNpart:
assumes l: "length cl = length dl" and dl: "properL dl"
and P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and FP: "⋀ n. n < length dl ⟹ part {..< brn (dl!n)} (F n ` (P n))"
shows "part {..< brnL dl (length dl)} ((UNlift cl dl P F) ` (UNpart cl P))" (is "part ?C ?R")
proof-
have R: "?R = UNpart dl (%n. F n ` (P n))"
apply(rule UNlift_UNpart) using assms by auto
show ?thesis unfolding R apply(rule part_UNpart) using dl FP by auto
qed

lemma ss_wt_Par_UNlift:
assumes l: "length cl = length dl"
and cldl: "properL cl" "properL dl" and II: "II ∈ UNpart cl P"
and P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and FP: "⋀ n. n < length dl ⟹ part {..< brn (dl!n)} (F n ` (P n))"
and sw:
"⋀n I. ⟦n < length cl; I ∈ P n⟧ ⟹
sum (wt (cl ! n) s) I =
sum (wt (dl ! n) t) (F n I)"
and st: "s ≈ t"
shows
"sum (wt (Par cl) s) II =
sum (wt (Par dl) t) (UNlift cl dl P F II)" (is "?L = ?R")
proof-
let ?N = "length cl"
let ?p = "%n. 1 / ?N" let ?q = "%n. 1 / (length dl)"
let ?ss = "%n. s" let ?tt = "%n. t"
have sstt: "⋀ n. n < ?N ⟹ ?ss n ≈ ?tt n" using st by auto
have pq: "⋀ n. n < ?N ⟹ ?p n = ?q n" and sstt: "⋀ n. n < ?N ⟹ ?ss n ≈ ?tt n"
using assms l by auto
from II show ?thesis
proof(cases rule: UNpart_cases)
case (Local n I)
hence n: "n < ?N" "n < length dl" and I: "I ∈ P n"
and II: "II = shift cl n I" using l by auto
have I_sub: "I ⊆ {..< brn (cl!n)}" using n I P unfolding part_def by blast
hence FnI_sub: "F n I ⊆ {..< brn (dl!n)}" using n I FP unfolding part_def by blast
have "?L = (?p n) * sum (wt (cl ! n) (?ss n)) I"
unfolding II using n cldl I_sub by simp
also have "... = (?q n) * sum (wt (dl ! n) (?tt n)) (F n I)"
using n pq apply simp using I sw[of n I] unfolding l by auto
also have "... = ?R"
unfolding II using l cldl n FnI_sub P I by simp
finally show ?thesis .
qed
qed

(* *)

definition thetaSPar where
"thetaSPar ≡
{(Par cl, Par dl) |
cl dl. properL cl ∧ properL dl ∧ SbisL cl dl}"

lemma cont_eff_Par_UNlift:
assumes l: "length cl = length dl"
and cldl: "properL cl" "properL dl" "SbisL cl dl"
and II: "II ∈ UNpart cl P" and ii: "ii ∈ II" and jj: "jj ∈ UNlift cl dl P F II"
and P: "⋀ n. n < length cl ⟹ part {..< brn (cl!n)} (P n) ∧ {} ∉ P n"
and FP: "⋀ n. n < length dl ⟹ part {..< brn (dl!n)} (F n ` (P n))"
and eff_cont:
"⋀n I i j. ⟦n < length cl; I ∈ P n; i ∈ I; j ∈ F n I⟧ ⟹
eff (cl!n) s i ≈ eff (dl!n) t j ∧
cont (cl!n) s i ≈s cont (dl!n) t j"
and st: "s ≈ t"
shows
"eff (Par cl) s ii ≈ eff (Par dl) t jj ∧
(cont (Par cl) s ii, cont (Par dl) t jj) ∈ thetaSPar"
(is "?eff ∧ ?cont")
proof-
let ?N = "length cl"
let ?p = "%n. 1/?N" let ?q = "%n. 1/(length dl)"
let ?ss = "%n. s" let ?tt = "%n. t"
have sstt: "⋀ n. n < ?N ⟹ ?ss n ≈ ?tt n"
using st l by auto
have pq: "⋀ n. n < ?N ⟹ ?p n = ?q n" and sstt: "⋀ n. n < ?N ⟹ ?ss n ≈ ?tt n"
using assms l by auto
from II show ?thesis
proof(cases rule: UNpart_cases)
case (Local n I)
hence n: "n < length cl" "n < length dl" and I: "I ∈ P n"
and II: "II = shift cl n I" using l by auto
from ii II obtain i where i: "i ∈ I" and ii: "ii = brnL cl n + i"
unfolding shift_def by auto
have "i < brn (cl!n)" using i I n P unfolding part_def by blast note i = this i
have jj: "jj ∈ shift dl n (F n I)" using jj P n I unfolding II by simp
from jj II obtain j where j: "j ∈ F n I" and jj: "jj = brnL dl n + j"
unfolding shift_def by auto
have "j < brn (dl!n)" using j I n FP unfolding part_def by blast note j = this j
show ?thesis
proof
have "eff (cl!n) (?ss n) i ≈ eff (dl!n) (?tt n) j"
using n I i j eff_cont by blast
thus ?eff unfolding ii jj using st cldl n i j by simp
next
have "cont (cl!n) (?ss n) i ≈s cont (dl!n) (?tt n) j"
using n I i j eff_cont by blast
thus ?cont unfolding ii jj thetaSPar_def using n i j l cldl by simp
qed
qed
qed

lemma thetaSPar_Sretr: "thetaSPar ⊆ Sretr (thetaSPar)"
unfolding Sretr_def matchC_C_def proof safe
fix c d s t
assume c_d: "(c, d) ∈ thetaSPar" and st: "s ≈ t"
then obtain cl dl where
c: "c = Par cl" and d: "d = Par dl" and
cldl: "properL cl" "properL dl" "SbisL cl dl"
unfolding thetaSPar_def by blast
let ?N = "length cl"
let ?ss = "%n. s" let ?tt = "%n. t"
have N: "?N = length dl" using cldl by simp
have sstt: "⋀ n. n < ?N ⟹ ?ss n ≈ ?tt n"
using st N by auto
let ?phi = "%n PFn. mC_C Sbis (cl ! n) (dl ! n) (?ss n) (?tt n) (fst PFn) (snd PFn)"
{fix n assume n: "n < ?N"
hence "cl ! n ≈s dl ! n" using cldl by auto
hence "∃ PFn. ?phi n PFn" using n Sbis_mC_C sstt by fastforce
}
then obtain PF where phi: "⋀n. n < ?N ⟹ ?phi n (PF n)"
using bchoice[of "{..< ?N}" ?phi] by blast
define P F where "P = fst o PF" and "F = snd o PF"
have m: "⋀n. n < ?N ⟹ mC_C Sbis (cl ! n) (dl ! n) (?ss n) (?tt n) (P n) (F n)"
using phi unfolding P_def F_def by auto
(*  *)
have brn_c: "brn c = brnL cl ?N" unfolding c by simp
have brn_d: "brn d = brnL dl (length dl)" unfolding d by simp
have P: "⋀n. n < ?N ⟹ part {..< brn (cl ! n)} (P n) ∧ {} ∉ (P n)"
using m unfolding m_defsAll part_def by auto
have FP: "⋀n. n < length dl ⟹ part {..< brn (dl ! n)} (F n ` (P n)) ∧ {} ∉ F n ` (P n)"
using m N unfolding m_defsAll part_def by auto
have F: "⋀n. n < ?N ⟹ inj_on (F n) (P n)" using m unfolding m_defsAll by auto
have sw: "⋀n I. ⟦n < length cl; I ∈ P n⟧ ⟹
sum (wt (cl ! n) (?ss n)) I = sum (wt (dl ! n) (?tt n)) (F n I)"
using m unfolding mC_C_def mC_C_wt_def by auto
have eff_cont: "⋀n I i j. ⟦n < length cl; I ∈ P n; i ∈ I; j ∈ F n I⟧ ⟹
eff (cl!n) (?ss n) i ≈ eff (dl!n) (?tt n) j ∧
cont (cl!n) (?ss n) i ≈s cont (dl!n) (?tt n) j"
using m unfolding mC_C_def mC_C_eff_cont_def by auto
(*  *)
define Q G where "Q = UNpart cl P" and "G = UNlift cl dl P F"
note defi = Q_def G_def brn_c brn_d
show "∃Q G. mC_C (thetaSPar) c d s t Q G"
apply(rule exI[of _ Q]) apply(rule exI[of _ G])
unfolding mC_C_def proof (intro conjI)
show "mC_C_part c d Q G" unfolding mC_C_part_def proof(intro conjI)
show "{} ∉ Q" unfolding defi apply(rule emp_UNpart) using P by simp
show "{} ∉ G ` Q" unfolding defi apply(rule emp_UNlift_UNpart) using N P FP by auto
show "part {..<brn c} Q"
unfolding defi apply(rule part_UNpart) using cldl P by auto
show "part {..<brn d} (G ` Q)"
unfolding defi apply(rule part_UNlift_UNpart) using N cldl P FP by auto
qed
next
show "inj_on G Q"
unfolding defi apply(rule UNlift_inj_on) using N P FP F by auto
next
show "mC_C_wt c d s t Q G"
unfolding mC_C_wt_def defi proof clarify
fix I assume "I ∈ UNpart cl P"
thus "sum (wt c s) I = sum (wt d t) (UNlift cl dl P F I)"
unfolding c d apply(intro ss_wt_Par_UNlift)
using N cldl P FP sw st by auto
qed
next
show "mC_C_eff_cont (thetaSPar) c d s t Q G"
unfolding mC_C_eff_cont_def proof clarify
fix II ii jj assume II: "II ∈ Q" and ii: "ii ∈ II" and jj: "jj ∈ G II"
thus "eff c s ii ≈ eff d t jj ∧ (cont c s ii, cont d t jj) ∈ thetaSPar"
unfolding defi c d apply(intro cont_eff_Par_UNlift)
using N cldl P FP eff_cont st by blast+
qed
qed
qed

lemma thetaSPar_Sbis: "thetaSPar ⊆ Sbis"
using Sbis_raw_coind thetaSPar_Sretr by blast

theorem Par_Sbis[simp]:
assumes "properL cl" and "properL dl" "SbisL cl dl"
shows "Par cl ≈s Par dl"
using assms thetaSPar_Sbis unfolding thetaSPar_def by blast

subsection‹01-bisimilarity versus language constructs›

(* Discreetness: *)
lemma ZObis_pres_discr_L: "c ≈01 d ⟹ discr d ⟹ discr c"
proof (coinduction arbitrary: d c, clarsimp)
fix s i c d assume i: "i < brn c" and d: "discr d" and c_d: "c ≈01 d"
then obtain I0 P F where
match: "mC_ZOC ZObis c d s s I0 P F"
using ZObis_mC_ZOC[of c d s s] by blast
hence "⋃P = {..<brn c}"
using i unfolding mC_ZOC_def mC_ZOC_part_def part_def by simp
then obtain I where I: "I ∈ P" and i: "i ∈ I" using i by auto
show "s ≈ eff c s i ∧ ((∃d. cont c s i ≈01 d ∧ discr d) ∨ discr (cont c s i))"
proof(cases "I = I0")
case False
then obtain j where j: "j ∈ F I"
using match I False unfolding mC_ZOC_def mC_ZOC_part_def by blast
hence "j < brn d" using I match
unfolding mC_ZOC_def mC_ZOC_part_def part_def apply simp by blast
hence md: "discr (cont d s j)" and s: "s ≈ eff d s j"
using d discr_cont[of d j s] discr_eff_indis[of d j s] by auto
have "eff c s i ≈ eff d s j" and md2: "cont c s i ≈01 cont d s j"
using I i j match False unfolding mC_ZOC_def mC_ZOC_eff_cont_def by auto
hence "s ≈ eff c s i" using s indis_sym indis_trans by blast
thus ?thesis using md md2 by blast
next
case True
hence "s ≈ eff c s i ∧ cont c s i ≈01 d"
using match i ZObis_sym unfolding mC_ZOC_def mC_ZOC_eff_cont0_def by blast
thus ?thesis using d by blast
qed
qed

theorem ZObis_pres_discr_R:
assumes "discr c" and "c ≈01 d"
shows "discr d"
using assms ZObis_pres_discr_L ZObis_sym by blast

theorem ZObis_finished_discr_L:
assumes "c ≈01 d" and "proper d" and "finished d"
shows "discr c"
using assms ZObis_pres_discr_L by auto

theorem ZObis_finished_discr_R:
assumes "proper c" and "finished c" and "c ≈01 d"
shows "discr d"
using assms ZObis_pres_discr_R[of c d] by auto

theorem discr_ZObis[simp]:
assumes "proper c" and "proper d" and "discr c" and "discr d"
shows "c ≈01 d"
using assms by auto

(* Done: *)
theorem Done_ZObis[simp]:
"Done ≈01 Done"
by simp

(* Atm: *)
theorem Atm_ZObis[simp]:
assumes "compatAtm atm"
shows "Atm atm ≈01 Atm atm"
using assms by simp

(* Seq *)

definition thetaZOSeqI where
"thetaZOSeqI ≡
{(e ;; c, e ;; d) | e c d . siso e ∧ c ≈01 d}"

lemma thetaZOSeqI_ZOretr:
"thetaZOSeqI ⊆ ZOretr (thetaZOSeqI Un ZObis)"
unfolding ZOretr_def matchC_LC_def proof safe
fix c d s t
assume c_d: "(c, d) ∈ thetaZOSeqI" and st: "s ≈ t"
then obtain e c1 d1 where e: "siso e" and c1d1: "c1 ≈01 d1"
and c: "c = e ;; c1" and d: "d = e ;; d1"
unfolding thetaZOSeqI_def by auto
let ?I0 = "{}" let ?J0 = "{}"
let ?P = "{?I0} Un {{i} | i . i < brn e}"
let ?F = "%I. I"
show "∃I0 P F. mC_ZOC (thetaZOSeqI Un ZObis) c d s t I0 P F"
apply(rule exI[of _ ?I0])
apply(rule exI[of _ ?P]) apply(rule exI[of _ ?F])
unfolding mC_ZOC_def proof (intro conjI)
show "mC_ZOC_part c d s t ?I0 ?P ?F"
unfolding mC_ZOC_part_def proof (intro conjI)
show "part {..<brn c} ?P"
unfolding part_def proof safe
fix i assume "i < brn c"
thus "i ∈ ⋃ ?P" using c e st siso_cont_indis[of e s t] by auto
qed (unfold c, simp)
(*  *)
thus "part {..<brn d} (?F ` ?P)" unfolding c d by auto
qed auto
next
show "mC_ZOC_eff_cont (thetaZOSeqI Un ZObis) c d s t ?I0 ?P ?F"
unfolding mC_ZOC_eff_cont_def proof(intro allI impI, elim conjE)
fix I i j
assume I: "I ∈ ?P - {?I0}" and i: "i ∈ I" and j: "j ∈ I"
then obtain i' where "j ∈ ?F {i'}" and "i' < brn e"
using I j by auto
thus "eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ thetaZOSeqI ∪ ZObis"
using st c_d e i j I unfolding c d thetaZOSeqI_def
by (cases "finished (cont e s i')") auto
qed
qed (insert st c_d c, unfold m_defsAll thetaZOSeqI_def part_def, auto)
qed

lemma thetaZOSeqI_ZObis:
"thetaZOSeqI ⊆ ZObis"
using ZObis_coind thetaZOSeqI_ZOretr by blast

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

(*  *)

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

lemma thetaZOSeqD_ZOretr:
"thetaZOSeqD ⊆ ZOretr (thetaZOSeqD Un ZObis)"
unfolding ZOretr_def matchC_LC_def proof safe
fix c d s t
assume c_d: "(c, d) ∈ thetaZOSeqD" and st: "s ≈ t"
then obtain c1 c2 d1 d2 where
c1d1: "proper c1" "proper d1" "c1 ≈01 d1" and
c2d2: "proper c2" "proper d2" "discr c2" "discr d2"
and c: "c = c1 ;; c2" and d: "d = d1 ;; d2"
unfolding thetaZOSeqD_def by auto
from c1d1 st obtain P F I0
where match: "mC_ZOC ZObis c1 d1 s t I0 P F"
using ZObis_mC_ZOC by blast
have P: "⋃P = {..<brn c1}" and FP: "⋃(F ` P) = {..<brn d1}"
using match unfolding mC_ZOC_def mC_ZOC_part_def part_def by metis+
show "∃I0 P F. mC_ZOC (thetaZOSeqD Un ZObis) c d s t I0 P F"
apply(intro exI[of _ I0] exI[of _ P] exI[of _ F])
unfolding mC_ZOC_def proof (intro conjI)
have I0: "I0 ∈ P" using match unfolding m_defsAll by blast
show "mC_ZOC_eff_cont0 (thetaZOSeqD ∪ ZObis) c d s t I0 F"
unfolding mC_ZOC_eff_cont0_def proof(intro conjI ballI)
fix i assume i: "i ∈ I0"
let ?c1' = "cont c1 s i" let ?s' = "eff c1 s i"
have "i < brn c1" using i I0 P by blast note i = this i
have c1'd1: "?c1' ≈01 d1" "proper ?c1'"
using c1d1 i I0 match unfolding mC_ZOC_def mC_ZOC_eff_cont0_def by auto
show "s ≈ eff c s i"
using i match unfolding c mC_ZOC_def mC_ZOC_eff_cont0_def by simp
show "(cont c s i, d) ∈ thetaZOSeqD ∪ ZObis"
proof(cases "finished ?c1'")
case False note f_c1' = False
hence csi: "cont c s i = ?c1' ;; c2" using i unfolding c by simp
hence "(cont c s i, d) ∈ thetaZOSeqD"
using c1'd1 c1d1 c2d2 f_c1' i match
unfolding csi d ```