Theory AWN_Term_Graph

(*  Title:       AWN_Term_Graph.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)
theory AWN_Term_Graph
imports AWN_Cterms
begin

datatype ('p, 'l) node =
    RootNode 'p
  | InternalNode 'l

datatype ('p, 'l) link =
    ILink "('p, 'l) node" "('p, 'l) node"
  | ELink "('p, 'l) node" "('p, 'l) node"

definition gseqp'_fails where "gseqp'_fails = []"
declare [[code abort: gseqp'_fails]]

fun gseqp'
  :: "('s, 'm, 'p, 'l) seqp_env ⇒ ('s, 'm, 'p, 'l) seqp ⇒ ('p, 'l) node list"
where
    "gseqp' Γ ({l}⟨_⟩ _)                = [InternalNode l]"
  | "gseqp' Γ ({l}⟦_⟧ _)                = [InternalNode l]"
  | "gseqp' Γ ({l}unicast(_, _)._ ▹ _) = [InternalNode l]"
  | "gseqp' Γ ({l}broadcast(_). _)     = [InternalNode l]"
  | "gseqp' Γ ({l}groupcast(_, _). _)  = [InternalNode l]"
  | "gseqp' Γ ({l}send(_)._)           = [InternalNode l]"
  | "gseqp' Γ ({l}deliver(_)._)        = [InternalNode l]"
  | "gseqp' Γ ({l}receive(_)._)        = [InternalNode l]"
  | "gseqp' Γ (p1 ⊕ p2)                = gseqp' Γ p1 @ gseqp' Γ p2"
  | "gseqp' Γ (call(pn))               = gseqp'_fails"
(*
(* It would be better to define this function for all wellformed Γ, as shown
   below, but I can't get the code generator to work smoothly with the
   conditional simp rules. *)

  | "gseqp' Γ (call(pn))               = gseqp' Γ (Γ pn)"
  by pat_completeness auto

lemma gseqp'_termination:
  assumes "wellformed Γ"
    shows "gseqp'_dom (Γ, p)"
  proof -
    have gseqp'_rel':
      "gseqp'_rel = (λgq gp. (gq, gp) ∈ {((Γ, q), (Γ', p)). Γ = Γ' ∧ p ↝⇘Γ⇙ q})"
      by (rule ext)+ (auto simp: gseqp'_rel.simps elim: microstep.cases)

    from assms have "∀x. x ∈ acc {(q, p). p ↝⇘Γ⇙ q}"
      unfolding wellformed_def by (simp add: wf_acc_iff)
    hence "p ∈ acc {(q, p). p ↝⇘Γ⇙ q}" ..

    hence "(Γ, p) ∈ acc {((Γ, q), (Γ', p)). Γ = Γ' ∧ p ↝⇘Γ⇙ q}"
      by (rule acc_induct) (auto intro: accI)

    thus "gseqp'_dom (Γ, p)" unfolding gseqp'_rel' accp_acc_eq .
  qed

declare gseqp'.psimps [simp, code del]
lemmas gseqp'_psimps[simp] = gseqp'.psimps [OF gseqp'_termination]
   and gseqp'_pinduct = gseqp'.pinduct [OF gseqp'_termination]
*)

fun gseqp :: "('s, 'm, 'p, 'l) seqp_env ⇒ ('s, 'm, 'p, 'l) seqp
              ⇒ ('p, 'l) node list * ('p, 'l) node list * ('p, 'l) link list"
where
    "gseqp Γ ({l}⟨_⟩ p)                = (let me = InternalNode l in
                                          let (next, acc, links) = gseqp Γ p in
                                          ([me], me # acc, map (ILink me) next @ links))"
  | "gseqp Γ ({l}⟦_⟧ p)                = (let me = InternalNode l in
                                          let (next, acc, links) = gseqp Γ p in
                                          ([me], me # acc, map (ILink me) next @ links))"
  | "gseqp Γ (p1 ⊕ p2)                = (let (next1, acc1, links1) = gseqp Γ p1 in
                                          let (next2, acc2, links2) = gseqp Γ p2 in
                                          (next1 @ next2, acc1 @ acc2, links1 @ links2))"
  | "gseqp Γ ({l}unicast(_, _).p ▹ q) = (let me = InternalNode l in
                                          let (next1, acc1, links1) = gseqp Γ p in
                                          let (next2, acc2, links2) = gseqp Γ q in
                                          ([me], me # acc1 @ acc2,
                                        map (ELink me) (next1 @ next2) @ links1 @ links2))"
  | "gseqp Γ ({l}broadcast(_). p)     = (let me = InternalNode l in
                                          let (next, acc, links) = gseqp Γ p in
                                         ([me], me # acc, map (ELink me) next @ links))"
  | "gseqp Γ ({l}groupcast(_, _). p)  = (let me = InternalNode l in
                                          let (next, acc, links) = gseqp Γ p in
                                          ([me], me # acc, map (ELink me) next @ links))"
  | "gseqp Γ ({l}send(_).p)           = (let me = InternalNode l in
                                          let (next, acc, links) = gseqp Γ p in
                                          ([me], me # acc, map (ELink me) next @ links))"
  | "gseqp Γ ({l}deliver(_).p)        = (let me = InternalNode l in
                                          let (next, acc, links) = gseqp Γ p in
                                          ([me], me # acc, map (ELink me) next @ links))"
  | "gseqp Γ ({l}receive(_).p)        = (let me = InternalNode l in
                                          let (next, acc, links) = gseqp Γ p in
                                          ([me], me # acc, map (ELink me) next @ links))"
  | "gseqp Γ (call(pn))               = (gseqp' Γ (Γ pn), [], [])"

definition graph_of_other :: "('s, 'm, 'p, 'l) seqp_env
                              ⇒ (('p, 'l) node list * ('p, 'l) link list)
                              ⇒ 'p
                              ⇒ ('p, 'l) node list * ('p, 'l) link list"
where
  "graph_of_other Γ r pn = (let (next, acc, links) = gseqp Γ (Γ pn) in
                            (acc @ fst r, links @ snd r))"

definition graph_of_root :: "('s, 'm, 'p, 'l) seqp_env
                             ⇒ (('p, 'l) node list * ('p, 'l) link list)
                             ⇒ 'p
                             ⇒ ('p, 'l) node list * ('p, 'l) link list"
where
  "graph_of_root Γ r pn = (let me = RootNode pn in
                           let (next, acc, links) = gseqp Γ (Γ pn) in
                           (acc @ fst r @ [me], map (ILink me) next @ links @ snd r))"

definition graph_of_seqp :: "('s, 'm, 'p, 'l) seqp_env
                             ⇒ 'p list
                             ⇒ ('p, 'l) node list * ('p, 'l) link list"
where
  "graph_of_seqp Γ pns = map_prod (rev ∘ remdups) remdups
                           (foldl (graph_of_other Γ) (graph_of_root Γ ([], []) (hd pns)) (tl pns))"

definition graph_of_seqps :: "('s, 'm, 'p, 'l) seqp_env
                              ⇒ 'p list
                              ⇒ ('p, 'l) node list * ('p, 'l) link list"
where
  "graph_of_seqps Γ pns = map_prod (rev ∘ remdups) remdups (foldl (graph_of_root Γ) ([], [])
                                   (List.rev pns))"

end