Theory Probabilistic_Hierarchy
theory Probabilistic_Hierarchy
imports
"HOL-Probability.Probability"
Nonempty_Bounded_Set
"HOL-Eisbach.Eisbach"
begin
section ‹Bisimilarity›
definition bisimilar where
"bisimilar Q s1 s2 x y ≡ (∃R. R x y ∧ (∀x y. R x y ⟶ Q R (s1 x) (s2 y)))"
abbreviation "bisimilar_mc ≡ bisimilar (λR. rel_pmf R)"
abbreviation "bisimilar_dlts ≡ bisimilar (λR. rel_fun (=) (rel_option R))"
abbreviation "bisimilar_lts ≡ bisimilar (λR. rel_bset (rel_prod (=) R))"
abbreviation "bisimilar_react ≡ bisimilar (λR. rel_fun (=) (rel_option (rel_pmf R)))"
abbreviation "bisimilar_lmc ≡ bisimilar (λR. rel_prod (=) (rel_pmf R))"
abbreviation "bisimilar_lmdp ≡ bisimilar (λR. rel_prod (=) (rel_nebset (rel_pmf R)))"
abbreviation "bisimilar_gen ≡ bisimilar (λR. rel_option (rel_pmf (rel_prod (=) R)))"
abbreviation "bisimilar_str ≡ bisimilar (λR. rel_sum (rel_pmf R) (rel_option (rel_prod (=) R)))"
abbreviation "bisimilar_alt ≡ bisimilar (λR. rel_sum (rel_pmf R) (rel_bset (rel_prod (=) R)))"
abbreviation "bisimilar_sseg ≡ bisimilar (λR. rel_bset (rel_prod (=) (rel_pmf R)))"
abbreviation "bisimilar_seg ≡ bisimilar (λR. rel_bset (rel_pmf (rel_prod (=) R)))"
abbreviation "bisimilar_bun ≡ bisimilar (λR. rel_pmf (rel_bset (rel_prod (=) R)))"
abbreviation "bisimilar_pz ≡ bisimilar (λR. rel_bset (rel_pmf (rel_bset (rel_prod (=) R))))"
abbreviation "bisimilar_mg ≡ bisimilar (λR. rel_bset (rel_pmf (rel_bset (rel_sum (rel_prod (=) R) R))))"
section ‹Systems›
codatatype mc = MC "mc pmf"
codatatype 'a dlts = DLTS "'a ⇒ 'a dlts option"