src/HOL/UNITY/Simple/Reachability.thy

Converted 1 to 1'

(*  Title:      HOL/UNITY/Reachability
    ID:         $Id$
    Author:     Tanja Vos, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge

Reachability in Graphs

From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
*)

Reachability = Detects + 

types  edge = "(vertex*vertex)"

record state =
  reach :: vertex => bool
  nmsg  :: edge => nat

consts REACHABLE :: edge set
       root :: vertex
       E :: edge set
       V :: vertex set

inductive "REACHABLE"
  intrs
   base "v : V ==> ((v,v) : REACHABLE)"
   step "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"

constdefs
  reachable :: vertex => state set
  "reachable p == {s. reach s p}"

  nmsg_eq :: nat => edge  => state set
  "nmsg_eq k == %e. {s. nmsg s e = k}"

  nmsg_gt :: nat => edge  => state set
  "nmsg_gt k  == %e. {s. k < nmsg s e}"

  nmsg_gte :: nat => edge => state set
  "nmsg_gte k == %e. {s. k <= nmsg s e}"

  nmsg_lte  :: nat => edge => state set
  "nmsg_lte k  == %e. {s. nmsg s e <= k}"

  

  final :: state set
  "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"

rules
    Graph1 "root : V"

    Graph2 "(v,w) : E ==> (v : V) & (w : V)"

    MA1  "F : Always (reachable root)"

    MA2  "[|v:V|] ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"

    MA3  "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"

    MA4  "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"

    MA5  "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w))"

    MA6  "[|v:V|] ==> F : Stable (reachable v)"

    MA6b "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"

    MA7  "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"

end