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

lemma result_generat_lub [simp]:
  "xA. 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: 
  "xA. ¬ 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:
  "xA. ¬ 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