--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,72 @@
+(*  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
+