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