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). b∈s a}"

definition "pred_of_rel s ≡ λa b. (a,b)∈s"
definition "pred_of_succ s ≡ λa b. b∈s 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"

"b∈succ_of_rel r a ⟷ (a,b)∈r"
"b∈succ_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_pred (pred_of_succ s) = rel_of_succ s"

"rel_of_succ (succ_of_rel r) = r"
"rel_of_succ (succ_of_pred p) = rel_of_pred p"

"pred_of_rel (rel_of_pred p) = p"
"pred_of_rel (rel_of_succ s) = pred_of_succ s"

"pred_of_succ (succ_of_pred p) = p"
"pred_of_succ (succ_of_rel r) = pred_of_rel r"

"succ_of_rel (rel_of_succ s) = s"
"succ_of_rel (rel_of_pred p) = succ_of_pred p"

"succ_of_pred (pred_of_succ s) = s"
"succ_of_pred (pred_of_rel r) = succ_of_rel r"
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)"
"b∈m2r_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]:
"m2r_rel (rel_of_succ s) = rel_of_succ (m2r_succ s)"
"m2r_rel (rel_of_pred p) = rel_of_pred (m2r_pred p)"

"m2r_pred (pred_of_succ s) = pred_of_succ (m2r_succ s)"
"m2r_pred (pred_of_rel r) = pred_of_rel (m2r_rel r)"

"m2r_succ (succ_of_pred p) = succ_of_pred (m2r_pred p)"
"m2r_succ (succ_of_rel r) = succ_of_rel (m2r_rel r)"
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 ∃a∈en s. s'=ex a s"
definition "succ_of_enex enex ≡ λs. let (en,ex) = enex in {s'. ∃a∈en 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' ⟷ (∃a∈en s. s'=ex a s)"
"s'∈succ_of_enex (en,ex) s ⟷ (∃a∈en 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
```