src/HOL/UNITY/Simple/Reachability.thy

-(*  Title:      HOL/UNITY/Reachability
-    ID:         $Id$
+(*  Title:      HOL/UNITY/Reachability.thy
     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 in Graphs.
+
+From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2
+and 11.3.
 *)
 
 theory Reachability imports "../Detects" Reach begin
 
 types  edge = "(vertex*vertex)"

      "[| v \<in> V; w \<in> V |]  
       ==> F \<in> UNIV LeadsTo  
              ((reachable v <==> {s. (root,v): REACHABLE}) \<inter> nmsg_eq 0 (v,w))"
 apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast)
 apply (subgoal_tac
-	 "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
+         "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
               UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
               nmsg_eq 0 (v,w) ")
 apply simp
 apply (rule PSP_Stable2)
 apply (rule MA7)