# Theory Generat

```(* Title: Generat.thy
Author: Andreas Lochbihler, ETH Zurich *)

section ‹Generative probabilistic values›

theory Generat imports
Misc_CryptHOL
begin

subsection ‹Single-step generative›

datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat
= Pure (result: 'a)
| IO ("output": 'b) (continuation: "'c")

datatype_compat generat

lemma IO_code_cong: "out = out' ⟹ IO out c = IO out' c" by simp

lemma is_Pure_map_generat [simp]: "is_Pure (map_generat f g h x) = is_Pure x"
by(cases x) simp_all

lemma result_map_generat [simp]: "is_Pure x ⟹ result (map_generat f g h x) = f (result x)"
by(cases x) simp_all

lemma output_map_generat [simp]: "¬ is_Pure x ⟹ output (map_generat f g h x) = g (output x)"
by(cases x) simp_all

lemma continuation_map_generat [simp]: "¬ is_Pure x ⟹ continuation (map_generat f g h x) = h (continuation x)"
by(cases x) simp_all

lemma [simp]:
shows map_generat_eq_Pure:
"map_generat f g h generat = Pure x ⟷ (∃x'. generat = Pure x' ∧ x = f x')"
and Pure_eq_map_generat:
"Pure x = map_generat f g h generat ⟷ (∃x'. generat = Pure x' ∧ x = f x')"
by(cases generat; auto; fail)+

lemma [simp]:
shows map_generat_eq_IO:
"map_generat f g h generat = IO out c ⟷ (∃out' c'. generat = IO out' c' ∧ out = g out' ∧ c = h c')"
and IO_eq_map_generat:
"IO out c = map_generat f g h generat ⟷ (∃out' c'. generat = IO out' c' ∧ out = g out' ∧ c = h c')"
by(cases generat; auto; fail)+

lemma is_PureE [cases pred]:
assumes "is_Pure generat"
obtains (Pure) x where "generat = Pure x"
using assms by(auto simp add: is_Pure_def)

lemma not_is_PureE:
assumes "¬ is_Pure generat"
obtains (IO) out c where "generat = IO out c"
using assms by(cases generat) auto

lemma rel_generatI:
"⟦ is_Pure x ⟷ is_Pure y;
⟦ is_Pure x; is_Pure y ⟧ ⟹ A (result x) (result y);
⟦ ¬ is_Pure x; ¬ is_Pure y ⟧ ⟹ Out (output x) (output y) ∧ R (continuation x) (continuation y) ⟧
⟹ rel_generat A Out R x y"
by(cases x y rule: generat.exhaust[case_product generat.exhaust]) simp_all

lemma rel_generatD':
"rel_generat A Out R x y
⟹ (is_Pure x ⟷ is_Pure y) ∧
(is_Pure x ⟶ is_Pure y ⟶ A (result x) (result y)) ∧
(¬ is_Pure x ⟶ ¬ is_Pure y ⟶ Out (output x) (output y) ∧ R (continuation x) (continuation y))"
by(cases x y rule: generat.exhaust[case_product generat.exhaust]) simp_all

lemma rel_generatD:
assumes "rel_generat A Out R x y"
shows rel_generat_is_PureD: "is_Pure x ⟷ is_Pure y"
and rel_generat_resultD: "is_Pure x ∨ is_Pure y ⟹ A (result x) (result y)"
and rel_generat_outputD: "¬ is_Pure x ∨ ¬ is_Pure y ⟹ Out (output x) (output y)"
and rel_generat_continuationD: "¬ is_Pure x ∨ ¬ is_Pure y ⟹ R (continuation x) (continuation y)"
using rel_generatD'[OF assms] by simp_all

lemma rel_generat_mono:
"⟦ rel_generat A B C x y; ⋀x y. A x y ⟹ A' x y; ⋀x y. B x y ⟹ B' x y; ⋀x y. C x y ⟹ C' x y ⟧
⟹ rel_generat A' B' C' x y"
using generat.rel_mono[of A A' B B' C C'] by(auto simp add: le_fun_def)

lemma rel_generat_mono' [mono]:
"⟦ ⋀x y. A x y ⟶ A' x y; ⋀x y. B x y ⟶ B' x y; ⋀x y. C x y ⟶ C' x y ⟧
⟹ rel_generat A B C x y ⟶ rel_generat A' B' C' x y"
by(blast intro: rel_generat_mono)

lemma rel_generat_same:
"rel_generat A B C r r ⟷
(∀x ∈ generat_pures r. A x x) ∧
(∀out ∈ generat_outs r. B out out) ∧
(∀c ∈generat_conts r. C c c)"

lemma rel_generat_reflI:
"⟦ ⋀y. y ∈ generat_pures x ⟹ A y y;
⋀out. out ∈ generat_outs x ⟹ B out out;
⋀cont. cont ∈ generat_conts x ⟹ C cont cont ⟧
⟹ rel_generat A B C x x"
by(cases x) auto

lemma reflp_rel_generat [simp]: "reflp (rel_generat A B C) ⟷ reflp A ∧ reflp B ∧ reflp C"
by(auto 4 3 intro!: reflpI rel_generatI dest: reflpD reflpD[where x="Pure _"] reflpD[where x="IO _ _"])

lemma transp_rel_generatI:
assumes "transp A" "transp B" "transp C"
shows "transp (rel_generat A B C)"
by(rule transpI)(auto 6 5 dest: rel_generatD' intro!: rel_generatI intro: assms[THEN transpD] simp add: rel_fun_def)

lemma rel_generat_inf:
"inf (rel_generat A B C) (rel_generat A' B' C') = rel_generat (inf A A') (inf B B') (inf C C')"
(is "?lhs = ?rhs")
proof(rule antisym)
show "?lhs ≤ ?rhs"
by(auto elim!: generat.rel_cases simp add: rel_fun_def)
qed(auto elim: rel_generat_mono)

lemma rel_generat_Pure1: "rel_generat A B C (Pure x) = (λr. ∃y. r = Pure y ∧ A x y)"
by(rule ext)(case_tac r, simp_all)

lemma rel_generat_IO1: "rel_generat A B C (IO out c) = (λr. ∃out' c'. r = IO out' c' ∧ B out out' ∧ C c c')"
by(rule ext)(case_tac r, simp_all)

lemma not_is_Pure_conv: "¬ is_Pure r ⟷ (∃out c. r = IO out c)"
by(cases r) auto

lemma finite_generat_outs [simp]: "finite (generat_outs generat)"
by(cases generat) auto

lemma countable_generat_outs [simp]: "countable (generat_outs generat)"

lemma case_map_generat:
"case_generat pure io (map_generat a b d r) =
case_generat (pure ∘ a) (λout. io (b out) ∘ d) r"
by(cases r) simp_all

lemma continuation_in_generat_conts:
"¬ is_Pure r ⟹ continuation r ∈ generat_conts r"
by(cases r) auto

fun dest_IO :: "('a, 'out, 'c) generat ⇒ ('out × 'c) option"
where
"dest_IO (Pure _) = None"
| "dest_IO (IO out c) = Some (out, c)"

lemma dest_IO_eq_Some_iff [simp]: "dest_IO generat = Some (out, c) ⟷ generat = IO out c"
by(cases generat) simp_all

lemma dest_IO_eq_None_iff [simp]: "dest_IO generat = None ⟷ is_Pure generat"
by(cases generat) simp_all

lemma dest_IO_comp_Pure [simp]: "dest_IO ∘ Pure = (λ_. None)"

lemma dom_dest_IO: "dom dest_IO = {x. ¬ is_Pure x}"

definition generat_lub :: "('a set ⇒ 'b) ⇒ ('out set ⇒ 'out') ⇒ ('cont set ⇒ 'cont')
⇒ ('a, 'out, 'cont) generat set ⇒ ('b, 'out', 'cont') generat"
where
"generat_lub lub1 lub2 lub3 A =
(if ∃x∈A. is_Pure x then Pure (lub1 (result ` (A ∩ {f. is_Pure f})))
else IO (lub2 (output ` (A ∩ {f. ¬ is_Pure f}))) (lub3 (continuation ` (A ∩ {f. ¬ is_Pure f}))))"

lemma is_Pure_generat_lub [simp]:
"is_Pure (generat_lub lub1 lub2 lub3 A) ⟷ (∃x∈A. is_Pure x)"

lemma result_generat_lub [simp]:
"∃x∈A. is_Pure x ⟹ result (generat_lub lub1 lub2 lub3 A) = lub1 (result ` (A ∩ {f. is_Pure f}))"

lemma output_generat_lub:
"∀x∈A. ¬ is_Pure x ⟹ output (generat_lub lub1 lub2 lub3 A) = lub2 (output ` (A ∩ {f. ¬ is_Pure f}))"

lemma continuation_generat_lub:
"∀x∈A. ¬ is_Pure x ⟹ continuation (generat_lub lub1 lub2 lub3 A) = lub3 (continuation ` (A ∩ {f. ¬ is_Pure f}))"

lemma generat_lub_map [simp]:
"generat_lub lub1 lub2 lub3 (map_generat f g h ` A) = generat_lub (lub1 ∘ (`) f) (lub2 ∘ (`) g) (lub3 ∘ (`) h) A"
by(auto 4 3 simp add: generat_lub_def intro: arg_cong[where f=lub1] arg_cong[where f=lub2] arg_cong[where f=lub3] rev_image_eqI del: ext intro!: ext)

lemma map_generat_lub [simp]:
"map_generat f g h (generat_lub lub1 lub2 lub3 A) = generat_lub (f ∘ lub1) (g ∘ lub2) (h ∘ lub3) A"

abbreviation generat_lub' :: "('cont set ⇒ 'cont') ⇒ ('a, 'out, 'cont) generat set ⇒ ('a, 'out, 'cont') generat"
where "generat_lub' ≡ generat_lub (λA. THE x. x ∈ A) (λA. THE x. x ∈ A)"

fun rel_witness_generat :: "('a, 'c, 'e) generat × ('b, 'd, 'f) generat ⇒ ('a × 'b, 'c × 'd, 'e × 'f) generat" where
"rel_witness_generat (Pure x, Pure y) = Pure (x, y)"
| "rel_witness_generat (IO out c, IO out' c') = IO (out, out') (c, c')"

lemma rel_witness_generat:
assumes "rel_generat A C R x y"
shows pures_rel_witness_generat: "generat_pures (rel_witness_generat (x, y)) ⊆ {(a, b). A a b}"
and outs_rel_witness_generat: "generat_outs (rel_witness_generat (x, y)) ⊆ {(c, d). C c d}"
and conts_rel_witness_generat: "generat_conts (rel_witness_generat (x, y)) ⊆ {(e, f). R e f}"
and map1_rel_witness_generat: "map_generat fst fst fst (rel_witness_generat (x, y)) = x"
and map2_rel_witness_generat: "map_generat snd snd snd (rel_witness_generat (x, y)) = y"
using assms by(cases; simp; fail)+

lemmas set_rel_witness_generat = pures_rel_witness_generat outs_rel_witness_generat conts_rel_witness_generat

lemma rel_witness_generat1:
assumes "rel_generat A C R x y"
shows "rel_generat (λa (a', b). a = a' ∧ A a' b) (λc (c', d). c = c' ∧ C c' d) (λr (r', s). r = r' ∧ R r' s) x (rel_witness_generat (x, y))"
using map1_rel_witness_generat[OF assms, symmetric]
unfolding generat.rel_eq[symmetric] generat.rel_map
by(rule generat.rel_mono_strong)(auto dest: set_rel_witness_generat[OF assms, THEN subsetD])

lemma rel_witness_generat2:
assumes "rel_generat A C R x y"
shows "rel_generat (λ(a, b') b. b = b' ∧ A a b') (λ(c, d') d. d = d' ∧ C c d') (λ(r, s') s. s = s' ∧ R r s') (rel_witness_generat (x, y)) y"
using map2_rel_witness_generat[OF assms]
unfolding generat.rel_eq[symmetric] generat.rel_map
by(rule generat.rel_mono_strong)(auto dest: set_rel_witness_generat[OF assms, THEN subsetD])

end
```