src/Provers/trancl.ML
changeset 30190 479806475f3c
parent 26834 87a5b9ec3863
child 32215 87806301a813
equal deleted inserted replaced
30189:3633f560f4c3 30190:479806475f3c
     1 (*
     1 (*
     2   Title:	Transitivity reasoner for transitive closures of relations
     2     Title:      Transitivity reasoner for transitive closures of relations
     3   Id:		$Id$
     3     Author:     Oliver Kutter, TU Muenchen
     4   Author:	Oliver Kutter
       
     5   Copyright:	TU Muenchen
       
     6 *)
     4 *)
     7 
     5 
     8 (*
     6 (*
     9 
     7 
    10 The packages provides tactics trancl_tac and rtrancl_tac that prove
     8 The packages provides tactics trancl_tac and rtrancl_tac that prove
   333        end
   331        end
   334      | assemble nil _ = nil
   332      | assemble nil _ = nil
   335 
   333 
   336    (* Compute, for each adjacency list, the list with reversed edges,
   334    (* Compute, for each adjacency list, the list with reversed edges,
   337       and concatenate these lists. *)
   335       and concatenate these lists. *)
   338    val flipped = foldr (op @) nil (map flip g)
   336    val flipped = List.foldr (op @) nil (map flip g)
   339  
   337  
   340  in assemble g flipped end    
   338  in assemble g flipped end    
   341  
   339  
   342 (* *********************************************************************** *)
   340 (* *********************************************************************** *)
   343 (*                                                                         *)
   341 (*                                                                         *)
   357 
   355 
   358   fun dfs_visit g u  =
   356   fun dfs_visit g u  =
   359       let
   357       let
   360    val _ = visited := u :: !visited
   358    val _ = visited := u :: !visited
   361    val descendents =
   359    val descendents =
   362        foldr (fn ((v,l),ds) => if been_visited v then ds
   360        List.foldr (fn ((v,l),ds) => if been_visited v then ds
   363             else v :: dfs_visit g v @ ds)
   361             else v :: dfs_visit g v @ ds)
   364         nil (adjacent eq_comp g u)
   362         nil (adjacent eq_comp g u)
   365    in  descendents end
   363    in  descendents end
   366  
   364  
   367  in u :: dfs_visit g u end;
   365  in u :: dfs_visit g u end;