Theory Trace_Based
section‹Trace-Based Noninterference›
theory Trace_Based
imports Resumption_Based
begin
subsection‹Preliminaries›
lemma dist_sum:
fixes f :: "'a ⇒ real" and g :: "'a ⇒ real"
assumes "⋀i. i ∈ I ⟹ dist (f i) (g i) ≤ e i"
shows "dist (∑i∈I. f i) (∑i∈I. g i) ≤ (∑i∈I. e i)"
proof cases
assume "finite I" from this assms show ?thesis
proof induct
case (insert i I)
then have "dist (∑i∈insert i I. f i) (∑i∈insert i I. g i) ≤ dist (f i) (g i) + dist (∑i∈I. f i) (∑i∈I. g i)"
by (simp add: dist_triangle_add)
also have "… ≤ e i + (∑i∈I. e i)"
using insert by (intro add_mono) auto
finally show ?case using insert by simp
qed simp
qed simp
lemma dist_mult[simp]: "dist (x * y) (x * z) = ¦x¦ * dist y z"
unfolding dist_real_def abs_mult[symmetric] right_diff_distrib ..
lemma dist_divide[simp]: "dist (y / r) (z / r) = dist y z / ¦r¦"
unfolding dist_real_def abs_divide[symmetric] diff_divide_distrib ..
lemma dist_weighted_sum:
fixes f :: "'a ⇒ real" and g :: "'b ⇒ real"
assumes eps: "⋀i j. i ∈ I ⟹ j ∈ J ⟹ w i ≠ 0 ⟹ v j ≠ 0 ⟹ dist (f i) (g j) ≤ d i + e j"
and pos: "⋀i. i∈I ⟹ 0 ≤ w i" "⋀j. j∈J ⟹ 0 ≤ v j"
and sum: "(∑i∈I. w i) = 1" "(∑j∈J. v j) = 1"
shows "dist (∑i∈I. w i * f i) (∑j∈J. v j * g j) ≤ (∑i∈I. w i * d i) + (∑j∈J. v j * e j)"
proof -
let "?W h" = "(∑(i,j)∈I×J. (w i * v j) * h (i,j))"
{ fix g :: "'b ⇒ real"
have "(∑j∈J. v j * g j) = (∑i∈I. w i) * (∑j∈J. v j * g j)"
using sum by simp
also have "… = ?W (g∘snd)"
by (simp add: ac_simps sum_product sum.cartesian_product)
finally have "(∑j∈J. v j * g j) = ?W (g∘snd)" . }
moreover
{ fix f :: "'a ⇒ real"
have "(∑i∈I. w i * f i) = (∑i∈I. w i * f i) * (∑j∈J. v j)"
using sum by simp
also have "… = ?W (f∘fst)"
unfolding sum_product sum.cartesian_product by (simp add: ac_simps)
finally have "(∑i∈I. w i * f i) = ?W (f∘fst)" . }
moreover
{ have "dist (?W (f∘fst)) (?W (g∘snd)) ≤ ?W (λ(i,j). d i + e j)"
using eps pos
by (intro dist_sum)
(auto simp: mult_le_cancel_left zero_less_mult_iff mult_le_0_iff not_le[symmetric])
also have "… = ?W (d ∘ fst) + ?W (e ∘ snd)"
by (auto simp add: sum.distrib[symmetric] field_simps intro!: sum.cong)
finally have "dist (?W (f∘fst)) (?W (g∘snd)) ≤ ?W (d ∘ fst) + ?W (e ∘ snd)" by simp }
ultimately show ?thesis by simp
qed
lemma field_abs_le_zero_epsilon:
fixes x :: "'a::{linordered_field}"
assumes epsilon: "⋀e. 0 < e ⟹ ¦x¦ ≤ e"
shows "¦x¦ = 0"
proof (rule antisym)
show "¦x¦ ≤ 0"
proof (rule field_le_epsilon)
fix e :: 'a assume "0 < e" then show "¦x¦ ≤ 0 + e" by simp fact
qed
qed simp
lemma nat_nat_induct[case_names less]:
fixes P :: "nat ⇒ nat ⇒ bool"
assumes less: "⋀n m. (⋀j k. j + k < n + m ⟹ P j k) ⟹ P n m"
shows "P n m"
proof -
define N where "N ≡ n + m"
then show ?thesis
proof (induct N arbitrary: n m rule: nat_less_induct)
case 1 show "P n m"
apply (rule less)
apply (rule 1[rule_format])
apply auto
done
qed
qed
lemma part_insert:
assumes "part A P" assumes "X ∩ A = {}"
shows "part (A ∪ X) (insert X P)"
using assms by (auto simp: part_def)
lemma part_insert_subset:
assumes X: "part (A - X) P" "X ⊆ A"
shows "part A (insert X P)"
using X part_insert[of "A - X" P X] by (simp add: Un_absorb2)
lemma part_is_subset:
"part S P ⟹ p ∈ P ⟹ p ⊆ S"
unfolding part_def by (metis Union_upper)
lemma dist_nonneg_bounded:
fixes l u x y :: real
assumes "l ≤ x" "x ≤ u" "l ≤ y" "y ≤ u"
shows "dist x y ≤ u - l"
using assms unfolding dist_real_def by arith
lemma integrable_count_space_finite_support:
fixes f :: "'a ⇒ 'b::{banach,second_countable_topology}"
shows "finite {x∈X. f x ≠ 0} ⟹ integrable (count_space X) f"
by (auto simp: nn_integral_count_space integrable_iff_bounded)
lemma lebesgue_integral_point_measure:
fixes g :: "_ ⇒ real"
assumes f: "finite {a∈A. 0 < f a ∧ g a ≠ 0}"
shows "integral⇧L (point_measure A f) g = (∑a|a∈A ∧ 0 < f a ∧ g a ≠ 0. f a * g a)"
proof -
have eq: "{a ∈ A. max 0 (f a) ≠ 0 ∧ g a ≠ 0} = {a∈A. 0 < f a ∧ g a ≠ 0}"
by auto
have *: "ennreal (f x) = ennreal (max 0 (f x))" for x
by (cases "0 ≤ f x") (auto simp: max.absorb1 ennreal_neg)
show ?thesis
unfolding point_measure_def *
using f
apply (subst integral_real_density)
apply (auto simp add: integral_real_density lebesgue_integral_count_space_finite_support eq
intro!: sum.cong)
done
qed
lemma (in finite_measure) finite_measure_dist:
assumes AE: "AE x in M. x ∉ C ⟶ (x ∈ A ⟷ x ∈ B)"
assumes sets: "A ∈ sets M" "B ∈ sets M" "C ∈ sets M"
shows "dist (measure M A) (measure M B) ≤ measure M C"
proof -
{ have "measure M A ≤ measure M (B ∪ C)"
using AE sets by (auto intro: finite_measure_mono_AE)
also have "… ≤ measure M B + measure M C"
using sets by (auto intro: finite_measure_subadditive)
finally have A: "measure M A ≤ measure M B + measure M C" . }
moreover
{ have "measure M B ≤ measure M (A ∪ C)"
using AE sets by (auto intro: finite_measure_mono_AE)
also have "… ≤ measure M A + measure M C"
using sets by (auto intro: finite_measure_subadditive)
finally have B: "measure M B ≤ measure M A + measure M C" . }
ultimately show ?thesis
by (simp add: dist_real_def)
qed
lemma (in prob_space) prob_dist:
assumes AE: "AE x in M. ¬ C x ⟶ (A x ⟷ B x)"
assumes sets: "Measurable.pred M A" "Measurable.pred M B" "Measurable.pred M C"
shows "dist 𝒫(x in M. A x) 𝒫(x in M. B x) ≤ 𝒫(x in M. C x)"
using assms by (intro finite_measure_dist) auto
lemma Least_eq_0_iff: "(∃i::nat. P i) ⟹ (LEAST i. P i) = 0 ⟷ P 0"
by (metis LeastI_ex neq0_conv not_less_Least)
lemma case_nat_comp_Suc[simp]: "case_nat x f ∘ Suc = f"
by auto
lemma sum_eq_0_iff:
fixes f :: "_ ⇒ 'a :: {comm_monoid_add,ordered_ab_group_add}"
shows "finite A ⟹ (⋀i. i ∈ A ⟹ 0 ≤ f i) ⟹ (∑i∈A. f i) = 0 ⟷ (∀i∈A. f i = 0)"
apply rule
apply (blast intro: sum_nonneg_0)
apply simp
done
lemma sum_less_0_iff:
fixes f :: "_ ⇒ 'a :: {comm_monoid_add,ordered_ab_group_add}"
shows "finite A ⟹ (⋀i. i ∈ A ⟹ 0 ≤ f i) ⟹ 0 < (∑i∈A. f i) ⟷ (∃i∈A. 0 < f i)"
using sum_nonneg[of A f] sum_eq_0_iff[of A f] by (simp add: less_le)
context PL_Indis
begin
declare emp_gen[simp del]
interpretation pmf_as_function .
lift_definition wt_pmf :: "('test, 'atom, 'choice) cmd × 'state ⇒ nat pmf" is
"λ(c, s) i. if proper c then if i < brn c then wt c s i else 0 else if i = 0 then 1 else 0"
proof
let ?f = "λ(c, s) i. if proper c then if i < brn c then wt c s i else 0 else if i = 0 then 1 else 0"
fix cf show "∀i. 0 ≤ ?f cf i"
by (auto split: prod.split)
show "(∫⇧+i. ?f cf i ∂count_space UNIV) = 1"
by (subst nn_integral_count_space'[where A="if proper (fst cf) then {..<brn (fst cf)} else {0}" for n])
(auto split: prod.split)
qed
definition trans :: "('test, 'atom, 'choice) cmd × 'state ⇒ (('test, 'atom, 'choice) cmd × 'state) pmf" where
"trans cf = map_pmf (λi. if proper (fst cf) then cont_eff cf i else cf) (wt_pmf cf)"
sublocale T?: MC_syntax trans .
abbreviation "G cf ≡ set_pmf (trans cf)"
lemma set_pmf_map: "set_pmf (map_pmf f M) = f ` set_pmf M"
using pmf_set_map[of f] by (simp add: comp_def fun_eq_iff)
lemma set_pmf_wt:
"set_pmf (wt_pmf cf) = (if proper (fst cf) then {i. i < brn (fst cf) ∧ 0 < wt (fst cf) (snd cf) i} else {0})"
by (auto simp: set_eq_iff set_pmf_iff wt_pmf.rep_eq split: prod.split) (metis less_le wt_ge_0)
lemma G_eq:
"G cf = (if proper (fst cf) then {cont_eff cf i | i. i < brn (fst cf) ∧ 0 < wt (fst cf) (snd cf) i } else {cf})"
by (auto simp add: trans_def set_pmf_map set_pmf_wt)
lemma discrCf_G: "discrCf cf ⟹ cf' ∈ G cf ⟹ discrCf cf'"
using discrCf_cont[of cf] by (auto simp: G_eq split: if_split_asm)
lemma measurable_discrCf[measurable]: "Measurable.pred (count_space UNIV) discrCf"
by auto
lemma measurable_indis[measurable]: "Measurable.pred (count_space UNIV) (λx. snd x ≈ c)"
by auto
lemma integral_trans:
"proper (fst cf) ⟹
(∫x. f x ∂trans cf) = (∑i<brn (fst cf). wt (fst cf) (snd cf) i * f (cont_eff cf i))"
unfolding trans_def map_pmf_rep_eq
apply (simp add: integral_distr)
apply (subst integral_measure_pmf[of "{..< brn (fst cf)}"])
apply (auto simp: set_pmf_wt mult_ac wt_pmf.rep_eq split: prod.split)
done
subsection "Quasi strong termination traces"
abbreviation "qsend ≡ sfirst (holds discrCf)"
lemma qsend_eq_0_iff: "qsend cfT = 0 ⟷ discrCf (shd cfT)"
by (simp add: sfirst.simps[of _ cfT])
lemma qsend_eq_0[simp]: "discrCf cf ⟹ qsend (cf ## ω) = 0"
by (simp add: qsend_eq_0_iff)
lemma alw_discrCf: "enabled cf ω ⟹ discrCf cf ⟹ alw (holds discrCf) ω"
by (coinduction arbitrary: cf ω)
(auto simp add: HLD_iff elim: enabled.cases intro: discrCf_G simp del: split_paired_Ex)
lemma alw_discrCf_indis':
"enabled cf ω ⟹ discrCf cf ⟹ snd cf ≈ t ⟹ alw (holds (λcf'. snd cf' ≈ t)) ω"
proof (coinduction arbitrary: cf ω)
case alw with discrCf_eff_indis[of cf] show ?case
by (auto simp add: HLD_iff enabled.simps[of _ ω] G_eq
simp del: split_paired_Ex discrCf_eff_indis
intro!: exI[of _ "shd ω"]
split: if_split_asm)
(blast intro: indis_trans indis_sym)+
qed
lemma alw_discrCf_indis:
"enabled cf ω ⟹ discrCf cf ⟹ alw (holds (λcf'. snd cf' ≈ snd cf)) (cf ## ω)"
using alw_discrCf_indis'[of cf ω, OF _ _ indis_refl]
by (simp add: alw.simps[of _ "cf ## ω"] indis_refl)
lemma enabled_sdrop: "enabled cf ω ⟹ enabled ((cf ## ω) !! n) (sdrop n ω)"
proof (induction n arbitrary: cf ω)
case (Suc n) from Suc.IH[of "shd ω" "stl ω"] Suc.prems show ?case
unfolding enabled.simps[of cf] by simp
qed simp
lemma sfirst_eq_eSuc: "sfirst P ω = eSuc n ⟷ (¬ P ω) ∧ sfirst P (stl ω) = n"
by (subst sfirst.simps) auto
lemma qsend_snth: "qsend ω = enat n ⟹ discrCf (ω !! n)"
by (induction n arbitrary: ω)
(simp_all add: eSuc_enat[symmetric] enat_0 sfirst_eq_0 sfirst_eq_eSuc)
lemma indis_iff: "a ≈ d ⟹ b ≈ d ⟹ a ≈ c ⟷ b ≈ c"
by (metis indis_trans indis_sym indis_refl)
lemma enabled_qsend_indis:
assumes "enabled cf ω" "qsend (cf ## ω) ≤ n" "qsend (cf ## ω) ≤ m"
shows "snd ((cf ## ω) !! n) ≈ t ⟷ snd ((cf ## ω) !! m) ≈ t"
proof -
from assms obtain N :: nat where N: "qsend (cf ## ω) = N"
by (cases "qsend (cf ## ω)") auto
note discr_N = qsend_snth[OF this] and sd = enabled_sdrop[OF assms(1), of N]
have "⋀ω. ω !! N ## sdrop N (stl ω) = sdrop N ω"
by (induct N) auto
from this[of "cf ## ω"] have eq: "(cf ## ω) !! N ## sdrop N ω = sdrop N (cf ## ω)"
by simp
from discr_N alw_discrCf_indis[OF sd _] assms(2,3) show ?thesis
by (simp add: N alw_iff_sdrop le_iff_add[where 'a=nat] eq)
(metis indis_iff)
qed
lemma enabled_imp_UNTIL_alw_discrCf:
"enabled (shd ω) (stl ω) ⟹ (not (holds discrCf) until (alw (holds discrCf))) ω"
proof (coinduction arbitrary: ω)
case UNTIL then show ?case
using alw_discrCf[of "shd ω" "stl ω"]
by (cases "discrCf (shd ω)")
(simp_all add: enabled.simps[of "shd ω"] alw.simps[of _ ω])
qed
lemma less_qsend_iff_not_discrCf:
"enabled cf bT ⟹ n < qsend (cf ## bT) ⟷ ¬ discrCf ((cf ## bT) !! n)"
using enabled_imp_UNTIL_alw_discrCf[THEN less_sfirst_iff, of "cf ## bT"]
by (simp add: holds.simps[abs_def])
subsection "Terminating configurations"
definition "qstermCf cf ⟷ (∀cfT. enabled cf cfT ⟶ qsend (cf ## cfT) < ∞)"
lemma qstermCf_E:
"qstermCf cf ⟹ cf' ∈ G cf ⟹ qstermCf cf'"
apply (auto simp: qstermCf_def)
apply (erule_tac x="cf' ## cfT" in allE)
apply (auto simp: sfirst_Stream intro: enat_0 discrCf_G split: if_split_asm intro: enabled.intros)
done
abbreviation "eff_at cf bT n ≡ snd ((cf ## bT) !! n)"
abbreviation "cont_at cf bT n ≡ fst ((cf ## bT) !! n)"
definition "amSec c ⟷ (∀s1 s2 n t. s1 ≈ s2 ⟶
𝒫(bT in T.T (c, s1). eff_at (c, s1) bT n ≈ t) =
𝒫(bT in T.T (c, s2). eff_at (c, s2) bT n ≈ t))"
definition "eSec c ⟷ (∀s1 s2 t. s1 ≈ s2 ⟶
𝒫(bT in T.T (c, s1). ∃n. qsend ((c, s1) ## bT) = n ∧ eff_at (c, s1) bT n ≈ t) =
𝒫(bT in T.T (c, s2). ∃n. qsend ((c, s2) ## bT) = n ∧ eff_at (c, s2) bT n ≈ t))"
definition "aeT c ⟷ (∀s. AE bT in T.T (c,s). qsend ((c,s) ## bT) < ∞)"
lemma dist_Ps_upper_bound:
fixes cf1 cf2 :: "('test, 'atom, 'choice) cmd × 'state" and s :: "'state" and S
defines "S cf bT ≡ ∃n. qsend (cf ## bT) = n ∧ eff_at cf bT n ≈ s"
defines "Ps cf ≡ 𝒫(bT in T.T cf. S cf bT)"
defines "N cf n bT ≡ ¬ discrCf ((cf ## bT) !! n)"
defines "Pn cf n ≡ 𝒫(bT in T.T cf. N cf n bT)"
assumes bisim: "proper (fst cf1)" "proper (fst cf2)" "fst cf1 ≈01 fst cf2" "snd cf1 ≈ snd cf2"
shows "dist (Ps cf1) (Ps cf2) ≤ Pn cf1 n + Pn cf2 m"
using bisim proof (induct n m arbitrary: cf1 cf2 rule: nat_nat_induct)
case (less n m)
note ‹proper (fst cf1)›[simp, intro]
note ‹proper (fst cf2)›[simp, intro]
define W where "W c = sum (wt (fst c) (snd c))" for c
from ZObis_mC_ZOC[OF ‹fst cf1 ≈01 fst cf2› ‹snd cf1 ≈ snd cf2›]
obtain I0 P F where mC: "mC_ZOC ZObis (fst cf1) (fst cf2) (snd cf1) (snd cf2) I0 P F" by blast
then have P: "{} ∉ P - {I0}" "part {..<brn (fst cf1)} P" and "I0 ∈ P"
and FP: "{} ∉ F`(P-{I0})" "part {..<brn (fst cf2)} (F`P)" "inj_on F P"
and eff: "⋀q i j. q∈P ⟹ q≠I0 ⟹ i∈q ⟹ j∈F q ⟹ eff (fst cf1) (snd cf1) i ≈ eff (fst cf2) (snd cf2) j"
and cont: "⋀q i j. q∈P ⟹ q≠I0 ⟹ i∈q ⟹ j∈F q ⟹ cont (fst cf1) (snd cf1) i ≈01 cont (fst cf2) (snd cf2) j"
and wt:
"⋀I. I ∈ P - {I0} ⟹ W cf1 I0 < 1 ⟹ W cf2 (F I0) < 1 ⟹
W cf1 I / (1 - W cf1 I0) = W cf2 (F I) / (1 - W cf2 (F I0))"
and I0:
"⋀i. i ∈ I0 ⟹ snd cf1 ≈ eff (fst cf1) (snd cf1) i"
"⋀i. i ∈ I0 ⟹ cont (fst cf1) (snd cf1) i ≈01 fst cf2"
and FI0:
"⋀i. i ∈ F I0 ⟹ snd cf2 ≈ eff (fst cf2) (snd cf2) i"
"⋀i. i ∈ F I0 ⟹ fst cf1 ≈01 cont (fst cf2) (snd cf2) i"
unfolding mC_ZOC_def mC_ZOC_part_def mC_ZOC_eff_cont_def mC_ZOC_eff_cont0_def mC_ZOC_wt_def W_def
by simp_all
have "finite P" "inj_on F (P - {I0})" and FP': "finite (F`P)" "F I0 ∈ F`P"
using finite_part[OF _ P(2)] finite_part[OF _ FP(2)] ‹I0 ∈ P› ‹inj_on F P›
by (auto intro: inj_on_diff)
{ fix I i assume "I ∈ P" "i ∈ I"
with P have "0 ≤ wt (fst cf1) (snd cf1) i"
by (auto dest: part_is_subset intro!: wt_ge_0) }
note wt1_nneg[intro] = this
{ fix I i assume "I ∈ P" "i ∈ F I"
with FP have "0 ≤ wt (fst cf2) (snd cf2) i"
by (auto dest: part_is_subset intro!: wt_ge_0) }
note wt2_nneg[intro] = this
{ fix I assume "I ∈ P"
then have "0 ≤ W cf1 I"
unfolding W_def by (auto intro!: sum_nonneg) }
note W1_nneg[intro] = this
{ fix I assume "I ∈ P"
then have "0 ≤ W cf2 (F I)"
unfolding W_def by (auto intro!: sum_nonneg) }
note W2_nneg[intro] = this
show ?case
proof cases
{ fix n cf1 cf2 assume *: "fst cf1 ≈01 fst cf2" "snd cf1 ≈ snd cf2"
have "dist (Ps cf1) (Ps cf2) ≤ Pn cf1 0"
proof cases
assume cf1: "discrCf cf1"
moreover
note cf2 = ZObis_pres_discrCfR[OF cf1 *]
from cf1 cf2 have "S cf1 = (λbT. snd cf1 ≈ s)" "S cf2 = (λbT. snd cf2 ≈ s)"
unfolding S_def[abs_def] by (auto simp: enat_0[symmetric])
moreover from ‹snd cf1 ≈ snd cf2› have "snd cf1 ≈ s ⟷ snd cf2 ≈ s"
by (blast intro: indis_sym indis_trans)
ultimately show ?thesis
using T.prob_space by (cases "snd cf2 ≈ s") (simp_all add: Ps_def Pn_def measure_nonneg)
next
assume cf1: "¬ discrCf cf1"
then have "Pn cf1 0 = 1"
using T.prob_space by (simp add: Pn_def N_def)
moreover have "dist (Ps cf1) (Ps cf2) ≤ 1"
using dist_nonneg_bounded[where u=1 and l=0 and x="Ps cf1" and y="Ps cf2"]
by (auto simp add: dist_real_def Ps_def measure_nonneg split: abs_split)
ultimately show ?thesis by simp
qed }
note base_case = this
assume "n = 0 ∨ m = 0"
then show ?thesis
proof
assume "n = 0"
moreover
with T.prob_space ‹fst cf1 ≈01 fst cf2› ‹snd cf1 ≈ snd cf2›
have "dist (Ps cf1) (Ps cf2) ≤ Pn cf1 0"
by (intro base_case) (auto simp: Ps_def Pn_def)
moreover have "0 ≤ Pn cf2 m"
by (simp add: Pn_def measure_nonneg)
ultimately show ?thesis
by simp
next
assume "m = 0"
moreover
with T.prob_space ‹fst cf1 ≈01 fst cf2› ‹snd cf1 ≈ snd cf2›
have "dist (Ps cf2) (Ps cf1) ≤ Pn cf2 0"
by (intro base_case) (auto simp: Ps_def Pn_def intro: indis_sym ZObis_sym)
moreover have "0 ≤ Pn cf1 n"
by (simp add: Pn_def measure_nonneg)
ultimately show ?thesis
by (simp add: dist_commute)
qed
next
assume "¬ (n = 0 ∨ m = 0)"
then have "n ≠ 0" "m ≠ 0" by auto
then obtain n' m' where nm: "n = Suc n'" "m = Suc m'"
by (metis nat.exhaust)
define ps pn
where "ps cf I = (∑b∈I. wt (fst cf) (snd cf) b / W cf I * Ps (cont_eff cf b))"
and "pn cf I n = (∑b∈I. wt (fst cf) (snd cf) b / W cf I * Pn (cont_eff cf b) n)"
for cf I n
{ fix I assume "I ∈ P" "I ≠ I0" and W: "W cf1 I ≠ 0" "W cf2 (F I) ≠ 0"
then have "dist (ps cf1 I) (ps cf2 (F I)) ≤ pn cf1 I n' + pn cf2 (F I) m'"
unfolding ps_def pn_def
proof (intro dist_weighted_sum)
fix i j assume ij: "i ∈ I" "j ∈ F I"
assume "wt (fst cf1) (snd cf1) i / W cf1 I ≠ 0"
and "wt (fst cf2) (snd cf2) j / W cf2 (F I) ≠ 0"
from ‹I ∈ P› ij P(2) FP(2) have br: "i < brn (fst cf1)" "j < brn (fst cf2)"
by (auto dest: part_is_subset)
show "dist (Ps (cont_eff cf1 i)) (Ps (cont_eff cf2 j)) ≤
Pn (cont_eff cf1 i) n' + Pn (cont_eff cf2 j) m'"
proof (rule less.hyps)
show "n' + m' < n + m" using nm by simp
show "proper (fst (cont_eff cf1 i))" "proper (fst (cont_eff cf2 j))"
using br less.prems by (auto simp: cont_eff)
show "fst (cont_eff cf1 i) ≈01 fst (cont_eff cf2 j)"
"snd (cont_eff cf1 i) ≈ snd (cont_eff cf2 j)"
using cont[OF ‹I ∈ P› ‹I ≠ I0› ij] eff[OF ‹I ∈ P› ‹I ≠ I0› ij] by (auto simp: cont_eff)
qed
next
show "(∑b∈F I. wt (fst cf2) (snd cf2) b / W cf2 (F I)) = 1"
"(∑b∈I. wt (fst cf1) (snd cf1) b / W cf1 I) = 1"
using W by (auto simp: sum_divide_distrib[symmetric] sum_nonneg W_def)
qed auto }
note dist_n'_m' = this
{ fix I assume "I ∈ P" "I ≠ I0" and W: "W cf1 I = 0 ⟷ W cf2 (F I) = 0"
have "dist (ps cf1 I) (ps cf2 (F I)) ≤ pn cf1 I n' + pn cf2 (F I) m'"
proof cases
assume "W cf2 (F I) = 0"
then have "W cf2 (F I) = 0" "W cf1 I = 0" by (auto simp: W)
then show ?thesis by (simp add: ps_def pn_def)
next
assume "W cf2 (F I) ≠ 0"
then have "W cf1 I ≠ 0" "W cf2 (F I) ≠ 0" by (auto simp: W)
from dist_n'_m'[OF ‹I ∈ P› ‹I ≠ I0› this] show ?thesis .
qed }
note dist_n'_m'_W_iff = this
{ fix I j assume W: "W cf2 (F I0) ≠ 0"
from ‹I0 ∈ P› have "dist (∑i∈{()}. 1 * Ps cf1) (ps cf2 (F I0)) ≤ (∑i∈{()}. 1 * Pn cf1 n) + pn cf2 (F I0) m'"
unfolding ps_def pn_def
proof (intro dist_weighted_sum)
fix j assume "j ∈ F I0"
with FP(2) ‹I0 ∈ P› have br: "j < brn (fst cf2)"
by (auto dest: part_is_subset)
show "dist (Ps cf1) (Ps (cont_eff cf2 j)) ≤ Pn cf1 n + Pn (cont_eff cf2 j) m'"
proof (rule less.hyps)
show "n + m' < n + m" using nm by simp
show "proper (fst cf1)" "proper (fst (cont_eff cf2 j))"
using br by (auto simp: cont_eff)
show "fst cf1 ≈01 fst (cont_eff cf2 j)"
"snd cf1 ≈ snd (cont_eff cf2 j)"
using FI0[OF ‹j ∈ F I0›] ‹snd cf1 ≈ snd cf2›
by (auto simp: cont_eff intro: indis_trans)
qed
next
show "(∑b∈F I0. wt (fst cf2) (snd cf2) b / W cf2 (F I0)) = 1"
using W ‹I0 ∈ P› by (auto simp: sum_divide_distrib[symmetric] sum_nonneg W_def)
qed auto
then have "dist (Ps cf1) (ps cf2 (F I0)) ≤ Pn cf1 n + pn cf2 (F I0) m'"
by simp }
note dist_n_m' = this
{ fix I j assume W: "W cf1 I0 ≠ 0"
from ‹I0 ∈ P› have "dist (ps cf1 I0) (∑i∈{()}. 1 * Ps cf2) ≤ pn cf1 I0 n' + (∑i∈{()}. 1 * Pn cf2 m)"
unfolding ps_def pn_def
proof (intro dist_weighted_sum)
fix i assume "i ∈ I0"
with P(2) ‹I0 ∈ P› have br: "i < brn (fst cf1)"
by (auto dest: part_is_subset)
show "dist (Ps (cont_eff cf1 i)) (Ps cf2) ≤ Pn (cont_eff cf1 i) n' + Pn cf2 m"
proof (rule less.hyps)
show "n' + m < n + m" using nm by simp
show "proper (fst (cont_eff cf1 i))" "proper (fst cf2)"
using br less.prems by (auto simp: cont_eff)
show "fst (cont_eff cf1 i) ≈01 fst cf2"
"snd (cont_eff cf1 i) ≈ snd cf2"
using I0[OF ‹i ∈ I0›] ‹snd cf1 ≈ snd cf2›
by (auto simp: cont_eff intro: indis_trans indis_sym)
qed
next
show "(∑b∈I0. wt (fst cf1) (snd cf1) b / W cf1 I0) = 1"
using W ‹I0 ∈ P› by (auto simp: sum_divide_distrib[symmetric] sum_nonneg W_def)
qed auto
then have "dist (ps cf1 I0) (Ps cf2) ≤ pn cf1 I0 n' + Pn cf2 m"
by simp }
note dist_n'_m = this
have S_measurable[measurable]: "⋀cf. Measurable.pred T.S (S cf)"
unfolding S_def[abs_def]
by measurable
{ fix cf' cf assume cf[simp]: "proper (fst cf)" and cf': "cf' ∈ G cf"
let ?S = "λbT n. qsend bT = enat n ∧ snd (bT !! n) ≈ s"
{ fix bT n assume *: "?S (cf ## cf' ## bT) n" have "S cf' bT"
proof (cases n)
case 0 with * cf' show ?thesis
by (auto simp: S_def enat_0 sfirst_Stream G_eq split: if_split_asm intro!: exI[of _ 0])
(blast intro: indis_trans indis_sym discrCf_eff_indis)
next
case (Suc n) with * cf' show "S cf' bT"
by (auto simp: eSuc_enat[symmetric] sfirst_Stream S_def split: if_split_asm)
qed }
moreover
{ fix bT n assume "?S (cf' ## bT) n" with cf' have "?S (cf ## cf' ## bT) (if discrCf cf then 0 else Suc n)"
by (auto simp: eSuc_enat[symmetric] enat_0[symmetric] sfirst_Stream G_eq split: if_split_asm)
(blast intro: indis_trans indis_sym discrCf_eff_indis)
then have "S cf (cf' ## bT)"
by (auto simp: S_def) }
ultimately have "AE bT in T.T cf'. S cf (cf' ## bT) = S cf' bT"
by (auto simp: S_def) }
note S_sets = this
{ fix cf :: "('test, 'atom, 'choice) cmd × 'state" and P I0 S n st
assume cf[simp]: "proper (fst cf)" and P: "part {..<brn (fst cf)} P" and "finite P" "I0 ∈ P"
{ fix I i assume "I ∈ P" "i ∈ I"
with P have "0 ≤ wt (fst cf) (snd cf) i"
by (auto dest: part_is_subset intro!: wt_ge_0) }
note wt_nneg[simp] = this
assume S_measurable[measurable]: "⋀cf n. Measurable.pred T.S (λbT. S cf n bT)"
and S_next: "⋀cf cf' n. proper (fst cf) ⟹ cf' ∈ G cf ⟹
AE bT in T.T cf'. S cf (Suc n) (cf' ## bT) = S cf' n bT"
have finite_I: "⋀I. I ∈ P ⟹ finite I"
using finite_subset[OF part_is_subset[OF P]] by blast
let ?P = "λI. ∑i∈I. wt (fst cf) (snd cf) i * 𝒫(bT in T.T (cont_eff cf i). S (cont_eff cf i) n bT)"
let ?P' = "λI. W cf I * (∑i∈I. wt (fst cf) (snd cf) i / W cf I * 𝒫(bT in T.T (cont_eff cf i). S (cont_eff cf i) n bT))"
have "𝒫(bT in T.T cf. S cf (Suc n) bT) = (∫cf'. 𝒫(bT in T.T cf'. S cf' n bT) ∂trans cf)"
apply (subst T.prob_T[OF S_measurable])
apply (intro integral_cong_AE)
apply (auto simp: AE_measure_pmf_iff intro!: T.prob_eq_AE S_next simp del: space_T)
apply auto
done
also have "… = (∑I∈P. ?P I)"
unfolding integral_trans[OF cf] by (simp add: part_sum[OF P])
also have "… = (∑I∈P. ?P' I)"
using finite_I
by (auto intro!: sum.cong simp add: sum_distrib_left sum_nonneg_eq_0_iff W_def)
also have "… = ?P' I0 + (∑I∈P-{I0}. ?P' I)"
unfolding sum.remove[OF ‹finite P› ‹I0 ∈ P›] ..
finally have "𝒫(bT in T.T cf. S cf (Suc n) bT) = …" . }
note P_split = this
have Ps1: "Ps cf1 = W cf1 I0 * ps cf1 I0 + (∑I∈P-{I0}. W cf1 I * ps cf1 I)"
unfolding Ps_def ps_def using P(2) ‹finite P› ‹I0 ∈ P› by (intro P_split S_sets) simp_all
have "Ps cf2 = W cf2 (F I0) * ps cf2 (F I0) + (∑I∈F`P-{F I0}. W cf2 I * ps cf2 I)"
unfolding Ps_def ps_def using FP(2) ‹finite P› ‹I0 ∈ P› by (intro P_split S_sets) simp_all
moreover have F_diff: "F ` P - {F I0} = F ` (P - {I0})"
by (auto simp: ‹inj_on F P›[THEN inj_on_eq_iff] ‹I0 ∈ P›)
ultimately have Ps2: "Ps cf2 = W cf2 (F I0) * ps cf2 (F I0) + (∑I∈P-{I0}. W cf2 (F I) * ps cf2 (F I))"
by (simp add: sum.reindex ‹inj_on F (P-{I0})›)
have Pn1: "Pn cf1 n = W cf1 I0 * pn cf1 I0 n' + (∑I∈P-{I0}. W cf1 I * pn cf1 I n')"
unfolding Pn_def pn_def nm using P(2) ‹finite P› ‹I0 ∈ P› by (intro P_split) (simp_all add: N_def)
have "Pn cf2 m = W cf2 (F I0) * pn cf2 (F I0) m' + (∑I∈F`P-{F I0}. W cf2 I * pn cf2 I m')"
unfolding Pn_def pn_def nm using FP(2) ‹finite P› ‹I0 ∈ P› by (intro P_split) (simp_all add: N_def)
with F_diff have Pn2: "Pn cf2 m = W cf2 (F I0) * pn cf2 (F I0) m' + (∑I∈P-{I0}. W cf2 (F I) * pn cf2 (F I) m')"
by (simp add: sum.reindex ‹inj_on F (P-{I0})›)
show ?thesis
proof cases
assume "W cf1 I0 = 1 ∨ W cf2 (F I0) = 1"
then show ?thesis
proof
assume *: "W cf1 I0 = 1"
then have "W cf1 I0 = W cf1 {..<brn (fst cf1)}" by (simp add: W_def)
also have "… = W cf1 I0 + (∑I∈P - {I0}. W cf1 I)"
unfolding ‹part {..<brn (fst cf1)} P›[THEN part_sum] W_def
unfolding sum.remove[OF ‹finite P› ‹I0 ∈ P›] ..
finally have "(∑I∈P - {I0}. W cf1 I) = 0" by simp
then have "∀I∈P - {I0}. W cf1 I = 0"
using ‹finite P› by (subst (asm) sum_nonneg_eq_0_iff) auto
then have "Ps cf1 = ps cf1 I0" "Pn cf1 n = pn cf1 I0 n'"
unfolding Ps1 Pn1 * by simp_all
moreover note dist_n'_m *
ultimately show ?thesis by simp
next
assume *: "W cf2 (F I0) = 1"
then have "W cf2 (F I0) = W cf2 {..<brn (fst cf2)}" by (simp add: W_def)
also have "… = W cf2 (F I0) + (∑I∈F ` P - {F I0}. W cf2 I)"
unfolding FP(2)[THEN part_sum] W_def
unfolding sum.remove[OF FP'] ..
finally have "(∑I∈F`P - {F I0}. W cf2 I) = 0" by simp
then have "∀I∈F`P - {F I0}. W cf2 I = 0"
using ‹finite P› by (subst (asm) sum_nonneg_eq_0_iff) auto
then have "Ps cf2 = ps cf2 (F I0)" "Pn cf2 m = pn cf2 (F I0) m'"
unfolding Ps2 Pn2 * by (simp_all add: F_diff)
moreover note dist_n_m' *
ultimately show ?thesis by simp
qed
next
assume W_neq1: "¬ (W cf1 I0 = 1 ∨ W cf2 (F I0) = 1)"
moreover
{ fix cf :: "('test, 'atom, 'choice) cmd × 'state" and I P
assume "proper (fst cf)" "part {..<brn (fst (cf))} P" "I ∈ P"
then have "W cf I ≤ W cf {..<brn (fst (cf))}"
unfolding W_def
by (intro sum_mono2 part_is_subset) auto
then have "W cf I ≤ 1" using ‹proper (fst cf)› by (simp add: W_def) }
ultimately have wt_less1: "W cf1 I0 < 1" "W cf2 (F I0) < 1"
using FP(2) FP'(2) P(2) ‹I0 ∈ P›
unfolding le_less by blast+
{ fix I assume *: "I ∈ P - {I0}"
have "W cf1 I = 0 ⟷ W cf2 (F I) = 0"
using wt[OF * wt_less1] wt_less1 by auto
with * have "dist (ps cf1 I) (ps cf2 (F I)) ≤ pn cf1 I n' + pn cf2 (F I) m'"
by (intro dist_n'_m'_W_iff) auto }
note dist_eps = this
{ fix a b c d :: real
have "dist a b = dist ((a - c) + c) ((b - d) + d)" by simp
also have "… ≤ dist (a - c) (b - d) + dist c d"
using dist_triangle_add .
finally have "dist a b ≤ dist (a - c) (b - d) + dist c d" . }
note dist_triangle_diff = this
have dist_diff_diff: "⋀a b c d::real. dist (a - b) (c - d) ≤ dist a b + dist c d"
unfolding dist_real_def by auto
let ?v0 = "W cf1 I0" and ?w0 = "W cf2 (F I0)"
let ?v1 = "1 - ?v0" and ?w1 = "1 - ?w0"
let ?wQ = "(Ps cf2 - ?w0 * ps cf2 (F I0)) / ?w1"
let ?wP = "(Ps cf1 - ?v0 * ps cf1 I0) / ?v1"
let ?D = "(?w0 * ?v1 * Ps cf1 + ?w1 * ?v0 * ps cf1 I0)"
let ?E = "(?v0 * ?w1 * Ps cf2 + ?v1 * ?w0 * ps cf2 (F I0))"
have w0v0_less1: "?w0 * ?v0 < 1 * 1"
using wt_less1 ‹I0 ∈ P› by (intro mult_strict_mono) auto
then have neg_w0v0_nonneg: "0 ≤ 1 - ?w0 * ?v0" by simp
let ?e1 = "(∑I∈P-{I0}. W cf1 I / ?v1 * pn cf1 I n') +
(∑I∈P-{I0}. W cf2 (F I) / ?w1 * pn cf2 (F I) m')"
have "dist ((1 - ?w0 * ?v0) * Ps cf1) ((1 - ?w0 * ?v0) * Ps cf2) ≤
dist ((1 - ?w0 * ?v0) * Ps cf1 - ?D) ((1 - ?w0 * ?v0) * Ps cf2 - ?E) + dist ?D ?E"
by (rule dist_triangle_diff)
also have "… ≤ ?v1 * ?w1 * ?e1 + (?v1 * ?w0 * (Pn cf1 n + pn cf2 (F I0) m') + ?w1 * ?v0 * (pn cf1 I0 n' + Pn cf2 m))"
proof (rule add_mono)
{ have "?wP = (∑I∈P-{I0}. W cf1 I * ps cf1 I) / ?v1"
unfolding Ps1 by (simp add: field_simps)
also have "… = (∑I∈P-{I0}. W cf1 I / ?v1 * ps cf1 I)"
by (subst sum_divide_distrib) simp
finally have "?wP = (∑I∈P-{I0}. W cf1 I / ?v1 * ps cf1 I)" . }
moreover
{ have "?wQ = (∑I∈P-{I0}. W cf2 (F I) * ps cf2 (F I)) / ?w1"
using Ps2 by (simp add: field_simps)
also have "… = (∑I∈P-{I0}. W cf2 (F I) / ?w1 * ps cf2 (F I))"
by (subst sum_divide_distrib) simp
also have "… = (∑I∈P-{I0}. W cf1 I / ?v1 * ps cf2 (F I))"
using wt[OF _ wt_less1] by simp
finally have "?wQ = (∑I∈P-{I0}. W cf1 I / ?v1 * ps cf2 (F I))" . }
ultimately
have "dist ?wP ?wQ ≤ (∑I∈P-{I0}. W cf1 I / ?v1 * (pn cf1 I n' + pn cf2 (F I) m'))"
using wt_less1 dist_eps
by (simp, intro dist_sum)
(simp add: sum_nonneg divide_le_cancel mult_le_cancel_left not_le[symmetric] W1_nneg)
also have "… = ?e1"
unfolding sum.distrib[symmetric] using wt[OF _ wt_less1]
by (simp add: field_simps add_divide_distrib)
finally have "dist (?v1 * ?w1 * ?wP) (?v1 * ?w1 * ?wQ) ≤ ?v1 * ?w1 * ?e1"
using wt_less1 unfolding dist_mult by simp
also {
have "?v1 * ?w1 * ?wP = ?w1 * (?v0 * Ps cf1 + ?v1 * Ps cf1) - ?w1 * ?v0 * ps cf1 I0"
using wt_less1 unfolding divide_eq_eq by (simp add: field_simps)
also have "… = (1 - ?w0 * ?v0) * Ps cf1 - ?D"
by (simp add: field_simps)
finally have "?v1 * ?w1 * ?wP = (1 - ?w0 * ?v0) * Ps cf1 - ?D" . }
also {
have "?v1 * ?w1 * ?wQ = ?v1 * (?w0 * Ps cf2 + ?w1 * Ps cf2) - ?v1 * ?w0 * (ps cf2 (F I0))"
using wt_less1 unfolding divide_eq_eq by (simp add: field_simps)
also have "… = (1 - ?w0 * ?v0) * Ps cf2 - ?E"
by (simp add: field_simps)
finally have "?v1 * ?w1 * ?wQ = (1 - ?w0 * ?v0) * Ps cf2 - ?E" . }
finally show "dist ((1 - ?w0 * ?v0) * Ps cf1 - ?D) ((1 - ?w0 * ?v0) * Ps cf2 - ?E) ≤ ?v1 * ?w1 * ?e1" .
next
have "dist ?D ?E = dist
(?v1 * ?w0 * Ps cf1 - ?v1 * ?w0 * ps cf2 (F I0))
(?w1 * ?v0 * Ps cf2 - ?w1 * ?v0 * ps cf1 I0)"
unfolding dist_real_def by (simp add: ac_simps)
also have "… ≤ dist (?v1 * ?w0 * Ps cf1) (?v1 * ?w0 * ps cf2 (F I0)) +
dist (?w1 * ?v0 * Ps cf2) (?w1 * ?v0 * ps cf1 I0)"
using dist_diff_diff .
also have "… ≤ ?v1 * ?w0 * (Pn cf1 n + pn cf2 (F I0) m') + ?w1 * ?v0 * (pn cf1 I0 n' + Pn cf2 m)"
proof (rule add_mono)
show "dist (?v1 * ?w0 * Ps cf1) (?v1 * ?w0 * ps cf2 (F I0)) ≤ ?v1 * ?w0 * (Pn cf1 n + pn cf2 (F I0) m')"
using wt_less1 dist_n_m' ‹I0 ∈ P›
by (simp add: sum_nonneg mult_le_cancel_left not_le[symmetric] mult_le_0_iff W2_nneg)
show "dist (?w1 * ?v0 * Ps cf2) (?w1 * ?v0 * ps cf1 I0) ≤ ?w1 * ?v0 * (pn cf1 I0 n' + Pn cf2 m)"
using wt_less1 dist_n'_m ‹I0 ∈ P›
by (subst dist_commute)
(simp add: sum_nonneg mult_le_cancel_left not_le[symmetric] mult_le_0_iff W1_nneg)
qed
finally show "dist ?D ?E ≤ ?v1 * ?w0 * (Pn cf1 n + pn cf2 (F I0) m') + ?w1 * ?v0 * (pn cf1 I0 n' + Pn cf2 m)" .
qed
also have "… = ?w1 * (∑I∈P-{I0}. W cf1 I * pn cf1 I n') + ?v1 * (∑I∈P-{I0}. W cf2 (F I) * pn cf2 (F I) m') +
?v1 * ?w0 * (Pn cf1 n + pn cf2 (F I0) m') + ?w1 * ?v0 * (pn cf1 I0 n' + Pn cf2 m)"
using W_neq1 by (simp add: sum_divide_distrib[symmetric] add_divide_eq_iff divide_add_eq_iff)
also have "… = (1 - ?w0 * ?v0) * (Pn cf1 n + Pn cf2 m)"
unfolding Pn1 Pn2 by (simp add: field_simps)
finally show "dist (Ps cf1) (Ps cf2) ≤ Pn cf1 n + Pn cf2 m"
using neg_w0v0_nonneg w0v0_less1 by (simp add: mult_le_cancel_left)
qed
qed
qed
lemma AE_T_max_qsend_time:
fixes cf and e :: real assumes AE: "AE bT in T.T cf. qsend (cf ## bT) < ∞" "0 < e"
shows "∃N. 𝒫(bT in T.T cf. ¬ discrCf ((cf ## bT) !! N)) < e"
proof -
from AE_T_max_sfirst[OF _ AE] obtain N :: nat
where "𝒫(bT in T.T cf. N < qsend (cf ## bT)) < e"
by auto
also have "𝒫(bT in T.T cf. N < qsend (cf ## bT)) = 𝒫(bT in T.T cf. ¬ discrCf ((cf ## bT) !! N))"
using less_qsend_iff_not_discrCf[of cf] AE_T_enabled[of cf]
by (intro T.prob_eq_AE) auto
finally show ?thesis ..
qed
lemma Ps_eq:
fixes cf1 cf2 s and S
defines "S cf bT ≡ ∃n. qsend (cf ## bT) = n ∧ eff_at cf bT n ≈ s"
defines "Ps cf ≡ 𝒫(bT in T.T cf. S cf bT)"
assumes qsterm1: "AE bT in T.T cf1. qsend (cf1 ## bT) < ∞"
assumes qsterm2: "AE bT in T.T cf2. qsend (cf2 ## bT) < ∞"
and bisim: "proper (fst cf1)" "proper (fst cf2)" "fst cf1 ≈01 fst cf2" "snd cf1 ≈ snd cf2"
shows "Ps cf1 = Ps cf2"
proof -
let ?nT = "λcf n bT. ¬ discrCf ((cf ## bT) !! n)"
let ?PnT = "λcf n. 𝒫(bT in T.T cf. ?nT cf n bT)"
have "dist (Ps cf1) (Ps cf2) = 0"
unfolding dist_real_def
proof (rule field_abs_le_zero_epsilon)
fix e ::real assume "0 < e"
then have "0 < e / 2" by auto
from AE_T_max_qsend_time[OF qsterm1 this] AE_T_max_qsend_time[OF qsterm2 this]
obtain n m where "?PnT cf1 n < e / 2" "?PnT cf2 m < e / 2" by auto
moreover have "dist (Ps cf1) (Ps cf2) ≤ ?PnT cf1 n + ?PnT cf2 m"
unfolding Ps_def S_def using bisim by (rule dist_Ps_upper_bound)
ultimately show "¦Ps cf1 - Ps cf2¦ ≤ e"
unfolding dist_real_def by auto
qed
then show "Ps cf1 = Ps cf2" by auto
qed
lemma siso_trace:
assumes "siso c" "s ≈ t" "enabled (c, t) cfT"
shows "siso (cont_at (c, s) cfT n)"
and "cont_at (c, s) cfT n = cont_at (c, t) cfT n"
and "eff_at (c, s) cfT n ≈ eff_at (c, t) cfT n"
using assms
proof (induction n arbitrary: c s t cfT)
case (Suc n) case 1
with Suc(1)[of "fst (shd cfT)" "snd (shd cfT)" "snd (shd cfT)" "stl cfT"] show ?case
by (auto simp add: enabled.simps[of _ cfT] G_eq cont_eff indis_refl split: if_split_asm)
qed auto
lemma Sbis_trace:
assumes "proper (fst cf1)" "proper (fst cf2)" "fst cf1 ≈s fst cf2" "snd cf1 ≈ snd cf2"
shows "𝒫(cfT in T.T cf1. eff_at cf1 cfT n ≈ s') = 𝒫(cfT in T.T cf2. eff_at cf2 cfT n ≈ s')"
(is "?P cf1 n = ?P cf2 n")
using assms proof (induct n arbitrary: cf1 cf2)
case 0
show ?case
proof cases
assume "snd cf1 ≈ s'"
with ‹snd cf1 ≈ snd cf2› ‹fst cf1 ≈s fst cf2› have "snd cf1 ≈ s'" "snd cf2 ≈ s'"
by (metis indis_trans indis_sym)+
then show ?case
using T.prob_space by simp
next
assume "¬ snd cf1 ≈ s'"
with ‹snd cf1 ≈ snd cf2› ‹fst cf1 ≈s fst cf2› have "¬ snd cf1 ≈ s' ∧ ¬ snd cf2 ≈ s'"
by (metis indis_trans indis_sym)
then show ?case
by auto
qed
next
case (Suc n)
note ‹proper (fst cf1)›[simp] ‹proper (fst cf2)›[simp]
from Sbis_mC_C ‹fst cf1 ≈s fst cf2› ‹snd cf1 ≈ snd cf2›
obtain P F where mP: "mC_C Sbis (fst cf1) (fst cf2) (snd cf1) (snd cf2) P F"
by blast
then have
P: "part {..<brn (fst cf1)} P" "{} ∉ P" and
FP: "part {..<brn (fst cf2)} (F`P)" "{} ∉ F ` P" "inj_on F P" and
W: "⋀I. I ∈ P ⟹ sum (wt (fst cf1) (snd cf1)) I = sum (wt (fst cf2) (snd cf2)) (F I)" and
eff: "⋀I i j. I ∈ P ⟹ i ∈ I ⟹ j ∈ F I ⟹
eff (fst cf1) (snd cf1) i ≈ eff (fst cf2) (snd cf2) j" and
cont: "⋀I i j. I ∈ P ⟹ i ∈ I ⟹ j ∈ F I ⟹
cont (fst cf1) (snd cf1) i ≈s cont (fst cf2) (snd cf2) j"
unfolding mC_C_def mC_C_eff_cont_def mC_C_part_def mC_C_wt_def by metis+
{ fix cf1 :: "('test, 'atom, 'choice) cmd × 'state" and P assume cf[simp]: "proper (fst cf1)" and P: "part {..<brn (fst cf1)} P"
have "?P cf1 (Suc n) = (∫cf'. ?P cf' n ∂trans cf1)"
by (subst T.prob_T) auto
also have "… = (∑b<brn (fst cf1). wt (fst cf1) (snd cf1) b * ?P (cont_eff cf1 b) n)"
unfolding integral_trans[OF cf] ..
also have "… = (∑I∈P. ∑b∈I. wt (fst cf1) (snd cf1) b * ?P (cont_eff cf1 b) n)"
unfolding part_sum[OF P] ..
finally have "?P cf1 (Suc n) = …" . }
note split = this
{ fix I i assume "I ∈ P" "i ∈ I"
with ‹proper (fst cf1)› have "i < brn (fst cf1)"
using part_is_subset[OF P(1) ‹I ∈ P›] by auto }
note brn_cf[simp] = this
{ fix I i assume "I ∈ P" "i ∈ F I"
with ‹proper (fst cf2)› have "i < brn (fst cf2)"
using part_is_subset[OF FP(1), of "F I"] by auto }
note brn_cf2[simp] = this
{ fix I assume "I ∈ P"
with ‹{} ∉ P› obtain i where "i ∈ I" by (metis all_not_in_conv)
from ‹I ∈ P› FP have "F I ≠ {}" "F I ⊆ {..<brn (fst cf2)}"
by (auto simp: part_is_subset)
then obtain j where "j < brn (fst cf2)" "j ∈ F I" by auto
{ fix b assume "b ∈ F I"
then have "?P (cont_eff cf1 i) n = ?P (cont_eff cf2 b) n"
using ‹I ∈ P› ‹i ∈ I› cont eff
by (intro Suc) (auto simp add: cont_eff) }
note cont_d_const = this[symmetric]
{ fix a assume "a ∈ I"
with ‹I ∈ P› ‹i ∈ I› ‹j ∈ F I› cont eff
have "?P (cont_eff cf1 i) n = ?P (cont_eff cf2 j) n ∧
?P (cont_eff cf1 a) n = ?P (cont_eff cf2 j) n"
by (intro conjI Suc) (auto simp add: cont_eff)
then have "?P (cont_eff cf1 a) n = ?P (cont_eff cf1 i) n" by simp }
then have "(∑b∈I. wt (fst cf1) (snd cf1) b * ?P (cont_eff cf1 b) n) =
(∑b∈I. wt (fst cf1) (snd cf1) b) * ?P (cont_eff cf1 i) n"
by (simp add: sum_distrib_right)
also have "… = (∑b∈F I. wt (fst cf2) (snd cf2) b) * ?P (cont_eff cf1 i) n"
using W ‹I ∈ P› by auto
also have "… = (∑b∈F I. wt (fst cf2) (snd cf2) b * ?P (cont_eff cf2 b) n)"
using cont_d_const by (auto simp add: sum_distrib_right)
finally have "(∑b∈I. wt (fst cf1) (snd cf1) b * ?P (cont_eff cf1 b) n) = …" . }
note sum_eq = this
have "?P cf1 (Suc n) = (∑I∈P. ∑b∈I. wt (fst cf1) (snd cf1) b * ?P (cont_eff cf1 b) n)"
using ‹proper (fst cf1)› P(1) by (rule split)
also have "… = (∑I∈P. ∑b∈F I. wt (fst cf2) (snd cf2) b * ?P (cont_eff cf2 b) n)"
using sum_eq by simp
also have "… = (∑I∈F`P. ∑b∈I. wt (fst cf2) (snd cf2) b * ?P (cont_eff cf2 b) n)"
using ‹inj_on F P› by (simp add: sum.reindex)
also have "… = ?P cf2 (Suc n)"
using ‹proper (fst cf2)› FP(1) by (rule split[symmetric])
finally show ?case .
qed
subsection ‹Final Theorems›
theorem ZObis_eSec: "⟦proper c; c ≈01 c; aeT c⟧ ⟹ eSec c"
by (auto simp: aeT_def eSec_def intro!: Ps_eq[simplified])
theorem Sbis_amSec: "⟦proper c; c ≈s c⟧ ⟹ amSec c"
by (auto simp: amSec_def intro!: Sbis_trace[simplified])
theorem amSec_eSec:
assumes [simp]: "proper c" and "aeT c" "amSec c" shows "eSec c"
proof (unfold eSec_def, intro allI impI)
fix s1 s2 t assume "s1 ≈ s2"
let ?T = "λs bT. ∃n. qsend ((c, s) ## bT) = n ∧ eff_at (c,s) bT n ≈ t"
let ?P = "λs. 𝒫(bT in T.T (c, s). ?T s bT)"
have "dist (?P s1) (?P s2) = 0"
unfolding dist_real_def
proof (rule field_abs_le_zero_epsilon)
fix e :: real assume "0 < e"
then have "0 < e / 2" by simp
let ?N = "λs n bT. ¬ discrCf (((c,s) ## bT) !! n)"
from AE_T_max_qsend_time[OF _ ‹0 < e / 2›, of "(c,s1)"]
obtain N1 where N1: "𝒫(bT in T.T (c, s1). ?N s1 N1 bT) < e / 2"
using ‹aeT c› unfolding aeT_def by auto
from AE_T_max_qsend_time[OF _ ‹0 < e / 2›, of "(c,s2)"]
obtain N2 where N2: "𝒫(bT in T.T (c, s2). ?N s2 N2 bT) < e / 2"
using ‹aeT c› unfolding aeT_def by auto
define N where "N = max N1 N2"
let ?Tn = "λn s bT. eff_at (c,s) bT n ≈ t"
have "dist 𝒫(bT in T.T (c, s1). ?T s1 bT) 𝒫(bT in T.T (c, s1). ?Tn N s1 bT) ≤
𝒫(bT in T.T (c, s1). ?N s1 N1 bT)"
using ‹aeT c›[unfolded aeT_def, rule_format] AE_T_enabled AE_space
proof (intro T.prob_dist, eventually_elim, intro impI)
fix bT assume bT: "enabled (c,s1) bT" and "¬ ¬ discrCf (((c,s1) ## bT) !! N1)"
with bT have "qsend ((c,s1) ## bT) ≤ N1"
using less_qsend_iff_not_discrCf[of "(c,s1)" bT N1] by simp
then show "?T s1 bT ⟷ ?Tn N s1 bT"
using bT
by (cases "qsend ((c, s1) ## bT)")
(auto intro!: enabled_qsend_indis del: iffI simp: N_def)
qed measurable
moreover
have "dist 𝒫(bT in T.T (c, s2). ?T s2 bT) 𝒫(bT in T.T (c, s2). ?Tn N s2 bT) ≤
𝒫(bT in T.T (c, s2). ?N s2 N2 bT)"
using ‹aeT c›[unfolded aeT_def, rule_format] AE_T_enabled AE_space
proof (intro T.prob_dist, eventually_elim, intro impI)
fix bT assume bT: "enabled (c,s2) bT" "¬ ¬ discrCf (((c,s2) ## bT) !! N2)"
with bT have "qsend ((c,s2) ## bT) ≤ N2"
using less_qsend_iff_not_discrCf[of "(c,s2)" bT N2] by simp
then show "?T s2 bT ⟷ ?Tn N s2 bT"
using bT
by (cases "qsend ((c, s2) ## bT)")
(auto intro!: enabled_qsend_indis del: iffI simp: N_def)
qed measurable
ultimately have "dist 𝒫(bT in T.T (c, s1). ?T s1 bT) 𝒫(bT in T.T (c, s1). ?Tn N s1 bT) +
dist 𝒫(bT in T.T (c, s2). ?T s2 bT) 𝒫(bT in T.T (c, s1). ?Tn N s1 bT) ≤ e"
using ‹amSec c›[unfolded amSec_def, rule_format, OF ‹s1 ≈ s2›, of N t]
using N1 N2 by simp
from dist_triangle_le[OF this]
show "¦?P s1 - ?P s2¦ ≤ e" by (simp add: dist_real_def)
qed
then show "?P s1 = ?P s2"
by simp
qed
end
end