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