Theory Resumption_Based
section ‹Resumption-Based Noninterference›
theory Resumption_Based
imports Language_Semantics
begin
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›
definition part where
"part J P ≡
Union P = J ∧
(∀ J1 J2. J1 ∈ P ∧ J2 ∈ P ∧ J1 ≠ J2 ⟶ J1 ∩ J2 = {})"
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"
definition partGen where
"partGen P ≡ {gen P I | I . I ∈ P}"
definition finer where
"finer P Q ≡
(∀ J ∈ Q. J = Union {I ∈ P . I ⊆ J}) ∧
(P ≠ {} ⟶ Q ≠ {})"
definition partJoin where
"partJoin P Q ≡ partGen (P ∪ Q)"
definition compat where
"compat I theta f ≡ ∀ i j. {i, j} ⊆ I ∧ i ≠ j ⟶ (f i, f j) ∈ theta"
definition partCompat where
"partCompat P theta f ≡
∀ I ∈ P. compat I theta f"
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›
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)))"
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:›
definition Sretr where
"Sretr theta ≡
{(c, d). matchC_C theta c d}"
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
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
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
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
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
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
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›
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 :=