# Theory Step_Conv

theory Step_Conv
imports Main
begin
(* Different ways of representing transitions,
and functions to convert between them:

rel :: ('a × 'b) set
pred :: 'a ⇒ 'b ⇒ bool
succ :: 'a ⇒ 'b set
*)

definition "rel_of_pred s  {(a,b). s a b}"
definition "rel_of_succ s  {(a,b). bs a}"

definition "pred_of_rel s  λa b. (a,b)s"
definition "pred_of_succ s  λa b. bs a"

definition "succ_of_rel s  λa. {b. (a,b)s}"
definition "succ_of_pred s  λa. {b. s a b}"

lemma rps_expand[simp]:
"(a,b)rel_of_pred p  p a b"
"(a,b)rel_of_succ s  b  s a"

"pred_of_rel r a b  (a,b)r"
"pred_of_succ s a b  b  s a"

"bsucc_of_rel r a  (a,b)r"
"bsucc_of_pred p a  p a b"
unfolding rel_of_pred_def pred_of_rel_def
unfolding rel_of_succ_def succ_of_rel_def
unfolding pred_of_succ_def succ_of_pred_def
by auto

lemma rps_conv[simp]:
"rel_of_pred (pred_of_rel r) = r"

"rel_of_succ (succ_of_rel r) = r"

"pred_of_rel (rel_of_pred p) = p"

"succ_of_rel (rel_of_succ s) = s"

unfolding rel_of_pred_def pred_of_rel_def
unfolding rel_of_succ_def succ_of_rel_def
unfolding pred_of_succ_def succ_of_pred_def
by auto

(* Lifting transitions from option monad to option×option *)
definition m2r_rel :: "('a × 'a option) set  'a option rel"
where "m2r_rel r  {(Some a,b)|a b. (a,b)r}"

definition m2r_pred :: "('a  'a option  bool)  'a option  'a option  bool"
where "m2r_pred p  λNone  λ_. False | Some a  p a"

definition m2r_succ :: "('a  'a option set)  'a option  'a option set"
where "m2r_succ s  λNone  {} | Some a  s a"

lemma m2r_expand[simp]:
"(a,b)m2r_rel r  (a'. a=Some a'  (a',b)r)"
"m2r_pred p a b  (a'. a=Some a'  p a' b)"
"bm2r_succ s a  (a'. a=Some a'  b  s a')"
unfolding m2r_rel_def m2r_succ_def m2r_pred_def
by (auto split: option.splits)

lemma m2r_conv[simp]:

unfolding rel_of_pred_def pred_of_rel_def
unfolding rel_of_succ_def succ_of_rel_def
unfolding pred_of_succ_def succ_of_pred_def
unfolding m2r_rel_def m2r_succ_def m2r_pred_def
by (auto split: option.splits)

definition "rel_of_enex enex  let (en, ex) = enex in {(s, ex a s) |s a. a  en s}"
definition "pred_of_enex enex  λs s'. let (en,ex) = enex in aen s. s'=ex a s"
definition "succ_of_enex enex  λs. let (en,ex) = enex in {s'. aen s. s'=ex a s}"

lemma x_of_enex_expand[simp]:
"(s, s')  rel_of_enex (en, ex)  ( a  en s. s' = ex a s)"
"pred_of_enex (en,ex) s s'  (aen s. s'=ex a s)"
"s'succ_of_enex (en,ex) s  (aen s. s'=ex a s)"
unfolding rel_of_enex_def pred_of_enex_def succ_of_enex_def by auto

lemma x_of_enex_conv[simp]:
"rel_of_pred (pred_of_enex enex) = rel_of_enex enex"
"rel_of_succ (succ_of_enex enex) = rel_of_enex enex"
"pred_of_rel (rel_of_enex enex) = pred_of_enex enex"
"pred_of_succ (succ_of_enex enex) = pred_of_enex enex"
"succ_of_rel (rel_of_enex enex) = succ_of_enex enex"
"succ_of_pred (pred_of_enex enex) = succ_of_enex enex"
unfolding rel_of_enex_def pred_of_enex_def succ_of_enex_def
unfolding rel_of_pred_def rel_of_succ_def
unfolding pred_of_rel_def pred_of_succ_def
unfolding succ_of_rel_def succ_of_pred_def
by auto

end