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