(* 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
setup ‹Code_Simp.map_ss (Simplifier.add_cong @{thm IO_code_cong})›

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)"
by(cases r)(auto simp add: rel_fun_def)

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)"
by(simp add: countable_finite)

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)"
by(simp add: fun_eq_iff)

lemma dom_dest_IO: "dom dest_IO = {x. ¬ is_Pure x}"
by(auto simp add: not_is_Pure_conv)


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)"
by(simp add: generat_lub_def)

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

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

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

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"
by(simp add: generat_lub_def o_def)


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