section ‹Resumption-Based Noninterference› theory Resumption_Based imports Language_Semantics begin (* We introduce the resumption based notions: strong probabilistic bisimilarity ≈s and 01- probabilistic bisimilarity ≈01, and prove their basic properties. E.g., we prove that ≈s is symmetric and transitive. *) type_synonym 'a rel = "('a ×'a) set" subsection ‹Preliminaries› lemma int_emp[simp]: assumes "i > 0" shows "{..<i} ≠ {}" by (metis assms emptyE lessThan_iff) lemma inj_on_inv_into[simp]: assumes "inj_on F P" shows "inv_into P F ` (F ` P) = P" using assms by auto lemma inj_on_inv_into2[simp]: "inj_on (inv_into P F) (F ` P)" by (metis Hilbert_Choice.inj_on_inv_into subset_refl) lemma refl_gfp: assumes 1: "mono Retr" and 2: "⋀ theta. refl theta ⟹ refl (Retr theta)" shows "refl (gfp Retr)" proof- define bis where "bis = gfp Retr" define th where "th = Id Un bis" have "bis ⊆ Retr bis" using 1 unfolding bis_def by (metis gfp_unfold subset_refl) also have "... ⊆ Retr th" using 1 unfolding mono_def th_def by auto finally have "bis ⊆ Retr th" . moreover {have "refl th" unfolding th_def by (metis Un_commute refl_reflcl) hence "refl (Retr th)" using 2 by simp } ultimately have "Id ⊆ Retr th" unfolding th_def refl_on_def by auto hence "Id ⊆ bis" using 1 coinduct unfolding th_def bis_def by blast thus ?thesis unfolding bis_def refl_on_def by auto qed lemma sym_gfp: assumes 1: "mono Retr" and 2: "⋀ theta. sym theta ⟹ sym (Retr theta)" shows "sym (gfp Retr)" proof- define bis where "bis = gfp Retr" define th where "th = bis ^-1 Un bis" have "bis ⊆ Retr bis" using 1 unfolding bis_def by (metis gfp_unfold subset_refl) also have "... ⊆ Retr th" using 1 unfolding mono_def th_def by auto finally have "bis ⊆ Retr th" . moreover {have "sym th" unfolding th_def by (metis Un_commute sym_Un_converse) hence "sym (Retr th)" using 2 by simp } ultimately have "bis ^-1 ⊆ Retr th" by (metis Un_absorb2 Un_commute Un_upper1 converse_Un sym_conv_converse_eq) hence "bis ^-1 ⊆ bis" using 1 coinduct[of Retr "bis ^-1"] unfolding th_def bis_def by blast thus ?thesis unfolding bis_def sym_def by blast qed lemma trancl_trans[simp]: assumes "trans R" shows "P ^+ ⊆ R ⟷ P ⊆ R" proof- {assume "P ⊆ R" hence "P ^+ ⊆ R ^+" using trancl_mono by auto also have "R ^+ = R" using assms trans_trancl by auto finally have "P ^+ ⊆ R" . } thus ?thesis by auto qed lemma trans_gfp: assumes 1: "mono Retr" and 2: "⋀ theta. trans theta ⟹ trans (Retr theta)" shows "trans (gfp Retr)" proof- define bis where "bis = gfp Retr" define th where "th = bis ^+" have "bis ⊆ Retr bis" using 1 unfolding bis_def by (metis gfp_unfold subset_refl) also have "... ⊆ Retr th" using 1 unfolding mono_def th_def by (metis trancl_trans order_refl trans_trancl) finally have "bis ⊆ Retr th" . moreover {have "trans th" unfolding th_def by (metis th_def trans_trancl) hence "trans (Retr th)" using 2 by simp } ultimately have "bis ^+ ⊆ Retr th" by simp hence "bis ^+ ⊆ bis" using 1 coinduct unfolding th_def bis_def by (metis bis_def gfp_upperbound th_def) thus ?thesis unfolding bis_def trans_def by auto qed lemma O_subset_trans: assumes "r O r ⊆ r" shows "trans r" using assms unfolding trans_def by blast lemma trancl_imp_trans: assumes "r ^+ ⊆ r" shows "trans r" by (metis Int_absorb1 Int_commute trancl_trans assms subset_refl trans_trancl) lemma sym_trans_gfp: assumes 1: "mono Retr" and 2: "⋀ theta. sym theta ∧ trans theta ⟹ sym (Retr theta) ∧ trans (Retr theta)" shows "sym (gfp Retr) ∧ trans (gfp Retr)" proof- define bis where "bis = gfp Retr" define th where "th = (bis Un bis ^-1) ^+" have "bis ⊆ Retr bis" using 1 unfolding bis_def by (metis gfp_unfold subset_refl) also have "... ⊆ Retr th" using 1 unfolding mono_def th_def by (metis inf_sup_absorb le_iff_inf sup_aci(2) trancl_unfold) finally have "bis ⊆ Retr th" . hence "(bis Un bis ^-1) ^+ ⊆ ((Retr th) Un (Retr th) ^-1) ^+" by auto moreover {have "sym th" unfolding th_def by (metis sym_Un_converse sym_trancl) moreover have "trans th" unfolding th_def by (metis th_def trans_trancl) ultimately have "sym (Retr th) ∧ trans (Retr th)" using 2 by simp hence "((Retr th) Un (Retr th) ^-1) ^+ ⊆ Retr th" by (metis Un_absorb subset_refl sym_conv_converse_eq trancl_id) } ultimately have "(bis Un bis ^-1) ^+ ⊆ Retr th" by blast hence "(bis Un bis ^-1) ^+ ⊆ bis" using 1 coinduct unfolding th_def bis_def by (metis bis_def gfp_upperbound th_def) hence "bis ^-1 ⊆ bis" and "bis ^+ ⊆ bis" apply(metis equalityI gfp_upperbound le_supI1 subset_refl sym_Un_converse sym_conv_converse_eq th_def trancl_id trancl_imp_trans) by (metis Un_absorb ‹(bis ∪ bis¯)⇧^{+}⊆ bis› less_supI1 psubset_eq sym_Un_converse sym_conv_converse_eq sym_trancl trancl_id trancl_imp_trans) thus ?thesis unfolding bis_def sym_def using trancl_imp_trans by auto qed subsection ‹Infrastructure for partitions› (* Being a partition *) definition part where "part J P ≡ Union P = J ∧ (∀ J1 J2. J1 ∈ P ∧ J2 ∈ P ∧ J1 ≠ J2 ⟶ J1 ∩ J2 = {})" (* gen P I is the set generated from I using intersections with sets of P *) inductive_set gen for P :: "'a set set" and I :: "'a set" where incl[simp]: "i ∈ I ⟹ i ∈ gen P I" |ext[simp]: "⟦J ∈ P; j0 ∈ J; j0 ∈ gen P I; j ∈ J⟧ ⟹ j ∈ gen P I" (* Partition generated by a set *) definition partGen where "partGen P ≡ {gen P I | I . I ∈ P}" (* finer P Q means: as a partition, P is finer than Q; regarding P and Q as equivalence relations, we have Q included in P *) definition finer where "finer P Q ≡ (∀ J ∈ Q. J = Union {I ∈ P . I ⊆ J}) ∧ (P ≠ {} ⟶ Q ≠ {})" (* The join of two partitions; in terms of equivalence relations, this is the smallest equivalence containing both *) definition partJoin where "partJoin P Q ≡ partGen (P ∪ Q)" (* Compatibility of a function f w.r.t. a set I versus a relation theta *) definition compat where "compat I theta f ≡ ∀ i j. {i, j} ⊆ I ∧ i ≠ j ⟶ (f i, f j) ∈ theta" (* Compatibility of a function f w.r.t. a partition P versus a relation theta; if P is regarded as an equivalence class, we have the standard notion of compatibility *) definition partCompat where "partCompat P theta f ≡ ∀ I ∈ P. compat I theta f" (* Lifting a function F on a partition P to elements II of a potentially coarser partition *) definition lift where "lift P F II ≡ Union {F I | I . I ∈ P ∧ I ⊆ II}" text‹part:› lemma part_emp[simp]: "part J (insert {} P) = part J P" unfolding part_def by auto lemma finite_part[simp]: assumes "finite I" and "part I P" shows "finite P" using assms finite_UnionD unfolding part_def by auto lemma part_sum: assumes P: "part {..<n::nat} P" shows "(∑i<n. f i) = (∑p∈P. ∑i∈p. f i)" proof (subst sum.Union_disjoint [symmetric, simplified]) show "∀p∈P. finite p" proof fix p assume "p ∈ P" with P have "p ⊆ {0..<n}" by (auto simp: part_def) then show "finite p" by (rule finite_subset) simp qed show "∀A∈P. ∀B∈P. A ≠ B ⟶ A ∩ B = {}" using P by (auto simp: part_def) show "sum f {..<n} = sum f (⋃P)" using P by (auto simp: part_def atLeast0LessThan) qed lemma part_Un[simp]: assumes "part I1 P1" and "part I2 P2" and "I1 Int I2 = {}" shows "part (I1 Un I2) (P1 Un P2)" using assms unfolding part_def by (metis Union_Un_distrib Union_disjoint inf_aci(1) mem_simps(3)) lemma part_Un_singl[simp]: assumes "part K P" and "⋀ I. I ∈ P ⟹ I0 Int I = {}" shows "part (I0 Un K) ({I0} Un P)" using assms unfolding part_def by (metis complete_lattice_class.Sup_insert Int_commute insert_iff insert_is_Un) lemma part_Un_singl2: assumes "K01 = I0 Un K1" and "part K1 P" and "⋀ I. I ∈ P ⟹ I0 Int I = {}" shows "part K01 ({I0} Un P)" using assms part_Un_singl by blast lemma part_UN: assumes "⋀ n. n ∈ N ⟹ part (I n) (P n)" and "⋀ n1 n2. {n1,n2} ⊆ N ∧ n1 ≠ n2 ⟹ I n1 ∩ I n2 = {}" shows "part (UN n : N. I n) (UN n : N. P n)" using assms unfolding part_def apply auto apply (metis UnionE) apply (metis Union_upper disjoint_iff_not_equal insert_absorb insert_subset) by (metis UnionI disjoint_iff_not_equal) text‹gen:› lemma incl_gen[simp]: "I ⊆ gen P I" by auto lemma gen_incl_Un: "gen P I ⊆ I ∪ (Union P)" proof fix j assume "j ∈ gen P I" thus "j ∈ I ∪ ⋃P" apply induct by blast+ qed lemma gen_incl: assumes "I ∈ P" shows "gen P I ⊆ Union P" using assms gen_incl_Un[of P I] by blast lemma finite_gen: assumes "finite P" and "⋀ J. J ∈ P ⟹ finite J" and "finite I" shows "finite (gen P I)" by (metis assms finite_Union gen_incl_Un infinite_Un infinite_super) lemma subset_gen[simp]: assumes "J ∈ P" and "gen P I ∩ J ≠ {}" shows "J ⊆ gen P I" using assms gen.ext[of J P _ I] by blast lemma gen_subset_gen[simp]: assumes "J ∈ P" and "gen P I ∩ J ≠ {}" shows "gen P J ⊆ gen P I" proof- have J: "J ⊆ gen P I" using assms by auto show ?thesis proof fix i assume "i ∈ gen P J" thus "i ∈ gen P I" proof induct case (ext J' j0 j) thus ?case using gen.ext[of J' P j0 I j] by blast qed (insert J, auto) qed qed lemma gen_mono[simp]: assumes "I ⊆ J" shows "gen P I ⊆ gen P J" proof fix i assume "i ∈ gen P I" thus "i ∈ gen P J" proof induct case (ext I' j0 j) thus ?case using gen.ext[of I' P j0 J j] by blast qed (insert assms, auto) qed lemma gen_idem[simp]: "gen P (gen P I) = gen P I" proof- define J where "J = gen P I" have "I ⊆ J" unfolding J_def by auto hence "gen P I ⊆ gen P J" by simp moreover have "gen P J ⊆ gen P I" proof fix i assume "i ∈ gen P J" thus "i ∈ gen P I" proof induct case (ext J' j0 j) thus ?case using gen.ext[of J' P j0 I j] by blast qed (unfold J_def, auto) qed ultimately show ?thesis unfolding J_def by auto qed lemma gen_nchotomy: assumes "J ∈ P" shows "J ⊆ gen P I ∨ gen P I ∩ J = {}" using assms subset_gen[of J P I] by blast lemma gen_Union: assumes "I ∈ P" shows "gen P I = Union {J ∈ P . J ⊆ gen P I}" proof safe fix i assume i: "i ∈ gen P I" then obtain J where J: "J ∈ P" "i ∈ J" using assms gen_incl by blast hence "J ⊆ gen P I" using assms i gen_nchotomy by auto thus "i ∈ ⋃{J ∈ P. J ⊆ gen P I}" using J by auto qed auto lemma subset_gen2: assumes *: "{I,J} ⊆ P" and **: "gen P I ∩ gen P J ≠ {}" shows "I ⊆ gen P J" proof- {fix i0 i assume i0: "i0 ∈ I ∧ i0 ∉ gen P J" assume "i ∈ gen P I" hence "i ∉ gen P J" proof induct case (incl i) thus ?case using i0 gen_nchotomy[of I P J] * by blast next case (ext I' j0 j) thus ?case using gen.ext[of I' P j0 J j] gen_nchotomy[of I' P J] by blast qed } thus ?thesis using assms by auto qed lemma gen_subset_gen2[simp]: assumes "{I,J} ⊆ P" and "gen P I ∩ gen P J ≠ {}" shows "gen P I ⊆ gen P J" proof fix i assume "i ∈ gen P I" thus "i ∈ gen P J" proof induct case (incl i) thus ?case using assms subset_gen2 by auto next case (ext I' j0 j) thus ?case using gen.ext[of I' P j0 J j] by blast qed qed lemma gen_eq_gen: assumes "{I,J} ⊆ P" and "gen P I ∩ gen P J ≠ {}" shows "gen P I = gen P J" using assms gen_subset_gen2[of I J P] gen_subset_gen2[of J I P] by blast lemma gen_empty[simp]: "gen P {} = {}" proof- {fix j assume "j ∈ gen P {}" hence False apply induct by auto } thus ?thesis by auto qed lemma gen_empty2[simp]: "gen {} I = I" proof- {fix j assume "j ∈ gen {} I" hence "j ∈ I" apply induct by auto } thus ?thesis by auto qed lemma emp_gen[simp]: assumes "gen P I = {}" shows "I = {}" by (metis all_not_in_conv assms gen.incl) text‹partGen:› lemma partGen_ex: assumes "I ∈ P" shows "∃ J ∈ partGen P. I ⊆ J" using assms unfolding partGen_def apply(intro bexI[of _ "gen P I"]) by auto lemma ex_partGen: assumes "J ∈ partGen P" and j: "j ∈ J" shows "∃ I ∈ P. j ∈ I" proof- obtain I0 where I0: "I0 ∈ P" and J: "J = gen P I0" using assms unfolding partGen_def by auto thus ?thesis using j gen_incl[of I0 P] by auto qed lemma Union_partGen: "⋃ (partGen P) = ⋃ P" using ex_partGen[of _ P] partGen_ex[of _ P] by fastforce lemma Int_partGen: assumes *: "{I,J} ⊆ partGen P" and **: "I ∩ J ≠ {}" shows "I = J" proof- obtain I0 where I0: "I0 ∈ P" and I: "I = gen P I0" using assms unfolding partGen_def by auto obtain J0 where J0: "J0 ∈ P" and J: "J = gen P J0" using assms unfolding partGen_def by auto show ?thesis using gen_eq_gen[of I0 J0 P] I0 J0 ** unfolding I J by blast qed lemma part_partGen: "part (Union P) (partGen P)" unfolding part_def apply(intro conjI allI impI) apply (metis Union_partGen) using Int_partGen by blast lemma finite_partGen[simp]: assumes "finite P" shows "finite (partGen P)" using assms unfolding partGen_def by auto lemma emp_partGen[simp]: assumes "{} ∉ P" shows "{} ∉ partGen P" using assms unfolding partGen_def using emp_gen[of P] by blast text‹finer:› lemma finer_partGen: "finer P (partGen P)" unfolding finer_def partGen_def using gen_Union by auto lemma finer_nchotomy: assumes P: "part I0 P" and Q: "part I0 Q" and PQ: "finer P Q" and I: "I ∈ P" and II: "II ∈ Q" shows "I ⊆ II ∨ (I ∩ II = {})" proof(cases "I ∩ II = {}") case False then obtain i where i: "i ∈ I ∧ i ∈ II" by auto then obtain I' where "i ∈ I'" and I': "I' ∈ P ∧ I' ⊆ II" using PQ II unfolding finer_def by blast hence "I Int I' ≠ {}" using i by blast hence "I = I'" using I I' P unfolding part_def by auto hence "I ⊆ II" using I' by simp thus ?thesis by auto qed auto lemma finer_ex: assumes P: "part I0 P" and Q: "part I0 Q" and PQ: "finer P Q" and I: "I ∈ P" shows "∃ II. II ∈ Q ∧ I ⊆ II" proof(cases "I = {}") case True have "Q ≠ {}" using I PQ unfolding finer_def by auto then obtain JJ where "JJ ∈ Q" by auto with True show ?thesis by blast next case False then obtain i where i: "i ∈ I" by auto hence "i ∈ I0" using I P unfolding part_def by auto then obtain II where II: "II ∈ Q" and "i ∈ II" using Q unfolding part_def by auto hence "I Int II ≠ {}" using i by auto thus ?thesis using assms I II finer_nchotomy[of I0 P Q I II] by auto qed text‹partJoin:› lemma partJoin_commute: "partJoin P Q = partJoin Q P" unfolding partJoin_def partGen_def using Un_commute by metis lemma Union_partJoin_L: "Union P ⊆ Union (partJoin P Q)" unfolding partJoin_def partGen_def by auto lemma Union_partJoin_R: "Union Q ⊆ Union (partJoin P Q)" unfolding partJoin_def partGen_def by auto lemma part_partJoin[simp]: assumes "part I P" and "part I Q" shows "part I (partJoin P Q)" proof- have 1: "Union (P Un Q) = I" using assms unfolding part_def by auto show ?thesis using part_partGen[of "P Un Q"] unfolding 1 partJoin_def by auto qed lemma finer_partJoin_L[simp]: assumes *: "part I P" and **: "part I Q" shows "finer P (partJoin P Q)" proof- have 1: "part I (partJoin P Q)" using assms by simp {fix J j assume J: "J ∈ partJoin P Q" and j: "j ∈ J" hence "J ⊆ I" using 1 by (metis Union_upper part_def) with j have "j ∈ I" by auto then obtain J' where jJ': "j ∈ J'" and J': "J' ∈ P" using * unfolding part_def by auto hence "J ∩ J' ≠ {}" using j by auto moreover obtain J0 where "J = gen (P Un Q) J0" and "J0 ∈ P Un Q" using J unfolding partJoin_def partGen_def by blast ultimately have "J' ⊆ J" using J' gen_nchotomy[of J' "P Un Q" J0] by blast hence "j ∈ ⋃{J' ∈ P. J' ⊆ J}" using J' jJ' by blast } thus ?thesis unfolding finer_def unfolding partJoin_def partGen_def by blast qed lemma finer_partJoin_R[simp]: assumes *: "part I P" and **: "part I Q" shows "finer Q (partJoin P Q)" using assms finer_partJoin_L[of I Q P] partJoin_commute[of P Q] by auto lemma finer_emp[simp]: assumes "finer {} Q" shows "Q ⊆ { {} }" using assms unfolding finer_def by auto text‹compat:› lemma part_emp_R[simp]: "part I {} ⟷ I = {}" unfolding part_def by auto lemma part_emp_L[simp]: "part {} P ⟹ P ⊆ { {} }" unfolding part_def by auto lemma finite_partJoin[simp]: assumes "finite P" and "finite Q" shows "finite (partJoin P Q)" using assms unfolding partJoin_def by auto lemma emp_partJoin[simp]: assumes "{} ∉ P" and "{} ∉ Q" shows "{} ∉ partJoin P Q" using assms unfolding partJoin_def by auto text‹partCompat:› lemma partCompat_Un[simp]: "partCompat (P Un Q) theta f ⟷ partCompat P theta f ∧ partCompat Q theta f" unfolding partCompat_def by auto lemma partCompat_gen_aux: assumes theta: "sym theta" "trans theta" and fP: "partCompat P theta f" and I: "I ∈ P" and i: "i ∈ I" and j: "j ∈ gen P I" and ij: "i ≠ j" shows "(f i, f j) ∈ theta" using j ij proof induct case (incl j) thus ?case using fP I i unfolding partCompat_def compat_def by blast next case (ext J j0 j) show ?case proof(cases "i = j0") case False note case_i = False hence 1: "(f i, f j0) ∈ theta" using ext by blast show ?thesis proof(cases "j = j0") case True thus ?thesis using case_i 1 by simp next case False hence "(f j, f j0) ∈ theta" using ‹j0 ∈ J› ‹j ∈ J› ‹J ∈ P› using fP unfolding partCompat_def compat_def by auto hence "(f j0, f j) ∈ theta" using theta unfolding sym_def by simp thus ?thesis using 1 theta unfolding trans_def by blast qed next case True note case_i = True hence "j0 ≠ j" using ‹i ≠ j› by auto hence "(f j0, f j) ∈ theta" using ‹j0 ∈ J› ‹j ∈ J› ‹J ∈ P› using fP unfolding partCompat_def compat_def by auto thus ?thesis unfolding case_i . qed qed lemma partCompat_gen: assumes theta: "sym theta" "trans theta" and fP: "partCompat P theta f" and I: "I ∈ P" shows "compat (gen P I) theta f" unfolding compat_def proof clarify fix i j assume ij: "{i, j} ⊆ gen P I" "i ≠ j" show "(f i, f j) ∈ theta" proof(cases "i ∈ I") case True note i = True show ?thesis proof(cases "j ∈ I") case True thus ?thesis using i ij I fP unfolding partCompat_def compat_def by blast next case False hence "i ≠ j" using i by auto thus ?thesis using assms partCompat_gen_aux i ij by auto qed next case False note i = False show ?thesis proof(cases "j ∈ I") case True hence "j ≠ i" using i by auto hence "(f j, f i) ∈ theta" using assms partCompat_gen_aux[of theta P f I j i] True ij by auto thus ?thesis using theta unfolding sym_def by auto next case False note j = False show ?thesis proof(cases "I = {}") case True hence False using ij by simp thus ?thesis by simp next case False then obtain i0 where i0: "i0 ∈ I" by auto hence i0_not: "i0 ∉ {i,j}" using i j by auto have "(f i0, f i) ∈ theta" using assms i0 i0_not ij partCompat_gen_aux[of theta P f I i0 i] by blast hence "(f i, f i0) ∈ theta" using theta unfolding sym_def by auto moreover have "(f i0, f j) ∈ theta" using assms i0 i0_not ij partCompat_gen_aux[of theta P f I i0 j] by blast ultimately show ?thesis using theta unfolding trans_def by blast qed qed qed qed lemma partCompat_partGen: assumes "sym theta" and "trans theta" and "partCompat P theta f" shows "partCompat (partGen P) theta f" unfolding partCompat_def partGen_def using assms partCompat_gen[of theta P f] by auto lemma partCompat_partJoin[simp]: assumes "sym theta" and "trans theta" and "partCompat P theta f" and "partCompat Q theta f" shows "partCompat (partJoin P Q) theta f" by (metis assms partCompat_Un partCompat_partGen partJoin_def) text‹lift:› lemma inj_on_lift: assumes P: "part I0 P" and Q: "part I0 Q" and PQ: "finer P Q" and F: "inj_on F P" and FP: "part J0 (F ` P)" and emp: "{} ∉ F ` P" shows "inj_on (lift P F) Q" unfolding inj_on_def proof clarify fix II II' assume II: "II ∈ Q" and II': "II' ∈ Q" and eq: "lift P F II = lift P F II'" have 1: "II = Union {I ∈ P . I ⊆ II}" using PQ II unfolding finer_def by auto have 2: "II' = Union {I ∈ P . I ⊆ II'}" using PQ II' unfolding finer_def by auto {fix I assume I: "I ∈ P" "I ⊆ II" hence "F I ⊆ lift P F II" unfolding lift_def[abs_def] by blast hence 3: "F I ⊆ lift P F II'" unfolding eq . have "F I ≠ {}" using emp I FP by auto then obtain j where j: "j ∈ F I" by auto with 3 obtain I' where I': "I' ∈ P ∧ I' ⊆ II'" and "j ∈ F I'" unfolding lift_def [abs_def] by auto hence "F I Int F I' ≠ {}" using j by auto hence "F I = F I'" using FP I I' unfolding part_def by auto hence "I = I'" using F I I' unfolding inj_on_def by auto hence "I ⊆ II'" using I' by auto } hence a: "II ⊆ II'" using 1 2 by blast (* *) {fix I assume I: "I ∈ P" "I ⊆ II'" hence "F I ⊆ lift P F II'" unfolding lift_def [abs_def] by blast hence 3: "F I ⊆ lift P F II" unfolding eq . have "F I ≠ {}" using emp I FP by auto then obtain j where j: "j ∈ F I" by auto with 3 obtain I' where I': "I' ∈ P ∧ I' ⊆ II" and "j ∈ F I'" unfolding lift_def [abs_def] by auto hence "F I Int F I' ≠ {}" using j by auto hence "F I = F I'" using FP I I' unfolding part_def by auto hence "I = I'" using F I I' unfolding inj_on_def by auto hence "I ⊆ II" using I' by auto } hence "II' ⊆ II" using 1 2 by blast with a show "II = II'" by auto qed lemma part_lift: assumes P: "part I0 P" and Q: "part I0 Q" and PQ: "finer P Q" and F: "inj_on F P" and FP: "part J0 (F ` P)" and emp: "{} ∉ P" "{} ∉ F ` P" shows "part J0 (lift P F ` Q)" unfolding part_def proof (intro conjI allI impI) show "⋃(lift P F ` Q) = J0" proof safe fix j II assume "j ∈ lift P F II" and II: "II ∈ Q" then obtain I where "j ∈ F I" and "I ∈ P" and "I ⊆ II" unfolding lift_def by auto thus "j ∈ J0" using FP unfolding part_def by auto next fix j assume "j ∈ J0" then obtain J where J: "J ∈ F ` P" and j: "j ∈ J" using FP unfolding part_def by auto define I where "I = inv_into P F J" have j: "j ∈ F I" unfolding I_def using j J F by auto have I: "I ∈ P" unfolding I_def using F J by auto obtain II where "I ⊆ II" and "II ∈ Q" using P Q PQ I finer_ex[of I0 P Q I] by auto thus "j ∈ ⋃ (lift P F ` Q)" unfolding lift_def [abs_def] using j I by auto qed next fix JJ1 JJ2 assume JJ12: "JJ1 ∈ lift P F ` Q ∧ JJ2 ∈ lift P F ` Q ∧ JJ1 ≠ JJ2" then obtain II1 II2 where II12: "{II1,II2} ⊆ Q" and JJ1: "JJ1 = lift P F II1" and JJ2: "JJ2 = lift P F II2" by auto have "II1 ≠ II2" using JJ12 unfolding JJ1 JJ2 using II12 assms using inj_on_lift[of I0 P Q F] by auto hence 4: "II1 Int II2 = {}" using II12 Q unfolding part_def by auto show "JJ1 ∩ JJ2 = {}" proof(rule ccontr) assume "JJ1 ∩ JJ2 ≠ {}" then obtain j where j: "j ∈ JJ1" "j ∈ JJ2" by auto from j obtain I1 where "j ∈ F I1" and I1: "I1 ∈ P" "I1 ⊆ II1" unfolding JJ1 lift_def [abs_def] by auto moreover from j obtain I2 where "j ∈ F I2" and I2: "I2 ∈ P" "I2 ⊆ II2" unfolding JJ2 lift_def [abs_def] by auto ultimately have "F I1 Int F I2 ≠ {}" by blast hence "F I1 = F I2" using I1 I2 FP unfolding part_def by blast hence "I1 = I2" using I1 I2 F unfolding inj_on_def by auto moreover have "I1 ≠ {}" using I1 emp by auto ultimately have "II1 Int II2 ≠ {}" using I1 I2 by auto thus False using 4 by simp qed qed lemma finer_lift: assumes "finer P Q" shows "finer (F ` P) (lift P F ` Q)" unfolding finer_def proof (intro conjI ballI impI) fix JJ assume JJ: "JJ ∈ lift P F ` Q" show "JJ = ⋃ {J ∈ F ` P. J ⊆ JJ}" proof safe fix j assume j: "j ∈ JJ" obtain II where II: "II ∈ Q" and JJ: "JJ = lift P F II" using JJ by auto then obtain I where j: "j ∈ F I" and I: "I ∈ P ∧ I ⊆ II" and "F I ⊆ JJ" using j unfolding lift_def [abs_def] by auto thus "j ∈ ⋃{J ∈ F ` P. J ⊆ JJ}" using I j by auto qed auto next assume "F ` P ≠ {}" thus "lift P F ` Q ≠ {}" using assms unfolding lift_def [abs_def] finer_def by simp qed subsection ‹Basic setting for bisimilarity› locale PL_Indis = PL aval tval cval for aval :: "'atom ⇒ 'state ⇒ 'state" and tval :: "'test ⇒ 'state ⇒ bool" and cval :: "'choice ⇒ 'state ⇒ real" + fixes indis :: "'state rel" assumes equiv_indis: "equiv UNIV indis" (*******************************************) context PL_Indis begin no_notation eqpoll (infixl "≈" 50) abbreviation indisAbbrev (infix "≈" 50) where "s1 ≈ s2 ≡ (s1, s2) ∈ indis" lemma refl_indis: "refl indis" and trans_indis: "trans indis" and sym_indis: "sym indis" using equiv_indis unfolding equiv_def by auto lemma indis_refl[intro]: "s ≈ s" using refl_indis unfolding refl_on_def by simp lemma indis_trans[trans]: "⟦s ≈ s'; s' ≈ s''⟧ ⟹ s ≈ s''" using trans_indis unfolding trans_def by blast lemma indis_sym[sym]: "s ≈ s' ⟹ s' ≈ s" using sym_indis unfolding sym_def by blast subsection‹Discreetness› coinductive discr where intro: "(⋀ s i. i < brn c ⟶ s ≈ eff c s i ∧ discr (cont c s i)) ⟹ discr c" definition discrL where "discrL cl ≡ ∀ c ∈ set cl. discr c" lemma discrL_intro[intro]: assumes "⋀ c. c ∈ set cl ⟹ discr c" shows "discrL cl" using assms unfolding discrL_def by auto lemma discrL_discr[simp]: assumes "discrL cl" and "c ∈ set cl" shows "discr c" using assms unfolding discrL_def by simp lemma discrL_update[simp]: assumes cl: "discrL cl" and c': "discr c'" shows "discrL (cl[n := c'])" proof(cases "n < length cl") case True show ?thesis unfolding discrL_def proof safe fix c assume "c ∈ set (cl[n := c'])" hence "c ∈ insert c' (set cl)" using set_update_subset_insert by fastforce thus "discr c" using assms by (cases "c = c'") auto qed qed (insert cl, auto) text‹Coinduction for discreetness:› lemma discr_coind[consumes 1, case_names Hyp, induct pred: discr]: assumes *: "phi c" and **: "⋀ c s i. ⟦ phi c ; i < brn c⟧ ⟹ s ≈ eff c s i ∧ (phi (cont c s i) ∨ discr (cont c s i))" shows "discr c" using * apply(induct rule: discr.coinduct) using ** by auto lemma discr_raw_coind[consumes 1, case_names Hyp]: assumes *: "phi c" and **: "⋀ c s i. ⟦i < brn c; phi c⟧ ⟹ s ≈ eff c s i ∧ phi (cont c s i)" shows "discr c" using * apply(induct) using ** by blast text‹Discreetness versus transition:› lemma discr_cont[simp]: assumes *: "discr c" and **: "i < brn c" shows "discr (cont c s i)" using * apply(cases rule: discr.cases) using ** by blast lemma discr_eff_indis[simp]: assumes *: "discr c" and **: "i < brn c" shows "s ≈ eff c s i" using * apply(cases rule: discr.cases) using ** by blast subsection‹Self-isomorphism› coinductive siso where intro: "⟦⋀ s i. i < brn c ⟹ siso (cont c s i); ⋀ s t i. i < brn c ∧ s ≈ t ⟹ eff c s i ≈ eff c t i ∧ wt c s i = wt c t i ∧ cont c s i = cont c t i⟧ ⟹ siso c" definition sisoL where "sisoL cl ≡ ∀ c ∈ set cl. siso c" lemma sisoL_intro[intro]: assumes "⋀ c. c ∈ set cl ⟹ siso c" shows "sisoL cl" using assms unfolding sisoL_def by auto lemma sisoL_siso[simp]: assumes "sisoL cl" and "c ∈ set cl" shows "siso c" using assms unfolding sisoL_def by simp lemma sisoL_update[simp]: assumes cl: "sisoL cl" and c': "siso c'" shows "sisoL (cl[n := c'])" proof(cases "n < length cl") case True show ?thesis unfolding sisoL_def proof safe fix c assume "c ∈ set (cl[n := c'])" hence "c ∈ insert c' (set cl)" using set_update_subset_insert by fastforce thus "siso c" using assms by (cases "c = c'") auto qed qed (insert cl, auto) text‹Coinduction for self-isomorphism:› lemma siso_coind[consumes 1, case_names Obs Cont, induct pred: siso]: assumes *: "phi c" and **: "⋀ c s t i. ⟦i < brn c; phi c; s ≈ t⟧ ⟹ eff c s i ≈ eff c t i ∧ wt c s i = wt c t i ∧ cont c s i = cont c t i" and ***: "⋀ c s i. ⟦i < brn c; phi c⟧ ⟹ phi (cont c s i) ∨ siso (cont c s i)" shows "siso c" using * apply(induct rule: siso.coinduct) using ** *** by auto lemma siso_raw_coind[consumes 1, case_names Obs Cont]: assumes *: "phi c" and ***: "⋀ c s t i. ⟦i < brn c; phi c; s ≈ t⟧ ⟹ eff c s i ≈ eff c t i ∧ wt c s i = wt c t i ∧ cont c s i = cont c t i" and **: "⋀ c s i. ⟦i < brn c; phi c⟧ ⟹ phi (cont c s i)" shows "siso c" using * apply induct using ** *** by blast+ text‹Self-Isomorphism versus transition:› lemma siso_cont[simp]: assumes *: "siso c" and **: "i < brn c" shows "siso (cont c s i)" using * apply(cases rule: siso.cases) using ** by blast lemma siso_cont_indis[simp]: assumes *: "siso c" and **: "s ≈ t" "i < brn c" shows "eff c s i ≈ eff c t i ∧ wt c s i = wt c t i ∧ cont c s i = cont c t i" using * apply(cases rule: siso.cases) using ** by blast subsection‹Notions of bisimilarity› text‹Matchers› (* The notations are essentially the ones from the paper, except that, instead the paper's "Q" (which is redundant), we write "F P". Also, for the proper management of the proof, we have some intermediate predicates that compose the matchers. *) definition mC_C_part where "mC_C_part c d P F ≡ {} ∉ P ∧ {} ∉ F ` P ∧ part {..< brn c} P ∧ part {..< brn d} (F ` P)" definition mC_C_wt where "mC_C_wt c d s t P F ≡ ∀ I ∈ P. sum (wt c s) I = sum (wt d t) (F I)" definition mC_C_eff_cont where "mC_C_eff_cont theta c d s t P F ≡ ∀ I i j. I ∈ P ∧ i ∈ I ∧ j ∈ F I ⟶ eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ theta" definition mC_C where "mC_C theta 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 ∧ mC_C_eff_cont theta c d s t P F" definition matchC_C where "matchC_C theta c d ≡ ∀ s t. s ≈ t ⟶ (∃ P F. mC_C theta c d s t P F)" (* *) definition mC_ZOC_part where "mC_ZOC_part c d s t I0 P F ≡ {} ∉ P - {I0} ∧ {} ∉ F ` (P - {I0}) ∧ I0 ∈ P ∧ part {..< brn c} P ∧ part {..< brn d} (F ` P)" definition mC_ZOC_wt where "mC_ZOC_wt c d s t I0 P F ≡ sum (wt c s) I0 < 1 ∧ sum (wt d t) (F I0) < 1 ⟶ (∀ I ∈ P - {I0}. sum (wt c s) I / (1 - sum (wt c s) I0) = sum (wt d t) (F I) / (1 - sum (wt d t) (F I0)))" (* Note: In case either sum is 1, the above condition holds vacously. *) definition mC_ZOC_eff_cont0 where "mC_ZOC_eff_cont0 theta c d s t I0 F ≡ (∀ i ∈ I0. s ≈ eff c s i ∧ (cont c s i, d) ∈ theta) ∧ (∀ j ∈ F I0. t ≈ eff d t j ∧ (c, cont d t j) ∈ theta)" definition mC_ZOC_eff_cont where "mC_ZOC_eff_cont theta c d s t I0 P F ≡ ∀ I i j. I ∈ P - {I0} ∧ i ∈ I ∧ j ∈ F I ⟶ eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ theta" definition mC_ZOC where "mC_ZOC theta c d s t I0 P F ≡ mC_ZOC_part c d s t I0 P F ∧ inj_on F P ∧ mC_ZOC_wt c d s t I0 P F ∧ mC_ZOC_eff_cont0 theta c d s t I0 F ∧ mC_ZOC_eff_cont theta c d s t I0 P F" definition matchC_LC where "matchC_LC theta c d ≡ ∀ s t. s ≈ t ⟶ (∃ I0 P F. mC_ZOC theta c d s t I0 P F)" lemmas m_defs = mC_C_def mC_ZOC_def lemmas m_defsAll = mC_C_def mC_C_part_def mC_C_wt_def mC_C_eff_cont_def mC_ZOC_def mC_ZOC_part_def mC_ZOC_wt_def mC_ZOC_eff_cont0_def mC_ZOC_eff_cont_def lemmas match_defs = matchC_C_def matchC_LC_def lemma mC_C_mono: assumes "mC_C theta c d s t P F" and "theta ⊆ theta'" shows "mC_C theta' c d s t P F" using assms unfolding m_defsAll by fastforce+ lemma matchC_C_mono: assumes "matchC_C theta c d" and "theta ⊆ theta'" shows "matchC_C theta' c d" using assms mC_C_mono unfolding matchC_C_def by blast lemma mC_ZOC_mono: assumes "mC_ZOC theta c d s t I0 P F" and "theta ⊆ theta'" shows "mC_ZOC theta' c d s t I0 P F" using assms unfolding m_defsAll subset_eq by auto lemma matchC_LC_mono: assumes "matchC_LC theta c d" and "theta ⊆ theta'" shows "matchC_LC theta' c d" using assms mC_ZOC_mono unfolding matchC_LC_def by metis lemma Int_not_in_eq_emp: "P ∩ {I. I ∉ P} = {}" by blast lemma mC_C_mC_ZOC: assumes "mC_C theta c d s t P F" shows "mC_ZOC theta c d s t {} (P Un { {} }) (%I. if I ∈ P then F I else {})" (is "mC_ZOC theta c d s t ?I0 ?Q ?G") unfolding mC_ZOC_def proof(intro conjI) show "mC_ZOC_part c d s t ?I0 ?Q ?G" unfolding mC_ZOC_part_def using assms unfolding mC_C_def mC_C_part_def by (auto simp add: Int_not_in_eq_emp) next show "inj_on ?G ?Q" unfolding inj_on_def proof clarify fix I1 I2 assume I12: "I1 ∈ ?Q" "I2 ∈ ?Q" and G: "?G I1 = ?G I2" show "I1 = I2" proof(cases "I1 ∈ P") case True hence I2: "I2 ∈ P" apply(rule_tac ccontr) using G assms unfolding mC_C_def mC_C_part_def by auto with True G have "F I1 = F I2" by simp thus ?thesis using True I2 I12 assms unfolding mC_C_def inj_on_def by blast next case False note case1 = False hence I1: "I1 = {}" using I12 by blast show ?thesis proof(cases "I2 ∈ P") case False hence "I2 = {}" using I12 by blast thus ?thesis using I1 by blast next case True hence "I1 ∈ P" apply(rule_tac ccontr) using G assms unfolding mC_C_def mC_C_part_def by auto thus ?thesis using case1 by simp qed qed qed qed(insert assms, unfold m_defsAll, fastforce+) lemma matchC_C_matchC_LC: assumes "matchC_C theta c d" shows "matchC_LC theta c d" using assms mC_C_mC_ZOC unfolding match_defs by blast text‹Retracts:› (* Strong retract: *) definition Sretr where "Sretr theta ≡ {(c, d). matchC_C theta c d}" (* Zero-One retract: *) definition ZOretr where "ZOretr theta ≡ {(c,d). matchC_LC theta c d}" lemmas Retr_defs = Sretr_def ZOretr_def lemma mono_Retr: "mono Sretr" "mono ZOretr" unfolding mono_def Retr_defs by (auto simp add: matchC_C_mono matchC_LC_mono) lemma Retr_incl: "Sretr theta ⊆ ZOretr theta" unfolding Retr_defs using matchC_C_matchC_LC by blast+ text‹The associated bisimilarity relations:› definition Sbis where "Sbis ≡ gfp Sretr" definition ZObis where "ZObis ≡ gfp ZOretr" abbreviation Sbis_abbrev (infix "≈s" 55) where "c ≈s d ≡ (c, d) : Sbis" abbreviation ZObis_abbrev (infix "≈01" 55) where "c ≈01 d ≡ (c, d) : ZObis" lemmas bis_defs = Sbis_def ZObis_def (* Inclusions between bisimilarities: *) lemma bis_incl: "Sbis ≤ ZObis" unfolding bis_defs using Retr_incl gfp_mono by blast+ lemma bis_imp[simp]: "⋀ c1 c2. c1 ≈s c2 ⟹ c1 ≈01 c2" using bis_incl unfolding bis_defs by auto (* Sbis: *) lemma Sbis_prefix: "Sbis ≤ Sretr Sbis" unfolding Sbis_def using def_gfp_unfold mono_Retr(1) by blast lemma Sbis_fix: "Sretr Sbis = Sbis" unfolding Sbis_def by (metis def_gfp_unfold mono_Retr(1)) lemma Sbis_mC_C: assumes "c ≈s d" and "s ≈ t" shows "∃P F. mC_C Sbis c d s t P F" using assms Sbis_prefix unfolding Sretr_def matchC_C_def by auto lemma Sbis_coind: assumes "theta ≤ Sretr (theta Un Sbis)" shows "theta ≤ Sbis" using assms unfolding Sbis_def by (metis Sbis_def assms def_coinduct mono_Retr(1)) lemma Sbis_raw_coind: assumes "theta ≤ Sretr theta" shows "theta ≤ Sbis" proof- have "Sretr theta ⊆ Sretr (theta Un Sbis)" by (metis Un_upper1 monoD mono_Retr(1)) hence "theta ⊆ Sretr (theta Un Sbis)" using assms by blast thus ?thesis using Sbis_coind by blast qed (* Symmetry *) lemma mC_C_sym: assumes "mC_C theta c d s t P F" shows "mC_C (theta ^-1) d c t s (F ` P) (inv_into P F)" unfolding mC_C_def proof (intro conjI) show "mC_C_eff_cont (theta¯) d c t s (F ` P) (inv_into P F)" unfolding mC_C_eff_cont_def proof clarify fix i j I assume I: "I ∈ P" and j: "j ∈ F I" and "i ∈ inv_into P F (F I)" hence "i ∈ I" using assms unfolding mC_C_def by auto hence "eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ theta" using assms I j unfolding mC_C_def mC_C_eff_cont_def by auto thus "eff d t j ≈ eff c s i ∧ (cont d t j, cont c s i) ∈ theta¯" by (metis converseI indis_sym) qed qed(insert assms, unfold m_defsAll, auto) lemma matchC_C_sym: assumes "matchC_C theta c d" shows "matchC_C (theta ^-1) d c" unfolding matchC_C_def proof clarify fix t s assume "t ≈ s" hence "s ≈ t" by (metis indis_sym) then obtain P F where "mC_C theta c d s t P F" using assms unfolding matchC_C_def by blast hence "mC_C (theta¯) d c t s (F ` P) (inv_into P F)" using mC_C_sym by auto thus "∃Q G. mC_C (theta¯) d c t s Q G" by blast qed lemma Sretr_sym: assumes "sym theta" shows "sym (Sretr theta)" unfolding sym_def proof clarify fix c d assume "(c, d) ∈ Sretr theta" hence "(d, c) ∈ Sretr (theta ^-1)" unfolding Sretr_def using matchC_C_sym by simp thus "(d, c) ∈ Sretr theta" using assms by (metis sym_conv_converse_eq) qed lemma sym_Sbis: "sym Sbis" by (metis Sbis_def Sretr_sym mono_Retr(1) sym_gfp) lemma Sbis_sym: "c ≈s d ⟹ d ≈s c" using sym_Sbis unfolding sym_def by blast (* Transitivity: *) lemma mC_C_trans: assumes *: "mC_C theta1 c d s t P F" and **: "mC_C theta2 d e t u (F ` P) G" shows "mC_C (theta1 O theta2) c e s u P (G o F)" unfolding mC_C_def proof (intro conjI) show "mC_C_part c e P (G ∘ F)" using assms unfolding mC_C_def mC_C_part_def by (auto simp add: image_comp) next show "inj_on (G ∘ F) P" using assms unfolding mC_C_def by (auto simp add: comp_inj_on) next show "mC_C_eff_cont (theta1 O theta2) c e s u P (G ∘ F)" unfolding mC_C_eff_cont_def proof clarify fix I i k assume I: "I ∈ P" and i: "i ∈ I" and k: "k ∈ (G ∘ F) I" have "F I ≠ {}" using * I unfolding mC_C_def mC_C_part_def by auto then obtain j where j: "j ∈ F I" by auto have "eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ theta1" using I i j * unfolding mC_C_def mC_C_eff_cont_def by auto moreover have "eff d t j ≈ eff e u k ∧ (cont d t j, cont e u k) ∈ theta2" using I j k ** unfolding mC_C_def mC_C_eff_cont_def by auto ultimately show "eff c s i ≈ eff e u k ∧ (cont c s i, cont e u k) ∈ theta1 O theta2" using indis_trans by blast qed qed(insert assms, unfold m_defsAll, auto) lemma mC_C_finer: assumes *: "mC_C theta c d s t P F" and theta: "trans theta" and Q: "finer P Q" "finite Q" "{} ∉ Q" "part {..<brn c} Q" and c: "partCompat Q indis (eff c s)" "partCompat Q theta (cont c s)" shows "mC_C theta c d s t Q (lift P F)" unfolding mC_C_def proof (intro conjI) show "mC_C_part c d Q (lift P F)" unfolding mC_C_part_def proof(intro conjI) show "{} ∉ lift P F ` Q" unfolding lift_def [abs_def] proof clarify fix II assume 1: "{} = ⋃{F I |I. I ∈ P ∧ I ⊆ II}" and II: "II ∈ Q" hence "II ≠ {}" using Q by auto then obtain I where I: "I ∈ P" and "I ⊆ II" using Q II unfolding finer_def by blast hence "F I = {}" using 1 by auto thus False using * I unfolding mC_C_def mC_C_part_def by auto qed next show "part {..<brn d} (lift P F ` Q)" using Q * part_lift[of "{..<brn c}" P Q F "{..<brn d}"] unfolding mC_C_def mC_C_part_def by auto qed (insert Q, auto) next show "inj_on (lift P F) Q" using Q * inj_on_lift[of "{..<brn c}" P Q F "{..<brn d}"] unfolding mC_C_def mC_C_part_def by auto next show "mC_C_wt c d s t Q (lift P F)" unfolding mC_C_wt_def proof clarify fix II assume II: "II ∈ Q" define S where "S = {I ∈ P . I ⊆ II}" have II: "II = (UN I : S . id I)" using II Q unfolding finer_def S_def by auto have S: "⋀ I J. ⟦I : S; J : S; I ≠ J⟧ ⟹ id I Int id J = {}" "finite S" unfolding S_def using * finite_part[of "{..<brn c}" P] unfolding mC_C_def mC_C_part_def part_def by auto have SS: "∀I∈S. finite I" "∀i∈S. finite (F i)" unfolding S_def using * unfolding mC_C_def mC_C_part_def part_def apply simp_all apply (metis complete_lattice_class.Sup_upper finite_lessThan finite_subset) by (metis finite_UN finite_UnionD finite_lessThan) have SSS: "∀i∈S. ∀j∈S. i ≠ j ⟶ F i ∩ F j = {}" proof clarify fix I J assume "I ∈ S" and "J ∈ S" and diff: "I ≠ J" hence IJ: "{I,J} ⊆ P" unfolding S_def by simp hence "F I ≠ F J" using * diff unfolding mC_C_def inj_on_def by auto thus "F I ∩ F J = {}" using * IJ unfolding mC_C_def mC_C_part_def part_def by auto qed have "sum (wt c s) II = sum (sum (wt c s)) S" unfolding II using S SS sum.UNION_disjoint[of S id "wt c s"] by simp also have "... = sum (% I. sum (wt d t) (F I)) S" apply(rule sum.cong) using S apply force unfolding S_def using * unfolding mC_C_def mC_C_part_def mC_C_wt_def by auto also have "... = sum (wt d t) (UN I : S . F I)" unfolding lift_def using S sum.UNION_disjoint[of S F "wt d t"] S SS SSS by simp also have "(UN I : S . F I) = lift P F II" unfolding lift_def S_def by auto finally show "sum (wt c s) II = sum (wt d t) (lift P F II)" . qed next show "mC_C_eff_cont theta c d s t Q (lift P F)" unfolding mC_C_eff_cont_def proof clarify fix II i j assume II: "II ∈ Q" and i: "i ∈ II" and "j ∈ lift P F II" then obtain I where j: "j ∈ F I" and I: "I ∈ P ∧ I ⊆ II" unfolding lift_def by auto hence "I ≠ {}" using * unfolding mC_C_def mC_C_part_def by auto then obtain i' where i': "i' ∈ I" by auto hence 1: "eff c s i' ≈ eff d t j ∧ (cont c s i', cont d t j) ∈ theta" using * j I unfolding 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) ∈ theta" proof(cases "i' = i") case True show ?thesis using 1 unfolding True . next case False moreover have "i' ∈ II" using I i' by auto ultimately have "eff c s i ≈ eff c s i' ∧ (cont c s i, cont c s i') ∈ theta" using i II c unfolding partCompat_def compat_def by auto thus ?thesis using 1 indis_trans theta unfolding trans_def by blast qed qed qed lemma mC_C_partCompat_eff: assumes *: "mC_C theta c d s t P F" shows "partCompat P indis (eff c s)" unfolding partCompat_def compat_def proof clarify fix I i i' assume I: "I ∈ P" and ii': "{i, i'} ⊆ I" "i ≠ i'" hence "F I ≠ {}" using * unfolding m_defsAll by blast then obtain j where j: "j ∈ F I" by auto from ii' j I have 1: "eff c s i ≈ eff d t j" using * unfolding m_defsAll by blast from ii' j I have 2: "eff c s i' ≈ eff d t j" using * unfolding m_defsAll by blast from 1 2 show "eff c s i ≈ eff c s i'" using indis_trans indis_sym by blast qed lemma mC_C_partCompat_cont: assumes *: "mC_C theta c d s t P F" and theta: "sym theta" "trans theta" shows "partCompat P theta (cont c s)" unfolding partCompat_def compat_def proof clarify fix I i i' assume I: "I ∈ P" and ii': "{i, i'} ⊆ I" "i ≠ i'" hence "F I ≠ {}" using * unfolding m_defsAll by blast then obtain j where j: "j ∈ F I" by auto from ii' j I have 1: "(cont c s i, cont d t j) ∈ theta" using * unfolding m_defsAll by blast from ii' j I have 2: "(cont c s i', cont d t j) ∈ theta" using * unfolding m_defsAll by blast from 1 2 show "(cont c s i, cont c s i') ∈ theta" using theta unfolding trans_def sym_def by blast qed lemma matchC_C_sym_trans: assumes *: "matchC_C theta c1 c" and **: "matchC_C theta c c2" and theta: "sym theta" "trans theta" shows "matchC_C theta c1 c2" unfolding matchC_C_def proof clarify fix s1 s2 assume s1s2: "s1 ≈ s2" define s where "s = s1" have s: "s ≈ s1 ∧ s ≈ s2" unfolding s_def using s1s2 by auto have th: "theta ^-1 = theta" "theta O theta ⊆ theta" using theta by (metis sym_conv_converse_eq trans_O_subset)+ hence *: "matchC_C theta c c1" by (metis * matchC_C_sym) from s * obtain P1 F1 where m1: "mC_C theta c c1 s s1 P1 F1" unfolding matchC_C_def by blast from s ** obtain P2 F2 where m2: "mC_C theta c c2 s s2 P2 F2" unfolding matchC_C_def by blast define P where "P = partJoin P1 P2" (* *) have P: "finer P1 P ∧ finer P2 P ∧ finite P ∧ {} ∉ P ∧ part {..< brn c} P" using m1 m2 finer_partJoin_L finite_partJoin emp_partJoin part_partJoin finite_part[of "{..< brn c}" P] unfolding P_def mC_C_def mC_C_part_def by force (* *) have "mC_C theta c c1 s s1 P (lift P1 F1)" proof(rule mC_C_finer) show "partCompat P indis (eff c s)" unfolding P_def apply(rule partCompat_partJoin) using m1 m2 sym_indis trans_indis mC_C_partCompat_eff by auto next show "partCompat P theta (cont c s)" unfolding P_def apply(rule partCompat_partJoin) using m1 m2 theta mC_C_partCompat_cont by auto qed(insert P m1 theta, auto) hence A: "mC_C theta c1 c s1 s (lift P1 F1 ` P) (inv_into P (lift P1 F1))" using mC_C_sym[of theta c c1 s s1 P "lift P1 F1"] unfolding th by blast (* *) have B: "mC_C theta c c2 s s2 P (lift P2 F2)" proof(rule mC_C_finer) show "partCompat P indis (eff c s)" unfolding P_def apply(rule partCompat_partJoin) using m1 m2 sym_indis trans_indis mC_C_partCompat_eff by auto next show "partCompat P theta (cont c s)" unfolding P_def apply(rule partCompat_partJoin) using m1 m2 theta mC_C_partCompat_cont by auto qed(insert P m2 theta, auto) (* *) have "inj_on (lift P1 F1) P" apply(rule inj_on_lift) using m1 m2 P unfolding m_defsAll by auto hence "inv_into P (lift P1 F1) ` lift P1 F1 ` P = P" by (metis inj_on_inv_into) hence "mC_C (theta O theta) c1 c2 s1 s2 (lift P1 F1 ` P) (lift P2 F2 o (inv_into P (lift P1 F1)))" apply - apply(rule mC_C_trans[of theta c1 c s1 s _ _ theta c2 s2]) using A B by auto hence "mC_C theta c1 c2 s1 s2 (lift P1 F1 ` P) (lift P2 F2 o (inv_into P (lift P1 F1)))" using th mC_C_mono by blast thus "∃R H. mC_C theta c1 c2 s1 s2 R H" by blast qed lemma Sretr_sym_trans: assumes "sym theta ∧ trans theta" shows "trans (Sretr theta)" unfolding trans_def proof clarify fix c d e assume "(c, d) ∈ Sretr theta" and "(d, e) ∈ Sretr theta" thus "(c, e) ∈ Sretr theta" unfolding Sretr_def using assms matchC_C_sym_trans by blast qed lemma trans_Sbis: "trans Sbis" by (metis Sbis_def Sretr_sym Sretr_sym_trans mono_Retr sym_trans_gfp) lemma Sbis_trans: "⟦c ≈s d; d ≈s e⟧ ⟹ c ≈s e" using trans_Sbis unfolding trans_def by blast (* ZObis: *) lemma ZObis_prefix: "ZObis ≤ ZOretr ZObis" unfolding ZObis_def using def_gfp_unfold mono_Retr(2) by blast lemma ZObis_fix: "ZOretr ZObis = ZObis" unfolding ZObis_def by (metis def_gfp_unfold mono_Retr(2)) lemma ZObis_mC_ZOC: assumes "c ≈01 d" and "s ≈ t" shows "∃I0 P F. mC_ZOC ZObis c d s t I0 P F" using assms ZObis_prefix unfolding ZOretr_def matchC_LC_def by blast lemma ZObis_coind: assumes "theta ≤ ZOretr (theta Un ZObis)" shows "theta ≤ ZObis" using assms unfolding ZObis_def by (metis ZObis_def assms def_coinduct mono_Retr(2)) lemma ZObis_raw_coind: assumes "theta ≤ ZOretr theta" shows "theta ≤ ZObis" proof- have "ZOretr theta ⊆ ZOretr (theta Un ZObis)" by (metis Un_upper1 monoD mono_Retr) hence "theta ⊆ ZOretr (theta Un ZObis)" using assms by blast thus ?thesis using ZObis_coind by blast qed (* Symmetry *) lemma mC_ZOC_sym: assumes theta: "sym theta" and *: "mC_ZOC theta c d s t I0 P F" shows "mC_ZOC theta d c t s (F I0) (F ` P) (inv_into P F)" unfolding mC_ZOC_def proof (intro conjI) show "mC_ZOC_part d c t s (F I0) (F ` P) (inv_into P F)" unfolding mC_ZOC_part_def proof(intro conjI) have 0: "inj_on F P" "I0 ∈ P" using * unfolding mC_ZOC_def mC_ZOC_part_def by blast+ have "inv_into P F ` (F ` P - {F I0}) = inv_into P F ` (F ` (P - {I0}))" using 0 inj_on_image_set_diff[of F P P "{I0}", OF _ Set.Diff_subset] by simp also have "... = P - {I0}" using 0 by (metis Diff_subset inv_into_image_cancel) finally have "inv_into P F ` (F ` P - {F I0}) = P - {I0}" . thus "{} ∉ inv_into P F ` (F ` P - {F I0})" using * unfolding mC_ZOC_def mC_ZOC_part_def by simp (* *) have "part {..<brn c} P" using * unfolding mC_ZOC_def mC_ZOC_part_def by blast thus "part {..<brn c} (inv_into P F ` F ` P)" using 0 by auto qed(insert *, unfold mC_ZOC_def mC_ZOC_part_def, blast+) next have 0: "inj_on F P" "I0 ∈ P" using * unfolding mC_ZOC_def mC_ZOC_part_def by blast+ show "mC_ZOC_wt d c t s (F I0) (F ` P) (inv_into P F)" unfolding mC_ZOC_wt_def proof(intro conjI ballI impI) fix J assume "J ∈ F ` P - {F I0}" and le_1: "sum (wt d t) (F I0) < 1 ∧ sum (wt c s) (inv_into P F (F I0)) < 1" then obtain I where I: "I ∈ P - {I0}" and J: "J = F I" by (metis image_iff member_remove remove_def) have 2: "inv_into P F J = I" unfolding J using 0 I by simp have 3: "inv_into P F (F I0) = I0" using 0 by simp show "sum (wt d t) J / (1 - sum (wt d t) (F I0)) = sum (wt c s) (inv_into P F J) / (1 - sum (wt c s) (inv_into P F (F I0)))" unfolding 2 3 unfolding J using * I le_1 unfolding mC_ZOC_def mC_ZOC_wt_def by (metis 3 J) qed next show "mC_ZOC_eff_cont theta d c t s (F I0) (F ` P) (inv_into P F)" unfolding mC_ZOC_eff_cont_def proof(intro allI impI, elim conjE) fix i j J assume "J ∈ F ` P - {F I0}" and j: "j ∈ J" and i: "i ∈ inv_into P F J" then obtain I where J: "J = F I" and I: "I ∈ P - {I0}" by (metis image_iff member_remove remove_def) hence "i ∈ I" using assms i unfolding mC_ZOC_def by auto hence "eff c s i ≈ eff d t j ∧ (cont c s i, cont d t j) ∈ theta" using assms I j unfolding mC_ZOC_def mC_ZOC_eff_cont_def J by auto thus "eff d t j ≈ eff c s i ∧ (cont d t j, cont c s i) ∈ theta" by (metis assms indis_sym sym_def) qed qed(insert assms, unfold sym_def m_defsAll, auto) lemma matchC_LC_sym: assumes *: "sym theta" and "matchC_LC theta c d" shows "matchC_LC theta d c" unfolding matchC_LC_def proof clarify fix t s assume "t ≈ s" hence "s ≈ t" by (metis indis_sym) then obtain I0 P F where "mC_ZOC theta c d s t I0 P F" using assms unfolding matchC_LC_def by blast hence "mC_ZOC theta d c t s (F I0) (F ` P) (inv_into P F)" using mC_ZOC_sym * by auto thus "∃I0 Q G. mC_ZOC theta d c t s I0 Q G" by blast qed lemma ZOretr_sym: assumes "sym theta" shows "sym (ZOretr theta)" unfolding sym_def proof clarify fix c d assume "(c, d) ∈ ZOretr theta" hence "(d, c) ∈ ZOretr theta" unfolding ZOretr_def using assms matchC_LC_sym by simp thus "(d, c) ∈ ZOretr theta" using assms by (metis sym_conv_converse_eq) qed lemma sym_ZObis: "sym ZObis" by (metis ZObis_def ZOretr_sym mono_Retr sym_gfp) lemma ZObis_sym: "c ≈01 d ⟹ d ≈01 c" using sym_ZObis unfolding sym_def by blast subsection ‹List versions of the bisimilarities› (* For Sbis: *) definition SbisL where "SbisL cl dl ≡ length cl = length dl ∧ (∀ n < length cl. cl ! n ≈s dl ! n)" lemma SbisL_intro[intro]: assumes "length cl = length dl" and "⋀ n. ⟦n < length cl; n < length dl⟧ ⟹ cl ! n ≈s dl ! n" shows "SbisL cl dl" using assms unfolding SbisL_def by auto lemma SbisL_length[simp]: assumes "SbisL cl dl" shows "length cl = length dl" using assms unfolding SbisL_def by simp lemma SbisL_Sbis[simp]: assumes "SbisL cl dl" and "n < length cl ∨ n < length dl" shows "cl ! n ≈s dl ! n" using assms unfolding SbisL_def by simp lemma SbisL_update[simp]: assumes cldl: "SbisL cl dl" and c'd': "c' ≈s d'" shows "SbisL (cl [n := c']) (dl [n := d'])" (is "SbisL ?cl' ?dl'") proof(cases "n < length cl") case True show ?thesis proof fix m assume m: "m < length ?cl'" "m < length ?dl'" thus "?cl' ! m ≈s ?dl' ! m" using assms by (cases "m = n") auto qed (insert cldl, simp) qed (insert cldl, simp) lemma SbisL_update_L[simp]: assumes "SbisL cl dl" and "c' ≈s dl!n" shows "SbisL (cl[n := c']) dl" proof- let ?d' = "dl!n" have "SbisL (cl[n := c']) (dl[n := ?d'])" apply(rule SbisL_update) using assms by auto thus ?thesis by simp qed lemma SbisL_update_R[simp]: assumes "SbisL cl dl" and "cl!n ≈s d'" shows "SbisL cl (dl[n := d'])" proof- let ?c' = "cl!n" have "SbisL (cl[n := ?c']) (dl[n :=