# Theory Resumption_Based

```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
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 :=```